tuned
authornipkow
Wed Sep 23 09:14:22 2015 +0200 (2015-09-23)
changeset 61231cc6969542f8d
parent 61230 e367b93f78e5
child 61232 c46faf9762f7
tuned
src/HOL/Data_Structures/AList_Upd_Del.thy
src/HOL/Data_Structures/List_Ins_Del.thy
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Sep 22 17:13:13 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Wed Sep 23 09:14:22 2015 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  "map_of [] = (\<lambda>a. None)" |
     1.5  "map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
     1.6  
     1.7 -text \<open>Updating into an association list:\<close>
     1.8 +text \<open>Updating an association list:\<close>
     1.9  
    1.10  fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
    1.11  "upd_list a b [] = [(a,b)]" |
    1.12 @@ -58,6 +58,7 @@
    1.13  by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
    1.14  
    1.15  lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
    1.16 +lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds
    1.17  
    1.18  
    1.19  subsection \<open>Lemmas for @{const upd_list}\<close>
    1.20 @@ -136,4 +137,6 @@
    1.21  lemmas del_list_sorted =
    1.22    del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
    1.23  
    1.24 +lemmas del_list_simps = sorted_lems del_list_sorted
    1.25 +
    1.26  end
     2.1 --- a/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Sep 22 17:13:13 2015 +0200
     2.2 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Sep 23 09:14:22 2015 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4    ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
     2.5  by(induction xs) (auto simp: sorted_lems)
     2.6  
     2.7 -lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
     2.8 +lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
     2.9  
    2.10  
    2.11  subsection \<open>Delete one occurrence of an element from a list:\<close>
    2.12 @@ -123,7 +123,7 @@
    2.13     del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" 
    2.14  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
    2.15  
    2.16 -lemmas del_simps = sorted_lems
    2.17 +lemmas del_list_simps = sorted_lems
    2.18    del_list_sorted1
    2.19    del_list_sorted2
    2.20    del_list_sorted3
     3.1 --- a/src/HOL/Data_Structures/RBT.thy	Tue Sep 22 17:13:13 2015 +0200
     3.2 +++ b/src/HOL/Data_Structures/RBT.thy	Wed Sep 23 09:14:22 2015 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (* Author: Tobias Nipkow *)
     3.5  
     3.6 -section \<open>Red-Black Trees\<close>
     3.7 +section \<open>Red-Black Tree\<close>
     3.8  
     3.9  theory RBT
    3.10  imports Tree2
     4.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Tue Sep 22 17:13:13 2015 +0200
     4.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Wed Sep 23 09:14:22 2015 +0200
     4.3 @@ -5,15 +5,9 @@
     4.4  theory RBT_Map
     4.5  imports
     4.6    RBT_Set
     4.7 -  Map_by_Ordered
     4.8 +  Lookup2
     4.9  begin
    4.10  
    4.11 -fun lookup :: "('a::linorder * 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b option" where
    4.12 -"lookup Leaf x = None" |
    4.13 -"lookup (Node _ l (a,b) r) x =
    4.14 -  (if x < a then lookup l x else
    4.15 -   if x > a then lookup r x else Some b)"
    4.16 -
    4.17  fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
    4.18  "update x y Leaf = R Leaf (x,y) Leaf" |
    4.19  "update x y (B l (a,b) r) =
    4.20 @@ -41,12 +35,6 @@
    4.21  
    4.22  subsection "Functional Correctness Proofs"
    4.23  
    4.24 -lemma lookup_eq:
    4.25 -  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    4.26 -by(induction t)
    4.27 -  (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    4.28 -
    4.29 -
    4.30  lemma inorder_update:
    4.31    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    4.32  by(induction x y t rule: update.induct)
    4.33 @@ -60,7 +48,7 @@
    4.34   "sorted1(inorder t2) \<Longrightarrow>  inorder(deleteR x t1 a t2) =
    4.35      inorder t1 @ a # del_list x (inorder t2)"
    4.36  by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct)
    4.37 -  (auto simp: del_list_sorted sorted_lems inorder_combine inorder_balL inorder_balR)
    4.38 +  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    4.39  
    4.40  
    4.41  interpretation Map_by_Ordered
     5.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Sep 22 17:13:13 2015 +0200
     5.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Sep 23 09:14:22 2015 +0200
     5.3 @@ -35,29 +35,27 @@
     5.4  
     5.5  lemma inorder_bal:
     5.6    "inorder(bal l a r) = inorder l @ a # inorder r"
     5.7 -by(induction l a r rule: bal.induct) (auto simp: sorted_lems)
     5.8 +by(induction l a r rule: bal.induct) (auto)
     5.9  
    5.10  lemma inorder_insert:
    5.11    "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
    5.12 -by(induction a t rule: insert.induct) (auto simp: ins_simps inorder_bal)
    5.13 +by(induction a t rule: insert.induct) (auto simp: ins_list_simps inorder_bal)
    5.14  
    5.15  lemma inorder_red: "inorder(red t) = inorder t"
    5.16 -by(induction t) (auto simp: sorted_lems)
    5.17 +by(induction t) (auto)
    5.18  
    5.19  lemma inorder_balL:
    5.20    "inorder(balL l a r) = inorder l @ a # inorder r"
    5.21 -by(induction l a r rule: balL.induct)
    5.22 -  (auto simp: sorted_lems inorder_bal inorder_red)
    5.23 +by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_red)
    5.24  
    5.25  lemma inorder_balR:
    5.26    "inorder(balR l a r) = inorder l @ a # inorder r"
    5.27 -by(induction l a r rule: balR.induct)
    5.28 -  (auto simp: sorted_lems inorder_bal inorder_red)
    5.29 +by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_red)
    5.30  
    5.31  lemma inorder_combine:
    5.32    "inorder(combine l r) = inorder l @ inorder r"
    5.33  by(induction l r rule: combine.induct)
    5.34 -  (auto simp: sorted_lems inorder_balL inorder_balR split: tree.split color.split)
    5.35 +  (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    5.36  
    5.37  lemma inorder_delete:
    5.38   "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
    5.39 @@ -66,7 +64,7 @@
    5.40   "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
    5.41      inorder l @ a # del_list x (inorder r)"
    5.42  by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    5.43 -  (auto simp: del_simps inorder_combine inorder_balL inorder_balR)
    5.44 +  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    5.45  
    5.46  interpretation Set_by_Ordered
    5.47  where empty = Leaf and isin = isin and insert = insert and delete = delete
     6.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Tue Sep 22 17:13:13 2015 +0200
     6.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Wed Sep 23 09:14:22 2015 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  
     6.5  theory Tree_Map
     6.6  imports
     6.7 -  "~~/src/HOL/Library/Tree"
     6.8 +  Tree_Set
     6.9    Map_by_Ordered
    6.10  begin
    6.11  
    6.12 @@ -20,10 +20,6 @@
    6.13      else if a=x then Node l (a,b) r
    6.14      else Node l (x,y) (update a b r))"
    6.15  
    6.16 -fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    6.17 -"del_min (Node Leaf a r) = (a, r)" |
    6.18 -"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
    6.19 -
    6.20  fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    6.21  "delete k Leaf = Leaf" |
    6.22  "delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
    6.23 @@ -35,9 +31,7 @@
    6.24  
    6.25  lemma lookup_eq:
    6.26    "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    6.27 -apply (induction t)
    6.28 -apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    6.29 -done
    6.30 +by (induction t) (auto simp: map_of_simps split: option.split)
    6.31  
    6.32  
    6.33  lemma inorder_update:
    6.34 @@ -49,12 +43,11 @@
    6.35    "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
    6.36     x # inorder t' = inorder t"
    6.37  by(induction t arbitrary: t' rule: del_min.induct)
    6.38 -  (auto simp: sorted_lems split: prod.splits)
    6.39 +  (auto simp: del_list_simps split: prod.splits)
    6.40  
    6.41  lemma inorder_delete:
    6.42    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    6.43 -by(induction t)
    6.44 -  (auto simp: del_list_sorted sorted_lems dest!: del_minD split: prod.splits)
    6.45 +by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
    6.46  
    6.47  
    6.48  interpretation Map_by_Ordered
     7.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Tue Sep 22 17:13:13 2015 +0200
     7.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Wed Sep 23 09:14:22 2015 +0200
     7.3 @@ -43,7 +43,7 @@
     7.4  
     7.5  lemma inorder_insert:
     7.6    "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
     7.7 -by(induction t) (auto simp: ins_simps)
     7.8 +by(induction t) (auto simp: ins_list_simps)
     7.9  
    7.10  
    7.11  lemma del_minD:
    7.12 @@ -54,7 +54,7 @@
    7.13  
    7.14  lemma inorder_delete:
    7.15    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    7.16 -by(induction t) (auto simp: del_simps del_minD split: prod.splits)
    7.17 +by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
    7.18  
    7.19  
    7.20  interpretation Set_by_Ordered