# HG changeset patch
# User huffman
# Date 1320386674 -3600
# Node ID 04b21922ed68cf9ad780191c125771d9aa097294
# Parent  ede9dc025150bd2aed0ea506b672cf6add7f837a
ex/Tree23.thy: simpler definition of ordered-ness predicate

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 \<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
 
 lemma ord0_add0: "ord0 t \<Longrightarrow> 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. *}