[STATEMENT]
theorem welltyped_aggressive_imp_defensive:
  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t 
  \<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> t\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal t
[PROOF STEP]
apply (unfold exec_all_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, t) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal t
[PROOF STEP]
apply (erule rtrancl_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal s
 2. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; (y, z) \<in> {(s, t). exec (G, s) = Some t}; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (simp add: exec_all_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; (y, z) \<in> {(s, t). exec (G, s) = Some t}; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (fold exec_all_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (frule BV_correct, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y; G,Phi \<turnstile>JVM y \<surd>\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (simp add: exec_all_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; (Normal s, Normal y) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> (Normal s, Normal z) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*
[PROOF STEP]
apply (rule rtrancl_trans, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; (Normal s, Normal y) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> (Normal y, Normal z) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done