author | bulwahn |
Tue, 10 Jan 2012 15:48:10 +0100 | |
changeset 46171 | 19f68d7671f0 |
parent 43815 | 4f6e2965d821 |
child 49190 | e1e1d427747d |
permissions | -rw-r--r-- |
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 |
|
37765 | 15 |
"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 |
|
37765 | 18 |
"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 |
||
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
37765
diff
changeset
|
61 |
instantiation option :: (order) bot |
30662 | 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 |