# HG changeset patch
# User huffman
# Date 1320315486 -3600
# Node ID 26b6179b5a450783b7444cc299b26319a481a139
# Parent  4ef9220b886bfb26a03d43246757de27dba7aae0
ex/Tree23.thy: prove that insertion preserves tree balance and order

diff -r 4ef9220b886b -r 26b6179b5a45 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Thu Nov 03 18:10:47 2011 +1100
+++ b/src/HOL/ex/Tree23.thy	Thu Nov 03 11:18:06 2011 +0100
@@ -159,6 +159,25 @@
 "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)"
 
+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))"
+
+lemma opt_less_simps [simp]:
+  "opt_less None y = True"
+  "opt_less x None = True"
+  "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
+"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)
+
 fun height :: "'a tree23 \<Rightarrow> nat" where
 "height Empty = 0" |
 "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
@@ -170,6 +189,132 @@
 "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)"
 
+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)"
+
+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)
+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
+
+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
+
+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)"
+
+lemma gtree_simps [simp]:
+  "gtree (Stay t) = t"
+  "gtree (Sprout l p r) = Branch2 l p r"
+unfolding gtree_def by simp_all
+
+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
+ apply (induct t arbitrary: k1 k2)
+   apply simp
+  apply clarsimp
+  apply (rule_tac a=k and b=a in ord_cases)
+    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 (rule_tac a=k and b=a in ord_cases)
+   apply simp
+   apply (case_tac "add k y t1", simp, simp)
+  apply simp
+ apply simp
+ apply (rule_tac a=k and b=aa in ord_cases)
+   apply simp
+   apply (case_tac "add k y t2", simp, simp)
+  apply simp
+ apply simp
+ apply (case_tac "add k y t3", simp, simp)
+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')
+
 text{* This is a little test harness and should be commented out once the
 above functions have been proved correct. *}