26241

1 
(* Title: HOL/Library/Option_ord.thy


2 
Author: Florian Haftmann, TU Muenchen


3 
*)


4 

26263

5 
header {* Canonical order on option type *}

26241

6 


7 
theory Option_ord

30662

8 
imports Option Main

26241

9 
begin


10 

30662

11 
instantiation option :: (preorder) preorder

26241

12 
begin


13 


14 
definition less_eq_option where

28562

15 
[code del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True  Some x \<Rightarrow> (case y of None \<Rightarrow> False  Some y \<Rightarrow> x \<le> y))"

26241

16 


17 
definition less_option where

28562

18 
[code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False  Some y \<Rightarrow> (case x of None \<Rightarrow> True  Some x \<Rightarrow> x < y))"

26241

19 

26258

20 
lemma less_eq_option_None [simp]: "None \<le> x"

26241

21 
by (simp add: less_eq_option_def)


22 

26258

23 
lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"

26241

24 
by simp


25 

26258

26 
lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"

26241

27 
by (cases x) (simp_all add: less_eq_option_def)


28 

26258

29 
lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"

26241

30 
by (simp add: less_eq_option_def)


31 

26258

32 
lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"

26241

33 
by (simp add: less_eq_option_def)


34 

26258

35 
lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"

26241

36 
by (simp add: less_option_def)


37 

26258

38 
lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"

26241

39 
by (cases x) (simp_all add: less_option_def)


40 

26258

41 
lemma less_option_None_Some [simp]: "None < Some x"

26241

42 
by (simp add: less_option_def)


43 

26258

44 
lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"

26241

45 
by simp


46 

26258

47 
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"

26241

48 
by (simp add: less_option_def)


49 

30662

50 
instance proof


51 
qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)

26241

52 


53 
end


54 

30662

55 
instance option :: (order) order proof


56 
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)


57 


58 
instance option :: (linorder) linorder proof


59 
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)


60 


61 
instantiation option :: (preorder) bot


62 
begin


63 


64 
definition "bot = None"


65 


66 
instance proof


67 
qed (simp add: bot_option_def)


68 


69 
end


70 


71 
instantiation option :: (top) top


72 
begin


73 


74 
definition "top = Some top"


75 


76 
instance proof


77 
qed (simp add: top_option_def less_eq_option_def split: option.split)

26241

78 


79 
end

30662

80 


81 
instance option :: (wellorder) wellorder proof


82 
fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"


83 
assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"


84 
have "P None" by (rule H) simp


85 
then have P_Some [case_names Some]:


86 
"\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"


87 
proof 


88 
fix z


89 
assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"


90 
with `P None` show "P z" by (cases z) simp_all


91 
qed


92 
show "P z" proof (cases z rule: P_Some)


93 
case (Some w)


94 
show "(P o Some) w" proof (induct rule: less_induct)


95 
case (less x)


96 
have "P (Some x)" proof (rule H)


97 
fix y :: "'a option"


98 
assume "y < Some x"


99 
show "P y" proof (cases y rule: P_Some)


100 
case (Some v) with `y < Some x` have "v < x" by simp


101 
with less show "(P o Some) v" .


102 
qed


103 
qed


104 
then show ?case by simp


105 
qed


106 
qed


107 
qed


108 


109 
end
