# HG changeset patch
# User wenzelm
# Date 1465404344 -7200
# Node ID 576fb8068ba6a4700ec49509c062f31663bca2b6
# Parent  94d1f820130fb29c684b5d5bcf798ae7b393930c
tuned proofs;

diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -354,7 +354,7 @@
         obtain D fs where
           hp: "hp (the_Addr x) = Some (D,fs)" and
           D:  "G \<turnstile> D \<preceq>C C"
-          by - (drule non_npD, assumption, clarsimp)
+          by (auto dest: non_npD)
         hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
         moreover
         from wf mth hp D
@@ -366,9 +366,9 @@
         hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
           by (simp only: list_all2_rev)
         hence "list_all2 (conf G hp) (rev aps) apTs" by simp
-        with wf widen        
+        from wf this widen
         have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
-          by - (rule list_all2_conf_widen) 
+          by (rule list_all2_conf_widen) 
         ultimately
         have "?P1 \<and> ?P2 \<and> ?P3" by blast
       }
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -89,10 +89,9 @@
     from set
     have "C \<in> set (match_any G pc (e#es))" by simp
     moreover
-    from False C
+    from False
     have "\<not> match_exception_entry G C pc e"
-      by - (erule contrapos_nn, 
-            auto simp add: match_exception_entry_def)
+      by (rule contrapos_nn) (use C in \<open>auto simp add: match_exception_entry_def\<close>)
     with m
     have "match_exception_table G C pc (e#es) = Some pc'" by simp
     moreover note C
@@ -571,7 +570,7 @@
       }
       ultimately
       show ?thesis by (rule that)
-    qed (insert xp', auto) \<comment> "the other instructions don't generate exceptions"
+    qed (use xp' in auto) \<comment> "the other instructions don't generate exceptions"
 
     from state' meth hp_ok "class" frames phi_pc' frame' prehp
     have ?thesis by (unfold correct_state_def) simp
@@ -772,10 +771,9 @@
     (is "state' = Norm (?hp', ?f # frs)")
     by simp    
   moreover
-  from wf hp heap_ok is_class_X
+  from hp heap_ok
   have hp': "G \<turnstile>h ?hp' \<surd>"
-    by - (rule hconf_newref, 
-          auto simp add: oconf_def dest: fields_is_type)
+    by (rule hconf_newref) (use wf is_class_X in \<open>auto simp add: oconf_def dest: fields_is_type\<close>)
   moreover
   from hp
   have sup: "hp \<le>| ?hp'" by (rule hext_new)
@@ -786,10 +784,9 @@
     apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
     done      
   moreover
-  from hp frames wf heap_ok is_class_X
+  from hp frames
   have "correct_frames G ?hp' phi rT sig frs"
-    by - (rule correct_frames_newref, 
-          auto simp add: oconf_def dest: fields_is_type)
+    by (rule correct_frames_newref)
   moreover
   from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref)
   ultimately
@@ -851,10 +848,8 @@
     s': "phi C sig ! Suc pc = Some (ST', LT')"
     by (simp add: norm_eff_def split_paired_Ex) blast
 
-  from X 
-  obtain T where
-    X_Ref: "X = RefT T"
-    by - (drule widen_RefT2, erule exE, rule that)
+  from X obtain T where X_Ref: "X = RefT T"
+    by (blast dest: widen_RefT2)
   
   from s ins frame 
   obtain 
@@ -871,7 +866,7 @@
     stk':   "stk = opTs @ oX # stk'" and
     l_o:    "length opTs = length apTs" 
             "length stk' = length ST"  
-    by - (drule approx_stk_append, auto)
+    by (auto dest: approx_stk_append)
 
   from oX X_Ref
   have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T"
@@ -909,7 +904,7 @@
         "G \<turnstile> rT' \<preceq> rT0"
     by (auto dest: subtype_widen_methd intro: that)
   
-  from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans)
+  from mD(2) mX(2) have rT': "G \<turnstile> rT' \<preceq> rT" by (rule widen_trans)
   
   from is_class X'_subcls D_subcls
   have is_class_D: "is_class G D" by (auto dest: subcls_is_class2)
@@ -1351,19 +1346,18 @@
   apply (auto simp add: sup_state_conv approx_val_def dest!: widen_RefT split: err.splits)
   done  
 
-theorem
-  fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
-  assumes welltyped:   "wt_jvm_prog \<Gamma> \<Phi>" and
-          main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"  
-  shows typesafe:
-  "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+theorem typesafe:
+  fixes G :: jvm_prog ("\<Gamma>")
+    and Phi :: prog_type ("\<Phi>")
+  assumes welltyped:   "wt_jvm_prog \<Gamma> \<Phi>"
+    and main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+    and exec_all: "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s"
+  shows "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
 proof -
-  from welltyped main_method
-  have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
-  moreover
-  assume "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s"
-  ultimately  
-  show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
+  from welltyped main_method have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>"
+    by (rule BV_correct_initial)
+  with welltyped exec_all show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
+    by (rule BV_correct)
 qed
   
 end
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -55,7 +55,7 @@
     fix b 
     assume "length (l # ls) = length (b::ty list)" 
     with Cons
-    show "?Q (l # ls) b" by - (cases b, auto)
+    show "?Q (l # ls) b" by (cases b) auto
   qed
 qed
  
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/Comp/TypeInf.thy
--- a/src/HOL/MicroJava/Comp/TypeInf.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -4,7 +4,7 @@
 
 (* Exact position in theory hierarchy still to be determined *)
 theory TypeInf
-imports "../J/WellType" "~~/src/HOL/Eisbach/Eisbach"
+imports "../J/WellType"
 begin
 
 
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -131,7 +131,7 @@
 lemma semilat_errI [intro]:
   assumes semilat: "semilat (A, r, f)"
   shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
-  apply(insert semilat)
+  using semilat
   apply (simp only: semilat_Def closed_def plussub_def lesub_def 
     lift2_def Err.le_def err_def)
   apply (simp split: err.split)
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -65,7 +65,7 @@
 
 lemma (in lbv) le_top [simp, intro]:
   "x <=_r \<top>"
-  by (insert top) simp
+  using top by simp
   
 
 lemma (in lbv) merge_mono:
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -121,7 +121,7 @@
 
 lemma (in lbv) bottom_le [simp, intro]:
   "\<bottom> <=_r x"
-  by (insert bot) (simp add: bottom_def)
+  using bot by (simp add: bottom_def)
 
 lemma (in lbv) le_bottom [simp]:
   "x <=_r \<bottom> = (x = \<bottom>)"
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -135,14 +135,14 @@
   (*<*) by (auto intro: order_trans) (*>*)
   
 lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+  (*<*) using semilat by (simp add: semilat_Def) (*>*)
 
 lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+  (*<*) using semilat by (simp add: semilat_Def) (*>*)
 
 lemma (in Semilat) lub [simp, intro?]:
   "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+  (*<*) using semilat by (simp add: semilat_Def) (*>*)
 
 lemma (in Semilat) plus_le_conv [simp]:
   "\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)"
diff -r 94d1f820130f -r 576fb8068ba6 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Wed Jun 08 11:53:43 2016 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Wed Jun 08 18:45:44 2016 +0200
@@ -6,7 +6,12 @@
 
 section \<open>Some Auxiliary Definitions\<close>
 
-theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
+theory JBasis
+imports
+  Main
+  "~~/src/HOL/Library/Transitive_Closure_Table"
+  "~~/src/HOL/Eisbach/Eisbach"
+begin
 
 lemmas [simp] = Let_def