diff -r ede9dc025150 -r 04b21922ed68 src/HOL/ex/Tree23.thy --- a/src/HOL/ex/Tree23.thy Thu Nov 03 17:40:50 2011 +0100 +++ b/src/HOL/ex/Tree23.thy Fri Nov 04 07:04:34 2011 +0100 @@ -137,27 +137,7 @@ "del0 k t = (case del (Some k) t of None \ t | Some(_,(_,t')) \ t')" -(* yes, this is rather slow *) -fun ord0 :: "'a tree23 \ bool" -and ordl :: "key \ 'a tree23 \ bool" -and ordr :: "'a tree23 \ key \ bool" -and ordlr :: "key \ 'a tree23 \ key \ bool" -where -"ord0 Empty = True" | -"ord0 (Branch2 l p r) = (ordr l (fst p) & ordl (fst p) r)" | -"ord0 (Branch3 l p m q r) = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | - -"ordl _ Empty = True" | -"ordl x (Branch2 l p r) = (ordlr x l (fst p) & ordl (fst p) r)" | -"ordl x (Branch3 l p m q r) = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | - -"ordr Empty _ = True" | -"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" | -"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" | - -"ordlr x Empty y = (x < y)" | -"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)" +text {* Specifying correctness *} definition opt_less :: "key option \ key option \ bool" where "opt_less x y = (case x of None \ True | Some a \ (case y of None \ True | Some b \ a < b))" @@ -168,15 +148,13 @@ "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 \ 'a tree23 \ key option \ bool" where +primrec ord' :: "key option \ 'a tree23 \ key option \ 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 \ (case y of None \ ord0 t | Some y' \ ordr t y') - | Some x' \ (case y of None \ ordl x' t | Some y' \ ordlr x' t y'))" -by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split) +definition ord0 :: "'a tree23 \ bool" where + "ord0 t = ord' None t None" fun height :: "'a tree23 \ nat" where "height Empty = 0" | @@ -313,7 +291,7 @@ done lemma ord0_add0: "ord0 t \ ord0 (add0 k y t)" -using ord'_add0 [of None t None k y] by (simp add: ord') + by (simp add: ord0_def ord'_add0) text {* The @{term "del"} function preserves balance. *}