ex/Tree23.thy: simpler definition of ordered-ness predicate
authorhuffman
Fri Nov 04 07:04:34 2011 +0100 (2011-11-04)
changeset 4533304b21922ed68
parent 45332 ede9dc025150
child 45334 3f74e041e05c
ex/Tree23.thy: simpler definition of ordered-ness predicate
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/ex/Tree23.thy	Thu Nov 03 17:40:50 2011 +0100
     1.2 +++ b/src/HOL/ex/Tree23.thy	Fri Nov 04 07:04:34 2011 +0100
     1.3 @@ -137,27 +137,7 @@
     1.4  "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
     1.5  
     1.6  
     1.7 -(* yes, this is rather slow *)
     1.8 -fun ord0 :: "'a tree23 \<Rightarrow> bool"
     1.9 -and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
    1.10 -and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
    1.11 -and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool"
    1.12 -where
    1.13 -"ord0 Empty = True" |
    1.14 -"ord0 (Branch2 l p r)  = (ordr l (fst p) & ordl (fst p) r)" |
    1.15 -"ord0 (Branch3 l p m q r)  = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
    1.16 -
    1.17 -"ordl _ Empty = True" |
    1.18 -"ordl x (Branch2 l p r)  = (ordlr x l (fst p) & ordl (fst p) r)" |
    1.19 -"ordl x (Branch3 l p m q r)  = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
    1.20 -
    1.21 -"ordr Empty _ = True" |
    1.22 -"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" |
    1.23 -"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" |
    1.24 -
    1.25 -"ordlr x Empty y = (x < y)" |
    1.26 -"ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
    1.27 -"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)"
    1.28 +text {* Specifying correctness *}
    1.29  
    1.30  definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
    1.31    "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
    1.32 @@ -168,15 +148,13 @@
    1.33    "opt_less (Some a) (Some b) = (a < b)"
    1.34  unfolding opt_less_def by (auto simp add: ord_def split: option.split)
    1.35  
    1.36 -fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
    1.37 +primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
    1.38  "ord' x Empty y = opt_less x y" |
    1.39  "ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
    1.40  "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)"
    1.41  
    1.42 -lemma ord':
    1.43 -  "ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
    1.44 -    | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
    1.45 -by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
    1.46 +definition ord0 :: "'a tree23 \<Rightarrow> bool" where
    1.47 +  "ord0 t = ord' None t None"
    1.48  
    1.49  fun height :: "'a tree23 \<Rightarrow> nat" where
    1.50  "height Empty = 0" |
    1.51 @@ -313,7 +291,7 @@
    1.52  done
    1.53  
    1.54  lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
    1.55 -using ord'_add0 [of None t None k y] by (simp add: ord')
    1.56 +  by (simp add: ord0_def ord'_add0)
    1.57  
    1.58  text {* The @{term "del"} function preserves balance. *}
    1.59