author  Manuel Eberl <eberlm@in.tum.de> 
Mon, 26 Mar 2018 16:14:16 +0200  
changeset 67951  655aa11359dc 
parent 67829  2a6ef5ba4822 
child 68980  5717fbc55521 
permissions  rwrr 
26241  1 
(* Title: HOL/Library/Option_ord.thy 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

60500  5 
section \<open>Canonical order on option type\<close> 
26241  6 

7 
theory Option_ord 

67006  8 
imports Main 
26241  9 
begin 
10 

49190  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) 

18 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
60679
diff
changeset

19 
syntax 
49190  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) 

24 

25 

30662  26 
instantiation option :: (preorder) preorder 
26241  27 
begin 
28 

29 
definition less_eq_option where 

37765  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))" 
26241  31 

32 
definition less_option where 

37765  33 
"x < y \<longleftrightarrow> (case y of None \<Rightarrow> False  Some y \<Rightarrow> (case x of None \<Rightarrow> True  Some x \<Rightarrow> x < y))" 
26241  34 

26258  35 
lemma less_eq_option_None [simp]: "None \<le> x" 
26241  36 
by (simp add: less_eq_option_def) 
37 

26258  38 
lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True" 
26241  39 
by simp 
40 

26258  41 
lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None" 
26241  42 
by (cases x) (simp_all add: less_eq_option_def) 
43 

26258  44 
lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False" 
26241  45 
by (simp add: less_eq_option_def) 
46 

26258  47 
lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y" 
26241  48 
by (simp add: less_eq_option_def) 
49 

26258  50 
lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False" 
26241  51 
by (simp add: less_option_def) 
52 

26258  53 
lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z" 
26241  54 
by (cases x) (simp_all add: less_option_def) 
55 

26258  56 
lemma less_option_None_Some [simp]: "None < Some x" 
26241  57 
by (simp add: less_option_def) 
58 

26258  59 
lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True" 
26241  60 
by simp 
61 

26258  62 
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y" 
26241  63 
by (simp add: less_option_def) 
64 

60679  65 
instance 
66 
by standard 

67 
(auto simp add: less_eq_option_def less_option_def less_le_not_le 

68 
elim: order_trans split: option.splits) 

26241  69 

60679  70 
end 
30662  71 

60679  72 
instance option :: (order) order 
73 
by standard (auto simp add: less_eq_option_def less_option_def split: option.splits) 

74 

75 
instance option :: (linorder) linorder 

76 
by standard (auto simp add: less_eq_option_def less_option_def split: option.splits) 

30662  77 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
49190
diff
changeset

78 
instantiation option :: (order) order_bot 
30662  79 
begin 
80 

60679  81 
definition bot_option where "\<bottom> = None" 
30662  82 

60679  83 
instance 
84 
by standard (simp add: bot_option_def) 

30662  85 

86 
end 

87 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
49190
diff
changeset

88 
instantiation option :: (order_top) order_top 
30662  89 
begin 
90 

60679  91 
definition top_option where "\<top> = Some \<top>" 
30662  92 

60679  93 
instance 
94 
by standard (simp add: top_option_def less_eq_option_def split: option.split) 

26241  95 

96 
end 

30662  97 

60679  98 
instance option :: (wellorder) wellorder 
99 
proof 

100 
fix P :: "'a option \<Rightarrow> bool" 

101 
fix z :: "'a option" 

30662  102 
assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" 
103 
have "P None" by (rule H) simp 

67091  104 
then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P \<circ> Some) x" for z 
60679  105 
using \<open>P None\<close> that by (cases z) simp_all 
106 
show "P z" 

107 
proof (cases z rule: P_Some) 

30662  108 
case (Some w) 
67091  109 
show "(P \<circ> Some) w" 
60679  110 
proof (induct rule: less_induct) 
30662  111 
case (less x) 
60679  112 
have "P (Some x)" 
113 
proof (rule H) 

30662  114 
fix y :: "'a option" 
115 
assume "y < Some x" 

60679  116 
show "P y" 
117 
proof (cases y rule: P_Some) 

118 
case (Some v) 

119 
with \<open>y < Some x\<close> have "v < x" by simp 

67091  120 
with less show "(P \<circ> Some) v" . 
30662  121 
qed 
122 
qed 

123 
then show ?case by simp 

124 
qed 

125 
qed 

126 
qed 

127 

49190  128 
instantiation option :: (inf) inf 
129 
begin 

130 

131 
definition inf_option where 

132 
"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)))" 

133 

60679  134 
lemma inf_None_1 [simp, code]: "None \<sqinter> y = None" 
49190  135 
by (simp add: inf_option_def) 
136 

60679  137 
lemma inf_None_2 [simp, code]: "x \<sqinter> None = None" 
49190  138 
by (cases x) (simp_all add: inf_option_def) 
139 

60679  140 
lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)" 
49190  141 
by (simp add: inf_option_def) 
142 

143 
instance .. 

144 

30662  145 
end 
49190  146 

147 
instantiation option :: (sup) sup 

148 
begin 

149 

150 
definition sup_option where 

151 
"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)))" 

152 

60679  153 
lemma sup_None_1 [simp, code]: "None \<squnion> y = y" 
49190  154 
by (simp add: sup_option_def) 
155 

60679  156 
lemma sup_None_2 [simp, code]: "x \<squnion> None = x" 
49190  157 
by (cases x) (simp_all add: sup_option_def) 
158 

60679  159 
lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)" 
49190  160 
by (simp add: sup_option_def) 
161 

162 
instance .. 

163 

164 
end 

165 

60679  166 
instance option :: (semilattice_inf) semilattice_inf 
167 
proof 

49190  168 
fix x y z :: "'a option" 
169 
show "x \<sqinter> y \<le> x" 

60679  170 
by (cases x, simp_all, cases y, simp_all) 
49190  171 
show "x \<sqinter> y \<le> y" 
60679  172 
by (cases x, simp_all, cases y, simp_all) 
49190  173 
show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z" 
60679  174 
by (cases x, simp_all, cases y, simp_all, cases z, simp_all) 
49190  175 
qed 
176 

60679  177 
instance option :: (semilattice_sup) semilattice_sup 
178 
proof 

49190  179 
fix x y z :: "'a option" 
180 
show "x \<le> x \<squnion> y" 

60679  181 
by (cases x, simp_all, cases y, simp_all) 
49190  182 
show "y \<le> x \<squnion> y" 
60679  183 
by (cases x, simp_all, cases y, simp_all) 
49190  184 
fix x y z :: "'a option" 
185 
show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x" 

60679  186 
by (cases y, simp_all, cases z, simp_all, cases x, simp_all) 
49190  187 
qed 
188 

189 
instance option :: (lattice) lattice .. 

190 

191 
instance option :: (lattice) bounded_lattice_bot .. 

192 

193 
instance option :: (bounded_lattice_top) bounded_lattice_top .. 

194 

195 
instance option :: (bounded_lattice_top) bounded_lattice .. 

196 

197 
instance option :: (distrib_lattice) distrib_lattice 

198 
proof 

199 
fix x y z :: "'a option" 

200 
show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

60679  201 
by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute) 
202 
qed 

49190  203 

204 
instantiation option :: (complete_lattice) complete_lattice 

205 
begin 

206 

207 
definition Inf_option :: "'a option set \<Rightarrow> 'a option" where 

208 
"\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))" 

209 

60679  210 
lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None" 
49190  211 
by (simp add: Inf_option_def) 
212 

213 
definition Sup_option :: "'a option set \<Rightarrow> 'a option" where 

214 
"\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))" 

215 

60679  216 
lemma empty_Sup [simp]: "\<Squnion>{} = None" 
49190  217 
by (simp add: Sup_option_def) 
218 

60679  219 
lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None" 
49190  220 
by (simp add: Sup_option_def) 
221 

60679  222 
instance 
223 
proof 

49190  224 
fix x :: "'a option" and A 
225 
assume "x \<in> A" 

226 
then show "\<Sqinter>A \<le> x" 

227 
by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower) 

228 
next 

229 
fix z :: "'a option" and A 

230 
assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" 

231 
show "z \<le> \<Sqinter>A" 

232 
proof (cases z) 

233 
case None then show ?thesis by simp 

234 
next 

235 
case (Some y) 

236 
show ?thesis 

237 
by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *) 

238 
qed 

239 
next 

240 
fix x :: "'a option" and A 

241 
assume "x \<in> A" 

242 
then show "x \<le> \<Squnion>A" 

243 
by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper) 

244 
next 

245 
fix z :: "'a option" and A 

246 
assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" 

247 
show "\<Squnion>A \<le> z " 

248 
proof (cases z) 

249 
case None 

250 
with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None) 

251 
then have "A = {} \<or> A = {None}" by blast 

252 
then show ?thesis by (simp add: Sup_option_def) 

253 
next 

254 
case (Some y) 

255 
from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" . 

256 
with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y" 

257 
by (simp add: in_these_eq) 

258 
then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least) 

259 
with Some show ?thesis by (simp add: Sup_option_def) 

260 
qed 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
49190
diff
changeset

261 
next 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
49190
diff
changeset

262 
show "\<Squnion>{} = (\<bottom>::'a option)" 
60679  263 
by (auto simp: bot_option_def) 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
49190
diff
changeset

264 
show "\<Sqinter>{} = (\<top>::'a option)" 
60679  265 
by (auto simp: top_option_def Inf_option_def) 
49190  266 
qed 
267 

268 
end 

269 

270 
lemma Some_Inf: 

271 
"Some (\<Sqinter>A) = \<Sqinter>(Some ` A)" 

272 
by (auto simp add: Inf_option_def) 

273 

274 
lemma Some_Sup: 

275 
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)" 

276 
by (auto simp add: Sup_option_def) 

277 

278 
lemma Some_INF: 

279 
"Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))" 

56166  280 
using Some_Inf [of "f ` A"] by (simp add: comp_def) 
49190  281 

282 
lemma Some_SUP: 

283 
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))" 

56166  284 
using Some_Sup [of "f ` A"] by (simp add: comp_def) 
49190  285 

67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

286 
lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A f. \<forall>Y\<in>A. f Y \<in> Y} Inf" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

287 
proof (cases "{} \<in> A") 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

288 
case True 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

289 
then show ?thesis 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

290 
by (rule INF_lower2, simp_all) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

291 
next 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

292 
case False 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

293 
from this have X: "{} \<notin> A" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

294 
by simp 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

295 
then show ?thesis 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

296 
proof (cases "{None} \<in> A") 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

297 
case True 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

298 
then show ?thesis 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

299 
by (rule INF_lower2, simp_all) 
49190  300 
next 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

301 
case False 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

302 

655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

303 
{fix y 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

304 
assume A: "y \<in> A" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

305 
have "Sup (y  {None}) = Sup y" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

306 
by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

307 
from A and this have "(\<exists>z. y  {None} = z  {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y  {None})" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

308 
by auto 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

309 
} 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

310 
from this have A: "Sup ` A = (Sup ` {y  {None}  y. y\<in>A})" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

311 
by (auto simp add: image_def) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

312 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

313 
have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

314 
= {y. \<exists>x\<in>ya  {None}. y = the x} \<and> ya \<in> A" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

315 
by (rule exI, auto) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

316 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

317 
have [simp]: "\<And>y. y \<in> A \<Longrightarrow> 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

318 
(\<exists>ya. y  {None} = ya  {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y  {None}. ya = the x} 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

319 
= \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

320 
apply (safe, blast) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

321 
by (rule arg_cong [of _ _ Sup], auto) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

322 
{fix y 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

323 
assume [simp]: "y \<in> A" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

324 
have "\<exists>x. (\<exists>y. x = {ya. \<exists>x\<in>y  {None}. ya = the x} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} = \<Squnion>x" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

325 
and "\<exists>x. (\<exists>y. x = y  {None} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y  {None}. ya = the x} = \<Squnion>{y. \<exists>xa. xa \<in> x \<and> (\<exists>y. xa = Some y) \<and> y = the xa}" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

326 
apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

327 
by (rule exI [of _ "y  {None}"], simp) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

328 
} 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

329 
from this have C: "(\<lambda>x. (\<Squnion>Option.these x)) ` {y  {None} y. y \<in> A} = (Sup ` {the ` (y  {None}) y. y \<in> A})" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

330 
by (simp add: image_def Option.these_def, safe, simp_all) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

331 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

332 
have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

333 
by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

334 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

335 
define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y  {None}))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

336 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

337 
have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y  {None}" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

338 
by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

339 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

340 
have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y  {None})" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

341 
by (metis F_def G empty_iff some_in_eq) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

342 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

343 
have "Some \<bottom> \<le> Inf (F ` A)" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

344 
by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

345 
less_eq_option_Some singletonI) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

346 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

347 
from this have "Inf (F ` A) \<noteq> None" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

348 
by (cases "\<Sqinter>x\<in>A. F x", simp_all) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

349 

655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

350 
from this have "Inf (F ` A) \<noteq> None \<and> Inf (F ` A) \<in> Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y}" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

351 
using F by auto 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

352 

67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

353 
from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y}" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

354 
by blast 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

355 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

356 
from this have E:" Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

357 
by blast 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

358 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

359 
have [simp]: "((\<Squnion>x\<in>{f ` A f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

360 
by (metis (no_types, lifting) E Sup_option_def \<open>\<exists>x. x \<noteq> None \<and> x \<in> Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y}\<close> 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

361 
ex_in_conv option.simps(3)) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

362 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

363 
have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y  {None} y. y \<in> A}) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

364 
= ((\<lambda>x. (\<Squnion> Option.these x)) ` {y  {None} y. y \<in> A})" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

365 
by (metis image_image these_image_Some_eq) 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

366 
{ 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

367 
fix f 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

368 
assume A: "\<And> Y . (\<exists>y. Y = the ` (y  {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y" 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

369 

67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

370 
have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa  {None}. y = the a} = f (the ` (xa  {None}))" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

371 
by (simp add: image_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

372 
from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x\<in>A. f {y. \<exists>a\<in>xa  {None}. y = the a} = f (the ` (x  {None}))" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

373 
by blast 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

374 
have "\<And>xa. xa \<in> A \<Longrightarrow> f (the ` (xa  {None})) = f {y. \<exists>a \<in> xa  {None}. y = the a} \<and> xa \<in> A" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

375 
by (simp add: image_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

376 
from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x. f (the ` (xa  {None})) = f {y. \<exists>a\<in>x  {None}. y = the a} \<and> x \<in> A" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

377 
by blast 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

378 

67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

379 
{ 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

380 
fix Y 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

381 
have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y  {None}))) \<in> Y" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

382 
using A [of "the ` (Y  {None})"] apply (simp add: image_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

383 
using option.collapse by fastforce 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

384 
} 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

385 
from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y  {None}))) \<in> Y" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

386 
by blast 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

387 
have [simp]: "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x  {None}. y = the x})) = \<Sqinter>{Some (f {y. \<exists>a\<in>x  {None}. y = the a}) x. x \<in> A}" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

388 
by (simp add: Setcompr_eq_image) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

389 

655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

390 
have [simp]: "\<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> \<Sqinter>{Some (f {y. \<exists>a\<in>x  {None}. y = the a}) x. x \<in> A} = \<Sqinter>x" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

391 
apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x  {None}. y = the a})  x . x\<in> A}"], safe) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

392 
by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y  {None})))) "], safe, simp_all) 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

393 

67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

394 
{ 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

395 
fix xb 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

396 
have "xb \<in> A \<Longrightarrow> (\<Sqinter>x\<in>{{ya. \<exists>x\<in>y  {None}. ya = the x} y. y \<in> A}. f x) \<le> f {y. \<exists>x\<in>xb  {None}. y = the x}" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

397 
apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb  {None}. y = the x}"]) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

398 
by blast+ 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

399 
} 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

400 
from this have [simp]: "(\<Sqinter>x\<in>{the ` (y  {None}) y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y  {None}))))" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

401 
apply (simp add: Inf_option_def image_def Option.these_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

402 
by (rule Inf_greatest, clarsimp) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

403 

655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

404 
have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y  {None})))) \<in> Option.these (Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y})" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

405 
apply (simp add: Option.these_def image_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

406 
apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x  {None}. y = the x}))"], simp) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

407 
by (simp add: Inf_option_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

408 

655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

409 
have "(\<Sqinter>x\<in>{the ` (y  {None}) y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y})" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

410 
by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y  {None})) )) ` A))"], simp_all) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

411 
} 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

412 
from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y  {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow> 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

413 
(\<Sqinter>x\<in>{the ` (y  {None}) y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y})" 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

414 
by blast 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

415 

67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

416 

67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

417 
have [simp]: "\<And> x . x\<in>{y  {None} y. y \<in> A} \<Longrightarrow> x \<noteq> {} \<and> x \<noteq> {None}" 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

418 
using F by fastforce 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

419 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

420 
have "(Inf (Sup `A)) = (Inf (Sup ` {y  {None}  y. y\<in>A}))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

421 
by (subst A, simp) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

422 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

423 
also have "... = (\<Sqinter>x\<in>{y  {None} y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

424 
by (simp add: Sup_option_def) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

425 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

426 
also have "... = (\<Sqinter>x\<in>{y  {None} y. y \<in> A}. Some (\<Squnion>Option.these x))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

427 
using G by fastforce 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

428 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

429 
also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y  {None} y. y \<in> A}))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

430 
by (simp add: Inf_option_def, safe) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

431 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

432 
also have "... = Some (\<Sqinter> ((\<lambda>x. (\<Squnion>Option.these x)) ` {y  {None} y. y \<in> A}))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

433 
by (simp add: B) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

434 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

435 
also have "... = Some (Inf (Sup ` {the ` (y  {None}) y. y \<in> A}))" 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

436 
by (unfold C, simp) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

437 
thm Inf_Sup 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

438 
also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y  {None}) y. y \<in> A} f. \<forall>Y. (\<exists>y. Y = the ` (y  {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) " 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

439 
by (simp add: Inf_Sup) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

440 

2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

441 
also have "... \<le> SUPREMUM {f ` A f. \<forall>Y\<in>A. f Y \<in> Y} Inf" 
67951
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

442 
proof (cases "SUPREMUM {f ` A f. \<forall>Y\<in>A. f Y \<in> Y} Inf") 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

443 
case None 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

444 
then show ?thesis by (simp add: less_eq_option_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

445 
next 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

446 
case (Some a) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

447 
then show ?thesis 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

448 
apply simp 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

449 
apply (rule Sup_least, safe) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

450 
apply (simp add: Sup_option_def) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

451 
apply (cases "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

452 
by (drule X, simp) 
655aa11359dc
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents:
67829
diff
changeset

453 
qed 
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

454 
finally show ?thesis by simp 
49190  455 
qed 
456 
qed 

457 

67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

458 
instance option :: (complete_distrib_lattice) complete_distrib_lattice 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

459 
by (standard, simp add: option_Inf_Sup) 
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset

460 

60679  461 
instance option :: (complete_linorder) complete_linorder .. 
49190  462 

463 

464 
no_notation 

465 
bot ("\<bottom>") and 

466 
top ("\<top>") and 

467 
inf (infixl "\<sqinter>" 70) and 

468 
sup (infixl "\<squnion>" 65) and 

469 
Inf ("\<Sqinter>_" [900] 900) and 

470 
Sup ("\<Squnion>_" [900] 900) 

471 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
60679
diff
changeset

472 
no_syntax 
49190  473 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 
474 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

475 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 

476 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

477 

478 
end 