Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
c739e71fd6ff
Commit
ca9928b0
authored
Nov 27, 2020
by
Gerwin Klein
Browse files
new entry Finite-Map-Extras
parent
cace3e947231
Changes
10
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
c739e71f
...
...
@@ -9906,3 +9906,14 @@ abstract =
used for type-safe conversions between the SI system and others, like
the British Imperial System (BIS).
[Finite-Map-Extras]
title = Finite Map Extras
author = Javier Díaz <mailto:javier.diaz.manzi@gmail.com>
topic = Computer science/Data structures
date = 2020-10-12
notify = javier.diaz.manzi@gmail.com
abstract =
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
thys/Finite-Map-Extras/Finite_Map_Extras.thy
0 → 100644
View file @
c739e71f
This diff is collapsed.
Click to expand it.
thys/Finite-Map-Extras/ROOT
0 → 100644
View file @
c739e71f
chapter AFP
session "Finite-Map-Extras" (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Library"
theories
Finite_Map_Extras
document_files
"root.tex"
thys/Finite-Map-Extras/document/root.tex
0 → 100644
View file @
c739e71f
\documentclass
[11pt,a4paper]
{
article
}
\usepackage
{
isabelle,isabellesym
}
\usepackage
{
latexsym
}
\usepackage
{
amssymb
}
\usepackage
{
pdfsetup
}
\addtolength
{
\hoffset
}{
-1,5cm
}
\addtolength
{
\textwidth
}{
3cm
}
%\urlstyle{rm}
\isabellestyle
{
it
}
\begin{document}
\title
{
Finite Map Extras
}
\author
{
Javier D
\'
iaz
\\\url
{
<javier.diaz.manzi@gmail.com>
}}
\maketitle
\begin{abstract}
This includes useful syntactic sugar, new operators and functions and their associated lemmas for
finite maps which currently are not present in the standard
\texttt
{
Finite
\_
Map
}
theory.
\end{abstract}
\tableofcontents
\parindent
0pt
\parskip
0.5ex
\input
{
session
}
\end{document}
thys/ROOTS
View file @
c739e71f
...
...
@@ -164,6 +164,7 @@ FileRefinement
FinFun
Finger-Trees
Finite_Automata_HF
Finite-Map-Extras
First_Order_Terms
First_Welfare_Theorem
Fishburn_Impossibility
...
...
web/entries/Finite-Map-Extras.html
0 → 100644
View file @
c739e71f
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
Finite Map Extras - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
F
</font>
inite
<font
class=
"first"
>
M
</font>
ap
<font
class=
"first"
>
E
</font>
xtras
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
Finite Map Extras
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
Javier Díaz (javier /dot/ diaz /dot/ manzi /at/ gmail /dot/ com)
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-10-12
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Finite-Map-Extras-AFP,
author = {Javier Díaz},
title = {Finite Map Extras},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{http://isa-afp.org/entries/Finite-Map-Extras.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Finite-Map-Extras-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/index.html
View file @
c739e71f
...
...
@@ -114,6 +114,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<a
href=
"https://www-users.cs.york.ac.uk/~simonf/"
>
Simon Foster
</a>
and
<a
href=
"https://www.lri.fr/~wolff/"
>
Burkhart Wolff
</a>
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-10-12:
<a
href=
"entries/Finite-Map-Extras.html"
>
Finite Map Extras
</a>
<br>
Author:
Javier Díaz
</td>
</tr>
<tr>
<td
class=
"entry"
>
...
...
web/rss.xml
View file @
c739e71f
...
...
@@ -62,6 +62,17 @@ construction is validated by a test-set of known equivalences between
both quantities and SI units. Moreover, the presented theory can be
used for type-safe conversions between the SI system and others, like
the British Imperial System (BIS).
</description>
</item>
<item>
<title>
Finite Map Extras
</title>
<link>
https://www.isa-afp.org/entries/Finite-Map-Extras.html
</link>
<guid>
https://www.isa-afp.org/entries/Finite-Map-Extras.html
</guid>
<dc:creator>
Javier Díaz
</dc:creator>
<pubDate>
12 Oct 2020 00:00:00 +0000
</pubDate>
<description>
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
</description>
</item>
<item>
<title>
A Formal Model of the Safely Composable Document Object Model with Shadow Roots
</title>
...
...
@@ -578,19 +589,5 @@ Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of ZFC, we construct a proper generic extension and
show that the latter also satisfies ZFC.
</description>
</item>
<item>
<title>
Banach-Steinhaus Theorem
</title>
<link>
https://www.isa-afp.org/entries/Banach_Steinhaus.html
</link>
<guid>
https://www.isa-afp.org/entries/Banach_Steinhaus.html
</guid>
<dc:creator>
Dominique Unruh, Jose Manuel Rodriguez Caballero
</dc:creator>
<pubDate>
02 May 2020 00:00:00 +0000
</pubDate>
<description>
We formalize in Isabelle/HOL a result
due to S. Banach and H. Steinhaus known as
the Banach-Steinhaus theorem or Uniform boundedness principle: a
pointwise-bounded family of continuous linear operators from a Banach
space to a normed space is uniformly bounded. Our approach is an
adaptation to Isabelle/HOL of a proof due to A. Sokal.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
c739e71f
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
c739e71f
...
...
@@ -289,6 +289,7 @@
<a
href=
"entries/Interval_Arithmetic_Word32.html"
>
Interval_Arithmetic_Word32
</a>
<a
href=
"entries/ADS_Functor.html"
>
ADS_Functor
</a>
<a
href=
"entries/Relational_Disjoint_Set_Forests.html"
>
Relational_Disjoint_Set_Forests
</a>
<a
href=
"entries/Finite-Map-Extras.html"
>
Finite-Map-Extras
</a>
</div>
<h3>
Functional programming
</h3>
<div
class=
"list"
>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment