# HG changeset patch
# User nipkow
# Date 1446485730 -3600
# Node ID a88e07c8d0d5bb285f0eebf0a6ec76c05ea3dc75
# Parent  e3984606b4b6f20ffa074005157f5879699528f4
tuned names and optimized comparison order

diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/AList_Upd_Del.thy
--- 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 =
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/List_Ins_Del.thy
--- 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
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/RBT.thy
--- 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))" |
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/Set_by_Ordered.thy
--- 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
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/Tree23_Map.thy
--- 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>
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/Tree23_Set.thy
--- 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. *}
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/Tree_Map.thy
--- 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')"
 
 
diff -r e3984606b4b6 -r a88e07c8d0d5 src/HOL/Data_Structures/Tree_Set.thy
--- 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')"