# HG changeset patch
# User nipkow
# Date 1447263146 -3600
# Node ID 44c9198f210cf74a8ee6bb25314691564c2e0715
# Parent  7ffc9c4f1f740f6cad5de078422bbbd37c4713f0
no CRLF

diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/AList_Upd_Del.thy
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,142 +1,142 @@
-(* Author: Tobias Nipkow *)
-
-section {* Association List Update and Deletion *}
-
-theory AList_Upd_Del
-imports Sorted_Less
-begin
-
-abbreviation "sorted1 ps \<equiv> sorted(map fst ps)"
-
-text{* Define own @{text map_of} function to avoid pulling in an unknown
-amount of lemmas implicitly (via the simpset). *}
-
-hide_const (open) map_of
-
-fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"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 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 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 x y ps) = (map_of ps)(x := Some y)"
-by(induction ps) auto
-
-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 (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 @ [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 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>
-   map_of ps x = None"
-by (meson less_trans map_of_None sorted_Cons_iff)
-
-lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
-  map_of ps x = None"
-by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
-
-lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
-lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds
-
-
-subsection \<open>Lemmas for @{const upd_list}\<close>
-
-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 @ [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 @ [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
-
-(*
-lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
-by(induction xs) auto
-
-lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
-apply(induction xs rule: sorted.induct)
-apply auto
-by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
-
-lemma set_del_list_eq [simp]: "distinct xs ==> set(del_list x xs) = set xs - {x}"
-apply(induct xs)
- apply simp
-apply simp
-apply blast
-done
-*)
-
-
-subsection \<open>Lemmas for @{const del_list}\<close>
-
-lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)"
-apply(induction ps)
- apply simp
-apply(case_tac ps)
-apply auto
-by (meson order.strict_trans sorted_Cons_iff)
-
-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 @ [(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 @ (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 @ (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 @ (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 @ (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 =
-  del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
-
-lemmas del_list_simps = sorted_lems del_list_sorted
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Association List Update and Deletion *}
+
+theory AList_Upd_Del
+imports Sorted_Less
+begin
+
+abbreviation "sorted1 ps \<equiv> sorted(map fst ps)"
+
+text{* Define own @{text map_of} function to avoid pulling in an unknown
+amount of lemmas implicitly (via the simpset). *}
+
+hide_const (open) map_of
+
+fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"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 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 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 x y ps) = (map_of ps)(x := Some y)"
+by(induction ps) auto
+
+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 (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 @ [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 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>
+   map_of ps x = None"
+by (meson less_trans map_of_None sorted_Cons_iff)
+
+lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  map_of ps x = None"
+by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
+
+lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
+lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds
+
+
+subsection \<open>Lemmas for @{const upd_list}\<close>
+
+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 @ [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 @ [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
+
+(*
+lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
+by(induction xs) auto
+
+lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
+
+lemma set_del_list_eq [simp]: "distinct xs ==> set(del_list x xs) = set xs - {x}"
+apply(induct xs)
+ apply simp
+apply simp
+apply blast
+done
+*)
+
+
+subsection \<open>Lemmas for @{const del_list}\<close>
+
+lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)"
+apply(induction ps)
+ apply simp
+apply(case_tac ps)
+apply auto
+by (meson order.strict_trans sorted_Cons_iff)
+
+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 @ [(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 @ (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 @ (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 @ (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 @ (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 =
+  del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
+
+lemmas del_list_simps = sorted_lems del_list_sorted
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Cmp.thy
--- a/src/HOL/Data_Structures/Cmp.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Cmp.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,21 +1,21 @@
-(* Author: Tobias Nipkow *)
-
-section {* Three-Way Comparison *}
-
-theory Cmp
-imports Main
-begin
-
-datatype cmp = LT | EQ | GT
-
-class cmp = linorder +
-fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
-assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
-assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
-assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
-
-lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
-  (if c = LT then l else if c = GT then g else e)"
-by(simp split: cmp.split)
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Three-Way Comparison *}
+
+theory Cmp
+imports Main
+begin
+
+datatype cmp = LT | EQ | GT
+
+class cmp = linorder +
+fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
+assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
+assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
+assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+
+lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
+  (if c = LT then l else if c = GT then g else e)"
+by(simp split: cmp.split)
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Less_False.thy
--- a/src/HOL/Data_Structures/Less_False.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Less_False.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,31 +1,31 @@
-(* Author: Tobias Nipkow *)
-
-section {* Improved Simproc for $<$ *}
-
-theory Less_False
-imports Main
-begin
-
-simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
-  let
-    fun prp t thm = Thm.full_prop_of thm aconv t;
-
-    val eq_False_if_not = @{thm eq_False} RS iffD2
-
-    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
-      let val prems = Simplifier.prems_of ctxt;
-          val le = Const (@{const_name less_eq}, T);
-          val t = HOLogic.mk_Trueprop(le $ s $ r);
-      in case find_first (prp t) prems of
-           NONE =>
-             let val t = HOLogic.mk_Trueprop(less $ s $ r)
-             in case find_first (prp t) prems of
-                  NONE => NONE
-                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
-             end
-         | SOME thm => NONE
-      end;
-  in prove_less_False (Thm.term_of ct) end
-*}
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Improved Simproc for $<$ *}
+
+theory Less_False
+imports Main
+begin
+
+simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
+  let
+    fun prp t thm = Thm.full_prop_of thm aconv t;
+
+    val eq_False_if_not = @{thm eq_False} RS iffD2
+
+    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
+      let val prems = Simplifier.prems_of ctxt;
+          val le = Const (@{const_name less_eq}, T);
+          val t = HOLogic.mk_Trueprop(le $ s $ r);
+      in case find_first (prp t) prems of
+           NONE =>
+             let val t = HOLogic.mk_Trueprop(less $ s $ r)
+             in case find_first (prp t) prems of
+                  NONE => NONE
+                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
+             end
+         | SOME thm => NONE
+      end;
+  in prove_less_False (Thm.term_of ct) end
+*}
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,149 +1,149 @@
-(* Author: Tobias Nipkow *)
-
-section {* List Insertion and Deletion *}
-
-theory List_Ins_Del
-imports Sorted_Less
-begin
-
-subsection \<open>Elements in a list\<close>
-
-fun elems :: "'a list \<Rightarrow> 'a set" where
-"elems [] = {}" |
-"elems (x#xs) = Set.insert x (elems xs)"
-
-lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)"
-by (induction xs) auto
-
-lemma elems_eq_set: "elems xs = set xs"
-by (induction xs) auto
-
-lemma sorted_Cons_iff:
-  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))"
-by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff)
-
-lemma sorted_snoc_iff:
-  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
-by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
-
-text{* The above two rules introduce quantifiers. It turns out
-that in practice this is not a problem because of the simplicity of
-the "isin" functions that implement @{const elems}. Nevertheless
-it is possible to avoid the quantifiers with the help of some rewrite rules: *}
-
-lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
-by (simp add: sorted_Cons_iff)
-
-lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
-by (simp add: sorted_snoc_iff)
-
-lemma sorted_ConsD2: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
-using leD sorted_ConsD by blast
-
-lemma sorted_snocD2: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
-using leD sorted_snocD by blast
-
-lemmas elems_simps = sorted_lems elems_app
-lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
-lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD sorted_ConsD2 sorted_snocD2
-
-
-subsection \<open>Inserting into an ordered list without duplicates:\<close>
-
-fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"ins_list x [] = [x]" |
-"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: "elems (ins_list x xs) = insert x (elems xs)"
-by(induction xs) auto
-
-lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
-apply(induction xs rule: sorted.induct)
-apply auto
-by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
-
-lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
-by(induction xs rule: sorted.induct) auto
-
-lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
-  ins_list x (xs @ a # ys) =
-  (if a \<le> x then xs @ ins_list x (a#ys) else ins_list x xs @ (a#ys))"
-by(induction xs) (auto simp: sorted_lems)
-
-text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two
-corollaries speed up proofs.\<close>
-
-corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
-  ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
-by(simp add: ins_list_sorted)
-
-corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
-  ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"
-by(auto simp: ins_list_sorted)
-
-lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
-
-
-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 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
-
-lemma elems_del_list_eq:
-  "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
-apply(induct xs)
- apply simp
-apply (simp add: elems_eq_set)
-apply blast
-done
-
-lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
-apply(induction xs rule: sorted.induct)
-apply auto
-by (meson order.strict_trans sorted_Cons_iff)
-
-lemma del_list_sorted: "sorted (xs @ a # ys) \<Longrightarrow>
-  del_list x (xs @ a # ys) = (if x < a then del_list x xs @ a # ys else xs @ del_list x (a # ys))"
-by(induction xs)
-  (fastforce simp: sorted_lems sorted_Cons_iff elems_eq_set intro!: del_list_idem)+
-
-text\<open>In principle, @{thm del_list_sorted} suffices, but the following
-corollaries speed up proofs.\<close>
-
-corollary del_list_sorted1: "sorted (xs @ a # ys) \<Longrightarrow> a \<le> x \<Longrightarrow>
-  del_list x (xs @ a # ys) = xs @ del_list x (a # ys)"
-by (auto simp: del_list_sorted)
-
-corollary del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow>
-  del_list x (xs @ a # ys) = del_list x xs @ a # ys"
-by (auto simp: del_list_sorted)
-
-corollary del_list_sorted3:
-  "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 (auto simp: del_list_sorted sorted_lems)
-
-corollary del_list_sorted4:
-  "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 (auto simp: del_list_sorted sorted_lems)
-
-corollary del_list_sorted5:
-  "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 (auto simp: del_list_sorted sorted_lems)
-
-lemmas del_list_simps = sorted_lems
-  del_list_sorted1
-  del_list_sorted2
-  del_list_sorted3
-  del_list_sorted4
-  del_list_sorted5
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* List Insertion and Deletion *}
+
+theory List_Ins_Del
+imports Sorted_Less
+begin
+
+subsection \<open>Elements in a list\<close>
+
+fun elems :: "'a list \<Rightarrow> 'a set" where
+"elems [] = {}" |
+"elems (x#xs) = Set.insert x (elems xs)"
+
+lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)"
+by (induction xs) auto
+
+lemma elems_eq_set: "elems xs = set xs"
+by (induction xs) auto
+
+lemma sorted_Cons_iff:
+  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))"
+by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff)
+
+lemma sorted_snoc_iff:
+  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
+by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
+
+text{* The above two rules introduce quantifiers. It turns out
+that in practice this is not a problem because of the simplicity of
+the "isin" functions that implement @{const elems}. Nevertheless
+it is possible to avoid the quantifiers with the help of some rewrite rules: *}
+
+lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
+by (simp add: sorted_Cons_iff)
+
+lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
+by (simp add: sorted_snoc_iff)
+
+lemma sorted_ConsD2: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_ConsD by blast
+
+lemma sorted_snocD2: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_snocD by blast
+
+lemmas elems_simps = sorted_lems elems_app
+lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
+lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD sorted_ConsD2 sorted_snocD2
+
+
+subsection \<open>Inserting into an ordered list without duplicates:\<close>
+
+fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"ins_list x [] = [x]" |
+"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: "elems (ins_list x xs) = insert x (elems xs)"
+by(induction xs) auto
+
+lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
+
+lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
+by(induction xs rule: sorted.induct) auto
+
+lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
+  ins_list x (xs @ a # ys) =
+  (if a \<le> x then xs @ ins_list x (a#ys) else ins_list x xs @ (a#ys))"
+by(induction xs) (auto simp: sorted_lems)
+
+text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two
+corollaries speed up proofs.\<close>
+
+corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
+by(simp add: ins_list_sorted)
+
+corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
+  ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"
+by(auto simp: ins_list_sorted)
+
+lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
+
+
+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 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
+
+lemma elems_del_list_eq:
+  "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
+apply(induct xs)
+ apply simp
+apply (simp add: elems_eq_set)
+apply blast
+done
+
+lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (meson order.strict_trans sorted_Cons_iff)
+
+lemma del_list_sorted: "sorted (xs @ a # ys) \<Longrightarrow>
+  del_list x (xs @ a # ys) = (if x < a then del_list x xs @ a # ys else xs @ del_list x (a # ys))"
+by(induction xs)
+  (fastforce simp: sorted_lems sorted_Cons_iff elems_eq_set intro!: del_list_idem)+
+
+text\<open>In principle, @{thm del_list_sorted} suffices, but the following
+corollaries speed up proofs.\<close>
+
+corollary del_list_sorted1: "sorted (xs @ a # ys) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  del_list x (xs @ a # ys) = xs @ del_list x (a # ys)"
+by (auto simp: del_list_sorted)
+
+corollary del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow>
+  del_list x (xs @ a # ys) = del_list x xs @ a # ys"
+by (auto simp: del_list_sorted)
+
+corollary del_list_sorted3:
+  "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 (auto simp: del_list_sorted sorted_lems)
+
+corollary del_list_sorted4:
+  "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 (auto simp: del_list_sorted sorted_lems)
+
+corollary del_list_sorted5:
+  "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 (auto simp: del_list_sorted sorted_lems)
+
+lemmas del_list_simps = sorted_lems
+  del_list_sorted1
+  del_list_sorted2
+  del_list_sorted3
+  del_list_sorted4
+  del_list_sorted5
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Map_by_Ordered.thy
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,59 +1,59 @@
-(* Author: Tobias Nipkow *)
-
-section {* Implementing Ordered Maps *}
-
-theory Map_by_Ordered
-imports AList_Upd_Del
-begin
-
-locale Map =
-fixes empty :: "'m"
-fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
-fixes invar :: "'m \<Rightarrow> bool"
-assumes "map_of empty = (\<lambda>_. None)"
-assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
-assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
-assumes "invar empty"
-assumes "invar m \<Longrightarrow> invar(update a b m)"
-assumes "invar m \<Longrightarrow> invar(delete a m)"
-
-locale Map_by_Ordered =
-fixes empty :: "'t"
-fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
-fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
-fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
-fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
-fixes wf :: "'t \<Rightarrow> bool"
-assumes empty: "inorder empty = []"
-assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
-  lookup t a = map_of (inorder t) a"
-assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
-  inorder(update a b t) = upd_list a b (inorder t)"
-assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
-  inorder(delete a t) = del_list a (inorder t)"
-assumes wf_empty:  "wf empty"
-assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
-assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
-begin
-
-sublocale Map
-  empty update delete "map_of o inorder" "\<lambda>t. wf t \<and> sorted1 (inorder t)"
-proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty)
-next
-  case 2 thus ?case by(simp add: update map_of_ins_list)
-next
-  case 3 thus ?case by(simp add: delete map_of_del_list)
-next
-  case 4 thus ?case by(simp add: empty wf_empty)
-next
-  case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
-next
-  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
-qed
-
-end
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Implementing Ordered Maps *}
+
+theory Map_by_Ordered
+imports AList_Upd_Del
+begin
+
+locale Map =
+fixes empty :: "'m"
+fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes invar :: "'m \<Rightarrow> bool"
+assumes "map_of empty = (\<lambda>_. None)"
+assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
+assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+assumes "invar empty"
+assumes "invar m \<Longrightarrow> invar(update a b m)"
+assumes "invar m \<Longrightarrow> invar(delete a m)"
+
+locale Map_by_Ordered =
+fixes empty :: "'t"
+fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
+fixes wf :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  lookup t a = map_of (inorder t) a"
+assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  inorder(update a b t) = upd_list a b (inorder t)"
+assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  inorder(delete a t) = del_list a (inorder t)"
+assumes wf_empty:  "wf empty"
+assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
+assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
+begin
+
+sublocale Map
+  empty update delete "map_of o inorder" "\<lambda>t. wf t \<and> sorted1 (inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: empty)
+next
+  case 2 thus ?case by(simp add: update map_of_ins_list)
+next
+  case 3 thus ?case by(simp add: delete map_of_del_list)
+next
+  case 4 thus ?case by(simp add: empty wf_empty)
+next
+  case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
+next
+  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+qed
+
+end
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Set_by_Ordered.thy
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,64 +1,64 @@
-(* Author: Tobias Nipkow *)
-
-section {* Implementing Ordered Sets *}
-
-theory Set_by_Ordered
-imports List_Ins_Del
-begin
-
-locale Set =
-fixes empty :: "'s"
-fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
-fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
-fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
-fixes set :: "'s \<Rightarrow> 'a set"
-fixes invar :: "'s \<Rightarrow> bool"
-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"
-fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
-fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
-fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
-fixes inorder :: "'t \<Rightarrow> 'a list"
-fixes inv :: "'t \<Rightarrow> bool"
-assumes empty: "inorder empty = []"
-assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  isin t x = (x \<in> elems (inorder t))"
-assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(insert x t) = ins_list x (inorder t)"
-assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-assumes inv_empty:  "inv empty"
-assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
-assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
-begin
-
-sublocale Set
-  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
-proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty)
-next
-  case 2 thus ?case by(simp add: isin)
-next
-  case 3 thus ?case by(simp add: insert set_ins_list)
-next
-  case (4 s x) thus ?case
-    using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
-next
-  case 5 thus ?case by(simp add: empty inv_empty)
-next
-  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
-next
-  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
-qed
-
-end
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Implementing Ordered Sets *}
+
+theory Set_by_Ordered
+imports List_Ins_Del
+begin
+
+locale Set =
+fixes empty :: "'s"
+fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
+fixes set :: "'s \<Rightarrow> 'a set"
+fixes invar :: "'s \<Rightarrow> bool"
+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"
+fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
+fixes inorder :: "'t \<Rightarrow> 'a list"
+fixes inv :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  isin t x = (x \<in> elems (inorder t))"
+assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(insert x t) = ins_list x (inorder t)"
+assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+assumes inv_empty:  "inv empty"
+assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
+assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
+begin
+
+sublocale Set
+  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: empty)
+next
+  case 2 thus ?case by(simp add: isin)
+next
+  case 3 thus ?case by(simp add: insert set_ins_list)
+next
+  case (4 s x) thus ?case
+    using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
+next
+  case 5 thus ?case by(simp add: empty inv_empty)
+next
+  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
+next
+  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
+qed
+
+end
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Sorted_Less.thy
--- a/src/HOL/Data_Structures/Sorted_Less.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,54 +1,54 @@
-(* Author: Tobias Nipkow *)
-
-section {* Lists Sorted wrt $<$ *}
-
-theory Sorted_Less
-imports Less_False
-begin
-
-hide_const sorted
-
-text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
-Could go into theory List under a name like @{term sorted_less}.\<close>
-
-fun sorted :: "'a::linorder list \<Rightarrow> bool" where
-"sorted [] = True" |
-"sorted [x] = True" |
-"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
-
-lemma sorted_Cons_iff:
-  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
-by(induction xs rule: sorted.induct) auto
-
-lemma sorted_snoc_iff:
-  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
-by(induction xs rule: sorted.induct) auto
-
-lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
-by(simp add: sorted_Cons_iff)
-
-lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
-by(rule ASSUMPTION_D [THEN sorted_cons])
-
-lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
-by(simp add: sorted_snoc_iff)
-
-lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
-by(rule ASSUMPTION_D [THEN sorted_snoc])
-
-lemma sorted_mid_iff:
-  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
-by(induction xs rule: sorted.induct) auto
-
-lemma sorted_mid_iff2:
-  "sorted(x # xs @ y # ys) =
-  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
-by(induction xs rule: sorted.induct) auto
-
-lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
-  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
-by(rule sorted_mid_iff)
-
-lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Lists Sorted wrt $<$ *}
+
+theory Sorted_Less
+imports Less_False
+begin
+
+hide_const sorted
+
+text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
+Could go into theory List under a name like @{term sorted_less}.\<close>
+
+fun sorted :: "'a::linorder list \<Rightarrow> bool" where
+"sorted [] = True" |
+"sorted [x] = True" |
+"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
+
+lemma sorted_Cons_iff:
+  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_snoc_iff:
+  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
+by(simp add: sorted_Cons_iff)
+
+lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
+by(rule ASSUMPTION_D [THEN sorted_cons])
+
+lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
+by(simp add: sorted_snoc_iff)
+
+lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
+by(rule ASSUMPTION_D [THEN sorted_snoc])
+
+lemma sorted_mid_iff:
+  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_mid_iff2:
+  "sorted(x # xs @ y # ys) =
+  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
+  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(rule sorted_mid_iff)
+
+lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree23.thy
--- a/src/HOL/Data_Structures/Tree23.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,43 +1,43 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>2-3 Trees\<close>
-
-theory Tree23
-imports Main
-begin
-
-class height =
-fixes height :: "'a \<Rightarrow> nat"
-
-datatype 'a tree23 =
-  Leaf |
-  Node2 "'a tree23" 'a "'a tree23" |
-  Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"
-
-fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
-"inorder Leaf = []" |
-"inorder(Node2 l a r) = inorder l @ a # inorder r" |
-"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
-
-
-instantiation tree23 :: (type)height
-begin
-
-fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where
-"height Leaf = 0" |
-"height (Node2 l _ r) = Suc(max (height l) (height r))" |
-"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
-
-instance ..
-
-end
-
-text \<open>Balanced:\<close>
-
-fun bal :: "'a tree23 \<Rightarrow> bool" where
-"bal Leaf = True" |
-"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
-"bal (Node3 l _ m _ r) =
-  (bal l & bal m & bal r & height l = height m & height m = height r)"
-
-end
+(* Author: Tobias Nipkow *)
+
+section \<open>2-3 Trees\<close>
+
+theory Tree23
+imports Main
+begin
+
+class height =
+fixes height :: "'a \<Rightarrow> nat"
+
+datatype 'a tree23 =
+  Leaf |
+  Node2 "'a tree23" 'a "'a tree23" |
+  Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"
+
+fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
+"inorder Leaf = []" |
+"inorder(Node2 l a r) = inorder l @ a # inorder r" |
+"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
+
+
+instantiation tree23 :: (type)height
+begin
+
+fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where
+"height Leaf = 0" |
+"height (Node2 l _ r) = Suc(max (height l) (height r))" |
+"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
+
+instance ..
+
+end
+
+text \<open>Balanced:\<close>
+
+fun bal :: "'a tree23 \<Rightarrow> bool" where
+"bal Leaf = True" |
+"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
+"bal (Node3 l _ m _ r) =
+  (bal l & bal m & bal r & height l = height m & height m = height r)"
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree234.thy
--- a/src/HOL/Data_Structures/Tree234.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,45 +1,45 @@
-(* Author: Tobias Nipkow *)
-
-section {* 2-3-4 Trees *}
-
-theory Tree234
-imports Main
-begin
-
-class height =
-fixes height :: "'a \<Rightarrow> nat"
-
-datatype 'a tree234 =
-  Leaf |
-  Node2 "'a tree234" 'a "'a tree234" |
-  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
-  Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
-
-fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
-"inorder Leaf = []" |
-"inorder(Node2 l a r) = inorder l @ a # inorder r" |
-"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
-"inorder(Node4 l a m b n c r) = inorder l @ a # inorder m @ b # inorder n @ c # inorder r"
-
-
-instantiation tree234 :: (type)height
-begin
-
-fun height_tree234 :: "'a tree234 \<Rightarrow> nat" where
-"height Leaf = 0" |
-"height (Node2 l _ r) = Suc(max (height l) (height r))" |
-"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
-"height (Node4 l _ m _ n _ r) = Suc(max (height l) (max (height m) (max (height n) (height r))))"
-
-instance ..
-
-end
-
-text{* Balanced: *}
-fun bal :: "'a tree234 \<Rightarrow> bool" where
-"bal Leaf = True" |
-"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
-"bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
-"bal (Node4 l _ m _ n _ r) = (bal l & bal m & bal n & bal r & height l = height m & height m = height n & height n = height r)"
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* 2-3-4 Trees *}
+
+theory Tree234
+imports Main
+begin
+
+class height =
+fixes height :: "'a \<Rightarrow> nat"
+
+datatype 'a tree234 =
+  Leaf |
+  Node2 "'a tree234" 'a "'a tree234" |
+  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
+  Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
+
+fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
+"inorder Leaf = []" |
+"inorder(Node2 l a r) = inorder l @ a # inorder r" |
+"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
+"inorder(Node4 l a m b n c r) = inorder l @ a # inorder m @ b # inorder n @ c # inorder r"
+
+
+instantiation tree234 :: (type)height
+begin
+
+fun height_tree234 :: "'a tree234 \<Rightarrow> nat" where
+"height Leaf = 0" |
+"height (Node2 l _ r) = Suc(max (height l) (height r))" |
+"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
+"height (Node4 l _ m _ n _ r) = Suc(max (height l) (max (height m) (max (height n) (height r))))"
+
+instance ..
+
+end
+
+text{* Balanced: *}
+fun bal :: "'a tree234 \<Rightarrow> bool" where
+"bal Leaf = True" |
+"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
+"bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
+"bal (Node4 l _ m _ n _ r) = (bal l & bal m & bal n & bal r & height l = height m & height m = height n & height n = height r)"
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,181 +1,181 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>A 2-3-4 Tree Implementation of Maps\<close>
-
-theory Tree234_Map
-imports
-  Tree234_Set
-  "../Data_Structures/Map_by_Ordered"
-begin
-
-subsection \<open>Map operations on 2-3-4 trees\<close>
-
-fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"lookup Leaf x = None" |
-"lookup (Node2 l (a,b) r) x = (case cmp x a of
-  LT \<Rightarrow> lookup l x |
-  GT \<Rightarrow> lookup r x |
-  EQ \<Rightarrow> Some b)" |
-"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
-  LT \<Rightarrow> lookup l x |
-  EQ \<Rightarrow> Some b1 |
-  GT \<Rightarrow> (case cmp x a2 of
-          LT \<Rightarrow> lookup m x |
-          EQ \<Rightarrow> Some b2 |
-          GT \<Rightarrow> lookup r x))" |
-"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of
-  LT \<Rightarrow> (case cmp x a1 of
-           LT \<Rightarrow> lookup t1 x | EQ \<Rightarrow> Some b1 | GT \<Rightarrow> lookup t2 x) |
-  EQ \<Rightarrow> Some b2 |
-  GT \<Rightarrow> (case cmp x a3 of
-           LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
-
-fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
-"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
-"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
-   LT \<Rightarrow> (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)) |
-   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
-   GT \<Rightarrow> (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) = (case cmp x (fst ab1) of
-   LT \<Rightarrow> (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)) |
-   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
-   GT \<Rightarrow> (case cmp x (fst ab2) of
-           LT \<Rightarrow> (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)) |
-           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
-           GT \<Rightarrow> (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))))" |
-"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
-   LT \<Rightarrow> (case cmp x (fst ab1) of
-            LT \<Rightarrow> (case upd x y t1 of
-                     T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4)
-                  | Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) |
-            EQ \<Rightarrow> T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) |
-            GT \<Rightarrow> (case upd x y t2 of
-                    T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4)
-                  | Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) |
-   EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) |
-   GT \<Rightarrow> (case cmp x (fst ab3) of
-            LT \<Rightarrow> (case upd x y t3 of
-                    T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
-                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
-            EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
-            GT \<Rightarrow> (case upd x y t4 of
-                    T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
-                  | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
-
-definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
-"update x y t = tree\<^sub>i(upd x y t)"
-
-fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
-"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 (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
-  T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
-     if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
-     if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
-     else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
-"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
-  LT \<Rightarrow> node21 (del x l) ab1 r |
-  GT \<Rightarrow> node22 l ab1 (del x r) |
-  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
-"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
-  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
-  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
-  GT \<Rightarrow> (case cmp x (fst ab2) of
-           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
-           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
-           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
-"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
-  LT \<Rightarrow> (case cmp x (fst ab1) of
-           LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
-           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
-           GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
-  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
-  GT \<Rightarrow> (case cmp x (fst ab3) of
-          LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
-          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
-          GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
-
-definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
-"delete x t = tree\<^sub>d(del x t)"
-
-
-subsection "Functional correctness"
-
-lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by (induction t) (auto simp: map_of_simps split: option.split)
-
-
-lemma inorder_upd:
-  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
-by(induction t)
-  (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
-
-lemma inorder_update:
-  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
-by(simp add: update_def inorder_upd)
-
-
-lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
-by(induction t rule: del.induct)
-  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
-(* 200 secs (2015) *)
-
-lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del)
-
-
-subsection \<open>Balancedness\<close>
-
-lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
-by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
-
-lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
-by (simp add: update_def bal_upd)
-
-
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
-by(induction x t rule: del.induct)
-  (auto simp add: heights height_del_min split: prod.split)
-(* 20 secs (2015) *)
-
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
-by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
-(* 100 secs (2015) *)
-
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
-
-
-subsection \<open>Overall Correctness\<close>
-
-interpretation T234_Map: Map_by_Ordered
-where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = bal
-proof (standard, goal_cases)
-  case 2 thus ?case by(simp add: lookup)
-next
-  case 3 thus ?case by(simp add: inorder_update)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 6 thus ?case by(simp add: bal_update)
-next
-  case 7 thus ?case by(simp add: bal_delete)
-qed simp+
-
-end
+(* Author: Tobias Nipkow *)
+
+section \<open>A 2-3-4 Tree Implementation of Maps\<close>
+
+theory Tree234_Map
+imports
+  Tree234_Set
+  "../Data_Structures/Map_by_Ordered"
+begin
+
+subsection \<open>Map operations on 2-3-4 trees\<close>
+
+fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node2 l (a,b) r) x = (case cmp x a of
+  LT \<Rightarrow> lookup l x |
+  GT \<Rightarrow> lookup r x |
+  EQ \<Rightarrow> Some b)" |
+"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
+  LT \<Rightarrow> lookup l x |
+  EQ \<Rightarrow> Some b1 |
+  GT \<Rightarrow> (case cmp x a2 of
+          LT \<Rightarrow> lookup m x |
+          EQ \<Rightarrow> Some b2 |
+          GT \<Rightarrow> lookup r x))" |
+"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of
+  LT \<Rightarrow> (case cmp x a1 of
+           LT \<Rightarrow> lookup t1 x | EQ \<Rightarrow> Some b1 | GT \<Rightarrow> lookup t2 x) |
+  EQ \<Rightarrow> Some b2 |
+  GT \<Rightarrow> (case cmp x a3 of
+           LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
+
+fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
+"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
+"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
+   LT \<Rightarrow> (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)) |
+   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
+   GT \<Rightarrow> (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) = (case cmp x (fst ab1) of
+   LT \<Rightarrow> (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)) |
+   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
+   GT \<Rightarrow> (case cmp x (fst ab2) of
+           LT \<Rightarrow> (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)) |
+           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
+           GT \<Rightarrow> (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))))" |
+"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
+   LT \<Rightarrow> (case cmp x (fst ab1) of
+            LT \<Rightarrow> (case upd x y t1 of
+                     T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4)
+                  | Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) |
+            EQ \<Rightarrow> T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) |
+            GT \<Rightarrow> (case upd x y t2 of
+                    T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4)
+                  | Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) |
+   EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) |
+   GT \<Rightarrow> (case cmp x (fst ab3) of
+            LT \<Rightarrow> (case upd x y t3 of
+                    T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
+                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
+            EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
+            GT \<Rightarrow> (case upd x y t4 of
+                    T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
+                  | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
+
+definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
+"update x y t = tree\<^sub>i(upd x y t)"
+
+fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
+"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 (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
+  T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
+     if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
+     if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
+     else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
+"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
+  LT \<Rightarrow> node21 (del x l) ab1 r |
+  GT \<Rightarrow> node22 l ab1 (del x r) |
+  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
+"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
+  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
+  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
+  GT \<Rightarrow> (case cmp x (fst ab2) of
+           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
+           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
+           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
+"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
+  LT \<Rightarrow> (case cmp x (fst ab1) of
+           LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
+           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
+           GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
+  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
+  GT \<Rightarrow> (case cmp x (fst ab3) of
+          LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
+          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
+          GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
+
+definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
+"delete x t = tree\<^sub>d(del x t)"
+
+
+subsection "Functional correctness"
+
+lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by (induction t) (auto simp: map_of_simps split: option.split)
+
+
+lemma inorder_upd:
+  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
+by(induction t)
+  (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
+
+lemma inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
+by(simp add: update_def inorder_upd)
+
+
+lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+by(induction t rule: del.induct)
+  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
+(* 200 secs (2015) *)
+
+lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del)
+
+
+subsection \<open>Balancedness\<close>
+
+lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
+by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
+
+lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
+by (simp add: update_def bal_upd)
+
+
+lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+by(induction x t rule: del.induct)
+  (auto simp add: heights height_del_min split: prod.split)
+(* 20 secs (2015) *)
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+by(induction x t rule: del.induct)
+  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
+(* 100 secs (2015) *)
+
+corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
+by(simp add: delete_def bal_tree\<^sub>d_del)
+
+
+subsection \<open>Overall Correctness\<close>
+
+interpretation T234_Map: Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: lookup)
+next
+  case 3 thus ?case by(simp add: inorder_update)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 6 thus ?case by(simp add: bal_update)
+next
+  case 7 thus ?case by(simp add: bal_delete)
+qed simp+
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,513 +1,513 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>A 2-3-4 Tree Implementation of Sets\<close>
-
-theory Tree234_Set
-imports
-  Tree234
-  Cmp
-  "../Data_Structures/Set_by_Ordered"
-begin
-
-subsection \<open>Set operations on 2-3-4 trees\<close>
-
-fun isin :: "'a::cmp tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
-"isin Leaf x = False" |
-"isin (Node2 l a r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
-"isin (Node3 l a m b r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
-   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))" |
-"isin (Node4 t1 a t2 b t3 c t4) x = (case cmp x b of
-  LT \<Rightarrow> (case cmp x a of
-          LT \<Rightarrow> isin t1 x |
-          EQ \<Rightarrow> True |
-          GT \<Rightarrow> isin t2 x) |
-  EQ \<Rightarrow> True |
-  GT \<Rightarrow> (case cmp x c of
-          LT \<Rightarrow> isin t3 x |
-          EQ \<Rightarrow> True |
-          GT \<Rightarrow> isin t4 x))"
-
-datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234"
-
-fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where
-"tree\<^sub>i (T\<^sub>i t) = t" |
-"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
-
-fun ins :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
-"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
-"ins x (Node2 l a r) =
-   (case cmp x a of
-      LT \<Rightarrow> (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)) |
-      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
-      GT \<Rightarrow> (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) =
-   (case cmp x a of
-      LT \<Rightarrow> (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)) |
-      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-      GT \<Rightarrow> (case cmp x b of
-               GT \<Rightarrow> (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)) |
-               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-               LT \<Rightarrow> (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))))" |
-"ins a (Node4 l x1 m x2 n x3 r) =
-   (if a < x2 then
-      if a < x1 then
-        (case ins a l of
-           T\<^sub>i l' => T\<^sub>i (Node4 l' x1 m x2 n x3 r)
-         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node3 m x2 n x3 r))
-      else if a=x1 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
-      else (case ins a m of
-                T\<^sub>i m' => T\<^sub>i (Node4 l x1 m' x2 n x3 r)
-              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node3 m2 x2 n x3 r))
-    else if a=x2 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
-    else if a < x3 then
-           (case ins a n of
-              T\<^sub>i n' => T\<^sub>i (Node4 l x1 m x2 n' x3 r)
-            | Up\<^sub>i n1 q n2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n1 q n2 x3 r))
-         else if a=x3 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
-         else (case ins a r of
-              T\<^sub>i r' => T\<^sub>i (Node4 l x1 m x2 n x3 r')
-            | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n x3 r1 q r2))
-)"
-
-hide_const insert
-
-definition insert :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
-"insert x t = tree\<^sub>i(ins x t)"
-
-datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
-
-fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where
-"tree\<^sub>d (T\<^sub>d x) = x" |
-"tree\<^sub>d (Up\<^sub>d x) = x"
-
-fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
-"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" |
-"node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
-"node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
-
-fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" |
-"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" |
-"node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
-"node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
-
-fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
-"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
-"node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"
-
-fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
-"node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
-
-fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
-"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
-"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
-
-fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
-"node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
-"node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
-"node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
-
-fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
-"node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
-"node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
-"node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
-
-fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
-"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
-"node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
-"node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
-"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"
-
-fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
-"node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
-"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
-"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
-
-fun del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
-"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
-"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
-"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
-"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
-"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
-"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))"
-
-fun del :: "'a::cmp \<Rightarrow> 'a tree234 \<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 (Node4 Leaf a Leaf b Leaf c Leaf) =
-  T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else
-     if k=b then Node3 Leaf a Leaf c Leaf else
-     if k=c then Node3 Leaf a Leaf b Leaf
-     else Node4 Leaf a Leaf b Leaf c Leaf)" |
-"del k (Node2 l a r) = (case cmp k a of
-  LT \<Rightarrow> node21 (del k l) a r |
-  GT \<Rightarrow> node22 l a (del k r) |
-  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
-"del k (Node3 l a m b r) = (case cmp k a of
-  LT \<Rightarrow> node31 (del k l) a m b r |
-  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
-  GT \<Rightarrow> (case cmp k b of
-           LT \<Rightarrow> node32 l a (del k m) b r |
-           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
-           GT \<Rightarrow> node33 l a m b (del k r)))" |
-"del k (Node4 l a m b n c r) = (case cmp k b of
-  LT \<Rightarrow> (case cmp k a of
-          LT \<Rightarrow> node41 (del k l) a m b n c r |
-          EQ \<Rightarrow> let (a',m') = del_min m in node42 l a' m' b n c r |
-          GT \<Rightarrow> node42 l a (del k m) b n c r) |
-  EQ \<Rightarrow> let (b',n') = del_min n in node43 l a m b' n' c r |
-  GT \<Rightarrow> (case cmp k c of
-           LT \<Rightarrow> node43 l a m b (del k n) c r |
-           EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
-           GT \<Rightarrow> node44 l a m b n c (del k r)))"
-
-definition delete :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
-"delete x t = tree\<^sub>d(del x t)"
-
-
-subsection "Functional correctness"
-
-subsubsection \<open>Functional correctness of isin:\<close>
-
-lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps1 ball_Un)
-
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
-
-
-subsubsection \<open>Functional correctness of insert:\<close>
-
-lemma inorder_ins:
-  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
-by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits)
-
-lemma inorder_insert:
-  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
-by(simp add: insert_def inorder_ins)
-
-
-subsubsection \<open>Functional correctness of delete\<close>
-
-lemma inorder_node21: "height r > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
-by(induct l' a r rule: node21.induct) auto
-
-lemma inorder_node22: "height l > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
-by(induct l a r' rule: node22.induct) auto
-
-lemma inorder_node31: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
-by(induct l' a m b r rule: node31.induct) auto
-
-lemma inorder_node32: "height r > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
-by(induct l a m' b r rule: node32.induct) auto
-
-lemma inorder_node33: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
-by(induct l a m b r' rule: node33.induct) auto
-
-lemma inorder_node41: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r"
-by(induct l' a m b n c r rule: node41.induct) auto
-
-lemma inorder_node42: "height l > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r"
-by(induct l a m b n c r rule: node42.induct) auto
-
-lemma inorder_node43: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r"
-by(induct l a m b n c r rule: node43.induct) auto
-
-lemma inorder_node44: "height n > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)"
-by(induct l a m b n c r rule: node44.induct) auto
-
-lemmas inorder_nodes = inorder_node21 inorder_node22
-  inorder_node31 inorder_node32 inorder_node33
-  inorder_node41 inorder_node42 inorder_node43 inorder_node44
-
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
-  x # inorder(tree\<^sub>d t') = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
-  (auto simp: inorder_nodes split: prod.splits)
-
-lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
-by(induction t rule: del.induct)
-  (auto simp: inorder_nodes del_list_simps del_minD split: prod.splits)
-  (* 150 secs (2015) *)
-
-lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del)
-
-
-subsection \<open>Balancedness\<close>
-
-subsubsection "Proofs for insert"
-
-text{* First a standard proof that @{const ins} preserves @{const bal}. *}
-
-instantiation up\<^sub>i :: (type)height
-begin
-
-fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
-"height (T\<^sub>i t) = height t" |
-"height (Up\<^sub>i l a r) = height l"
-
-instance ..
-
-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, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
-
-
-text{* Now an alternative proof (by Brian Huffman) that runs faster because
-two properties (balance and height) are combined in one predicate. *}
-
-inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where
-"full 0 Leaf" |
-"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
-"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" |
-"\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)"
-
-inductive_cases full_elims:
-  "full n Leaf"
-  "full n (Node2 l p r)"
-  "full n (Node3 l p m q r)"
-  "full n (Node4 l p m q m' q' r)"
-
-inductive_cases full_0_elim: "full 0 t"
-inductive_cases full_Suc_elim: "full (Suc n) t"
-
-lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
-  by (auto elim: full_0_elim intro: full.intros)
-
-lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_Suc_Node2_iff [simp]:
-  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_Suc_Node3_iff [simp]:
-  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_Suc_Node4_iff [simp]:
-  "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
-  by (induct set: full, simp_all)
-
-lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
-  by (induct set: full, auto dest: full_imp_height)
-
-lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
-  by (induct t, simp_all)
-
-lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
-  by (auto elim!: bal_imp_full full_imp_bal)
-
-text {* The @{const "insert"} function either preserves the height of the
-tree, or increases it by one. The constructor returned by the @{term
-"insert"} function determines which: A return value of the form @{term
-"T\<^sub>i t"} indicates that the height will be the same. A value of the
-form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
-
-primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
-"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
-"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
-
-lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
-by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split)
-
-text {* The @{const insert} operation preserves balance. *}
-
-lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
-unfolding bal_iff_full insert_def
-apply (erule exE)
-apply (drule full\<^sub>i_ins [of _ _ a])
-apply (cases "ins a t")
-apply (auto intro: full.intros)
-done
-
-
-subsubsection "Proofs for delete"
-
-instantiation up\<^sub>d :: (type)height
-begin
-
-fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
-"height (T\<^sub>d t) = height t" |
-"height (Up\<^sub>d t) = height t + 1"
-
-instance ..
-
-end
-
-lemma bal_tree\<^sub>d_node21:
-  "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))"
-by(induct l a r rule: node21.induct) auto
-
-lemma bal_tree\<^sub>d_node22:
-  "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))"
-by(induct l a r rule: node22.induct) auto
-
-lemma bal_tree\<^sub>d_node31:
-  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))"
-by(induct l a m b r rule: node31.induct) auto
-
-lemma bal_tree\<^sub>d_node32:
-  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))"
-by(induct l a m b r rule: node32.induct) auto
-
-lemma bal_tree\<^sub>d_node33:
-  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))"
-by(induct l a m b r rule: node33.induct) auto
-
-lemma bal_tree\<^sub>d_node41:
-  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))"
-by(induct l a m b n c r rule: node41.induct) auto
-
-lemma bal_tree\<^sub>d_node42:
-  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))"
-by(induct l a m b n c r rule: node42.induct) auto
-
-lemma bal_tree\<^sub>d_node43:
-  "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))"
-by(induct l a m b n c r rule: node43.induct) auto
-
-lemma bal_tree\<^sub>d_node44:
-  "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))"
-by(induct l a m b n c r rule: node44.induct) auto
-
-lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
-  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
-  bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44
-
-lemma height_node21:
-   "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1"
-by(induct l a r rule: node21.induct)(simp_all add: max.assoc)
-
-lemma height_node22:
-   "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1"
-by(induct l a r rule: node22.induct)(simp_all add: max.assoc)
-
-lemma height_node31:
-  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
-
-lemma height_node32:
-  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
-
-lemma height_node33:
-  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
-
-lemma height_node41:
-  "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) =
-   max (height l) (max (height m) (max (height n) (height r))) + 1"
-by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)
-
-lemma height_node42:
-  "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) =
-   max (height l) (max (height m) (max (height n) (height r))) + 1"
-by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)
-
-lemma height_node43:
-  "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) =
-   max (height l) (max (height m) (max (height n) (height r))) + 1"
-by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)
-
-lemma height_node44:
-  "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) =
-   max (height l) (max (height m) (max (height n) (height r))) + 1"
-by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)
-
-lemmas heights = height_node21 height_node22
-  height_node31 height_node32 height_node33
-  height_node41 height_node42 height_node43 height_node44
-
-lemma height_del_min:
-  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights split: prod.splits)
-
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
-by(induction x t rule: del.induct)
-  (auto simp add: heights height_del_min split: prod.split)
-
-lemma bal_del_min:
-  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights height_del_min bals split: prod.splits)
-
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
-by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
-(* 60 secs (2015) *)
-
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
-
-subsection \<open>Overall Correctness\<close>
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = bal
-proof (standard, goal_cases)
-  case 2 thus ?case by(simp add: isin_set)
-next
-  case 3 thus ?case by(simp add: inorder_insert)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 6 thus ?case by(simp add: bal_insert)
-next
-  case 7 thus ?case by(simp add: bal_delete)
-qed simp+
-
-end
+(* Author: Tobias Nipkow *)
+
+section \<open>A 2-3-4 Tree Implementation of Sets\<close>
+
+theory Tree234_Set
+imports
+  Tree234
+  Cmp
+  "../Data_Structures/Set_by_Ordered"
+begin
+
+subsection \<open>Set operations on 2-3-4 trees\<close>
+
+fun isin :: "'a::cmp tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node2 l a r) x =
+  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
+"isin (Node3 l a m b r) x =
+  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
+   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))" |
+"isin (Node4 t1 a t2 b t3 c t4) x = (case cmp x b of
+  LT \<Rightarrow> (case cmp x a of
+          LT \<Rightarrow> isin t1 x |
+          EQ \<Rightarrow> True |
+          GT \<Rightarrow> isin t2 x) |
+  EQ \<Rightarrow> True |
+  GT \<Rightarrow> (case cmp x c of
+          LT \<Rightarrow> isin t3 x |
+          EQ \<Rightarrow> True |
+          GT \<Rightarrow> isin t4 x))"
+
+datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234"
+
+fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where
+"tree\<^sub>i (T\<^sub>i t) = t" |
+"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
+
+fun ins :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
+"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
+"ins x (Node2 l a r) =
+   (case cmp x a of
+      LT \<Rightarrow> (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)) |
+      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
+      GT \<Rightarrow> (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) =
+   (case cmp x a of
+      LT \<Rightarrow> (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)) |
+      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+      GT \<Rightarrow> (case cmp x b of
+               GT \<Rightarrow> (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)) |
+               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+               LT \<Rightarrow> (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))))" |
+"ins a (Node4 l x1 m x2 n x3 r) =
+   (if a < x2 then
+      if a < x1 then
+        (case ins a l of
+           T\<^sub>i l' => T\<^sub>i (Node4 l' x1 m x2 n x3 r)
+         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node3 m x2 n x3 r))
+      else if a=x1 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
+      else (case ins a m of
+                T\<^sub>i m' => T\<^sub>i (Node4 l x1 m' x2 n x3 r)
+              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node3 m2 x2 n x3 r))
+    else if a=x2 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
+    else if a < x3 then
+           (case ins a n of
+              T\<^sub>i n' => T\<^sub>i (Node4 l x1 m x2 n' x3 r)
+            | Up\<^sub>i n1 q n2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n1 q n2 x3 r))
+         else if a=x3 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
+         else (case ins a r of
+              T\<^sub>i r' => T\<^sub>i (Node4 l x1 m x2 n x3 r')
+            | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n x3 r1 q r2))
+)"
+
+hide_const insert
+
+definition insert :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
+"insert x t = tree\<^sub>i(ins x t)"
+
+datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
+
+fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where
+"tree\<^sub>d (T\<^sub>d x) = x" |
+"tree\<^sub>d (Up\<^sub>d x) = x"
+
+fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
+"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" |
+"node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
+"node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
+
+fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
+"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" |
+"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" |
+"node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
+"node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
+
+fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
+"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
+"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
+"node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"
+
+fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
+"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
+"node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
+
+fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
+"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
+"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
+"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
+
+fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
+"node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
+"node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
+"node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
+
+fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
+"node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
+"node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
+"node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
+
+fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
+"node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
+"node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
+"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"
+
+fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
+"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
+"node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
+"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
+"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
+
+fun del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
+"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
+"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
+"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
+"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
+"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
+"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))"
+
+fun del :: "'a::cmp \<Rightarrow> 'a tree234 \<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 (Node4 Leaf a Leaf b Leaf c Leaf) =
+  T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else
+     if k=b then Node3 Leaf a Leaf c Leaf else
+     if k=c then Node3 Leaf a Leaf b Leaf
+     else Node4 Leaf a Leaf b Leaf c Leaf)" |
+"del k (Node2 l a r) = (case cmp k a of
+  LT \<Rightarrow> node21 (del k l) a r |
+  GT \<Rightarrow> node22 l a (del k r) |
+  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+"del k (Node3 l a m b r) = (case cmp k a of
+  LT \<Rightarrow> node31 (del k l) a m b r |
+  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+  GT \<Rightarrow> (case cmp k b of
+           LT \<Rightarrow> node32 l a (del k m) b r |
+           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+           GT \<Rightarrow> node33 l a m b (del k r)))" |
+"del k (Node4 l a m b n c r) = (case cmp k b of
+  LT \<Rightarrow> (case cmp k a of
+          LT \<Rightarrow> node41 (del k l) a m b n c r |
+          EQ \<Rightarrow> let (a',m') = del_min m in node42 l a' m' b n c r |
+          GT \<Rightarrow> node42 l a (del k m) b n c r) |
+  EQ \<Rightarrow> let (b',n') = del_min n in node43 l a m b' n' c r |
+  GT \<Rightarrow> (case cmp k c of
+           LT \<Rightarrow> node43 l a m b (del k n) c r |
+           EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
+           GT \<Rightarrow> node44 l a m b n c (del k r)))"
+
+definition delete :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
+"delete x t = tree\<^sub>d(del x t)"
+
+
+subsection "Functional correctness"
+
+subsubsection \<open>Functional correctness of isin:\<close>
+
+lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps1 ball_Un)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps2)
+
+
+subsubsection \<open>Functional correctness of insert:\<close>
+
+lemma inorder_ins:
+  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
+by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits)
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
+by(simp add: insert_def inorder_ins)
+
+
+subsubsection \<open>Functional correctness of delete\<close>
+
+lemma inorder_node21: "height r > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
+by(induct l' a r rule: node21.induct) auto
+
+lemma inorder_node22: "height l > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
+by(induct l a r' rule: node22.induct) auto
+
+lemma inorder_node31: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
+by(induct l' a m b r rule: node31.induct) auto
+
+lemma inorder_node32: "height r > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
+by(induct l a m' b r rule: node32.induct) auto
+
+lemma inorder_node33: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
+by(induct l a m b r' rule: node33.induct) auto
+
+lemma inorder_node41: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r"
+by(induct l' a m b n c r rule: node41.induct) auto
+
+lemma inorder_node42: "height l > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r"
+by(induct l a m b n c r rule: node42.induct) auto
+
+lemma inorder_node43: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r"
+by(induct l a m b n c r rule: node43.induct) auto
+
+lemma inorder_node44: "height n > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)"
+by(induct l a m b n c r rule: node44.induct) auto
+
+lemmas inorder_nodes = inorder_node21 inorder_node22
+  inorder_node31 inorder_node32 inorder_node33
+  inorder_node41 inorder_node42 inorder_node43 inorder_node44
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
+  x # inorder(tree\<^sub>d t') = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: inorder_nodes split: prod.splits)
+
+lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+by(induction t rule: del.induct)
+  (auto simp: inorder_nodes del_list_simps del_minD split: prod.splits)
+  (* 150 secs (2015) *)
+
+lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del)
+
+
+subsection \<open>Balancedness\<close>
+
+subsubsection "Proofs for insert"
+
+text{* First a standard proof that @{const ins} preserves @{const bal}. *}
+
+instantiation up\<^sub>i :: (type)height
+begin
+
+fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
+"height (T\<^sub>i t) = height t" |
+"height (Up\<^sub>i l a r) = height l"
+
+instance ..
+
+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, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
+
+
+text{* Now an alternative proof (by Brian Huffman) that runs faster because
+two properties (balance and height) are combined in one predicate. *}
+
+inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where
+"full 0 Leaf" |
+"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
+"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" |
+"\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)"
+
+inductive_cases full_elims:
+  "full n Leaf"
+  "full n (Node2 l p r)"
+  "full n (Node3 l p m q r)"
+  "full n (Node4 l p m q m' q' r)"
+
+inductive_cases full_0_elim: "full 0 t"
+inductive_cases full_Suc_elim: "full (Suc n) t"
+
+lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
+  by (auto elim: full_0_elim intro: full.intros)
+
+lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Node2_iff [simp]:
+  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Node3_iff [simp]:
+  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Node4_iff [simp]:
+  "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
+  by (induct set: full, simp_all)
+
+lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
+  by (induct set: full, auto dest: full_imp_height)
+
+lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
+  by (induct t, simp_all)
+
+lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
+  by (auto elim!: bal_imp_full full_imp_bal)
+
+text {* The @{const "insert"} function either preserves the height of the
+tree, or increases it by one. The constructor returned by the @{term
+"insert"} function determines which: A return value of the form @{term
+"T\<^sub>i t"} indicates that the height will be the same. A value of the
+form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
+
+primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
+"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
+"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
+
+lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
+by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split)
+
+text {* The @{const insert} operation preserves balance. *}
+
+lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
+unfolding bal_iff_full insert_def
+apply (erule exE)
+apply (drule full\<^sub>i_ins [of _ _ a])
+apply (cases "ins a t")
+apply (auto intro: full.intros)
+done
+
+
+subsubsection "Proofs for delete"
+
+instantiation up\<^sub>d :: (type)height
+begin
+
+fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
+"height (T\<^sub>d t) = height t" |
+"height (Up\<^sub>d t) = height t + 1"
+
+instance ..
+
+end
+
+lemma bal_tree\<^sub>d_node21:
+  "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))"
+by(induct l a r rule: node21.induct) auto
+
+lemma bal_tree\<^sub>d_node22:
+  "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))"
+by(induct l a r rule: node22.induct) auto
+
+lemma bal_tree\<^sub>d_node31:
+  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))"
+by(induct l a m b r rule: node31.induct) auto
+
+lemma bal_tree\<^sub>d_node32:
+  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))"
+by(induct l a m b r rule: node32.induct) auto
+
+lemma bal_tree\<^sub>d_node33:
+  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))"
+by(induct l a m b r rule: node33.induct) auto
+
+lemma bal_tree\<^sub>d_node41:
+  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))"
+by(induct l a m b n c r rule: node41.induct) auto
+
+lemma bal_tree\<^sub>d_node42:
+  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))"
+by(induct l a m b n c r rule: node42.induct) auto
+
+lemma bal_tree\<^sub>d_node43:
+  "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))"
+by(induct l a m b n c r rule: node43.induct) auto
+
+lemma bal_tree\<^sub>d_node44:
+  "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))"
+by(induct l a m b n c r rule: node44.induct) auto
+
+lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
+  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
+  bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44
+
+lemma height_node21:
+   "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1"
+by(induct l a r rule: node21.induct)(simp_all add: max.assoc)
+
+lemma height_node22:
+   "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1"
+by(induct l a r rule: node22.induct)(simp_all add: max.assoc)
+
+lemma height_node31:
+  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
+
+lemma height_node32:
+  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
+
+lemma height_node33:
+  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
+
+lemma height_node41:
+  "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) =
+   max (height l) (max (height m) (max (height n) (height r))) + 1"
+by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)
+
+lemma height_node42:
+  "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) =
+   max (height l) (max (height m) (max (height n) (height r))) + 1"
+by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)
+
+lemma height_node43:
+  "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) =
+   max (height l) (max (height m) (max (height n) (height r))) + 1"
+by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)
+
+lemma height_node44:
+  "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) =
+   max (height l) (max (height m) (max (height n) (height r))) + 1"
+by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)
+
+lemmas heights = height_node21 height_node22
+  height_node31 height_node32 height_node33
+  height_node41 height_node42 height_node43 height_node44
+
+lemma height_del_min:
+  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+by(induct t arbitrary: x t' rule: del_min.induct)
+  (auto simp: heights split: prod.splits)
+
+lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+by(induction x t rule: del.induct)
+  (auto simp add: heights height_del_min split: prod.split)
+
+lemma bal_del_min:
+  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+by(induct t arbitrary: x t' rule: del_min.induct)
+  (auto simp: heights height_del_min bals split: prod.splits)
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+by(induction x t rule: del.induct)
+  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
+(* 60 secs (2015) *)
+
+corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
+by(simp add: delete_def bal_tree\<^sub>d_del)
+
+subsection \<open>Overall Correctness\<close>
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 6 thus ?case by(simp add: bal_insert)
+next
+  case 7 thus ?case by(simp add: bal_delete)
+qed simp+
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,136 +1,136 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>A 2-3 Tree Implementation of Maps\<close>
-
-theory Tree23_Map
-imports
-  Tree23_Set
-  Map_by_Ordered
-begin
-
-fun lookup :: "('a::cmp * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"lookup Leaf x = None" |
-"lookup (Node2 l (a,b) r) x = (case cmp x a of
-  LT \<Rightarrow> lookup l x |
-  GT \<Rightarrow> lookup r x |
-  EQ \<Rightarrow> Some b)" |
-"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
-  LT \<Rightarrow> lookup l x |
-  EQ \<Rightarrow> Some b1 |
-  GT \<Rightarrow> (case cmp x a2 of
-          LT \<Rightarrow> lookup m x |
-          EQ \<Rightarrow> Some b2 |
-          GT \<Rightarrow> lookup r x))"
-
-fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
-"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
-"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
-   LT \<Rightarrow> (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)) |
-   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
-   GT \<Rightarrow> (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) = (case cmp x (fst ab1) of
-   LT \<Rightarrow> (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)) |
-   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
-   GT \<Rightarrow> (case cmp x (fst ab2) of
-           LT \<Rightarrow> (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)) |
-           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
-           GT \<Rightarrow> (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::cmp \<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::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
-"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) = (case cmp x (fst ab1) of
-  LT \<Rightarrow> node21 (del x l) ab1 r |
-  GT \<Rightarrow> node22 l ab1 (del x r) |
-  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
-"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
-  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
-  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
-  GT \<Rightarrow> (case cmp x (fst ab2) of
-           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
-           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
-           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
-
-definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
-"delete x t = tree\<^sub>d(del x t)"
-
-
-subsection \<open>Functional Correctness\<close>
-
-lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by (induction t) (auto simp: map_of_simps split: option.split)
-
-
-lemma inorder_upd:
-  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
-by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
-
-corollary inorder_update:
-  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
-by(simp add: update_def inorder_upd)
-
-
-lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
-by(induction t rule: del.induct)
-  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
-
-corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del)
-
-
-subsection \<open>Balancedness\<close>
-
-lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd a b t)) \<and> height(upd a b t) = height t"
-by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
-
-corollary bal_update: "bal t \<Longrightarrow> bal (update a b t)"
-by (simp add: update_def bal_upd)
-
-
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
-by(induction x t rule: del.induct)
-  (auto simp add: heights max_def height_del_min split: prod.split)
-
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
-by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
-
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
-
-
-subsection \<open>Overall Correctness\<close>
-
-interpretation T23_Map: Map_by_Ordered
-where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = bal
-proof (standard, goal_cases)
-  case 2 thus ?case by(simp add: lookup)
-next
-  case 3 thus ?case by(simp add: inorder_update)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 6 thus ?case by(simp add: bal_update)
-next
-  case 7 thus ?case by(simp add: bal_delete)
-qed simp+
-
-end
+(* Author: Tobias Nipkow *)
+
+section \<open>A 2-3 Tree Implementation of Maps\<close>
+
+theory Tree23_Map
+imports
+  Tree23_Set
+  Map_by_Ordered
+begin
+
+fun lookup :: "('a::cmp * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node2 l (a,b) r) x = (case cmp x a of
+  LT \<Rightarrow> lookup l x |
+  GT \<Rightarrow> lookup r x |
+  EQ \<Rightarrow> Some b)" |
+"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
+  LT \<Rightarrow> lookup l x |
+  EQ \<Rightarrow> Some b1 |
+  GT \<Rightarrow> (case cmp x a2 of
+          LT \<Rightarrow> lookup m x |
+          EQ \<Rightarrow> Some b2 |
+          GT \<Rightarrow> lookup r x))"
+
+fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
+"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
+"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
+   LT \<Rightarrow> (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)) |
+   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
+   GT \<Rightarrow> (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) = (case cmp x (fst ab1) of
+   LT \<Rightarrow> (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)) |
+   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
+   GT \<Rightarrow> (case cmp x (fst ab2) of
+           LT \<Rightarrow> (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)) |
+           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
+           GT \<Rightarrow> (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::cmp \<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::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
+"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) = (case cmp x (fst ab1) of
+  LT \<Rightarrow> node21 (del x l) ab1 r |
+  GT \<Rightarrow> node22 l ab1 (del x r) |
+  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
+"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
+  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
+  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
+  GT \<Rightarrow> (case cmp x (fst ab2) of
+           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
+           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
+           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
+
+definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
+"delete x t = tree\<^sub>d(del x t)"
+
+
+subsection \<open>Functional Correctness\<close>
+
+lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by (induction t) (auto simp: map_of_simps split: option.split)
+
+
+lemma inorder_upd:
+  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
+by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
+
+corollary inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
+by(simp add: update_def inorder_upd)
+
+
+lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+by(induction t rule: del.induct)
+  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
+
+corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del)
+
+
+subsection \<open>Balancedness\<close>
+
+lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd a b t)) \<and> height(upd a b t) = height t"
+by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
+
+corollary bal_update: "bal t \<Longrightarrow> bal (update a b t)"
+by (simp add: update_def bal_upd)
+
+
+lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+by(induction x t rule: del.induct)
+  (auto simp add: heights max_def height_del_min split: prod.split)
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+by(induction x t rule: del.induct)
+  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
+
+corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
+by(simp add: delete_def bal_tree\<^sub>d_del)
+
+
+subsection \<open>Overall Correctness\<close>
+
+interpretation T23_Map: Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: lookup)
+next
+  case 3 thus ?case by(simp add: inorder_update)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 6 thus ?case by(simp add: bal_update)
+next
+  case 7 thus ?case by(simp add: bal_delete)
+qed simp+
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,372 +1,372 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>A 2-3 Tree Implementation of Sets\<close>
-
-theory Tree23_Set
-imports
-  Tree23
-  Cmp
-  Set_by_Ordered
-begin
-
-fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
-"isin Leaf x = False" |
-"isin (Node2 l a r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
-"isin (Node3 l a m b r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
-   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))"
-
-datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
-
-fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
-"tree\<^sub>i (T\<^sub>i t) = t" |
-"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
-
-fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
-"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
-"ins x (Node2 l a r) =
-   (case cmp x a of
-      LT \<Rightarrow> (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)) |
-      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
-      GT \<Rightarrow> (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) =
-   (case cmp x a of
-      LT \<Rightarrow> (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)) |
-      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-      GT \<Rightarrow> (case cmp x b of
-               GT \<Rightarrow> (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)) |
-               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-               LT \<Rightarrow> (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::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"insert x t = tree\<^sub>i(ins x t)"
-
-datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
-
-fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
-"tree\<^sub>d (T\<^sub>d x) = x" |
-"tree\<^sub>d (Up\<^sub>d x) = x"
-
-(* Variation: return None to signal no-change *)
-
-fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
-"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
-"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
-
-fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
-"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
-"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
-
-fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
-"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
-
-fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
-
-fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
-"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
-
-fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
-"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
-"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
-"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
-"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
-
-fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
-where
-"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) = (case cmp x a of
-  LT \<Rightarrow> node21 (del x l) a r |
-  GT \<Rightarrow> node22 l a (del x r) |
-  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
-"del x (Node3 l a m b r) = (case cmp x a of
-  LT \<Rightarrow> node31 (del x l) a m b r |
-  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
-  GT \<Rightarrow> (case cmp x b of
-          LT \<Rightarrow> node32 l a (del x m) b r |
-          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
-          GT \<Rightarrow> node33 l a m b (del x r)))"
-
-definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"delete x t = tree\<^sub>d(del x t)"
-
-
-subsection "Functional Correctness"
-
-subsubsection "Proofs for isin"
-
-lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps1 ball_Un)
-
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
-
-
-subsubsection "Proofs for insert"
-
-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)
-
-lemma inorder_insert:
-  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
-by(simp add: insert_def inorder_ins)
-
-
-subsubsection "Proofs for delete"
-
-lemma inorder_node21: "height r > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
-by(induct l' a r rule: node21.induct) auto
-
-lemma inorder_node22: "height l > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
-by(induct l a r' rule: node22.induct) auto
-
-lemma inorder_node31: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
-by(induct l' a m b r rule: node31.induct) auto
-
-lemma inorder_node32: "height r > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
-by(induct l a m' b r rule: node32.induct) auto
-
-lemma inorder_node33: "height m > 0 \<Longrightarrow>
-  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
-by(induct l a m b r' rule: node33.induct) auto
-
-lemmas inorder_nodes = inorder_node21 inorder_node22
-  inorder_node31 inorder_node32 inorder_node33
-
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
-  x # inorder(tree\<^sub>d t') = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
-  (auto simp: inorder_nodes split: prod.splits)
-
-lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
-by(induction t rule: del.induct)
-  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
-
-lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del)
-
-
-subsection \<open>Balancedness\<close>
-
-
-subsubsection "Proofs for insert"
-
-text{* First a standard proof that @{const ins} preserves @{const bal}. *}
-
-instantiation up\<^sub>i :: (type)height
-begin
-
-fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
-"height (T\<^sub>i t) = height t" |
-"height (Up\<^sub>i l a r) = height l"
-
-instance ..
-
-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) (* 15 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. *}
-
-inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
-"full 0 Leaf" |
-"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
-"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)"
-
-inductive_cases full_elims:
-  "full n Leaf"
-  "full n (Node2 l p r)"
-  "full n (Node3 l p m q r)"
-
-inductive_cases full_0_elim: "full 0 t"
-inductive_cases full_Suc_elim: "full (Suc n) t"
-
-lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
-  by (auto elim: full_0_elim intro: full.intros)
-
-lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_Suc_Node2_iff [simp]:
-  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_Suc_Node3_iff [simp]:
-  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
-  by (auto elim: full_elims intro: full.intros)
-
-lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
-  by (induct set: full, simp_all)
-
-lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
-  by (induct set: full, auto dest: full_imp_height)
-
-lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
-  by (induct t, simp_all)
-
-lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
-  by (auto elim!: bal_imp_full full_imp_bal)
-
-text {* The @{const "insert"} function either preserves the height of the
-tree, or increases it by one. The constructor returned by the @{term
-"insert"} function determines which: A return value of the form @{term
-"T\<^sub>i t"} indicates that the height will be the same. A value of the
-form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
-
-fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
-"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
-"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
-
-lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
-by (induct rule: full.induct) (auto split: up\<^sub>i.split)
-
-text {* The @{const insert} operation preserves balance. *}
-
-lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
-unfolding bal_iff_full insert_def
-apply (erule exE)
-apply (drule full\<^sub>i_ins [of _ _ a])
-apply (cases "ins a t")
-apply (auto intro: full.intros)
-done
-
-
-subsection "Proofs for delete"
-
-instantiation up\<^sub>d :: (type)height
-begin
-
-fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
-"height (T\<^sub>d t) = height t" |
-"height (Up\<^sub>d t) = height t + 1"
-
-instance ..
-
-end
-
-lemma bal_tree\<^sub>d_node21:
-  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
-by(induct l' a r rule: node21.induct) auto
-
-lemma bal_tree\<^sub>d_node22:
-  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
-by(induct l a r' rule: node22.induct) auto
-
-lemma bal_tree\<^sub>d_node31:
-  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
-by(induct l' a m b r rule: node31.induct) auto
-
-lemma bal_tree\<^sub>d_node32:
-  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
-by(induct l a m' b r rule: node32.induct) auto
-
-lemma bal_tree\<^sub>d_node33:
-  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
-by(induct l a m b r' rule: node33.induct) auto
-
-lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
-  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
-
-lemma height'_node21:
-   "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
-by(induct l' a r rule: node21.induct)(simp_all)
-
-lemma height'_node22:
-   "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
-by(induct l a r' rule: node22.induct)(simp_all)
-
-lemma height'_node31:
-  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
-
-lemma height'_node32:
-  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
-
-lemma height'_node33:
-  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
-by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
-
-lemmas heights = height'_node21 height'_node22
-  height'_node31 height'_node32 height'_node33
-
-lemma height_del_min:
-  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights split: prod.splits)
-
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
-by(induction x t rule: del.induct)
-  (auto simp: heights max_def height_del_min split: prod.splits)
-
-lemma bal_del_min:
-  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights height_del_min bals split: prod.splits)
-
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
-by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
-
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
-
-
-subsection \<open>Overall Correctness\<close>
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = bal
-proof (standard, goal_cases)
-  case 2 thus ?case by(simp add: isin_set)
-next
-  case 3 thus ?case by(simp add: inorder_insert)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 6 thus ?case by(simp add: bal_insert)
-next
-  case 7 thus ?case by(simp add: bal_delete)
-qed simp+
-
-end
+(* Author: Tobias Nipkow *)
+
+section \<open>A 2-3 Tree Implementation of Sets\<close>
+
+theory Tree23_Set
+imports
+  Tree23
+  Cmp
+  Set_by_Ordered
+begin
+
+fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node2 l a r) x =
+  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
+"isin (Node3 l a m b r) x =
+  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
+   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))"
+
+datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
+
+fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
+"tree\<^sub>i (T\<^sub>i t) = t" |
+"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
+
+fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
+"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
+"ins x (Node2 l a r) =
+   (case cmp x a of
+      LT \<Rightarrow> (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)) |
+      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
+      GT \<Rightarrow> (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) =
+   (case cmp x a of
+      LT \<Rightarrow> (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)) |
+      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+      GT \<Rightarrow> (case cmp x b of
+               GT \<Rightarrow> (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)) |
+               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+               LT \<Rightarrow> (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::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+"insert x t = tree\<^sub>i(ins x t)"
+
+datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
+
+fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
+"tree\<^sub>d (T\<^sub>d x) = x" |
+"tree\<^sub>d (Up\<^sub>d x) = x"
+
+(* Variation: return None to signal no-change *)
+
+fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
+"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
+"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
+
+fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
+"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
+"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
+"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
+
+fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
+"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
+"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
+
+fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
+"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
+
+fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
+"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
+"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
+
+fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
+"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
+"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
+"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
+"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
+
+fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
+where
+"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) = (case cmp x a of
+  LT \<Rightarrow> node21 (del x l) a r |
+  GT \<Rightarrow> node22 l a (del x r) |
+  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+"del x (Node3 l a m b r) = (case cmp x a of
+  LT \<Rightarrow> node31 (del x l) a m b r |
+  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+  GT \<Rightarrow> (case cmp x b of
+          LT \<Rightarrow> node32 l a (del x m) b r |
+          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+          GT \<Rightarrow> node33 l a m b (del x r)))"
+
+definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+"delete x t = tree\<^sub>d(del x t)"
+
+
+subsection "Functional Correctness"
+
+subsubsection "Proofs for isin"
+
+lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps1 ball_Un)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps2)
+
+
+subsubsection "Proofs for insert"
+
+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)
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
+by(simp add: insert_def inorder_ins)
+
+
+subsubsection "Proofs for delete"
+
+lemma inorder_node21: "height r > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
+by(induct l' a r rule: node21.induct) auto
+
+lemma inorder_node22: "height l > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
+by(induct l a r' rule: node22.induct) auto
+
+lemma inorder_node31: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
+by(induct l' a m b r rule: node31.induct) auto
+
+lemma inorder_node32: "height r > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
+by(induct l a m' b r rule: node32.induct) auto
+
+lemma inorder_node33: "height m > 0 \<Longrightarrow>
+  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
+by(induct l a m b r' rule: node33.induct) auto
+
+lemmas inorder_nodes = inorder_node21 inorder_node22
+  inorder_node31 inorder_node32 inorder_node33
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
+  x # inorder(tree\<^sub>d t') = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: inorder_nodes split: prod.splits)
+
+lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+by(induction t rule: del.induct)
+  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
+
+lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del)
+
+
+subsection \<open>Balancedness\<close>
+
+
+subsubsection "Proofs for insert"
+
+text{* First a standard proof that @{const ins} preserves @{const bal}. *}
+
+instantiation up\<^sub>i :: (type)height
+begin
+
+fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
+"height (T\<^sub>i t) = height t" |
+"height (Up\<^sub>i l a r) = height l"
+
+instance ..
+
+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) (* 15 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. *}
+
+inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
+"full 0 Leaf" |
+"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
+"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)"
+
+inductive_cases full_elims:
+  "full n Leaf"
+  "full n (Node2 l p r)"
+  "full n (Node3 l p m q r)"
+
+inductive_cases full_0_elim: "full 0 t"
+inductive_cases full_Suc_elim: "full (Suc n) t"
+
+lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
+  by (auto elim: full_0_elim intro: full.intros)
+
+lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Node2_iff [simp]:
+  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Node3_iff [simp]:
+  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
+  by (induct set: full, simp_all)
+
+lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
+  by (induct set: full, auto dest: full_imp_height)
+
+lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
+  by (induct t, simp_all)
+
+lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
+  by (auto elim!: bal_imp_full full_imp_bal)
+
+text {* The @{const "insert"} function either preserves the height of the
+tree, or increases it by one. The constructor returned by the @{term
+"insert"} function determines which: A return value of the form @{term
+"T\<^sub>i t"} indicates that the height will be the same. A value of the
+form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
+
+fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
+"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
+"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
+
+lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
+by (induct rule: full.induct) (auto split: up\<^sub>i.split)
+
+text {* The @{const insert} operation preserves balance. *}
+
+lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
+unfolding bal_iff_full insert_def
+apply (erule exE)
+apply (drule full\<^sub>i_ins [of _ _ a])
+apply (cases "ins a t")
+apply (auto intro: full.intros)
+done
+
+
+subsection "Proofs for delete"
+
+instantiation up\<^sub>d :: (type)height
+begin
+
+fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
+"height (T\<^sub>d t) = height t" |
+"height (Up\<^sub>d t) = height t + 1"
+
+instance ..
+
+end
+
+lemma bal_tree\<^sub>d_node21:
+  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
+by(induct l' a r rule: node21.induct) auto
+
+lemma bal_tree\<^sub>d_node22:
+  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
+by(induct l a r' rule: node22.induct) auto
+
+lemma bal_tree\<^sub>d_node31:
+  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
+by(induct l' a m b r rule: node31.induct) auto
+
+lemma bal_tree\<^sub>d_node32:
+  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
+by(induct l a m' b r rule: node32.induct) auto
+
+lemma bal_tree\<^sub>d_node33:
+  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
+  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
+by(induct l a m b r' rule: node33.induct) auto
+
+lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
+  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
+
+lemma height'_node21:
+   "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
+by(induct l' a r rule: node21.induct)(simp_all)
+
+lemma height'_node22:
+   "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
+by(induct l a r' rule: node22.induct)(simp_all)
+
+lemma height'_node31:
+  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
+
+lemma height'_node32:
+  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
+
+lemma height'_node33:
+  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
+   max (height l) (max (height m) (height r)) + 1"
+by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
+
+lemmas heights = height'_node21 height'_node22
+  height'_node31 height'_node32 height'_node33
+
+lemma height_del_min:
+  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+by(induct t arbitrary: x t' rule: del_min.induct)
+  (auto simp: heights split: prod.splits)
+
+lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+by(induction x t rule: del.induct)
+  (auto simp: heights max_def height_del_min split: prod.splits)
+
+lemma bal_del_min:
+  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+by(induct t arbitrary: x t' rule: del_min.induct)
+  (auto simp: heights height_del_min bals split: prod.splits)
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+by(induction x t rule: del.induct)
+  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
+
+corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
+by(simp add: delete_def bal_tree\<^sub>d_del)
+
+
+subsection \<open>Overall Correctness\<close>
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 6 thus ?case by(simp add: bal_insert)
+next
+  case 7 thus ?case by(simp add: bal_delete)
+qed simp+
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,66 +1,66 @@
-(* Author: Tobias Nipkow *)
-
-section {* Unbalanced Tree as Map *}
-
-theory Tree_Map
-imports
-  Tree_Set
-  Map_by_Ordered
-begin
-
-fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"lookup Leaf x = None" |
-"lookup (Node l (a,b) r) x =
-  (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
-
-fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"update x y Leaf = Node Leaf (x,y) Leaf" |
-"update x y (Node l (a,b) r) = (case cmp x a of
-   LT \<Rightarrow> Node (update x y l) (a,b) r |
-   EQ \<Rightarrow> Node l (x,y) r |
-   GT \<Rightarrow> Node l (a,b) (update x y r))"
-
-fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete x Leaf = Leaf" |
-"delete x (Node l (a,b) r) = (case cmp x a of
-  LT \<Rightarrow> Node (delete x l) (a,b) r |
-  GT \<Rightarrow> Node l (a,b) (delete x r) |
-  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
-
-
-subsection "Functional Correctness Proofs"
-
-lemma lookup_eq:
-  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by (induction t) (auto simp: map_of_simps split: option.split)
-
-
-lemma inorder_update:
-  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
-by(induction t) (auto simp: upd_list_simps)
-
-
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
-   x # inorder t' = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
-  (auto simp: del_list_simps split: prod.splits)
-
-lemma inorder_delete:
-  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
-
-interpretation Map_by_Ordered
-where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by(simp add: lookup_eq)
-next
-  case 3 thus ?case by(simp add: inorder_update)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Unbalanced Tree as Map *}
+
+theory Tree_Map
+imports
+  Tree_Set
+  Map_by_Ordered
+begin
+
+fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node l (a,b) r) x =
+  (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
+
+fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"update x y Leaf = Node Leaf (x,y) Leaf" |
+"update x y (Node l (a,b) r) = (case cmp x a of
+   LT \<Rightarrow> Node (update x y l) (a,b) r |
+   EQ \<Rightarrow> Node l (x,y) r |
+   GT \<Rightarrow> Node l (a,b) (update x y r))"
+
+fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"delete x Leaf = Leaf" |
+"delete x (Node l (a,b) r) = (case cmp x a of
+  LT \<Rightarrow> Node (delete x l) (a,b) r |
+  GT \<Rightarrow> Node l (a,b) (delete x r) |
+  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma lookup_eq:
+  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by (induction t) (auto simp: map_of_simps split: option.split)
+
+
+lemma inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
+by(induction t) (auto simp: upd_list_simps)
+
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
+   x # inorder t' = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: del_list_simps split: prod.splits)
+
+lemma inorder_delete:
+  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
+
+interpretation Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: lookup_eq)
+next
+  case 3 thus ?case by(simp add: inorder_update)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed (rule TrueI)+
+
+end
diff -r 7ffc9c4f1f74 -r 44c9198f210c src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Wed Nov 11 18:32:26 2015 +0100
@@ -1,75 +1,75 @@
-(* Author: Tobias Nipkow *)
-
-section {* Tree Implementation of Sets *}
-
-theory Tree_Set
-imports
-  "~~/src/HOL/Library/Tree"
-  Cmp
-  Set_by_Ordered
-begin
-
-fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
-"isin Leaf x = False" |
-"isin (Node l a r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)"
-
-hide_const (open) insert
-
-fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert x Leaf = Node Leaf x Leaf" |
-"insert x (Node l a r) = (case cmp x a of
-      LT \<Rightarrow> Node (insert x l) a r |
-      EQ \<Rightarrow> Node l a r |
-      GT \<Rightarrow> 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::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete x Leaf = Leaf" |
-"delete x (Node l a r) = (case cmp x a of
-  LT \<Rightarrow>  Node (delete x l) a r |
-  GT \<Rightarrow>  Node l a (delete x r) |
-  EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
-
-
-subsection "Functional Correctness Proofs"
-
-lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps1)
-
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
-
-
-lemma inorder_insert:
-  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
-by(induction t) (auto simp: ins_list_simps)
-
-
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
-   x # inorder t' = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
-  (auto simp: sorted_lems split: prod.splits)
-
-lemma inorder_delete:
-  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by(simp add: isin_set)
-next
-  case 3 thus ?case by(simp add: inorder_insert)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Tree Implementation of Sets *}
+
+theory Tree_Set
+imports
+  "~~/src/HOL/Library/Tree"
+  Cmp
+  Set_by_Ordered
+begin
+
+fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node l a r) x =
+  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)"
+
+hide_const (open) insert
+
+fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"insert x Leaf = Node Leaf x Leaf" |
+"insert x (Node l a r) = (case cmp x a of
+      LT \<Rightarrow> Node (insert x l) a r |
+      EQ \<Rightarrow> Node l a r |
+      GT \<Rightarrow> 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::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"delete x Leaf = Leaf" |
+"delete x (Node l a r) = (case cmp x a of
+  LT \<Rightarrow>  Node (delete x l) a r |
+  GT \<Rightarrow>  Node l a (delete x r) |
+  EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps1)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps2)
+
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+by(induction t) (auto simp: ins_list_simps)
+
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
+   x # inorder t' = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: sorted_lems split: prod.splits)
+
+lemma inorder_delete:
+  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed (rule TrueI)+
+
+end