Commit c557ab8b authored by Gerwin Klein's avatar Gerwin Klein

merge from afp-2021

......@@ -44,7 +44,7 @@ default_isabelle_tool()
ISABELLE_VERSION="Isabelle$VERSION"
ISABELLE_TOOL="$ISABELLE_RELEASES/$ISABELLE_VERSION/bin/isabelle"
if [[ "$OSTYPE" == darwin* && ! -x "$ISABELLE_TOOL" ]]; then
ISABELLE_TOOL="$ISABELLE_RELEASES/${ISABELLE_VERSION}.app/Isabelle/bin/isabelle"
ISABELLE_TOOL="$ISABELLE_RELEASES/${ISABELLE_VERSION}.app/bin/isabelle"
fi
fi
fi
......
......@@ -122,7 +122,7 @@ if [ "$1" != "-" ]; then
mv $EXPORT.tar.gz $TARS/
echo "Generating HTML for [$@]"
$ISABELLE_TOOL afp_build -- -v -c $@ || fail "isabelle afp_build failed on [$@]"
$ISABELLE_TOOL afp_build -- -v -c -j 2 $@ || fail "isabelle afp_build failed on [$@]"
cd $EXPORT/thys
for ENTRY in $@; do
......
......@@ -9676,6 +9676,23 @@ abstract =
p<sub><em>i</em></sub> for
i&gt;k.</p>
[Formal_Puiseux_Series]
title = Formal Puiseux Series
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
topic = Mathematics/Algebra
date = 2021-02-17
notify = eberlm@in.tum.de
abstract =
<p>Formal Puiseux series are generalisations of formal power
series and formal Laurent series that also allow for fractional
exponents. They have the following general form: \[\sum_{i=N}^\infty
a_{i/d} X^{i/d}\] where <em>N</em> is an integer and
<em>d</em> is a positive integer.</p> <p>This
entry defines these series including their basic algebraic properties.
Furthermore, it proves the Newton–Puiseux Theorem, namely that the
Puiseux series over an algebraically closed field of characteristic 0
are also algebraically closed.</p>
[Gaussian_Integers]
title = Gaussian Integers
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
......@@ -10266,3 +10283,29 @@ abstract =
used for the proof of the strong law is a particularly quick and slick
one based on ergodic theory, which was formalised by Gouëzel in
another AFP entry.</p>
[BTree]
title = A Verified Imperative Implementation of B-Trees
author = Niels Mündler <mailto:n.muendler@tum.de>
topic = Computer science/Data structures
date = 2021-02-24
notify = n.muendler@tum.de
abstract =
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bayer and McCreight [ACM 1970]. The
implementation supports set membership and insertion queries with
efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the <a
href="https://www.isa-afp.org/entries/Refine_Imperative_HOL.html">
Isabelle Refinement Framework </a> . The code can be exported to
the programming languages SML and Scala. We examine the runtime of all
operations indirectly by reproducing results of the logarithmic
relationship between height and the number of nodes. The results are
discussed in greater detail in the corresponding <a
href="https://mediatum.ub.tum.de/1596550">Bachelor's
Thesis</a>.
......@@ -20,3 +20,4 @@
2018 = 2018-08-16
2019 = 2019-06-10
2020 = 2020-04-16
2021 = 2021-02-21
This diff is collapsed.
......@@ -17,13 +17,25 @@ your own developments. If you would like to make your work available to others
<i>without</i> having to include the AFP articles you depend on, here is how to do it.
</p>
<p>
If you are using Isabelle2020, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, you should run the following command
<a href="#1">[1]</a> to make the AFP session ROOTS available to Isabelle:</p>
If you are using Isabelle2021, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, for Linux/Mac you can run the following command to make the AFP session ROOTS available to Isabelle:</p>
<p>
<pre class="code">
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2020/ROOTS
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
</pre>
This adds the path <code>/home/myself/afp/thys/</code> to the ROOTS file, which
Isabelle will scan by default. You can also manually edit and/or create that
ROOTS file. There are many other ways to achieve the same outcome, this is just
one option.
</p>
<p>
For Windows, the idea is the same just the path is slightly different. If the
AFP is in <code>C:\afp</code>, you should be able to run the following in a
Cygwin terminal.
<pre class="code">
echo "/cygdrive/c/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
</pre>
</p>
<p>
You can now refer to article <code>ABC</code> from the AFP in some theory of
......@@ -39,10 +51,6 @@ manner.</p>
<p>&nbsp;</p>
<p>
<a name="1">[1]:</a> Tested for Linux and Mac installations &dash; it should be the same under cygwin on Windows.
</p>
<p>
</td></tr>
</tbody>
</table>
......
theory Array_SBlit
imports "Separation_Logic_Imperative_HOL.Array_Blit"
begin
section "Same array Blit"
text "The standard framework already provides a function to copy array
elements."
term blit
thm blit_rule
thm blit.simps
(* Same array BLIT *)
definition "sblit a s d l \<equiv> blit a s a d l"
text "When copying values within arrays,
blit only works for moving elements to the left."
lemma sblit_rule[sep_heap_rules]:
assumes LEN:
"si+len \<le> length lsrc"
and DST_SM: "di \<le> si"
shows
"< src \<mapsto>\<^sub>a lsrc >
sblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding sblit_def
using LEN DST_SM
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "\<And>x. lsrc ! si # take len (drop (Suc si) lsrc) @ x
= take (Suc len) (drop si lsrc) @ x"
apply simp
by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc
less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
Nat.trans_le_add2)
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "A reverse blit"
text "The function rblit may be used to copy elements a defined offset to the right"
(* Right BLIT or Reverse BLIT *)
primrec rblit :: "_ array \<Rightarrow> nat \<Rightarrow> _ array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
"rblit _ _ _ _ 0 = return ()"
| "rblit src si dst di (Suc l) = do {
x \<leftarrow> Array.nth src (si+l);
Array.upd (di+l) x dst;
rblit src si dst di l
}"
text "For separated arrays it is equivalent to normal blit.
The proof follows similarly to the corresponding proof for blit."
lemma rblit_rule[sep_heap_rules]:
assumes LEN: "si+len \<le> length lsrc" "di+len \<le> length ldst"
shows
"< src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a ldst >
rblit src si dst di len
<\<lambda>_. src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst)
>"
using LEN
proof (induction len arbitrary: ldst)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "drop (di + len) (ldst[di + len := lsrc ! (si + len)])
= lsrc ! (si + len) # drop (Suc (di + len)) ldst"
by (metis Cons_nth_drop_Suc Suc.prems(2) Suc_le_eq add_Suc_right drop_upd_irrelevant length_list_update lessI nth_list_update_eq)
have "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length (drop si lsrc)"
using Suc.prems(1) by force
then show "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
by (metis (no_types) Suc.prems(1) add_leD1 nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\<And>x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
definition "srblit a s d l \<equiv> rblit a s a d l"
text "However, within arrays we can now copy to the right."
lemma srblit_rule[sep_heap_rules]:
assumes LEN:
"di+len \<le> length lsrc"
and DST_GR: "di \<ge> si"
shows
"< src \<mapsto>\<^sub>a lsrc >
srblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding srblit_def
using LEN DST_GR
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
= take len (drop si lsrc)"
sledgehammer
by (metis Suc.prems(2) ab_semigroup_add_class.add.commute add_le_cancel_right take_drop take_update_cancel)
have [simp]: "drop (di + len) (lsrc[di + len := lsrc ! (si + len)])
= lsrc ! (si+len) # drop (Suc di + len) lsrc"
by (metis Suc.prems(1) add_Suc_right add_Suc_shift add_less_cancel_left append_take_drop_id le_imp_less_Suc le_refl plus_1_eq_Suc same_append_eq take_update_cancel upd_conv_take_nth_drop)
have "take len (drop si lsrc) @
[lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length lsrc - si"
using Suc.prems(1) Suc.prems(2) by linarith
then show ?thesis
by (metis (no_types) Suc.prems(1) Suc.prems(2) add_leD1 le_add_diff_inverse length_drop nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\<And>x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "Modeling target language blit"
text "For convenience, a function that is oblivious to the direction of the shift
is defined."
definition "safe_sblit a s d l \<equiv>
if s > d then
sblit a s d l
else
srblit a s d l
"
text "We obtain a heap rule similar to the one of blit,
but for copying within one array."
lemma safe_sblit_rule[sep_heap_rules]:
assumes LEN:
"len > 0 \<longrightarrow> di+len \<le> length lsrc \<and> si+len \<le> length lsrc"
shows
"< src \<mapsto>\<^sub>a lsrc >
safe_sblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding safe_sblit_def
using LEN
apply(cases len)
apply(sep_auto simp add: sblit_def srblit_def)[]
apply sep_auto
done
(* Compare this to blit_rule *)
thm blit_rule
thm safe_sblit_rule
subsection "Code Generator Setup"
text "Note that the requirement for correctness
is even weaker here than in SML.
We therefore manually handle the case where length is 0 (in which case nothing happens at all)."
code_printing code_module "array_sblit" \<rightharpoonup> (SML)
\<open>
fun array_sblit src si di len = (
if len > 0 then
ArraySlice.copy {
di = IntInf.toInt di,
src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
dst = src}
else ()
)
\<close>
definition safe_sblit' where
[code del]: "safe_sblit' src si di len
= safe_sblit src (nat_of_integer si) (nat_of_integer di)
(nat_of_integer len)"
lemma [code]:
"safe_sblit src si di len
= safe_sblit' src (integer_of_nat si) (integer_of_nat di)
(integer_of_nat len)" by (simp add: safe_sblit'_def)
(* TODO: Export to other languages: OCaml, Haskell *)
code_printing constant safe_sblit' \<rightharpoonup>
(SML) "(fn/ ()/ => /array'_sblit _ _ _ _)"
and (Scala) "{ ('_: Unit)/=>/
def safescopy(src: Array['_], srci: Int, dsti: Int, len: Int) = {
if (len > 0)
System.arraycopy(src, srci, src, dsti, len)
else
()
}
safescopy(_.array,_.toInt,_.toInt,_.toInt)
}"
export_code safe_sblit checking SML Scala
subsection "Derived operations"
definition array_shr where
"array_shr a i k \<equiv> do {
l \<leftarrow> Array.len a;
safe_sblit a i (i+k) (l-(i+k))
}"
find_theorems "Array.len"
lemma array_shr_rule[sep_heap_rules]:
"< src \<mapsto>\<^sub>a lsrc >
array_shr src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i+k) lsrc @ take (length lsrc - (i+k)) (drop i lsrc))
>"
unfolding array_shr_def
by sep_auto
lemma array_shr_rule_alt:
"< src \<mapsto>\<^sub>a lsrc >
array_shr src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (length lsrc) (take (i+k) lsrc @ (drop i lsrc)))
>"
by (sep_auto simp add: min_def)
definition array_shl where
"array_shl a i k \<equiv> do {
l \<leftarrow> Array.len a;
safe_sblit a i (i-k) (l-i)
}
"
lemma array_shl_rule[sep_heap_rules]:
"
< src \<mapsto>\<^sub>a lsrc >
array_shl src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (i - k + (length lsrc - i)) lsrc)
>"
unfolding array_shl_def
by sep_auto
lemma array_shl_rule_alt:
"
\<lbrakk>i \<le> length lsrc; k \<le> i\<rbrakk> \<Longrightarrow>
< src \<mapsto>\<^sub>a lsrc >
array_shl src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (length lsrc - k) lsrc)
>"
by sep_auto
end
\ No newline at end of file
theory BTree
imports Main "HOL-Data_Structures.Sorted_Less" "HOL-Data_Structures.Cmp"
begin
(* some setup to cover up the redefinition of sorted in Sorted_Less
but keep the lemmas *)
hide_const (open) Sorted_Less.sorted
abbreviation "sorted_less \<equiv> Sorted_Less.sorted"
section "Definition of the B-Tree"
subsection "Datatype definition"
text "B-trees can be considered to have all data stored interleaved
as child nodes and separating elements (also keys or indices).
We define them to either be a Node that holds a list of pairs of children
and indices or be a completely empty Leaf."
datatype 'a btree = Leaf | Node "('a btree * 'a) list" "'a btree"
type_synonym 'a btree_list = "('a btree * 'a) list"
type_synonym 'a btree_pair = "('a btree * 'a)"
abbreviation subtrees where "subtrees xs \<equiv> (map fst xs)"
abbreviation separators where "separators xs \<equiv> (map snd xs)"
subsection "Inorder and Set"
text "The set of B-tree elements is defined automatically."
thm btree.set
value "set_btree (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
text "The inorder view is defined with the help of the concat function."
fun inorder :: "'a btree \<Rightarrow> 'a list" where
"inorder Leaf = []" |
"inorder (Node ts t) = concat (map (\<lambda> (sub, sep). inorder sub @ [sep]) ts) @ inorder t"
abbreviation "inorder_pair \<equiv> \<lambda>(sub,sep). inorder sub @ [sep]"
abbreviation "inorder_list ts \<equiv> concat (map inorder_pair ts)"
(* this abbreviation makes handling the list much nicer *)
thm inorder.simps
value "inorder (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
subsection "Height and Balancedness"
class height =
fixes height :: "'a \<Rightarrow> nat"
instantiation btree :: (type) height
begin
fun height_btree :: "'a btree \<Rightarrow> nat" where
"height Leaf = 0" |
"height (Node ts t) = Suc (Max (height ` (set (subtrees ts@[t]))))"
instance ..
end
text "Balancedness is defined is close accordance to the definition by Ernst"
fun bal:: "'a btree \<Rightarrow> bool" where
"bal Leaf = True" |
"bal (Node ts t) = (
(\<forall>sub \<in> set (subtrees ts). height sub = height t) \<and>
(\<forall>sub \<in> set (subtrees ts). bal sub) \<and> bal t
)"
value "height (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
subsection "Order"
text "The order of a B-tree is defined just as in the original paper by Bayer."
(* alt1: following knuths definition to allow for any
natural number as order and resolve ambiguity *)
(* alt2: use range [k,2*k] allowing for valid btrees
from k=1 onwards NOTE this is what I ended up implementing *)
fun order:: "nat \<Rightarrow> 'a btree \<Rightarrow> bool" where
"order k Leaf = True" |
"order k (Node ts t) = (
(length ts \<ge> k) \<and>
(length ts \<le> 2*k) \<and>
(\<forall>sub \<in> set (subtrees ts). order k sub) \<and> order k t
)"
text \<open>The special condition for the root is called \textit{root\_order}\<close>
(* the invariant for the root of the btree *)
fun root_order:: "nat \<Rightarrow> 'a btree \<Rightarrow> bool" where
"root_order k Leaf = True" |
"root_order k (Node ts t) = (
(length ts > 0) \<and>
(length ts \<le> 2*k) \<and>
(\<forall>s \<in> set (subtrees ts). order k s) \<and> order k t
)"
subsection "Auxiliary Lemmas"
(* auxiliary lemmas when handling sets *)
lemma separators_split:
"set (separators (l@(a,b)#r)) = set (separators l) \<union> set (separators r) \<union> {b}"
by simp
lemma subtrees_split:
"set (subtrees (l@(a,b)#r)) = set (subtrees l) \<union> set (subtrees r) \<union> {a}"
by simp
(* height and set lemmas *)
lemma finite_set_ins_swap:
assumes "finite A"
shows "max a (Max (Set.insert b A)) = max b (Max (Set.insert a A))"
using Max_insert assms max.commute max.left_commute by fastforce
lemma finite_set_in_idem:
assumes "finite A"
shows "max a (Max (Set.insert a A)) = Max (Set.insert a A)"
using Max_insert assms max.commute max.left_commute by fastforce
lemma height_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf"
by (induction t) (auto)
lemma height_btree_order:
"height (Node (ls@[a]) t) = height (Node (a#ls) t)"
by simp
lemma height_btree_sub:
"height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
by simp
lemma height_btree_last:
"height (Node ((sub,x)#ts) t) = max (height (Node ts sub)) (Suc (height t))"
by (induction ts) auto
lemma set_btree_inorder: "set (inorder t) = set_btree t"
apply(induction t)
apply(auto)
done
lemma child_subset: "p \<in> set t \<Longrightarrow> set_btree (fst p) \<subseteq> set_btree (Node t n)"
apply(induction p arbitrary: t n)
apply(auto)
done
lemma some_child_sub:
assumes "(sub,sep) \<in> set t"
shows "sub \<in> set (subtrees t)"
and "sep \<in> set (separators t)"
using assms by force+
(* balancedness lemmas *)
lemma bal_all_subtrees_equal: "bal (Node ts t) \<Longrightarrow> (\<forall>s1 \<in> set (subtrees ts). \<forall>s2 \<in> set (subtrees ts). height s1 = height s2)"
by (metis BTree.bal.simps(2))
lemma fold_max_set: "\<forall>x \<in> set t. x = f \<Longrightarrow> fold max t f = f"
apply(induction t)
apply(auto simp add: max_def_raw)
done
lemma height_bal_tree: "bal (Node ts t) \<Longrightarrow> height (Node ts t) = Suc (height t)"
by (induction ts) auto
lemma bal_split_last:
assumes "bal (Node (ls@(sub,sep)#rs) t)"
shows "bal (Node (ls@rs) t)"
and "height (Node (ls@(sub,sep)#rs) t) = height (Node (ls@rs) t)"
using assms by auto
lemma bal_split_right:
assumes "bal (Node (ls@rs) t)"
shows "bal (Node rs t)"
and "height (Node rs t) = height (Node (ls@rs) t)"
using assms by (auto simp add: image_constant_conv)
lemma bal_split_left:
assumes "bal (Node (ls@(a,b)#rs) t)"
shows "bal (Node ls a)"
and "height (Node ls a) = height (Node (ls@(a,b)#rs) t)"
using assms by (auto simp add: image_constant_conv)
lemma bal_substitute: "\<lbrakk>bal (Node (ls@(a,b)#rs) t); height t = height c; bal c\<rbrakk> \<Longrightarrow> bal (Node (ls@(c,b)#rs) t)"
unfolding bal.simps
by auto
lemma bal_substitute_subtree: "\<lbrakk>bal (Node (ls@(a,b)#rs) t); height a = height c; bal c\<rbrakk> \<Longrightarrow> bal (Node (ls@(c,b)#rs) t)"
using bal_substitute
by auto
lemma bal_substitute_separator: "bal (Node (ls@(a,b)#rs) t) \<Longrightarrow> bal (Node (ls@(a,c)#rs) t)"
unfolding bal.simps
by auto
(* order lemmas *)
lemma order_impl_root_order: "\<lbrakk>k > 0; order k t\<rbrakk> \<Longrightarrow> root_order k t"
apply(cases t)
apply(auto)
done
(* sorted inorder implies that some sublists are sorted. This can be followed directly *)
lemma sorted_inorder_list_separators: "sorted_less (inorder_list ts) \<Longrightarrow> sorted_less (separators ts)"
apply(induction ts)
apply (auto simp add: sorted_lems)
done
corollary sorted_inorder_separators: "sorted_less (inorder (Node ts t)) \<Longrightarrow> sorted_less (separators ts)"
using sorted_inorder_list_separators sorted_wrt_append