src/HOL/Library/Option_ord.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 56166 9a241bc276cd child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
1 (*  Title:      HOL/Library/Option_ord.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 header {* Canonical order on option type *}
7 theory Option_ord
8 imports Option Main
9 begin
11 notation
12   bot ("\<bottom>") and
13   top ("\<top>") and
14   inf  (infixl "\<sqinter>" 70) and
15   sup  (infixl "\<squnion>" 65) and
16   Inf  ("\<Sqinter>_" [900] 900) and
17   Sup  ("\<Squnion>_" [900] 900)
19 syntax (xsymbols)
20   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
21   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
22   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
23   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
26 instantiation option :: (preorder) preorder
27 begin
29 definition less_eq_option where
30   "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))"
32 definition less_option where
33   "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
35 lemma less_eq_option_None [simp]: "None \<le> x"
38 lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"
39   by simp
41 lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"
42   by (cases x) (simp_all add: less_eq_option_def)
44 lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"
47 lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"
50 lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"
53 lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"
54   by (cases x) (simp_all add: less_option_def)
56 lemma less_option_None_Some [simp]: "None < Some x"
59 lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"
60   by simp
62 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
65 instance proof
66 qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
68 end
70 instance option :: (order) order proof
71 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
73 instance option :: (linorder) linorder proof
74 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
76 instantiation option :: (order) order_bot
77 begin
79 definition bot_option where
80   "\<bottom> = None"
82 instance proof
85 end
87 instantiation option :: (order_top) order_top
88 begin
90 definition top_option where
91   "\<top> = Some \<top>"
93 instance proof
94 qed (simp add: top_option_def less_eq_option_def split: option.split)
96 end
98 instance option :: (wellorder) wellorder proof
99   fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
100   assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
101   have "P None" by (rule H) simp
102   then have P_Some [case_names Some]:
103     "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
104   proof -
105     fix z
106     assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
107     with `P None` show "P z" by (cases z) simp_all
108   qed
109   show "P z" proof (cases z rule: P_Some)
110     case (Some w)
111     show "(P o Some) w" proof (induct rule: less_induct)
112       case (less x)
113       have "P (Some x)" proof (rule H)
114         fix y :: "'a option"
115         assume "y < Some x"
116         show "P y" proof (cases y rule: P_Some)
117           case (Some v) with `y < Some x` have "v < x" by simp
118           with less show "(P o Some) v" .
119         qed
120       qed
121       then show ?case by simp
122     qed
123   qed
124 qed
126 instantiation option :: (inf) inf
127 begin
129 definition inf_option where
130   "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
132 lemma inf_None_1 [simp, code]:
133   "None \<sqinter> y = None"
136 lemma inf_None_2 [simp, code]:
137   "x \<sqinter> None = None"
138   by (cases x) (simp_all add: inf_option_def)
140 lemma inf_Some [simp, code]:
141   "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
144 instance ..
146 end
148 instantiation option :: (sup) sup
149 begin
151 definition sup_option where
152   "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
154 lemma sup_None_1 [simp, code]:
155   "None \<squnion> y = y"
158 lemma sup_None_2 [simp, code]:
159   "x \<squnion> None = x"
160   by (cases x) (simp_all add: sup_option_def)
162 lemma sup_Some [simp, code]:
163   "Some x \<squnion> Some y = Some (x \<squnion> y)"
166 instance ..
168 end
170 instantiation option :: (semilattice_inf) semilattice_inf
171 begin
173 instance proof
174   fix x y z :: "'a option"
175   show "x \<sqinter> y \<le> x"
176     by - (cases x, simp_all, cases y, simp_all)
177   show "x \<sqinter> y \<le> y"
178     by - (cases x, simp_all, cases y, simp_all)
179   show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
180     by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
181 qed
183 end
185 instantiation option :: (semilattice_sup) semilattice_sup
186 begin
188 instance proof
189   fix x y z :: "'a option"
190   show "x \<le> x \<squnion> y"
191     by - (cases x, simp_all, cases y, simp_all)
192   show "y \<le> x \<squnion> y"
193     by - (cases x, simp_all, cases y, simp_all)
194   fix x y z :: "'a option"
195   show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
196     by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
197 qed
199 end
201 instance option :: (lattice) lattice ..
203 instance option :: (lattice) bounded_lattice_bot ..
205 instance option :: (bounded_lattice_top) bounded_lattice_top ..
207 instance option :: (bounded_lattice_top) bounded_lattice ..
209 instance option :: (distrib_lattice) distrib_lattice
210 proof
211   fix x y z :: "'a option"
212   show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
213     by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
214 qed
216 instantiation option :: (complete_lattice) complete_lattice
217 begin
219 definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
220   "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
222 lemma None_in_Inf [simp]:
223   "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
226 definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
227   "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
229 lemma empty_Sup [simp]:
230   "\<Squnion>{} = None"
233 lemma singleton_None_Sup [simp]:
234   "\<Squnion>{None} = None"
237 instance proof
238   fix x :: "'a option" and A
239   assume "x \<in> A"
240   then show "\<Sqinter>A \<le> x"
241     by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
242 next
243   fix z :: "'a option" and A
244   assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
245   show "z \<le> \<Sqinter>A"
246   proof (cases z)
247     case None then show ?thesis by simp
248   next
249     case (Some y)
250     show ?thesis
251       by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
252   qed
253 next
254   fix x :: "'a option" and A
255   assume "x \<in> A"
256   then show "x \<le> \<Squnion>A"
257     by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
258 next
259   fix z :: "'a option" and A
260   assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
261   show "\<Squnion>A \<le> z "
262   proof (cases z)
263     case None
264     with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
265     then have "A = {} \<or> A = {None}" by blast
266     then show ?thesis by (simp add: Sup_option_def)
267   next
268     case (Some y)
269     from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
270     with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
272     then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
273     with Some show ?thesis by (simp add: Sup_option_def)
274   qed
275 next
276   show "\<Squnion>{} = (\<bottom>::'a option)"
277   by (auto simp: bot_option_def)
278 next
279   show "\<Sqinter>{} = (\<top>::'a option)"
280   by (auto simp: top_option_def Inf_option_def)
281 qed
283 end
285 lemma Some_Inf:
286   "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
287   by (auto simp add: Inf_option_def)
289 lemma Some_Sup:
290   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
291   by (auto simp add: Sup_option_def)
293 lemma Some_INF:
294   "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
295   using Some_Inf [of "f ` A"] by (simp add: comp_def)
297 lemma Some_SUP:
298   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
299   using Some_Sup [of "f ` A"] by (simp add: comp_def)
301 instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
302 begin
304 instance proof
305   fix a :: "'a option" and B
306   show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
307   proof (cases a)
308     case None
309     then show ?thesis by (simp add: INF_def)
310   next
311     case (Some c)
312     show ?thesis
313     proof (cases "None \<in> B")
314       case True
315       then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
316         by (auto intro!: antisym INF_lower2 INF_greatest)
317       with True Some show ?thesis by simp
318     next
319       case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
320       from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
321       then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
322         by (simp add: Some_INF Some_Inf comp_def)
323       with Some B show ?thesis by (simp add: Some_image_these_eq)
324     qed
325   qed
326   show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
327   proof (cases a)
328     case None
329     then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
330   next
331     case (Some c)
332     show ?thesis
333     proof (cases "B = {} \<or> B = {None}")
334       case True
335       then show ?thesis by auto
336     next
337       have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
338         by auto
339       then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
340         and SUP_B: "\<And>f. (\<Squnion>x \<in> B. f x) = (\<Squnion>x \<in> {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}. f x)"
341         by simp_all
342       have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
343         by (simp add: bot_option_def [symmetric])
344       have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
345         by (simp add: bot_option_def [symmetric])
346       case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
347       moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
348         by simp
349       ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
350         by (simp add: Some_SUP Some_Sup comp_def)
351       with Some show ?thesis
352         by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
353     qed
354   qed
355 qed
357 end
359 instantiation option :: (complete_linorder) complete_linorder
360 begin
362 instance ..
364 end
367 no_notation
368   bot ("\<bottom>") and
369   top ("\<top>") and
370   inf  (infixl "\<sqinter>" 70) and
371   sup  (infixl "\<squnion>" 65) and
372   Inf  ("\<Sqinter>_" [900] 900) and
373   Sup  ("\<Squnion>_" [900] 900)
375 no_syntax (xsymbols)
376   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
377   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
378   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
379   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
381 end