--- 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
}
--- 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
--- 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
--- 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
--- 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)
--- 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:
--- 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>)"
--- 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)"
--- 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