# HG changeset patch
# User nipkow
# Date 957523893 -7200
# Node ID b55e2354d71e873fd70730edc7e1dbf5c074652c
# Parent  4a3612f30865071d47465f56c845230c7e96c188
Added AVL

diff -r 4a3612f30865 -r b55e2354d71e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 04 18:40:57 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri May 05 12:51:33 2000 +0200
@@ -413,9 +413,9 @@
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
-$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \
+$(LOG)/HOL-ex.gz: $(OUT)/HOL  ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
   ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
-  ex/NatSum.thy ex/Primes.ML ex/Primes.thy \
+  ex/NatSum.thy ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
   ex/Factorization.ML ex/Factorization.thy \
   ex/Primrec.ML ex/Primrec.thy \
   ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
diff -r 4a3612f30865 -r b55e2354d71e src/HOL/ex/AVL.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/AVL.ML	Fri May 05 12:51:33 2000 +0200
@@ -0,0 +1,307 @@
+(*  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);
+by (arith_tac 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 (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);
+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 (forward_tac [isbal_insert_left] 1);
+   by (Asm_full_simp_tac 1); 
+  ba 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 (forward_tac [isbal_insert_right] 1);
+   by (Asm_full_simp_tac 1); 
+  ba 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 4a3612f30865 -r b55e2354d71e src/HOL/ex/AVL.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/AVL.thy	Fri May 05 12:51:33 2000 +0200
@@ -0,0 +1,97 @@
+(*  Title:      HOL/ex/AVL.thy
+    ID:         $Id$
+    Author:     Cornelia Pusch and Tobias Nipkow
+    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 +
+
+datatype tree = ET | MKT nat tree tree
+
+consts
+ height :: "tree => nat"
+ isin   :: "nat => tree => bool"
+ isord  :: "tree => bool"
+ isbal  :: "tree => bool"
+
+primrec
+"height ET = 0"
+"height (MKT n l r) = Suc(max (height l) (height r))"
+
+primrec
+"isin k ET = False"
+"isin k (MKT n l r) = (k=n | isin k l | isin 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)"
+
+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)"
+
+
+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"
+
+consts
+ r_rot,l_rot,lr_rot,rl_rot :: "nat * tree * tree => tree"
+
+recdef r_rot "{}"
+"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"
+
+recdef lr_rot "{}"
+"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)"
+
+
+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)"
+
+ 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)"
+
+consts
+ insert :: "nat => tree => tree"
+primrec
+"insert x ET = MKT x ET ET"
+"insert x (MKT n l r) = 
+   (if x=n
+    then MKT n l r
+    else if x<n
+         then let l' = insert x l
+              in if height l' = Suc(Suc(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))
+                 then r_bal n l r'
+                 else MKT n l r')"
+
+end
diff -r 4a3612f30865 -r b55e2354d71e src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu May 04 18:40:57 2000 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri May 05 12:51:33 2000 +0200
@@ -23,6 +23,7 @@
 time_use     "mesontest.ML";
 time_use     "mesontest2.ML";
 time_use_thy "BT";
+time_use_thy "AVL";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "Puzzle";