author huffman Fri, 04 Nov 2011 07:04:34 +0100 changeset 45333 04b21922ed68 parent 45332 ede9dc025150 child 45334 3f74e041e05c
ex/Tree23.thy: simpler definition of ordered-ness predicate
 src/HOL/ex/Tree23.thy file | annotate | diff | comparison | revisions
```--- 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 \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"

-(* yes, this is rather slow *)
-fun ord0 :: "'a tree23 \<Rightarrow> bool"
-and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
-and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
-and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> 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 \<Rightarrow> key option \<Rightarrow> bool" where
"opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> 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 \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
+primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> 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 \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
-    | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
-by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
+definition ord0 :: "'a tree23 \<Rightarrow> bool" where
+  "ord0 t = ord' None t None"

fun height :: "'a tree23 \<Rightarrow> nat" where
"height Empty = 0" |
@@ -313,7 +291,7 @@
done