# HG changeset patch # User nipkow # Date 1447833298 -3600 # Node ID ce6320b9ef9bbaf992d3477c37131fe09cdf07de # Parent df4a03527b565f7df9b2136c054f9785738b96c8 moved lemmas diff -r df4a03527b56 -r ce6320b9ef9b src/HOL/Data_Structures/AList_Upd_Del.thy --- 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\Splay trees need two additional @{const upd_list} lemmas:\ + +lemma upd_list_Cons: + "sorted1 ((x,y) # xs) \ upd_list x y xs = (x,y) # xs" +by (induction xs) auto + +lemma upd_list_snoc: + "sorted1 (xs @ [(x,y)]) \ upd_list x y xs = xs @ [(x,y)]" +by(induction xs) (auto simp add: sorted_mid_iff2) + subsection \Lemmas for @{const del_list}\ @@ -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\Splay trees need two additional @{const del_list} lemmas:\ + +lemma del_list_notin_Cons: "sorted (x # map fst xs) \ del_list x xs = xs" +by(induction xs)(auto simp: sorted_Cons_iff) + +lemma del_list_sorted_app: + "sorted(map fst xs @ [x]) \ del_list x (xs @ ys) = xs @ del_list x ys" +by (induction xs) (auto simp: sorted_mid_iff2) end diff -r df4a03527b56 -r ce6320b9ef9b src/HOL/Data_Structures/List_Ins_Del.thy --- 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\Splay trees need two additional @{const ins_list} lemmas:\ + +lemma ins_list_Cons: "sorted (x # xs) \ ins_list x xs = x # xs" +by (induction xs) auto + +lemma ins_list_snoc: "sorted (xs @ [x]) \ ins_list x xs = xs @ [x]" +by(induction xs) (auto simp add: sorted_mid_iff2) + subsection \Delete one occurrence of an element from a list:\ @@ -140,4 +148,13 @@ del_list_sorted4 del_list_sorted5 +text\Splay trees need two additional @{const del_list} lemmas:\ + +lemma del_list_notin_Cons: "sorted (x # xs) \ del_list x xs = xs" +by(induction xs)(auto simp: sorted_Cons_iff) + +lemma del_list_sorted_app: + "sorted(xs @ [x]) \ del_list x (xs @ ys) = xs @ del_list x ys" +by (induction xs) (auto simp: sorted_mid_iff2) + end diff -r df4a03527b56 -r ce6320b9ef9b src/HOL/Data_Structures/Sorted_Less.thy --- 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\Splay trees need two additional @{const sorted} lemmas:\ + +lemma sorted_snoc_le: + "ASSUMPTION(sorted(xs @ [x])) \ x \ y \ sorted (xs @ [y])" +by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def) + +lemma sorted_Cons_le: + "ASSUMPTION(sorted(x # xs)) \ y \ x \ sorted (y # xs)" +by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def) + end diff -r df4a03527b56 -r ce6320b9ef9b src/HOL/Data_Structures/Splay_Map.thy --- 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) \ upd_list x y xs = (x,y) # xs" -by (induction xs) auto - -lemma upd_list_snoc: - "sorted1 (xs @ [(x,y)]) \ upd_list x y xs = xs @ [(x,y)]" -by(induction xs) (auto simp add: sorted_mid_iff2) - lemma inorder_update: "sorted1(inorder t) \ 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) \ del_list x xs = xs" -by(induction xs)(auto simp: sorted_Cons_iff) - -lemma del_list_sorted_app: - "sorted(map fst xs @ [x]) \ 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 \ sorted1(inorder t) \ inorder l @ [a] = inorder t \ r = Leaf" diff -r df4a03527b56 -r ce6320b9ef9b src/HOL/Data_Structures/Splay_Set.thy --- 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\Splay trees need two addition @{const sorted} lemmas:\ - -lemma sorted_snoc_le: - "ASSUMPTION(sorted(xs @ [x])) \ x \ y \ sorted (xs @ [y])" -by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def) - -lemma sorted_Cons_le: - "ASSUMPTION(sorted(x # xs)) \ y \ x \ 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\Splay trees need two addition @{const ins_list} lemmas:\ - -lemma ins_list_Cons: "sorted (x # xs) \ ins_list x xs = x # xs" -by (induction xs) auto - -lemma ins_list_snoc: "sorted (xs @ [x]) \ ins_list x xs = xs @ [x]" -by(induction xs) (auto simp add: sorted_mid_iff2) - lemma inorder_insert: "sorted(inorder t) \ 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\Splay trees need two addition @{const del_list} lemmas:\ - -lemma del_list_notin_Cons: "sorted (x # xs) \ del_list x xs = xs" -by(induction xs)(auto simp: sorted_Cons_iff) - -lemma del_list_sorted_app: - "sorted(xs @ [x]) \ 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 \ sorted(inorder t) \ inorder l @ [a] = inorder t \ r = Leaf"