# HG changeset patch
# User wenzelm
# Date 1320411139 -3600
# Node ID 2838109364f0f974990c1ffc61594fa0980603be
# Parent  f502f439305435023f77dac7e0b8b993ffda8f60# Parent  6e0a8aba99ec4d96638f72ea91ed9ac8c40ef7bd
merged

diff -r 6e0a8aba99ec -r 2838109364f0 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Fri Nov 04 00:07:45 2011 +0100
+++ b/src/HOL/ex/Tree23.thy	Fri Nov 04 13:52:19 2011 +0100
@@ -136,28 +136,7 @@
 definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
 "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
 
-
-(* yes, this is rather slow *)
-fun ord0 :: "'a tree23 \<Rightarrow> bool"
-and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
-and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
-and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool"
-where
-"ord0 Empty = True" |
-"ord0 (Branch2 l p r)  = (ordr l (fst p) & ordl (fst p) r)" |
-"ord0 (Branch3 l p m q r)  = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
-
-"ordl _ Empty = True" |
-"ordl x (Branch2 l p r)  = (ordlr x l (fst p) & ordl (fst p) r)" |
-"ordl x (Branch3 l p m q r)  = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
-
-"ordr Empty _ = True" |
-"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" |
-"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" |
-
-"ordlr x Empty y = (x < y)" |
-"ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
-"ordlr x (Branch3 l p m q r) y = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r y)"
+text {* Ordered trees *}
 
 definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
   "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
@@ -168,15 +147,42 @@
   "opt_less (Some a) (Some b) = (a < b)"
 unfolding opt_less_def by (auto simp add: ord_def split: option.split)
 
-fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
+primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
 "ord' x Empty y = opt_less x y" |
 "ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
 "ord' x (Branch3 l p m q r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) m (Some (fst q)) & ord' (Some (fst q)) r y)"
 
-lemma ord':
-  "ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
-    | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
-by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
+definition ord0 :: "'a tree23 \<Rightarrow> bool" where
+  "ord0 t = ord' None t None"
+
+text {* Balanced trees *}
+
+inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
+"full 0 Empty" |
+"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
+"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
+
+inductive_cases full_elims:
+  "full n Empty"
+  "full n (Branch2 l p r)"
+  "full n (Branch3 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 = Empty"
+  by (auto elim: full_0_elim intro: full.intros)
+
+lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Branch2_iff [simp]:
+  "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
+  by (auto elim: full_elims intro: full.intros)
+
+lemma full_Suc_Branch3_iff [simp]:
+  "full (Suc n) (Branch3 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)
 
 fun height :: "'a tree23 \<Rightarrow> nat" where
 "height Empty = 0" |
@@ -189,45 +195,49 @@
 "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
 "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
 
+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 @{term "add0"} function either preserves the height of the
 tree, or increases it by one. The constructor returned by the @{term
 "add"} function determines which: A return value of the form @{term
 "Stay t"} indicates that the height will be the same. A value of the
 form @{term "Sprout l p r"} indicates an increase in height. *}
 
-fun gheight :: "'a growth \<Rightarrow> nat" where
-"gheight (Stay t) = height t" |
-"gheight (Sprout l p r) = max (height l) (height r)"
+primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where
+"gfull n (Stay t) \<longleftrightarrow> full n t" |
+"gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r"
+
+lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
+by (induct set: full, auto split: ord.split growth.split)
 
-lemma gheight_add: "gheight (add k y t) = height t"
- apply (induct t)
-   apply simp
-  apply clarsimp
-  apply (case_tac "ord k a")
-    apply simp
-    apply (case_tac "add k y t1", simp, simp)
-   apply simp
-  apply simp
-  apply (case_tac "add k y t2", simp, simp)
- apply clarsimp
- apply (case_tac "ord k a")
-   apply simp
-   apply (case_tac "add k y t1", simp, simp)
-  apply simp
- apply simp
- apply (case_tac "ord k aa")
-   apply simp
-   apply (case_tac "add k y t2", simp, simp)
-  apply simp
- apply simp
- apply (case_tac "add k y t3", simp, simp)
+text {* The @{term "add0"} operation preserves balance. *}
+
+lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
+unfolding bal_iff_full add0_def
+apply (erule exE)
+apply (drule gfull_add [of _ _ k y])
+apply (cases "add k y t")
+apply (auto intro: full.intros)
 done
 
-lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'"
-  using gheight_add [of k y t] by simp
+text {* The @{term "add0"} operation preserves order. *}
 
-lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)"
-  using gheight_add [of k y t] by simp
+lemma ord_cases:
+  fixes a b :: int obtains
+  "ord a b = LESS" and "a < b" |
+  "ord a b = EQUAL" and "a = b" |
+  "ord a b = GREATER" and "a > b"
+unfolding ord_def by (rule linorder_cases [of a b]) auto
 
 definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
   "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
@@ -240,52 +250,6 @@
 lemma add0: "add0 k y t = gtree (add k y t)"
   unfolding add0_def by (simp split: growth.split)
 
-text {* The @{term "add0"} operation preserves balance. *}
-
-lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
-unfolding add0
- apply (induct t)
-   apply simp
-  apply clarsimp
-  apply (case_tac "ord k a")
-    apply simp
-    apply (case_tac "add k y t1")
-     apply (simp, drule add_eq_Stay_dest, simp)
-    apply (simp, drule add_eq_Sprout_dest, simp)
-   apply simp
-  apply simp
-  apply (case_tac "add k y t2")
-   apply (simp, drule add_eq_Stay_dest, simp)
-  apply (simp, drule add_eq_Sprout_dest, simp)
- apply clarsimp
- apply (case_tac "ord k a")
-   apply simp
-   apply (case_tac "add k y t1")
-    apply (simp, drule add_eq_Stay_dest, simp)
-   apply (simp, drule add_eq_Sprout_dest, simp)
-  apply simp
- apply simp
- apply (case_tac "ord k aa")
-   apply simp
-   apply (case_tac "add k y t2")
-    apply (simp, drule add_eq_Stay_dest, simp)
-   apply (simp, drule add_eq_Sprout_dest, simp)
-  apply simp
- apply simp
- apply (case_tac "add k y t3")
-  apply (simp, drule add_eq_Stay_dest, simp)
- apply (simp, drule add_eq_Sprout_dest, simp)
-done
-
-text {* The @{term "add0"} operation preserves order. *}
-
-lemma ord_cases:
-  fixes a b :: int obtains
-  "ord a b = LESS" and "a < b" |
-  "ord a b = EQUAL" and "a = b" |
-  "ord a b = GREATER" and "a > b"
-unfolding ord_def by (rule linorder_cases [of a b]) auto
-
 lemma ord'_add0:
   "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
 unfolding add0
@@ -313,7 +277,126 @@
 done
 
 lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
-using ord'_add0 [of None t None k y] by (simp add: ord')
+  by (simp add: ord0_def ord'_add0)
+
+text {* The @{term "del"} function preserves balance. *}
+
+lemma del_extra_simps:
+"l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
+ del k (Branch2 l p r) = (case compare k p of
+      LESS => (case del k l of None \<Rightarrow> None |
+        Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
+      | Some(p', (True, l')) => Some(p', case r of
+          Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
+        | Branch3 rl rp rm rq rr => (False, Branch2
+            (Branch2 l' p rl) rp (Branch2 rm rq rr))))
+    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
+        Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
+      | Some(p', (True, r')) => Some(p', case l of
+          Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
+        | Branch3 ll lp lm lq lr => (False, Branch2
+            (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
+"l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
+ del k (Branch3 l p m q r) = (case compare k q of
+      LESS => (case compare k p of
+        LESS => (case del k l of None \<Rightarrow> None |
+          Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
+        | Some(p', (True, l')) => Some(p', (False, case (m, r) of
+            (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
+          | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
+          | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
+              Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
+      | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
+          Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
+        | Some(p', (True, m')) => Some(p', (False, case (l, r) of
+            (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
+          | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
+          | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
+    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
+        Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
+      | Some(q', (True, r')) => Some(q', (False, case (l, m) of
+          (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
+        | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
+        | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
+            Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
+apply -
+apply (cases l, cases r, simp_all only: del.simps, simp)
+apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
+done
+
+fun dfull where
+"dfull n None \<longleftrightarrow> True" |
+"dfull n (Some (p, (True, t'))) \<longleftrightarrow> full n t'" |
+"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
+
+lemmas dfull_case_intros =
+  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)", standard]
+  option.exhaust [where y=y and P="dfull a (option_case b c y)", standard]
+  prod.exhaust [where y=y and P="dfull a (prod_case b y)", standard]
+  bool.exhaust [where y=y and P="dfull a (bool_case b c y)", standard]
+  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))", standard]
+  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
+
+lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
+proof -
+  { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
+    assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
+    and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
+    and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
+    and "full (Suc n) (Branch2 l p r)"
+    hence "dfull n (del k (Branch2 l p r))"
+     apply clarsimp
+     apply (cases n)
+      apply (cases k)
+       apply simp
+      apply (simp split: ord.split)
+     apply simp
+     apply (subst del_extra_simps, force)
+     (* This should work, but it is way too slow!
+     apply (force split: ord.split option.split bool.split tree23.split) *)
+     apply (simp | rule dfull_case_intros)+
+     done
+  } note A = this
+  { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
+    assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
+    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) m)"
+    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) m)"
+    and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
+    and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
+    and "full (Suc n) (Branch3 l p m q r)"
+    hence "dfull n (del k (Branch3 l p m q r))"
+     apply clarsimp
+     apply (cases n)
+      apply (cases k)
+       apply simp
+      apply (simp split: ord.split)
+     apply simp
+     apply (subst del_extra_simps, force)
+     apply (simp | rule dfull_case_intros)+
+     done
+  } note B = this
+  show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
+  proof (induct k t arbitrary: n rule: del.induct)
+    { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
+    { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
+    { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
+        by simp }
+    { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
+        by (simp split: ord.split) }
+    { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
+        by (simp split: ord.split) }
+    { case goal26 thus ?case by simp }
+  qed (fact A | fact B)+
+qed
+
+lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
+unfolding bal_iff_full del0_def
+apply (erule exE)
+apply (case_tac n, simp, simp)
+apply (frule dfull_del [where k="Some k"])
+apply (cases "del (Some k) t", force)
+apply (case_tac "a", rename_tac p b t', case_tac "b", auto)
+done
 
 text{* This is a little test harness and should be commented out once the
 above functions have been proved correct. *}
@@ -327,12 +410,15 @@
 
 text{* Some quick checks: *}
 
+lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
+  by (induct as t arbitrary: t rule: exec.induct,
+    simp_all add: bal_add0 bal_del0)
+
+lemma "bal(exec as Empty)"
+  by (simp add: bal_exec)
+
 lemma "ord0(exec as Empty)"
 quickcheck
 oops
 
-lemma "bal(exec as Empty)"
-quickcheck
-oops
-
-end
\ No newline at end of file
+end