--- a/src/HOL/Data_Structures/AList_Upd_Del.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy Mon Nov 02 18:35:30 2015 +0100
@@ -14,39 +14,39 @@
hide_const (open) map_of
fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"map_of [] = (\<lambda>a. None)" |
-"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
+"map_of [] = (\<lambda>x. None)" |
+"map_of ((a,b)#ps) = (\<lambda>x. if x=a then Some b else map_of ps x)"
text \<open>Updating an association list:\<close>
fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
-"upd_list a b [] = [(a,b)]" |
-"upd_list a b ((x,y)#ps) =
- (if a < x then (a,b)#(x,y)#ps else
- if a=x then (a,b)#ps else (x,y) # upd_list a b ps)"
+"upd_list x y [] = [(x,y)]" |
+"upd_list x y ((a,b)#ps) =
+ (if x < a then (x,y)#(a,b)#ps else
+ if x = a then (x,y)#ps else (a,b) # upd_list x y ps)"
fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where
-"del_list a [] = []" |
-"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)"
+"del_list x [] = []" |
+"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)"
subsection \<open>Lemmas for @{const map_of}\<close>
-lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)"
+lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)"
by(induction ps) auto
-lemma map_of_append: "map_of (ps @ qs) a =
- (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)"
+lemma map_of_append: "map_of (ps @ qs) x =
+ (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)"
by(induction ps)(auto)
-lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None"
+lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None"
by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
-lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None"
+lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None"
by (induction ps) (auto simp: sorted_lems)
lemma map_of_del_list: "sorted1 ps \<Longrightarrow>
- map_of(del_list a ps) = (map_of ps)(a := None)"
+ map_of(del_list x ps) = (map_of ps)(x := None)"
by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)
lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
@@ -63,19 +63,19 @@
subsection \<open>Lemmas for @{const upd_list}\<close>
-lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)"
-apply(induction ps)
+lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)"
+apply(induction ps)
apply simp
apply(case_tac ps)
apply auto
done
-lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow>
- upd_list a b (ps @ (x,y) # qs) = upd_list a b ps @ (x,y) # qs"
+lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow>
+ upd_list x y (ps @ (a,b) # qs) = upd_list x y ps @ (a,b) # qs"
by(induction ps) (auto simp: sorted_lems)
-lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow>
- upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
+lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow>
+ upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)"
by(induction ps) (auto simp: sorted_lems)
lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
@@ -110,28 +110,28 @@
lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
by (induct xs) auto
-lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow>
- del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)"
+lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+ del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)"
by (induction xs) (auto simp: sorted_mid_iff2)
-lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow>
- del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys"
+lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow>
+ del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys"
by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
lemma del_list_sorted3:
- "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow>
- del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs"
+ "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow>
+ del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
lemma del_list_sorted4:
- "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow>
- 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"
+ "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow>
+ 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"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
lemma del_list_sorted5:
- "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow>
- del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) =
- del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs"
+ "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow>
+ del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) =
+ del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
lemmas del_list_sorted =
--- a/src/HOL/Data_Structures/List_Ins_Del.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Mon Nov 02 18:35:30 2015 +0100
@@ -52,8 +52,8 @@
fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"ins_list x [] = [x]" |
-"ins_list x (y#zs) =
- (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)"
+"ins_list x (a#xs) =
+ (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
by(induction xs) auto
@@ -66,12 +66,12 @@
lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
by(induction xs rule: sorted.induct) auto
-lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow>
- ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)"
+lemma ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+ ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
by(induction xs) (auto simp: sorted_lems)
-lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow>
- ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
+lemma ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
+ ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"
by(induction xs) (auto simp: sorted_lems)
lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
@@ -80,8 +80,8 @@
subsection \<open>Delete one occurrence of an element from a list:\<close>
fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"del_list a [] = []" |
-"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)"
+"del_list x [] = []" |
+"del_list x (a#xs) = (if x=a then xs else a # del_list x xs)"
lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
by (induct xs) simp_all
@@ -99,28 +99,28 @@
apply auto
by (meson order.strict_trans sorted_Cons_iff)
-lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow>
- del_list y (xs @ x # ys) = xs @ del_list y (x # ys)"
+lemma del_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+ del_list x (xs @ a # ys) = xs @ del_list x (a # ys)"
by (induction xs) (auto simp: sorted_mid_iff2)
-lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow>
- del_list y (xs @ x # ys) = del_list y xs @ x # ys"
+lemma del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow>
+ del_list x (xs @ a # ys) = del_list x xs @ a # ys"
by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem)
lemma del_list_sorted3:
- "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow>
- del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs"
+ "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow>
+ del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2)
lemma del_list_sorted4:
- "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow>
- del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us"
+ "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow>
+ del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
lemma del_list_sorted5:
- "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow>
- del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) =
- del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs"
+ "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow>
+ del_list x (xs @ a # ys @ b # zs @ c # us @ d # vs) =
+ del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
lemmas del_list_simps = sorted_lems
--- a/src/HOL/Data_Structures/RBT.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Mon Nov 02 18:35:30 2015 +0100
@@ -27,23 +27,23 @@
"red (Node _ l a r) = R l a r"
fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
+"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
"balL t1 x t2 = R t1 x t2"
fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
-"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
-"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
+"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" |
+"balR (R t1 x (B t2 y t3)) z t4 = R (bal (red t1) x t2) y (B t3 z t4)" |
"balR t1 x t2 = R t1 x t2"
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"combine Leaf t = t" |
"combine t Leaf = t" |
-"combine (R a x b) (R c y d) = (case combine b c of
- R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
- bc \<Rightarrow> R a x (R bc y d))" |
+"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
+ R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
+ t23 \<Rightarrow> R t1 a (R t23 c t4))" |
"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy Mon Nov 02 18:35:30 2015 +0100
@@ -13,13 +13,13 @@
fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
fixes set :: "'s \<Rightarrow> 'a set"
fixes invar :: "'s \<Rightarrow> bool"
-assumes "set empty = {}"
-assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
-assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
-assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
-assumes "invar empty"
-assumes "invar s \<Longrightarrow> invar(insert a s)"
-assumes "invar s \<Longrightarrow> invar(delete a s)"
+assumes set_empty: "set empty = {}"
+assumes set_isin: "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
+assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
+assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
+assumes invar_empty: "invar empty"
+assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
+assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
locale Set_by_Ordered =
fixes empty :: "'t"
@@ -30,14 +30,14 @@
fixes wf :: "'t \<Rightarrow> bool"
assumes empty: "inorder empty = []"
assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
- isin t a = (a \<in> elems (inorder t))"
+ isin t x = (x \<in> elems (inorder t))"
assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
- inorder(insert a t) = ins_list a (inorder t)"
+ inorder(insert x t) = ins_list x (inorder t)"
assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
- inorder(delete a t) = del_list a (inorder t)"
+ inorder(delete x t) = del_list x (inorder t)"
assumes wf_empty: "wf empty"
-assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
-assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
+assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)"
+assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)"
begin
sublocale Set
@@ -49,8 +49,8 @@
next
case 3 thus ?case by(simp add: insert)
next
- case (4 s a) show ?case
- using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
+ case (4 s x) show ?case
+ using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
next
case 5 thus ?case by(simp add: empty wf_empty)
next
--- a/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 02 18:35:30 2015 +0100
@@ -21,53 +21,53 @@
else lookup r x)"
fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
-"upd a b Leaf = Up\<^sub>i Leaf (a,b) Leaf" |
-"upd a b (Node2 l xy r) =
- (if a < fst xy then
- (case upd a b l of
- T\<^sub>i l' => T\<^sub>i (Node2 l' xy r)
- | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 xy r))
- else if a = fst xy then T\<^sub>i (Node2 l (a,b) r)
+"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
+"upd x y (Node2 l ab r) =
+ (if x < fst ab then
+ (case upd x y l of
+ T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
+ | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r))
+ else if x = fst ab then T\<^sub>i (Node2 l (x,y) r)
else
- (case upd a b r of
- T\<^sub>i r' => T\<^sub>i (Node2 l xy r')
- | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l xy r1 q r2)))" |
-"upd a b (Node3 l xy1 m xy2 r) =
- (if a < fst xy1 then
- (case upd a b l of
- T\<^sub>i l' => T\<^sub>i (Node3 l' xy1 m xy2 r)
- | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) xy1 (Node2 m xy2 r))
- else if a = fst xy1 then T\<^sub>i (Node3 l (a,b) m xy2 r)
- else if a < fst xy2 then
- (case upd a b m of
- T\<^sub>i m' => T\<^sub>i (Node3 l xy1 m' xy2 r)
- | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l xy1 m1) q (Node2 m2 xy2 r))
- else if a = fst xy2 then T\<^sub>i (Node3 l xy1 m (a,b) r)
+ (case upd x y r of
+ T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
+ | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
+"upd x y (Node3 l ab1 m ab2 r) =
+ (if x < fst ab1 then
+ (case upd x y l of
+ T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
+ | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r))
+ else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r)
+ else if x < fst ab2 then
+ (case upd x y m of
+ T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
+ | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r))
+ else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r)
else
- (case upd a b r of
- T\<^sub>i r' => T\<^sub>i (Node3 l xy1 m xy2 r')
- | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l xy1 m) xy2 (Node2 r1 q r2)))"
+ (case upd x y r of
+ T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
+ | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2)))"
definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
"update a b t = tree\<^sub>i(upd a b t)"
fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d"
where
-"del k Leaf = T\<^sub>d Leaf" |
-"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
-"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=fst p then Node2 Leaf q Leaf
- else if k=fst q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
-"del k (Node2 l a r) = (if k<fst a then node21 (del k l) a r else
- if k > fst a then node22 l a (del k r) else
- let (a',t) = del_min r in node22 l a' t)" |
-"del k (Node3 l a m b r) = (if k<fst a then node31 (del k l) a m b r else
- if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else
- if k < fst b then node32 l a (del k m) b r else
- if k = fst b then let (b',r') = del_min r in node33 l a m b' r'
- else node33 l a m b (del k r))"
+"del x Leaf = T\<^sub>d Leaf" |
+"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
+"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
+ else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
+"del x (Node2 l ab1 r) = (if x<fst ab1 then node21 (del x l) ab1 r else
+ if x > fst ab1 then node22 l ab1 (del x r) else
+ let (ab1',t) = del_min r in node22 l ab1' t)" |
+"del x (Node3 l ab1 m ab2 r) = (if x<fst ab1 then node31 (del x l) ab1 m ab2 r else
+ if x = fst ab1 then let (ab1',m') = del_min m in node32 l ab1' m' ab2 r else
+ if x < fst ab2 then node32 l ab1 (del x m) ab2 r else
+ if x = fst ab2 then let (ab2',r') = del_min r in node33 l ab1 m ab2' r'
+ else node33 l ab1 m ab2 (del x r))"
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
-"delete k t = tree\<^sub>d(del k t)"
+"delete x t = tree\<^sub>d(del x t)"
subsection \<open>Functional Correctness\<close>
--- a/src/HOL/Data_Structures/Tree23_Set.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Mon Nov 02 18:35:30 2015 +0100
@@ -12,7 +12,7 @@
"isin Leaf x = False" |
"isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" |
"isin (Node3 l a m b r) x =
- (x < a \<and> isin l x \<or> x = a \<or> (x < b \<and> isin m x \<or> x = b \<or> isin r x))"
+ (x < a \<and> isin l x \<or> x > b \<and> isin r x \<or> x = a \<or> x = b \<or> isin m x)"
datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
@@ -21,37 +21,38 @@
"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
-"ins a Leaf = Up\<^sub>i Leaf a Leaf" |
-"ins a (Node2 l x r) =
- (if a < x then
- case ins a l of
- T\<^sub>i l' => T\<^sub>i (Node2 l' x r)
- | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r)
- else if a=x then T\<^sub>i (Node2 l x r)
+"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
+"ins x (Node2 l a r) =
+ (if x < a then
+ case ins x l of
+ T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
+ | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)
+ else if x=a then T\<^sub>i (Node2 l x r)
else
- case ins a r of
- T\<^sub>i r' => T\<^sub>i (Node2 l x r')
- | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2))" |
-"ins a (Node3 l x1 m x2 r) =
- (if a < x1 then
- case ins a l of
- T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r)
- | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node2 m x2 r)
- else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r)
- else if a < x2 then
- case ins a m of
- T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r)
- | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node2 m2 x2 r)
- else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r)
- else
- case ins a r of
- T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r')
- | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node2 r1 q r2))"
+ case ins x r of
+ T\<^sub>i r' => T\<^sub>i (Node2 l a r')
+ | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2))" |
+"ins x (Node3 l a m b r) =
+ (if x < a then
+ case ins x l of
+ T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
+ | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)
+ else
+ if x > b then
+ case ins x r of
+ T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
+ | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)
+ else
+ if x=a \<or> x = b then T\<^sub>i (Node3 l a m b r)
+ else
+ case ins x m of
+ T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
+ | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))"
hide_const insert
definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"insert a t = tree\<^sub>i(ins a t)"
+"insert x t = tree\<^sub>i(ins x t)"
datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
@@ -94,21 +95,21 @@
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
where
-"del k Leaf = T\<^sub>d Leaf" |
-"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
-"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
- else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
-"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else
- if k > a then node22 l a (del k r) else
+"del x Leaf = T\<^sub>d Leaf" |
+"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
+"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
+ else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
+"del x (Node2 l a r) = (if x<a then node21 (del x l) a r else
+ if x > a then node22 l a (del x r) else
let (a',t) = del_min r in node22 l a' t)" |
-"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else
- if k = a then let (a',m') = del_min m in node32 l a' m' b r else
- if k < b then node32 l a (del k m) b r else
- if k = b then let (b',r') = del_min r in node33 l a m b' r'
- else node33 l a m b (del k r))"
+"del x (Node3 l a m b r) = (if x<a then node31 (del x l) a m b r else
+ if x = a then let (a',m') = del_min m in node32 l a' m' b r else
+ if x < b then node32 l a (del x m) b r else
+ if x = b then let (b',r') = del_min r in node33 l a m b' r'
+ else node33 l a m b (del x r))"
definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"delete k t = tree\<^sub>d(del k t)"
+"delete x t = tree\<^sub>d(del x t)"
subsection "Functional Correctness"
@@ -127,7 +128,7 @@
lemma inorder_ins:
"sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
-by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
+by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) (* 38 secs in 2015 *)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
@@ -194,7 +195,7 @@
end
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
-by (induct t) (auto split: up\<^sub>i.split) (* 25 secs in 2015 *)
+by (induct t) (auto split: up\<^sub>i.split) (* 87 secs in 2015 *)
text{* Now an alternative proof (by Brian Huffman) that runs faster because
two properties (balance and height) are combined in one predicate. *}
--- a/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 02 18:35:30 2015 +0100
@@ -14,16 +14,16 @@
if x > a then lookup r x else Some b)"
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"update a b Leaf = Node Leaf (a,b) Leaf" |
-"update a b (Node l (x,y) r) =
- (if a < x then Node (update a b l) (x,y) r
- else if a=x then Node l (a,b) r
- else Node l (x,y) (update a b r))"
+"update x y Leaf = Node Leaf (x,y) Leaf" |
+"update x y (Node l (a,b) r) =
+ (if x < a then Node (update x y l) (a,b) r
+ else if x = a then Node l (x,y) r
+ else Node l (a,b) (update x y r))"
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete k Leaf = Leaf" |
-"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
- if k > a then Node l (a,b) (delete k r) else
+"delete x Leaf = Leaf" |
+"delete x (Node l (a,b) r) = (if x < a then Node (delete x l) (a,b) r else
+ if x > a then Node l (a,b) (delete x r) else
if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
--- a/src/HOL/Data_Structures/Tree_Set.thy Mon Nov 02 11:56:38 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy Mon Nov 02 18:35:30 2015 +0100
@@ -15,20 +15,20 @@
hide_const (open) insert
fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert a Leaf = Node Leaf a Leaf" |
-"insert a (Node l x r) =
- (if a < x then Node (insert a l) x r
- else if a=x then Node l x r
- else Node l x (insert a r))"
+"insert x Leaf = Node Leaf x Leaf" |
+"insert x (Node l a r) =
+ (if x < a then Node (insert x l) a r else
+ if x = a then Node l a r
+ else Node l a (insert x r))"
fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
"del_min (Node Leaf a r) = (a, r)" |
"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete k Leaf = Leaf" |
-"delete k (Node l a r) = (if k<a then Node (delete k l) a r else
- if k > a then Node l a (delete k r) else
+"delete x Leaf = Leaf" |
+"delete x (Node l a r) = (if x < a then Node (delete x l) a r else
+ if x > a then Node l a (delete x r) else
if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"