--- 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\
--- 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";
--- 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