--- a/src/HOL/Data_Structures/AList_Upd_Del.thy Tue Nov 17 15:51:48 2015 +0100
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy Wed Nov 18 08:54:58 2015 +0100
@@ -89,6 +89,16 @@
lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
+text\<open>Splay trees need two additional @{const upd_list} lemmas:\<close>
+
+lemma upd_list_Cons:
+ "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs"
+by (induction xs) auto
+
+lemma upd_list_snoc:
+ "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]"
+by(induction xs) (auto simp add: sorted_mid_iff2)
+
subsection \<open>Lemmas for @{const del_list}\<close>
@@ -137,6 +147,19 @@
by (auto simp: del_list_sorted sorted_lems)
lemmas del_list_simps = sorted_lems
- del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
+ del_list_sorted1
+ del_list_sorted2
+ del_list_sorted3
+ del_list_sorted4
+ del_list_sorted5
+
+text\<open>Splay trees need two additional @{const del_list} lemmas:\<close>
+
+lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs"
+by(induction xs)(auto simp: sorted_Cons_iff)
+
+lemma del_list_sorted_app:
+ "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
+by (induction xs) (auto simp: sorted_mid_iff2)
end
--- a/src/HOL/Data_Structures/List_Ins_Del.thy Tue Nov 17 15:51:48 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Wed Nov 18 08:54:58 2015 +0100
@@ -78,6 +78,14 @@
lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
+text\<open>Splay trees need two additional @{const ins_list} lemmas:\<close>
+
+lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
+by (induction xs) auto
+
+lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]"
+by(induction xs) (auto simp add: sorted_mid_iff2)
+
subsection \<open>Delete one occurrence of an element from a list:\<close>
@@ -140,4 +148,13 @@
del_list_sorted4
del_list_sorted5
+text\<open>Splay trees need two additional @{const del_list} lemmas:\<close>
+
+lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
+by(induction xs)(auto simp: sorted_Cons_iff)
+
+lemma del_list_sorted_app:
+ "sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
+by (induction xs) (auto simp: sorted_mid_iff2)
+
end
--- a/src/HOL/Data_Structures/Sorted_Less.thy Tue Nov 17 15:51:48 2015 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy Wed Nov 18 08:54:58 2015 +0100
@@ -51,4 +51,14 @@
lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
+text\<open>Splay trees need two additional @{const sorted} lemmas:\<close>
+
+lemma sorted_snoc_le:
+ "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
+by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def)
+
+lemma sorted_Cons_le:
+ "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
+by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def)
+
end
--- a/src/HOL/Data_Structures/Splay_Map.thy Tue Nov 17 15:51:48 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Map.thy Wed Nov 18 08:54:58 2015 +0100
@@ -118,16 +118,6 @@
by(induction x t arbitrary: l a r rule: splay.induct)
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
-(* more upd_list lemmas; unify with basic set? *)
-
-lemma upd_list_Cons:
- "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs"
-by (induction xs) auto
-
-lemma upd_list_snoc:
- "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]"
-by(induction xs) (auto simp add: sorted_mid_iff2)
-
lemma inorder_update:
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
@@ -136,15 +126,6 @@
subsubsection "Proofs for delete"
-(* more del_simp lemmas; unify with basic set? *)
-
-lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs"
-by(induction xs)(auto simp: sorted_Cons_iff)
-
-lemma del_list_sorted_app:
- "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
-by (induction xs) (auto simp: sorted_mid_iff2)
-
lemma inorder_splay_maxD:
"splay_max t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
inorder l @ [a] = inorder t \<and> r = Leaf"
--- a/src/HOL/Data_Structures/Splay_Set.thy Tue Nov 17 15:51:48 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 18 08:54:58 2015 +0100
@@ -1,6 +1,6 @@
(*
Author: Tobias Nipkow
-Function defs follow AFP entry Splay_Tree, proofs are new.
+Function follow AFP entry Splay_Tree, proofs are new.
*)
section "Splay Tree Implementation of Sets"
@@ -136,16 +136,6 @@
subsubsection "Proofs for insert"
-text\<open>Splay trees need two addition @{const sorted} lemmas:\<close>
-
-lemma sorted_snoc_le:
- "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
-by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def)
-
-lemma sorted_Cons_le:
- "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
-by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def)
-
lemma inorder_splay: "inorder(splay x t) = inorder t"
by(induction x t rule: splay.induct)
(auto simp: neq_Leaf_iff split: tree.split)
@@ -157,14 +147,6 @@
by(induction x t arbitrary: l a r rule: splay.induct)
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
-text\<open>Splay trees need two addition @{const ins_list} lemmas:\<close>
-
-lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
-by (induction xs) auto
-
-lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]"
-by(induction xs) (auto simp add: sorted_mid_iff2)
-
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
@@ -173,15 +155,6 @@
subsubsection "Proofs for delete"
-text\<open>Splay trees need two addition @{const del_list} lemmas:\<close>
-
-lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
-by(induction xs)(auto simp: sorted_Cons_iff)
-
-lemma del_list_sorted_app:
- "sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
-by (induction xs) (auto simp: sorted_mid_iff2)
-
lemma inorder_splay_maxD:
"splay_max t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
inorder l @ [a] = inorder t \<and> r = Leaf"