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