# HG changeset patch
# User kleing
# Date 1078115972 -3600
# Node ID a9880349671174affb868ed09ab8cfbb94fecbf8
# Parent  b62323c85134777910a45c1994ba5cf4c7eb9758
converted to Isar

diff -r b62323c85134 -r a98803496711 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 01 05:21:43 2004 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 01 05:39:32 2004 +0100
@@ -565,7 +565,7 @@
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
-$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
+$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.thy ex/Antiquote.thy \
   ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
   ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
   ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
diff -r b62323c85134 -r a98803496711 src/HOL/ex/AVL.ML
--- a/src/HOL/ex/AVL.ML	Mon Mar 01 05:21:43 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,305 +0,0 @@
-(*  Title:      HOL/ex/AVL.ML
-    ID:         $Id$
-    Author:     Cornelia Pusch and Tobias Nipkow
-    Copyright   1998  TUM
-*)
-
-(******************************    isbal    **********************************)
-
-Addsimps[Let_def];
-
-(* rotations preserve isbal property *)
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l = Right --> isbal l --> isbal r \
-\ --> isbal (lr_rot (n, l, r))";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree2" 1);
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-by (arith_tac 1);
-qed_spec_mp "isbal_lr_rot";
-
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l ~= Right --> isbal l --> isbal r \
-\ --> isbal (r_rot (n, l, r))";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "isbal_r_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r = Left --> isbal l --> isbal r \
-\ --> isbal (rl_rot (n, l, r))";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree1" 1);
- by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-by (arith_tac 1);
-qed_spec_mp "isbal_rl_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r ~= Left --> isbal l --> isbal r \
-\ --> isbal (l_rot (n, l, r))";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "isbal_l_rot";
-
-
-(* lemmas about height after rotation *)
-
-Goalw [bal_def]
-"bal l = Right --> height l = Suc(Suc(height r))   \
-\ -->     Suc(height (lr_rot (n, l, r)))  = height (MKT n l r) ";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree2" 1);
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "height_lr_rot";
-
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l ~= Right \
-\ --> Suc(height (r_rot (n, l, r))) = height (MKT n l r) | \
-\         height (r_rot (n, l, r))  = height (MKT n l r)";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "height_r_rot";
-
-
-Goalw [l_bal_def]
-"height l = Suc(Suc(height r))  \
-\ --> Suc(height (l_bal n l r)) = height (MKT n l r) | \
-\         height (l_bal n l r)  = height (MKT n l r)";
-by (case_tac "bal l = Right" 1);
- by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1);
-by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1);
-qed_spec_mp "height_l_bal";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r = Left \
-\ -->     Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree1" 1);
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "height_rl_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r ~= Left \
-\ --> Suc(height (l_rot (n, l, r))) = height (MKT n l r) | \
-\         height (l_rot (n, l, r))  = height (MKT n l r)";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-qed_spec_mp "height_l_rot";
-
-
-Goalw [r_bal_def]
-"height r = Suc(Suc(height l))  \
-\ --> Suc(height (r_bal n l r)) = height (MKT n l r) | \
-\         height (r_bal n l r)  = height (MKT n l r)";
-by (case_tac "bal r = Left" 1);
- by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1);
-by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1);
-qed_spec_mp "height_r_bal";
-
-
-(* lemma about height after insert *)
-Goal
-"isbal t  \
-\ --> height (insert x t) = height t | height (insert x t) = Suc(height t)";
-by (induct_tac "t" 1);
- by (Simp_tac 1);
-by (case_tac "x=nat" 1);
- by (Asm_simp_tac 1);
-by (case_tac "x<nat" 1);
- by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
-  by (forw_inst_tac [("n","nat")]  height_l_bal 1);  
-  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
-  by (fast_tac (claset() addss simpset()) 1);
- by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
- by (fast_tac (claset() addss simpset()) 1);
-by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
- by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
- by (fast_tac (claset() addss (simpset() addsimps [max_def])) 1);
-by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "height_insert";
-
-
-Goal
-"!!x. [| height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) |] \
-\ ==> isbal (MKT n (insert x l) r)";
-by (cut_inst_tac [("x","x"),("t","l")] height_insert 1);
- by (Asm_full_simp_tac 1); 
-by (fast_tac (claset() addss simpset()) 1);
-qed "isbal_insert_left";
-
-
-Goal
-"!!x. [| height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) |] \
-\ ==> isbal (MKT n l (insert x r))";
-by (cut_inst_tac [("x","x"),("t","r")] height_insert 1);
- by (Asm_full_simp_tac 1); 
-by (fast_tac (claset() addss simpset()) 1);
-qed "isbal_insert_right";
-
-(* insert-operation preserves isbal property *)
-
-Goal
-"isbal t --> isbal(insert x t)";
-by (induct_tac "t" 1);
- by (Simp_tac 1);
-by (case_tac "x=nat" 1);
- by (Asm_simp_tac 1); 
-by (case_tac "x<nat" 1);
- by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
-  by (case_tac "bal (insert x tree1) = Right" 1);
-   by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset() 
-	addsimps [l_bal_def])) 1);  
-  by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() 
-	addsimps [l_bal_def])) 1);  
- by (Clarify_tac 1);
- by (ftac isbal_insert_left 1);
-   by (Asm_full_simp_tac 1); 
-  by (assume_tac 1);
- by (Asm_full_simp_tac 1); 
-by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
- by (case_tac "bal (insert x tree2) = Left" 1);
-  by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset() 
-	addsimps [r_bal_def])) 1);  
- by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() 
-	addsimps [r_bal_def])) 1);  
-by (Clarify_tac 1);
-by (ftac isbal_insert_right 1);
-   by (Asm_full_simp_tac 1); 
-  by (assume_tac 1);
- by (Asm_full_simp_tac 1); 
-qed_spec_mp "isbal_insert";
-
-
-(******************************    isin    **********************************)
-
-
-(* rotations preserve isin property *)
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l = Right  \
-\ --> isin x (lr_rot (n, l, r)) = isin x (MKT n l r)";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree2" 1);
- by (Asm_simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "isin_lr_rot";
-
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l ~= Right  \
-\ --> isin x (r_rot (n, l, r)) = isin x (MKT n l r)";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "isin_r_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r = Left  \
-\ --> isin x (rl_rot (n, l, r)) = isin x (MKT n l r)";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree1" 1);
- by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "isin_rl_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r ~= Left  \
-\ --> isin x (l_rot (n, l, r)) = isin x (MKT n l r)";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed_spec_mp "isin_l_rot";
-
-
-(* isin insert *)
-
-Goal
-"isin y (insert x t) = (y=x | isin y t)";
-by (induct_tac "t" 1);
- by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
-	r_bal_def,isin_rl_rot,isin_l_rot]) 1);
-by (Blast_tac 1);
-qed "isin_insert";
-
-
-(******************************    isord    **********************************)
-
-(* rotations preserve isord property *)
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l = Right --> isord (MKT n l r) \
-\ --> isord (lr_rot (n, l, r))";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree2" 1);
- by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [less_trans])1);
-qed_spec_mp "isord_lr_rot";
-
-
-Goalw [bal_def]
-"height l = Suc(Suc(height r)) --> bal l ~= Right --> isord (MKT n l r) \
-\ --> isord (r_rot (n, l, r))";
-by (case_tac "l" 1); 
- by (Asm_simp_tac 1);
-by (auto_tac (claset() addIs [less_trans],simpset()));
-qed_spec_mp "isord_r_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r = Left --> isord (MKT n l r) \
-\ --> isord (rl_rot (n, l, r))";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (case_tac "tree1" 1);
- by (asm_simp_tac (simpset() addsimps [le_def]) 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [less_trans])1);
-qed_spec_mp "isord_rl_rot";
-
-
-Goalw [bal_def]
-"height r = Suc(Suc(height l)) --> bal r ~= Left --> isord (MKT n l r)  \
-\ --> isord (l_rot (n, l, r))";
-by (case_tac "r" 1); 
- by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [less_trans])1);
-qed_spec_mp "isord_l_rot";
-
-(* insert operation presreves isord property *)
-
-Goal
-"isord t --> isord(insert x t)";
-by (induct_tac "t" 1);
- by (Simp_tac 1);
-by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1);
- by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot,
-	isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1);  
-qed_spec_mp "isord_insert";
diff -r b62323c85134 -r a98803496711 src/HOL/ex/AVL.thy
--- a/src/HOL/ex/AVL.thy	Mon Mar 01 05:21:43 2004 +0100
+++ b/src/HOL/ex/AVL.thy	Mon Mar 01 05:39:32 2004 +0100
@@ -1,84 +1,96 @@
 (*  Title:      HOL/ex/AVL.thy
     ID:         $Id$
-    Author:     Cornelia Pusch and Tobias Nipkow
+    Author:     Cornelia Pusch and Tobias Nipkow, converted to Isar by Gerwin Klein
     Copyright   1998  TUM
-
-AVL trees: at the moment only insertion.
-This version works exclusively with nat.
-Balance check could be simplified by working with int:
-"isbal (MKT n l r) = (abs(int(height l) - int(height r)) <= 1 &
-                      isbal l & isbal r)"
 *)
 
-AVL = Main +
+header "AVL Trees"
+
+theory AVL = Main:
+
+text {* 
+  At the moment only insertion is formalized.
+
+  This theory would be a nice candidate for structured Isar proof
+  texts and for extensions (delete operation). 
+*}
+
+(*
+  This version works exclusively with nat. Balance check could be
+  simplified by working with int: 
+  is_bal (MKT n l r) = (abs(int(height l) - int(height r)) <= 1 & is_bal l & is_bal r)
+*)
 
 datatype tree = ET | MKT nat tree tree
 
 consts
- height :: "tree => nat"
- isin   :: "nat => tree => bool"
- isord  :: "tree => bool"
- isbal  :: "tree => bool"
+  height :: "tree \<Rightarrow> nat"
+  is_in  :: "nat \<Rightarrow> tree \<Rightarrow> bool"
+  is_ord :: "tree \<Rightarrow> bool"
+  is_bal :: "tree \<Rightarrow> bool"
 
 primrec
-"height ET = 0"
-"height (MKT n l r) = Suc(max (height l) (height r))"
+  "height ET = 0"
+  "height (MKT n l r) = 1 + max (height l) (height r)"
 
 primrec
-"isin k ET = False"
-"isin k (MKT n l r) = (k=n | isin k l | isin k r)"
+  "is_in k ET = False"
+  "is_in k (MKT n l r) = (k=n \<or> is_in k l \<or> is_in k r)"
 
 primrec
-"isord ET = True"
-"isord (MKT n l r) = ((! n'. isin n' l --> n' < n) &
-                      (! n'. isin n' r --> n < n') &
-                      isord l & isord r)"
+  "is_ord ET = True"
+  "is_ord (MKT n l r) = ((\<forall>n'. is_in n' l \<longrightarrow> n' < n) \<and>
+                        (\<forall>n'. is_in n' r \<longrightarrow> n < n') \<and>
+                        is_ord l \<and> is_ord r)"
 
 primrec
-"isbal ET = True"
-"isbal (MKT n l r) = ((height l = height r | 
-                       height l = Suc(height r) | 
-                       height r = Suc(height l)) & 
-                      isbal l & isbal r)"
+  "is_bal ET = True"
+  "is_bal (MKT n l r) = ((height l = height r \<or>
+                         height l = 1+height r \<or>
+                         height r = 1+height l) \<and> 
+                         is_bal l \<and> is_bal r)"
 
 
 datatype bal = Just | Left | Right
 
 constdefs
- bal :: "tree => bal"
-"bal t == case t of ET => Just
- | (MKT n l r) => if height l = height r then Just
-                  else if height l < height r then Right else Left"
+  bal :: "tree \<Rightarrow> bal"
+  "bal t \<equiv> case t of ET \<Rightarrow> Just
+                   | (MKT n l r) \<Rightarrow> if height l = height r then Just
+                                    else if height l < height r then Right else Left"
 
 consts
- r_rot,l_rot,lr_rot,rl_rot :: "nat * tree * tree => tree"
+  r_rot  :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
+  l_rot  :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
+  lr_rot :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
+  rl_rot :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
 
 recdef r_rot "{}"
-"r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
+  "r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
 
 recdef l_rot "{}"
-"l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
+  "l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
 
 recdef lr_rot "{}"
-"lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
+  "lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
 
 recdef rl_rot "{}"
-"rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
+  "rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
 
 
 constdefs 
- l_bal :: "nat => tree => tree => tree"
-"l_bal n l r == if bal l = Right 
-                then lr_rot (n, l, r)
-                else r_rot (n, l, r)"
+  l_bal :: "nat \<Rightarrow> tree \<Rightarrow> tree \<Rightarrow> tree"
+  "l_bal n l r \<equiv> if bal l = Right 
+                  then lr_rot (n, l, r)
+                  else r_rot (n, l, r)"
 
- r_bal :: "nat => tree => tree => tree"
-"r_bal n l r == if bal r = Left
-                then rl_rot (n, l, r)
-                else l_rot (n, l, r)"
+  r_bal :: "nat \<Rightarrow> tree \<Rightarrow> tree \<Rightarrow> tree"
+  "r_bal n l r \<equiv> if bal r = Left
+                  then rl_rot (n, l, r)
+                  else l_rot (n, l, r)"
 
 consts
- insert :: "nat => tree => tree"
+  insert :: "nat \<Rightarrow> tree \<Rightarrow> tree"
 primrec
 "insert x ET = MKT x ET ET"
 "insert x (MKT n l r) = 
@@ -86,12 +98,324 @@
     then MKT n l r
     else if x<n
          then let l' = insert x l
-              in if height l' = Suc(Suc(height r))
+              in if height l' = 2+height r
                  then l_bal n l' r
                  else MKT n l' r
          else let r' = insert x r
-              in if height r' = Suc(Suc(height l))
+              in if height r' = 2+height l
                  then r_bal n l r'
                  else MKT n l r')"
 
+
+
+subsection "is-bal"
+
+declare Let_def [simp]
+
+lemma is_bal_lr_rot: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right; is_bal l; is_bal r \<rbrakk>
+  \<Longrightarrow> is_bal (lr_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases l)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t2)
+ apply simp
+apply (simp add: max_def split: split_if_asm)
+apply arith
+done
+
+
+lemma is_bal_r_rot: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right; is_bal l; is_bal r \<rbrakk>
+  \<Longrightarrow> is_bal (r_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases "l")
+ apply simp
+apply (simp add: max_def split: split_if_asm)
+done
+
+
+lemma is_bal_rl_rot: 
+"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left; is_bal l; is_bal r \<rbrakk>
+  \<Longrightarrow> is_bal (rl_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t1)
+ apply (simp add: max_def split: split_if_asm)
+apply (simp add: max_def split: split_if_asm)
+apply arith
+done
+
+
+lemma is_bal_l_rot: 
+"\<lbrakk> height r = Suc(Suc(height l)); bal r \<noteq> Left; is_bal l; is_bal r \<rbrakk>
+  \<Longrightarrow> is_bal (l_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp 
+apply (simp add: max_def split: split_if_asm)
+done
+
+
+text {* Lemmas about height after rotation *}
+
+lemma height_lr_rot:
+"\<lbrakk> bal l = Right; height l = Suc(Suc(height r)) \<rbrakk>
+ \<Longrightarrow> Suc(height (lr_rot (n, l, r))) = height (MKT n l r) "
+apply (unfold bal_def)
+apply (cases l)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t2)
+ apply simp
+apply (simp add: max_def split: split_if_asm)
+done
+
+
+lemma height_r_rot: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right \<rbrakk>
+  \<Longrightarrow> Suc(height (r_rot (n, l, r))) = height (MKT n l r) \<or>
+          height (r_rot (n, l, r)) = height (MKT n l r)"
+apply (unfold bal_def)
+apply (cases l)
+ apply simp 
+apply (simp add: max_def split: split_if_asm)
+done
+
+
+lemma height_l_bal:
+"height l = Suc(Suc(height r))   
+  \<Longrightarrow> Suc(height (l_bal n l r)) = height (MKT n l r) |  
+          height (l_bal n l r)  = height (MKT n l r)"
+apply (unfold l_bal_def)
+apply (cases "bal l = Right")
+ apply (fastsimp dest: height_lr_rot)
+apply (fastsimp dest: height_r_rot)
+done
+
+
+lemma height_rl_rot [rule_format (no_asm)]: 
+"height r = Suc(Suc(height l)) \<longrightarrow> bal r = Left  
+  \<longrightarrow> Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t1)
+ apply simp
+apply (simp add: max_def split: split_if_asm)
+done
+
+
+lemma height_l_rot [rule_format (no_asm)]: 
+"height r = Suc(Suc(height l)) \<longrightarrow> bal r \<noteq> Left  
+ \<longrightarrow> Suc(height (l_rot (n, l, r))) = height (MKT n l r) \<or>  
+          height (l_rot (n, l, r)) = height (MKT n l r)"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply (simp add: max_def)
+done
+
+
+lemma height_r_bal: 
+"height r = Suc(Suc(height l))   
+  \<Longrightarrow> Suc(height (r_bal n l r)) = height (MKT n l r) \<or>  
+          height (r_bal n l r) = height (MKT n l r)"
+apply (unfold r_bal_def)
+apply (cases "bal r = Left")
+ apply (fastsimp dest: height_rl_rot)
+apply (fastsimp dest: height_l_rot)
+done
+
+lemma height_insert [rule_format (no_asm)]: 
+"is_bal t
+  \<longrightarrow> height (insert x t) = height t \<or> height (insert x t) = Suc(height t)"
+apply (induct_tac "t")
+ apply simp
+apply (rename_tac n t1 t2)
+apply (case_tac "x=n")
+ apply simp
+apply (case_tac "x<n")
+ apply (case_tac "height (insert x t1) = Suc (Suc (height t2))")
+  apply (frule_tac n = n in height_l_bal)
+  apply (simp add: max_def)
+  apply fastsimp
+ apply (simp add: max_def)
+ apply fastsimp
+apply (case_tac "height (insert x t2) = Suc (Suc (height t1))")
+ apply (frule_tac n = n in height_r_bal)
+ apply (fastsimp simp add: max_def)
+apply (simp add: max_def)
+apply fastsimp
+done
+
+
+lemma is_bal_insert_left: 
+"\<lbrakk>height (insert x l) \<noteq> Suc(Suc(height r)); is_bal (insert x l); is_bal (MKT n l r)\<rbrakk>  
+  \<Longrightarrow> is_bal (MKT n (insert x l) r)"
+apply (cut_tac x = "x" and t = "l" in height_insert)
+ apply simp
+apply fastsimp
+done
+
+
+lemma is_bal_insert_right: 
+"\<lbrakk> height (insert x r) \<noteq> Suc(Suc(height l)); is_bal (insert x r); is_bal (MKT n l r) \<rbrakk>
+  \<Longrightarrow> is_bal (MKT n l (insert x r))"
+apply (cut_tac x = "x" and t = "r" in height_insert)
+ apply simp
+apply fastsimp
+done
+
+
+lemma is_bal_insert [rule_format (no_asm)]: 
+"is_bal t \<longrightarrow> is_bal(insert x t)"
+apply (induct_tac "t")
+ apply simp
+apply (rename_tac n t1 t2)
+apply (case_tac "x=n")
+ apply simp
+apply (case_tac "x<n")
+ apply (case_tac "height (insert x t1) = Suc (Suc (height t2))")
+  apply (case_tac "bal (insert x t1) = Right")
+   apply (fastsimp intro: is_bal_lr_rot simp add: l_bal_def)
+  apply (fastsimp intro: is_bal_r_rot simp add: l_bal_def)
+ apply clarify
+ apply (frule is_bal_insert_left)
+   apply simp
+  apply assumption
+ apply simp
+apply (case_tac "height (insert x t2) = Suc (Suc (height t1))")
+ apply (case_tac "bal (insert x t2) = Left")
+  apply (fastsimp intro: is_bal_rl_rot simp add: r_bal_def)
+ apply (fastsimp intro: is_bal_l_rot simp add: r_bal_def)
+apply clarify
+apply (frule is_bal_insert_right)
+   apply simp
+  apply assumption
+ apply simp
+done
+
+
+subsection "is-in"
+
+lemma is_in_lr_rot: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right \<rbrakk>
+  \<Longrightarrow> is_in x (lr_rot (n, l, r)) = is_in x (MKT n l r)"
+apply (unfold bal_def)
+apply (cases l)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t2)
+ apply simp 
+apply fastsimp
+done
+
+
+lemma is_in_r_rot: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right \<rbrakk>
+  \<Longrightarrow> is_in x (r_rot (n, l, r)) = is_in x (MKT n l r)"
+apply (unfold bal_def)
+apply (cases l)
+ apply simp
+apply fastsimp
+done
+
+
+lemma is_in_rl_rot:
+"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left \<rbrakk>
+  \<Longrightarrow> is_in x (rl_rot (n, l, r)) = is_in x (MKT n l r)"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t1)
+ apply (simp add: max_def le_def)
+apply fastsimp
+done
+
+
+lemma is_in_l_rot:
+"\<lbrakk> height r = Suc(Suc(height l)); bal r ~= Left \<rbrakk>
+  \<Longrightarrow> is_in x (l_rot (n, l, r)) = is_in x (MKT n l r)"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply fastsimp
+done
+
+
+lemma is_in_insert: 
+"is_in y (insert x t) = (y=x \<or> is_in y t)"
+apply (induct t)
+ apply simp
+apply (simp add: l_bal_def is_in_lr_rot is_in_r_rot r_bal_def 
+                 is_in_rl_rot is_in_l_rot)
+apply blast
+done
+
+
+subsection "is-ord"
+
+lemma is_ord_lr_rot [rule_format (no_asm)]: 
+"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right; is_ord (MKT n l r) \<rbrakk>
+  \<Longrightarrow> is_ord (lr_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases l)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t2)
+ apply simp
+apply simp
+apply (blast intro: less_trans)
+done
+
+
+lemma is_ord_r_rot:
+"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right; is_ord (MKT n l r) \<rbrakk>
+  \<Longrightarrow> is_ord (r_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases l)
+apply (auto intro: less_trans)
+done
+
+
+lemma is_ord_rl_rot: 
+"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left; is_ord (MKT n l r) \<rbrakk>
+  \<Longrightarrow> is_ord (rl_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply (rename_tac t1 t2)
+apply (case_tac t1)
+ apply (simp add: le_def)
+apply simp
+apply (blast intro: less_trans)
+done
+
+
+lemma is_ord_l_rot: 
+"\<lbrakk> height r = Suc(Suc(height l)); bal r \<noteq> Left; is_ord (MKT n l r) \<rbrakk>
+  \<Longrightarrow> is_ord (l_rot (n, l, r))"
+apply (unfold bal_def)
+apply (cases r)
+ apply simp
+apply simp
+apply (blast intro: less_trans)
+done
+
+
+lemma is_ord_insert: 
+"is_ord t \<Longrightarrow> is_ord(insert x t)"
+apply (induct t)
+ apply simp
+apply (cut_tac m = "x" and n = "nat" in less_linear)
+apply (fastsimp simp add: l_bal_def is_ord_lr_rot is_ord_r_rot r_bal_def
+                          is_ord_l_rot is_ord_rl_rot is_in_insert)
+done
+
 end