tuned names and optimized comparison order
authornipkow
Mon Nov 02 18:35:30 2015 +0100 (2015-11-02)
changeset 61534a88e07c8d0d5
parent 61532 e3984606b4b6
child 61535 4133c0875e7b
tuned names and optimized comparison order
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/Set_by_Ordered.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_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	Mon Nov 02 11:56:38 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Nov 02 18:35:30 2015 +0100
     1.3 @@ -14,39 +14,39 @@
     1.4  hide_const (open) map_of
     1.5  
     1.6  fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
     1.7 -"map_of [] = (\<lambda>a. None)" |
     1.8 -"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
     1.9 +"map_of [] = (\<lambda>x. None)" |
    1.10 +"map_of ((a,b)#ps) = (\<lambda>x. if x=a then Some b else map_of ps x)"
    1.11  
    1.12  text \<open>Updating an association list:\<close>
    1.13  
    1.14  fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
    1.15 -"upd_list a b [] = [(a,b)]" |
    1.16 -"upd_list a b ((x,y)#ps) =
    1.17 -  (if a < x then (a,b)#(x,y)#ps else
    1.18 -  if a=x then (a,b)#ps else (x,y) # upd_list a b ps)"
    1.19 +"upd_list x y [] = [(x,y)]" |
    1.20 +"upd_list x y ((a,b)#ps) =
    1.21 +  (if x < a then (x,y)#(a,b)#ps else
    1.22 +  if x = a then (x,y)#ps else (a,b) # upd_list x y ps)"
    1.23  
    1.24  fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where
    1.25 -"del_list a [] = []" |
    1.26 -"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)"
    1.27 +"del_list x [] = []" |
    1.28 +"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)"
    1.29  
    1.30  
    1.31  subsection \<open>Lemmas for @{const map_of}\<close>
    1.32  
    1.33 -lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)"
    1.34 +lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)"
    1.35  by(induction ps) auto
    1.36  
    1.37 -lemma map_of_append: "map_of (ps @ qs) a =
    1.38 -  (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)"
    1.39 +lemma map_of_append: "map_of (ps @ qs) x =
    1.40 +  (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)"
    1.41  by(induction ps)(auto)
    1.42  
    1.43 -lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None"
    1.44 +lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None"
    1.45  by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
    1.46  
    1.47 -lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None"
    1.48 +lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None"
    1.49  by (induction ps) (auto simp: sorted_lems)
    1.50  
    1.51  lemma map_of_del_list: "sorted1 ps \<Longrightarrow>
    1.52 -  map_of(del_list a ps) = (map_of ps)(a := None)"
    1.53 +  map_of(del_list x ps) = (map_of ps)(x := None)"
    1.54  by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)
    1.55  
    1.56  lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
    1.57 @@ -63,19 +63,19 @@
    1.58  
    1.59  subsection \<open>Lemmas for @{const upd_list}\<close>
    1.60  
    1.61 -lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)"
    1.62 -apply(induction ps) 
    1.63 +lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)"
    1.64 +apply(induction ps)
    1.65   apply simp
    1.66  apply(case_tac ps)
    1.67   apply auto
    1.68  done
    1.69  
    1.70 -lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow>
    1.71 -  upd_list a b (ps @ (x,y) # qs) =  upd_list a b ps @ (x,y) # qs"
    1.72 +lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow>
    1.73 +  upd_list x y (ps @ (a,b) # qs) =  upd_list x y ps @ (a,b) # qs"
    1.74  by(induction ps) (auto simp: sorted_lems)
    1.75  
    1.76 -lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow>
    1.77 -  upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
    1.78 +lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow>
    1.79 +  upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)"
    1.80  by(induction ps) (auto simp: sorted_lems)
    1.81  
    1.82  lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
    1.83 @@ -110,28 +110,28 @@
    1.84  lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
    1.85  by (induct xs) auto
    1.86  
    1.87 -lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow>
    1.88 -  del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)"
    1.89 +lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \<Longrightarrow> a \<le> x \<Longrightarrow>
    1.90 +  del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)"
    1.91  by (induction xs) (auto simp: sorted_mid_iff2)
    1.92  
    1.93 -lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow>
    1.94 -  del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys"
    1.95 +lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow>
    1.96 +  del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys"
    1.97  by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
    1.98  
    1.99  lemma del_list_sorted3:
   1.100 -  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow>
   1.101 -  del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs"
   1.102 +  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow>
   1.103 +  del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs"
   1.104  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
   1.105  
   1.106  lemma del_list_sorted4:
   1.107 -  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow>
   1.108 -  del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) = del_list a (xs @ (x,x') # ys @ (y,y') # zs) @ (z,z') # us"
   1.109 +  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow>
   1.110 +  del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) = del_list x (xs @ (a,a') # ys @ (b,b') # zs) @ (c,c') # us"
   1.111  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
   1.112  
   1.113  lemma del_list_sorted5:
   1.114 -  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow>
   1.115 -   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) =
   1.116 -   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs" 
   1.117 +  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow>
   1.118 +   del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) =
   1.119 +   del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs" 
   1.120  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
   1.121  
   1.122  lemmas del_list_sorted =
     2.1 --- a/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Nov 02 11:56:38 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Nov 02 18:35:30 2015 +0100
     2.3 @@ -52,8 +52,8 @@
     2.4  
     2.5  fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     2.6  "ins_list x [] = [x]" |
     2.7 -"ins_list x (y#zs) =
     2.8 -  (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)"
     2.9 +"ins_list x (a#xs) =
    2.10 +  (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
    2.11  
    2.12  lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
    2.13  by(induction xs) auto
    2.14 @@ -66,12 +66,12 @@
    2.15  lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
    2.16  by(induction xs rule: sorted.induct) auto
    2.17  
    2.18 -lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow>
    2.19 -  ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)"
    2.20 +lemma ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
    2.21 +  ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
    2.22  by(induction xs) (auto simp: sorted_lems)
    2.23  
    2.24 -lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow>
    2.25 -  ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
    2.26 +lemma ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
    2.27 +  ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"
    2.28  by(induction xs) (auto simp: sorted_lems)
    2.29  
    2.30  lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
    2.31 @@ -80,8 +80,8 @@
    2.32  subsection \<open>Delete one occurrence of an element from a list:\<close>
    2.33  
    2.34  fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.35 -"del_list a [] = []" |
    2.36 -"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)"
    2.37 +"del_list x [] = []" |
    2.38 +"del_list x (a#xs) = (if x=a then xs else a # del_list x xs)"
    2.39  
    2.40  lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
    2.41  by (induct xs) simp_all
    2.42 @@ -99,28 +99,28 @@
    2.43  apply auto
    2.44  by (meson order.strict_trans sorted_Cons_iff)
    2.45  
    2.46 -lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow>
    2.47 -  del_list y (xs @ x # ys) = xs @ del_list y (x # ys)"
    2.48 +lemma del_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
    2.49 +  del_list x (xs @ a # ys) = xs @ del_list x (a # ys)"
    2.50  by (induction xs) (auto simp: sorted_mid_iff2)
    2.51  
    2.52 -lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow>
    2.53 -  del_list y (xs @ x # ys) = del_list y xs @ x # ys"
    2.54 +lemma del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow>
    2.55 +  del_list x (xs @ a # ys) = del_list x xs @ a # ys"
    2.56  by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem)
    2.57  
    2.58  lemma del_list_sorted3:
    2.59 -  "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow>
    2.60 -  del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs"
    2.61 +  "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow>
    2.62 +  del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs"
    2.63  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2)
    2.64  
    2.65  lemma del_list_sorted4:
    2.66 -  "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow>
    2.67 -  del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us"
    2.68 +  "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow>
    2.69 +  del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us"
    2.70  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
    2.71  
    2.72  lemma del_list_sorted5:
    2.73 -  "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow>
    2.74 -   del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) =
    2.75 -   del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" 
    2.76 +  "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow>
    2.77 +   del_list x (xs @ a # ys @ b # zs @ c # us @ d # vs) =
    2.78 +   del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs" 
    2.79  by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
    2.80  
    2.81  lemmas del_list_simps = sorted_lems
     3.1 --- a/src/HOL/Data_Structures/RBT.thy	Mon Nov 02 11:56:38 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT.thy	Mon Nov 02 18:35:30 2015 +0100
     3.3 @@ -27,23 +27,23 @@
     3.4  "red (Node _ l a r) = R l a r"
     3.5  
     3.6  fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     3.7 -"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
     3.8 +"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
     3.9  "balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
    3.10  "balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
    3.11  "balL t1 x t2 = R t1 x t2"
    3.12  
    3.13  fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.14  "balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
    3.15 -"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
    3.16 -"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
    3.17 +"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" |
    3.18 +"balR (R t1 x (B t2 y t3)) z t4 = R (bal (red t1) x t2) y (B t3 z t4)" |
    3.19  "balR t1 x t2 = R t1 x t2"
    3.20  
    3.21  fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.22  "combine Leaf t = t" |
    3.23  "combine t Leaf = t" |
    3.24 -"combine (R a x b) (R c y d) = (case combine b c of
    3.25 -    R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
    3.26 -    bc \<Rightarrow> R a x (R bc y d))" |
    3.27 +"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
    3.28 +    R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
    3.29 +    t23 \<Rightarrow> R t1 a (R t23 c t4))" |
    3.30  "combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
    3.31      R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
    3.32      t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
     4.1 --- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Mon Nov 02 11:56:38 2015 +0100
     4.2 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Mon Nov 02 18:35:30 2015 +0100
     4.3 @@ -13,13 +13,13 @@
     4.4  fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
     4.5  fixes set :: "'s \<Rightarrow> 'a set"
     4.6  fixes invar :: "'s \<Rightarrow> bool"
     4.7 -assumes "set empty = {}"
     4.8 -assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
     4.9 -assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
    4.10 -assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
    4.11 -assumes "invar empty"
    4.12 -assumes "invar s \<Longrightarrow> invar(insert a s)"
    4.13 -assumes "invar s \<Longrightarrow> invar(delete a s)"
    4.14 +assumes set_empty:    "set empty = {}"
    4.15 +assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
    4.16 +assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
    4.17 +assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
    4.18 +assumes invar_empty:  "invar empty"
    4.19 +assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
    4.20 +assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
    4.21  
    4.22  locale Set_by_Ordered =
    4.23  fixes empty :: "'t"
    4.24 @@ -30,14 +30,14 @@
    4.25  fixes wf :: "'t \<Rightarrow> bool"
    4.26  assumes empty: "inorder empty = []"
    4.27  assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    4.28 -  isin t a = (a \<in> elems (inorder t))"
    4.29 +  isin t x = (x \<in> elems (inorder t))"
    4.30  assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    4.31 -  inorder(insert a t) = ins_list a (inorder t)"
    4.32 +  inorder(insert x t) = ins_list x (inorder t)"
    4.33  assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    4.34 -  inorder(delete a t) = del_list a (inorder t)"
    4.35 +  inorder(delete x t) = del_list x (inorder t)"
    4.36  assumes wf_empty:  "wf empty"
    4.37 -assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
    4.38 -assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
    4.39 +assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)"
    4.40 +assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)"
    4.41  begin
    4.42  
    4.43  sublocale Set
    4.44 @@ -49,8 +49,8 @@
    4.45  next
    4.46    case 3 thus ?case by(simp add: insert)
    4.47  next
    4.48 -  case (4 s a) show ?case
    4.49 -    using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
    4.50 +  case (4 s x) show ?case
    4.51 +    using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
    4.52  next
    4.53    case 5 thus ?case by(simp add: empty wf_empty)
    4.54  next
     5.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Mon Nov 02 11:56:38 2015 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Mon Nov 02 18:35:30 2015 +0100
     5.3 @@ -21,53 +21,53 @@
     5.4     else lookup r x)"
     5.5  
     5.6  fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
     5.7 -"upd a b Leaf = Up\<^sub>i Leaf (a,b) Leaf" |
     5.8 -"upd a b (Node2 l xy r) =
     5.9 -   (if a < fst xy then
    5.10 -        (case upd a b l of
    5.11 -           T\<^sub>i l' => T\<^sub>i (Node2 l' xy r)
    5.12 -         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 xy r))
    5.13 -    else if a = fst xy then T\<^sub>i (Node2 l (a,b) r)
    5.14 +"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
    5.15 +"upd x y (Node2 l ab r) =
    5.16 +   (if x < fst ab then
    5.17 +        (case upd x y l of
    5.18 +           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
    5.19 +         | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r))
    5.20 +    else if x = fst ab then T\<^sub>i (Node2 l (x,y) r)
    5.21      else
    5.22 -        (case upd a b r of
    5.23 -           T\<^sub>i r' => T\<^sub>i (Node2 l xy r')
    5.24 -         | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l xy r1 q r2)))" |
    5.25 -"upd a b (Node3 l xy1 m xy2 r) =
    5.26 -   (if a < fst xy1 then
    5.27 -        (case upd a b l of
    5.28 -           T\<^sub>i l' => T\<^sub>i (Node3 l' xy1 m xy2 r)
    5.29 -         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) xy1 (Node2 m xy2 r))
    5.30 -    else if a = fst xy1 then T\<^sub>i (Node3 l (a,b) m xy2 r)
    5.31 -    else if a < fst xy2 then
    5.32 -             (case upd a b m of
    5.33 -                T\<^sub>i m' => T\<^sub>i (Node3 l xy1 m' xy2 r)
    5.34 -              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l xy1 m1) q (Node2 m2 xy2 r))
    5.35 -         else if a = fst xy2 then T\<^sub>i (Node3 l xy1 m (a,b) r)
    5.36 +        (case upd x y r of
    5.37 +           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
    5.38 +         | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
    5.39 +"upd x y (Node3 l ab1 m ab2 r) =
    5.40 +   (if x < fst ab1 then
    5.41 +        (case upd x y l of
    5.42 +           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
    5.43 +         | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r))
    5.44 +    else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r)
    5.45 +    else if x < fst ab2 then
    5.46 +             (case upd x y m of
    5.47 +                T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
    5.48 +              | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r))
    5.49 +         else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r)
    5.50           else
    5.51 -             (case upd a b r of
    5.52 -                T\<^sub>i r' => T\<^sub>i (Node3 l xy1 m xy2 r')
    5.53 -              | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l xy1 m) xy2 (Node2 r1 q r2)))"
    5.54 +             (case upd x y r of
    5.55 +                T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
    5.56 +              | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2)))"
    5.57  
    5.58  definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    5.59  "update a b t = tree\<^sub>i(upd a b t)"
    5.60  
    5.61  fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d"
    5.62  where
    5.63 -"del k Leaf = T\<^sub>d Leaf" |
    5.64 -"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
    5.65 -"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=fst p then Node2 Leaf q Leaf
    5.66 -  else if k=fst q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
    5.67 -"del k (Node2 l a r) = (if k<fst a then node21 (del k l) a r else
    5.68 -  if k > fst a then node22 l a (del k r) else
    5.69 -  let (a',t) = del_min r in node22 l a' t)" |
    5.70 -"del k (Node3 l a m b r) = (if k<fst a then node31 (del k l) a m b r else
    5.71 -  if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else
    5.72 -  if k < fst b then node32 l a (del k m) b r else
    5.73 -  if k = fst b then let (b',r') = del_min r in node33 l a m b' r'
    5.74 -  else node33 l a m b (del k r))"
    5.75 +"del x Leaf = T\<^sub>d Leaf" |
    5.76 +"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
    5.77 +"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
    5.78 +  else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
    5.79 +"del x (Node2 l ab1 r) = (if x<fst ab1 then node21 (del x l) ab1 r else
    5.80 +  if x > fst ab1 then node22 l ab1 (del x r) else
    5.81 +  let (ab1',t) = del_min r in node22 l ab1' t)" |
    5.82 +"del x (Node3 l ab1 m ab2 r) = (if x<fst ab1 then node31 (del x l) ab1 m ab2 r else
    5.83 +  if x = fst ab1 then let (ab1',m') = del_min m in node32 l ab1' m' ab2 r else
    5.84 +  if x < fst ab2 then node32 l ab1 (del x m) ab2 r else
    5.85 +  if x = fst ab2 then let (ab2',r') = del_min r in node33 l ab1 m ab2' r'
    5.86 +  else node33 l ab1 m ab2 (del x r))"
    5.87  
    5.88  definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    5.89 -"delete k t = tree\<^sub>d(del k t)"
    5.90 +"delete x t = tree\<^sub>d(del x t)"
    5.91  
    5.92  
    5.93  subsection \<open>Functional Correctness\<close>
     6.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Mon Nov 02 11:56:38 2015 +0100
     6.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Mon Nov 02 18:35:30 2015 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4  "isin Leaf x = False" |
     6.5  "isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" |
     6.6  "isin (Node3 l a m b r) x =
     6.7 -  (x < a \<and> isin l x \<or> x = a \<or> (x < b \<and> isin m x \<or> x = b \<or> isin r x))"
     6.8 +  (x < a \<and> isin l x \<or> x > b \<and> isin r x \<or> x = a \<or> x = b \<or> isin m x)"
     6.9  
    6.10  datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
    6.11  
    6.12 @@ -21,37 +21,38 @@
    6.13  "tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
    6.14  
    6.15  fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
    6.16 -"ins a Leaf = Up\<^sub>i Leaf a Leaf" |
    6.17 -"ins a (Node2 l x r) =
    6.18 -   (if a < x then
    6.19 -      case ins a l of
    6.20 -         T\<^sub>i l' => T\<^sub>i (Node2 l' x r)
    6.21 -       | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r)
    6.22 -    else if a=x then T\<^sub>i (Node2 l x r)
    6.23 +"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    6.24 +"ins x (Node2 l a r) =
    6.25 +   (if x < a then
    6.26 +      case ins x l of
    6.27 +         T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
    6.28 +       | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)
    6.29 +    else if x=a then T\<^sub>i (Node2 l x r)
    6.30      else
    6.31 -      case ins a r of
    6.32 -        T\<^sub>i r' => T\<^sub>i (Node2 l x r')
    6.33 -      | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2))" |
    6.34 -"ins a (Node3 l x1 m x2 r) =
    6.35 -   (if a < x1 then
    6.36 -      case ins a l of
    6.37 -        T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r)
    6.38 -      | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node2 m x2 r)
    6.39 -    else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r)
    6.40 -    else if a < x2 then
    6.41 -           case ins a m of
    6.42 -             T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r)
    6.43 -           | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node2 m2 x2 r)
    6.44 -         else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r)
    6.45 -         else
    6.46 -           case ins a r of
    6.47 -             T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r')
    6.48 -           | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node2 r1 q r2))"
    6.49 +      case ins x r of
    6.50 +        T\<^sub>i r' => T\<^sub>i (Node2 l a r')
    6.51 +      | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2))" |
    6.52 +"ins x (Node3 l a m b r) =
    6.53 +   (if x < a then
    6.54 +      case ins x l of
    6.55 +        T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
    6.56 +      | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)
    6.57 +    else
    6.58 +    if x > b then
    6.59 +      case ins x r of
    6.60 +        T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
    6.61 +      | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)
    6.62 +    else
    6.63 +    if x=a \<or> x = b then T\<^sub>i (Node3 l a m b r)
    6.64 +    else
    6.65 +      case ins x m of
    6.66 +        T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
    6.67 +      | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))"
    6.68  
    6.69  hide_const insert
    6.70  
    6.71  definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    6.72 -"insert a t = tree\<^sub>i(ins a t)"
    6.73 +"insert x t = tree\<^sub>i(ins x t)"
    6.74  
    6.75  datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
    6.76  
    6.77 @@ -94,21 +95,21 @@
    6.78  
    6.79  fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
    6.80  where
    6.81 -"del k Leaf = T\<^sub>d Leaf" |
    6.82 -"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
    6.83 -"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
    6.84 -  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
    6.85 -"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else
    6.86 -  if k > a then node22 l a (del k r) else
    6.87 +"del x Leaf = T\<^sub>d Leaf" |
    6.88 +"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
    6.89 +"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
    6.90 +  else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
    6.91 +"del x (Node2 l a r) = (if x<a then node21 (del x l) a r else
    6.92 +  if x > a then node22 l a (del x r) else
    6.93    let (a',t) = del_min r in node22 l a' t)" |
    6.94 -"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else
    6.95 -  if k = a then let (a',m') = del_min m in node32 l a' m' b r else
    6.96 -  if k < b then node32 l a (del k m) b r else
    6.97 -  if k = b then let (b',r') = del_min r in node33 l a m b' r'
    6.98 -  else node33 l a m b (del k r))"
    6.99 +"del x (Node3 l a m b r) = (if x<a then node31 (del x l) a m b r else
   6.100 +  if x = a then let (a',m') = del_min m in node32 l a' m' b r else
   6.101 +  if x < b then node32 l a (del x m) b r else
   6.102 +  if x = b then let (b',r') = del_min r in node33 l a m b' r'
   6.103 +  else node33 l a m b (del x r))"
   6.104  
   6.105  definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   6.106 -"delete k t = tree\<^sub>d(del k t)"
   6.107 +"delete x t = tree\<^sub>d(del x t)"
   6.108  
   6.109  
   6.110  subsection "Functional Correctness"
   6.111 @@ -127,7 +128,7 @@
   6.112  
   6.113  lemma inorder_ins:
   6.114    "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   6.115 -by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
   6.116 +by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) (* 38 secs in 2015 *)
   6.117  
   6.118  lemma inorder_insert:
   6.119    "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   6.120 @@ -194,7 +195,7 @@
   6.121  end
   6.122  
   6.123  lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   6.124 -by (induct t) (auto split: up\<^sub>i.split) (* 25 secs in 2015 *)
   6.125 +by (induct t) (auto split: up\<^sub>i.split) (* 87 secs in 2015 *)
   6.126  
   6.127  text{* Now an alternative proof (by Brian Huffman) that runs faster because
   6.128  two properties (balance and height) are combined in one predicate. *}
     7.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 02 11:56:38 2015 +0100
     7.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 02 18:35:30 2015 +0100
     7.3 @@ -14,16 +14,16 @@
     7.4    if x > a then lookup r x else Some b)"
     7.5  
     7.6  fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
     7.7 -"update a b Leaf = Node Leaf (a,b) Leaf" |
     7.8 -"update a b (Node l (x,y) r) =
     7.9 -   (if a < x then Node (update a b l) (x,y) r
    7.10 -    else if a=x then Node l (a,b) r
    7.11 -    else Node l (x,y) (update a b r))"
    7.12 +"update x y Leaf = Node Leaf (x,y) Leaf" |
    7.13 +"update x y (Node l (a,b) r) =
    7.14 +   (if x < a then Node (update x y l) (a,b) r
    7.15 +    else if x = a then Node l (x,y) r
    7.16 +    else Node l (a,b) (update x y r))"
    7.17  
    7.18  fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    7.19 -"delete k Leaf = Leaf" |
    7.20 -"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
    7.21 -  if k > a then Node l (a,b) (delete k r) else
    7.22 +"delete x Leaf = Leaf" |
    7.23 +"delete x (Node l (a,b) r) = (if x < a then Node (delete x l) (a,b) r else
    7.24 +  if x > a then Node l (a,b) (delete x r) else
    7.25    if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
    7.26  
    7.27  
     8.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Mon Nov 02 11:56:38 2015 +0100
     8.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Mon Nov 02 18:35:30 2015 +0100
     8.3 @@ -15,20 +15,20 @@
     8.4  hide_const (open) insert
     8.5  
     8.6  fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
     8.7 -"insert a Leaf = Node Leaf a Leaf" |
     8.8 -"insert a (Node l x r) =
     8.9 -   (if a < x then Node (insert a l) x r
    8.10 -    else if a=x then Node l x r
    8.11 -    else Node l x (insert a r))"
    8.12 +"insert x Leaf = Node Leaf x Leaf" |
    8.13 +"insert x (Node l a r) =
    8.14 +   (if x < a then Node (insert x l) a r else
    8.15 +    if x = a then Node l a r
    8.16 +    else Node l a (insert x r))"
    8.17  
    8.18  fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    8.19  "del_min (Node Leaf a r) = (a, r)" |
    8.20  "del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
    8.21  
    8.22  fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    8.23 -"delete k Leaf = Leaf" |
    8.24 -"delete k (Node l a r) = (if k<a then Node (delete k l) a r else
    8.25 -  if k > a then Node l a (delete k r) else
    8.26 +"delete x Leaf = Leaf" |
    8.27 +"delete x (Node l a r) = (if x < a then Node (delete x l) a r else
    8.28 +  if x > a then Node l a (delete x r) else
    8.29    if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    8.30  
    8.31