equal
deleted
inserted
replaced
13 datatype 'a err = Err | OK 'a |
13 datatype 'a err = Err | OK 'a |
14 |
14 |
15 types 'a ebinop = "'a => 'a => 'a err" |
15 types 'a ebinop = "'a => 'a => 'a err" |
16 'a esl = "'a set * 'a ord * 'a ebinop" |
16 'a esl = "'a set * 'a ord * 'a ebinop" |
17 |
17 |
18 |
|
19 consts |
18 consts |
20 ok_val :: "'a err => 'a" |
19 ok_val :: "'a err => 'a" |
21 primrec |
20 primrec |
22 "ok_val (OK x) = x" |
21 "ok_val (OK x) = x" |
23 |
|
24 |
22 |
25 constdefs |
23 constdefs |
26 lift :: "('a => 'b err) => ('a err => 'b err)" |
24 lift :: "('a => 'b err) => ('a err => 'b err)" |
27 "lift f e == case e of Err => Err | OK x => f x" |
25 "lift f e == case e of Err => Err | OK x => f x" |
28 |
26 |
58 strict :: "('a => 'b err) => ('a err => 'b err)" |
56 strict :: "('a => 'b err) => ('a err => 'b err)" |
59 primrec |
57 primrec |
60 "strict f Err = Err" |
58 "strict f Err = Err" |
61 "strict f (OK x) = f x" |
59 "strict f (OK x) = f x" |
62 |
60 |
|
61 lemma strict_Some [simp]: |
|
62 "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)" |
|
63 by (cases x, auto) |
63 |
64 |
64 lemma not_Err_eq: |
65 lemma not_Err_eq: |
65 "(x \<noteq> Err) = (\<exists>a. x = OK a)" |
66 "(x \<noteq> Err) = (\<exists>a. x = OK a)" |
66 by (cases x) auto |
67 by (cases x) auto |
67 |
68 |
68 lemma not_OK_eq: |
69 lemma not_OK_eq: |
69 "(\<forall>y. x \<noteq> OK y) = (x = Err)" |
70 "(\<forall>y. x \<noteq> OK y) = (x = Err)" |
70 by (cases x) auto |
71 by (cases x) auto |
71 |
|
72 |
|
73 |
72 |
74 lemma unfold_lesub_err: |
73 lemma unfold_lesub_err: |
75 "e1 <=_(le r) e2 == le r e1 e2" |
74 "e1 <=_(le r) e2 == le r e1 e2" |
76 by (simp add: lesub_def) |
75 by (simp add: lesub_def) |
77 |
76 |
166 by (simp add: err_def) |
165 by (simp add: err_def) |
167 |
166 |
168 lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)" |
167 lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)" |
169 by (auto simp add: err_def) |
168 by (auto simp add: err_def) |
170 |
169 |
171 (** lift **) |
170 section {* lift *} |
172 |
171 |
173 lemma lift_in_errI: |
172 lemma lift_in_errI: |
174 "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S" |
173 "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S" |
175 apply (unfold lift_def) |
174 apply (unfold lift_def) |
176 apply (simp split: err.split) |
175 apply (simp split: err.split) |
177 apply blast |
176 apply blast |
178 done |
177 done |
179 |
178 |
180 (** lift2 **) |
|
181 |
|
182 lemma Err_lift2 [simp]: |
179 lemma Err_lift2 [simp]: |
183 "Err +_(lift2 f) x = Err" |
180 "Err +_(lift2 f) x = Err" |
184 by (simp add: lift2_def plussub_def) |
181 by (simp add: lift2_def plussub_def) |
185 |
182 |
186 lemma lift2_Err [simp]: |
183 lemma lift2_Err [simp]: |
189 |
186 |
190 lemma OK_lift2_OK [simp]: |
187 lemma OK_lift2_OK [simp]: |
191 "OK x +_(lift2 f) OK y = x +_f y" |
188 "OK x +_(lift2 f) OK y = x +_f y" |
192 by (simp add: lift2_def plussub_def split: err.split) |
189 by (simp add: lift2_def plussub_def split: err.split) |
193 |
190 |
194 (** sup **) |
191 |
|
192 section {* sup *} |
195 |
193 |
196 lemma Err_sup_Err [simp]: |
194 lemma Err_sup_Err [simp]: |
197 "Err +_(Err.sup f) x = Err" |
195 "Err +_(Err.sup f) x = Err" |
198 by (simp add: plussub_def Err.sup_def Err.lift2_def) |
196 by (simp add: plussub_def Err.sup_def Err.lift2_def) |
199 |
197 |
218 "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)" |
216 "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)" |
219 apply (unfold Err.sup_def lift2_def plussub_def) |
217 apply (unfold Err.sup_def lift2_def plussub_def) |
220 apply (simp split: err.split) |
218 apply (simp split: err.split) |
221 done |
219 done |
222 |
220 |
223 (*** semilat (err A) (le r) f ***) |
221 section {* semilat (err A) (le r) f *} |
224 |
222 |
225 lemma semilat_le_err_Err_plus [simp]: |
223 lemma semilat_le_err_Err_plus [simp]: |
226 "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err" |
224 "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err" |
227 by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1]) |
225 by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1]) |
228 |
226 |
283 apply (erule subst) |
281 apply (erule subst) |
284 apply (blast intro: closedD) |
282 apply (blast intro: closedD) |
285 done |
283 done |
286 qed |
284 qed |
287 |
285 |
288 (*** semilat (err(Union AS)) ***) |
286 section {* semilat (err(Union AS)) *} |
289 |
287 |
290 (* FIXME? *) |
288 (* FIXME? *) |
291 lemma all_bex_swap_lemma [iff]: |
289 lemma all_bex_swap_lemma [iff]: |
292 "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))" |
290 "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))" |
293 by blast |
291 by blast |
301 apply clarify |
299 apply clarify |
302 apply simp |
300 apply simp |
303 apply fast |
301 apply fast |
304 done |
302 done |
305 |
303 |
306 (* If AS = {} the thm collapses to |
304 text {* |
307 order r & closed {Err} f & Err +_f Err = Err |
305 If @{term "AS = {}"} the thm collapses to |
308 which may not hold *) |
306 @{prop "order r & closed {Err} f & Err +_f Err = Err"} |
|
307 which may not hold |
|
308 *} |
309 lemma err_semilat_UnionI: |
309 lemma err_semilat_UnionI: |
310 "[| !A:AS. err_semilat(A, r, f); AS ~= {}; |
310 "[| !A:AS. err_semilat(A, r, f); AS ~= {}; |
311 !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] |
311 !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] |
312 ==> err_semilat(Union AS, r, f)" |
312 ==> err_semilat(Union AS, r, f)" |
313 apply (unfold semilat_def sl_def) |
313 apply (unfold semilat_def sl_def) |