--- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Feb 09 16:01:58 2001 +0100
@@ -58,9 +58,6 @@
(app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
-
-
-
end
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Feb 09 16:01:58 2001 +0100
@@ -25,6 +25,8 @@
apply (blast intro: wt_jvm_prog_impl_wt_instr)
done
+section {* Single Instructions *}
+
lemmas [iff] = not_Err_eq
lemma Load_correct:
@@ -73,22 +75,6 @@
done
-lemma NT_subtype_conv:
- "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
-proof -
- have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))"
- apply (erule widen.induct)
- apply auto
- apply (case_tac R)
- apply auto
- done
- note l = this
-
- show ?thesis
- by (force dest: l)
-qed
-
-
lemma Cast_conf2:
"[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
G\<turnstile>Class C\<preceq>T; is_class G C|]
@@ -157,7 +143,7 @@
apply clarsimp
apply (blast
intro:
- sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
+ hext_upd_obj approx_stk_imp_approx_stk_sup_heap
approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup_heap
approx_loc_imp_approx_loc_sup hconf_imp_hconf_field_update
correct_frames_imp_correct_frames_field_update conf_widen
@@ -165,11 +151,6 @@
widen_cfs_fields)
done
-lemma collapse_paired_All:
- "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
- by fast
-
-
lemma New_correct:
"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins);
@@ -233,7 +214,7 @@
auto simp add: oconf_def dest: fields_is_type)
moreover
from hp
- have sup: "hp \<le>| ?hp'" by (rule sup_heap_newref)
+ have sup: "hp \<le>| ?hp'" by (rule hext_new)
from hp frame less suc_pc wf
have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
apply (unfold correct_frame_def sup_state_conv)
@@ -255,8 +236,7 @@
ultimately
show ?thesis by auto
qed
-
-(****** Method Invocation ******)
+
lemmas [simp del] = split_paired_Ex
@@ -638,8 +618,6 @@
done
-(** instr correct **)
-
lemma instr_correct:
"[| wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins);
@@ -673,8 +651,7 @@
done
-
-(** Main **)
+section {* Main *}
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
--- a/src/HOL/MicroJava/BV/Correct.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Fri Feb 09 16:01:58 2001 +0100
@@ -76,23 +76,7 @@
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
("_,_ |-JVM _ [ok]" [51,51] 50)
-lemma sup_heap_newref:
- "hp oref = None ==> hp \<le>| hp(oref \<mapsto> obj)"
-proof (unfold hext_def, intro strip)
- fix a C fs
- assume "hp oref = None" and hp: "hp a = Some (C, fs)"
- hence "a \<noteq> oref" by auto
- hence "(hp (oref\<mapsto>obj)) a = hp a" by (rule fun_upd_other)
- with hp
- show "\<exists>fs'. (hp(oref\<mapsto>obj)) a = Some (C, fs')" by auto
-qed
-
-lemma sup_heap_update_value:
- "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
-by (simp add: hext_def)
-
-
-(** approx_val **)
+section {* approx-val *}
lemma approx_val_Err:
"approx_val G hp x Err"
@@ -136,7 +120,7 @@
done
-(** approx_loc **)
+section {* approx-loc *}
lemma approx_loc_Cons [iff]:
"approx_loc G hp (s#xs) (l#ls) =
@@ -196,7 +180,7 @@
lemmas [cong del] = conj_cong
-(** approx_stk **)
+section {* approx-stk *}
lemma approx_stk_rev_lem:
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
@@ -240,7 +224,7 @@
by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
-(** oconf **)
+section {* oconf *}
lemma correct_init_obj:
"[|is_class G C; wf_prog wt G|] ==>
@@ -260,7 +244,7 @@
"hp oref = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(oref\<mapsto>obj'))\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
apply simp
-apply (fast intro: conf_hext sup_heap_newref)
+apply (fast intro: conf_hext hext_new)
done
lemma oconf_imp_oconf_heap_update [rule_format]:
@@ -272,7 +256,7 @@
done
-(** hconf **)
+section {* hconf *}
lemma hconf_imp_hconf_newref [rule_format]:
"hp oref = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
@@ -288,7 +272,7 @@
simp add: obj_ty_def)
done
-(** correct_frames **)
+section {* correct-frames *}
lemmas [simp del] = fun_upd_apply
@@ -312,11 +296,11 @@
apply simp
apply (rule approx_stk_imp_approx_stk_sup_heap)
apply simp
- apply (rule sup_heap_update_value)
+ apply (rule hext_upd_obj)
apply simp
apply (rule approx_loc_imp_approx_loc_sup_heap)
apply simp
-apply (rule sup_heap_update_value)
+apply (rule hext_upd_obj)
apply simp
done
@@ -333,11 +317,11 @@
apply simp
apply (rule approx_stk_imp_approx_stk_sup_heap)
apply simp
- apply (rule sup_heap_newref)
+ apply (rule hext_new)
apply simp
apply (rule approx_loc_imp_approx_loc_sup_heap)
apply simp
-apply (rule sup_heap_newref)
+apply (rule hext_new)
apply simp
done
--- a/src/HOL/MicroJava/BV/DFA_Framework.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/DFA_Framework.thy Fri Feb 09 16:01:58 2001 +0100
@@ -2,14 +2,16 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
-
-The relationship between dataflow analysis and a welltyped-insruction predicate.
*)
header "Dataflow Analysis Framework"
theory DFA_Framework = Listn:
+text {*
+ The relationship between dataflow analysis and a welltyped-insruction predicate.
+*}
+
constdefs
bounded :: "(nat => nat list) => nat => bool"
"bounded succs n == !p<n. !q:set(succs p). q<n"
--- a/src/HOL/MicroJava/BV/DFA_err.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/DFA_err.thy Fri Feb 09 16:01:58 2001 +0100
@@ -3,7 +3,6 @@
Author: Gerwin Klein
Copyright 2000 TUM
-static and dynamic welltyping
*)
header "Static and Dynamic Welltyping"
--- a/src/HOL/MicroJava/BV/Err.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Fri Feb 09 16:01:58 2001 +0100
@@ -15,13 +15,11 @@
types 'a ebinop = "'a => 'a => 'a err"
'a esl = "'a set * 'a ord * 'a ebinop"
-
consts
ok_val :: "'a err => 'a"
primrec
"ok_val (OK x) = x"
-
constdefs
lift :: "('a => 'b err) => ('a err => 'b err)"
"lift f e == case e of Err => Err | OK x => f x"
@@ -60,6 +58,9 @@
"strict f Err = Err"
"strict f (OK x) = f x"
+lemma strict_Some [simp]:
+ "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
+ by (cases x, auto)
lemma not_Err_eq:
"(x \<noteq> Err) = (\<exists>a. x = OK a)"
@@ -69,8 +70,6 @@
"(\<forall>y. x \<noteq> OK y) = (x = Err)"
by (cases x) auto
-
-
lemma unfold_lesub_err:
"e1 <=_(le r) e2 == le r e1 e2"
by (simp add: lesub_def)
@@ -168,7 +167,7 @@
lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
by (auto simp add: err_def)
-(** lift **)
+section {* lift *}
lemma lift_in_errI:
"[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
@@ -177,8 +176,6 @@
apply blast
done
-(** lift2 **)
-
lemma Err_lift2 [simp]:
"Err +_(lift2 f) x = Err"
by (simp add: lift2_def plussub_def)
@@ -191,7 +188,8 @@
"OK x +_(lift2 f) OK y = x +_f y"
by (simp add: lift2_def plussub_def split: err.split)
-(** sup **)
+
+section {* sup *}
lemma Err_sup_Err [simp]:
"Err +_(Err.sup f) x = Err"
@@ -220,7 +218,7 @@
apply (simp split: err.split)
done
-(*** semilat (err A) (le r) f ***)
+section {* semilat (err A) (le r) f *}
lemma semilat_le_err_Err_plus [simp]:
"[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
@@ -285,7 +283,7 @@
done
qed
-(*** semilat (err(Union AS)) ***)
+section {* semilat (err(Union AS)) *}
(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
@@ -303,9 +301,11 @@
apply fast
done
-(* If AS = {} the thm collapses to
- order r & closed {Err} f & Err +_f Err = Err
- which may not hold *)
+text {*
+ If @{term "AS = {}"} the thm collapses to
+ @{prop "order r & closed {Err} f & Err +_f Err = Err"}
+ which may not hold
+*}
lemma err_semilat_UnionI:
"[| !A:AS. err_semilat(A, r, f); AS ~= {};
!A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |]
--- a/src/HOL/MicroJava/BV/JType.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Fri Feb 09 16:01:58 2001 +0100
@@ -21,7 +21,7 @@
| ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
subtype :: "'c prog => ty => ty => bool"
- "subtype G T1 T2 == G \\<turnstile> T1 \\<preceq> T2"
+ "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
is_ty :: "'c prog => ty => bool"
"is_ty G T == case T of PrimT P => True | RefT R =>
@@ -34,10 +34,10 @@
esl :: "'c prog => ty esl"
"esl G == (types G, subtype G, sup G)"
-lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
+lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
by (auto elim: widen.elims)
-lemma PrimT_PrimT2: "(G \\<turnstile> PrimT p \\<preceq> xb) = (xb = PrimT p)"
+lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
by (auto elim: widen.elims)
lemma is_tyI:
@@ -62,10 +62,10 @@
next
fix R assume R: "T = RefT R"
with wf
- have "R = ClassT Object \\<Longrightarrow> ?thesis" by simp
+ have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
moreover
from R wf ty
- have "R \\<noteq> ClassT Object \\<Longrightarrow> ?thesis"
+ have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
by (auto simp add: is_ty_def subcls1_def is_class_def
elim: converse_rtranclE
split: ref_ty.splits)
@@ -74,7 +74,6 @@
qed
qed
-
lemma order_widen:
"acyclic (subcls1 G) ==> order (subtype G)"
apply (unfold order_def lesub_def subtype_def)
@@ -163,7 +162,7 @@
lemma sup_subtype_greater:
"[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
is_type G t1; is_type G t2; sup G t1 t2 = OK s |]
- ==> subtype G t1 s \\<and> subtype G t2 s"
+ ==> subtype G t1 s \<and> subtype G t2 s"
proof -
assume wf_prog: "wf_prog wf_mb G"
assume single_valued: "single_valued (subcls1 G)"
@@ -173,16 +172,16 @@
assume is_class: "is_class G c1" "is_class G c2"
with wf_prog
obtain
- "G \\<turnstile> c1 \\<preceq>C Object"
- "G \\<turnstile> c2 \\<preceq>C Object"
+ "G \<turnstile> c1 \<preceq>C Object"
+ "G \<turnstile> c2 \<preceq>C Object"
by (blast intro: subcls_C_Object)
with wf_prog single_valued
obtain u where
"is_lub ((subcls1 G)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
with acyclic
- have "G \\<turnstile> c1 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \\<and>
- G \\<turnstile> c2 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
+ have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \<and>
+ G \<turnstile> c2 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
} note this [simp]
@@ -206,11 +205,11 @@
{ fix c1 c2 D
assume is_class: "is_class G c1" "is_class G c2"
- assume le: "G \\<turnstile> c1 \\<preceq>C D" "G \\<turnstile> c2 \\<preceq>C D"
+ assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
from wf_prog is_class
obtain
- "G \\<turnstile> c1 \\<preceq>C Object"
- "G \\<turnstile> c2 \\<preceq>C Object"
+ "G \<turnstile> c1 \<preceq>C Object"
+ "G \<turnstile> c2 \<preceq>C Object"
by (blast intro: subcls_C_Object)
with wf_prog single_valued
obtain u where
@@ -221,15 +220,15 @@
by (rule some_lub_conv)
moreover
from lub le
- have "G \\<turnstile> u \\<preceq>C D"
+ have "G \<turnstile> u \<preceq>C D"
by (simp add: is_lub_def is_ub_def)
ultimately
- have "G \\<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \\<preceq>C D"
+ have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
by blast
} note this [intro]
have [dest!]:
- "!!C T. G \\<turnstile> Class C \\<preceq> T ==> \\<exists>D. T=Class D \\<and> G \\<turnstile> C \\<preceq>C D"
+ "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
by (frule widen_Class, auto)
assume "is_type G a" "is_type G b" "is_type G c"
@@ -262,16 +261,16 @@
from wf_prog single_valued acyclic
have
- "(\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \\<and>
- (\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
+ "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and>
+ (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
moreover
from wf_prog single_valued acyclic
have
- "\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). \\<forall>z\\<in>err (types G).
- x <=_(le (subtype G)) z \\<and> y <=_(le (subtype G)) z \\<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
+ "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G).
+ x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
by (unfold lift2_def plussub_def lesub_def le_def)
(auto intro: sup_subtype_smallest sup_exists split: err.split)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Fri Feb 09 16:01:58 2001 +0100
@@ -33,7 +33,6 @@
"make_Cert G Phi == \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
in make_cert b (Phi C sig)"
-
lemmas [simp del] = split_paired_Ex
lemma make_cert_target:
@@ -47,8 +46,7 @@
lemma make_cert_contains_targets:
"pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
-proof (unfold contains_targets_def, intro strip, elim conjE)
-
+proof (unfold contains_targets_def, intro strip, elim conjE)
fix pc'
assume "pc < length ins"
"pc' \<in> set (succs (ins ! pc) pc)"
@@ -67,7 +65,6 @@
"fits ins (make_cert ins phi) phi"
by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
-
lemma fitsD:
"[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc);
pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
@@ -79,7 +76,6 @@
==> cert!pc = phi!pc"
by (auto simp add: fits_def)
-
lemma wtl_inst_mono:
"[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
@@ -312,7 +308,6 @@
show ?thesis by blast
qed
-
text {*
\medskip
Main induction over the instruction list.
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Feb 09 16:01:58 2001 +0100
@@ -282,8 +282,7 @@
theorem wtl_correct:
"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
-proof -
-
+proof -
assume wtl: "wtl_jvm_prog G cert"
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Fri Feb 09 16:01:58 2001 +0100
@@ -72,10 +72,6 @@
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
by (auto simp add: wtl_inst_def check_cert_def set_mem_eq)
-lemma strict_Some [simp]:
-"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
- by (cases x, auto)
-
lemma wtl_Cons:
"wtl_inst_list (i#is) G rT cert maxs max_pc pc s \<noteq> Err =
(\<exists>s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \<and>
--- a/src/HOL/MicroJava/BV/Opt.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Fri Feb 09 16:01:58 2001 +0100
@@ -137,8 +137,7 @@
assume x: "x : ?A"
assume y: "y : ?A"
- {
- fix a b
+ { fix a b
assume ab: "x = OK a" "y = OK b"
with x
@@ -180,97 +179,32 @@
moreover
- have "\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y"
- proof (intro strip)
- fix x y
- assume x: "x : ?A"
- assume y: "y : ?A"
-
- show "x <=_?r x +_?f y"
- proof -
- from ord
- have order_r: "order r" by simp
-
- { fix a b
- assume ok: "x = OK a" "y = OK b"
-
- { fix c d
- assume some: "a = Some c" "b = Some d"
-
- with x y ok
- obtain "c:A" "d:A" by simp
- then
- obtain "OK c : err A" "OK d : err A" by simp
- with ub1
- have OK: "OK c <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
- by blast
-
- { fix e assume "f c d = OK e"
- with OK
- have "c <=_r e"
- by (simp add: lesub_def Err.le_def plussub_def lift2_def)
- }
- with ok some
- have ?thesis
- by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def
- split: err.split)
- } note this [intro!]
-
- from ok
- have ?thesis
- by - (cases a, simp, cases b, simp add: order_r, blast)
- }
- thus ?thesis
- by - (cases x, simp, cases y, simp+)
- qed
- qed
-
- moreover
-
- have "\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y"
- proof (intro strip)
- fix x y
- assume x: "x : ?A"
- assume y: "y : ?A"
-
- show "y <=_?r x +_?f y"
- proof -
- from ord
- have order_r: "order r" by simp
-
- { fix a b
- assume ok: "x = OK a" "y = OK b"
-
- { fix c d
- assume some: "a = Some c" "b = Some d"
-
- with x y ok
- obtain "c:A" "d:A" by simp
- then
- obtain "OK c : err A" "OK d : err A" by simp
- with ub2
- have OK: "OK d <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
- by blast
-
- { fix e assume "f c d = OK e"
- with OK
- have "d <=_r e"
- by (simp add: lesub_def Err.le_def plussub_def lift2_def)
- }
- with ok some
- have ?thesis
- by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def
- split: err.split)
- } note this [intro!]
-
- from ok
- have ?thesis
- by - (cases a, simp add: order_r, cases b, simp, blast)
- }
- thus ?thesis
- by - (cases x, simp, cases y, simp+)
- qed
- qed
+ { fix a b c
+ assume "a \<in> opt A" "b \<in> opt A" "a +_(sup f) b = OK c"
+ moreover
+ from ord have "order r" by simp
+ moreover
+ { fix x y z
+ assume "x \<in> A" "y \<in> A"
+ hence "OK x \<in> err A \<and> OK y \<in> err A" by simp
+ with ub1 ub2
+ have "(OK x) <=_(Err.le r) (OK x) +_(lift2 f) (OK y) \<and>
+ (OK y) <=_(Err.le r) (OK x) +_(lift2 f) (OK y)"
+ by blast
+ moreover
+ assume "x +_f y = OK z"
+ ultimately
+ have "x <=_r z \<and> y <=_r z"
+ by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
+ }
+ ultimately
+ have "a <=_(le r) c \<and> b <=_(le r) c"
+ by (auto simp add: sup_def le_def lesub_def plussub_def
+ dest: order_refl split: option.splits err.splits)
+ }
+
+ hence "(\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y) \<and> (\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y)"
+ by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)
moreover
--- a/src/HOL/MicroJava/BV/Semilat.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Fri Feb 09 16:01:58 2001 +0100
@@ -152,7 +152,6 @@
apply simp
done
-(*** closed ***)
lemma closedD:
"[| closed A f; x:A; y:A |] ==> x +_f y : A"
@@ -163,7 +162,6 @@
lemma closed_UNIV [simp]: "closed UNIV f"
by (simp add: closed_def)
-(*** lub ***)
lemma is_lubD:
"is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
@@ -184,14 +182,12 @@
apply blast
done
-
lemma is_lub_bigger2 [iff]:
"is_lub (r^* ) x y x = ((y,x):r^* )"
apply (unfold is_lub_def is_ub_def)
apply blast
done
-
lemma extend_lub:
"[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |]
==> EX v. is_lub (r^* ) x' y v"