# HG changeset patch
# User kleing
# Date 981730918 -3600
# Node ID b830bf10bf711a77d92a48ef57fefd3c7bab2442
# Parent  32c1deea5bcd4ca06b0f259c3006d481d17c9a8f
tuned for 99-2 release

diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/BVSpec.thy
--- 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
 
 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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> 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/Correct.thy
--- 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
 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/DFA_Framework.thy
--- 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"
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/DFA_err.thy
--- 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"
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/Err.thy
--- 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) |] 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/JType.thy
--- 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)
 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/LBVComplete.thy
--- 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.
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/LBVCorrect.thy
--- 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 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/LBVSpec.thy
--- 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> 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/Opt.thy
--- 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
 
diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/Semilat.thy
--- 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"