585 "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
585 "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
586 \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)" |
586 \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)" |
587 by (auto simp add: correct_state_def Let_def) |
587 by (auto simp add: correct_state_def Let_def) |
588 |
588 |
589 |
589 |
590 lemma BV_correct_1 [rulify]: |
590 lemma BV_correct_1 [rulified]: |
591 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> |
591 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> |
592 \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
592 \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
593 apply (simp only: split_tupled_all) |
593 apply (simp only: split_tupled_all) |
594 apply (rename_tac xp hp frs) |
594 apply (rename_tac xp hp frs) |
595 apply (case_tac xp) |
595 apply (case_tac xp) |
615 apply assumption |
615 apply assumption |
616 apply (fast intro: BV_correct_1) |
616 apply (fast intro: BV_correct_1) |
617 done |
617 done |
618 |
618 |
619 |
619 |
620 theorem BV_correct [rulify]: |
620 theorem BV_correct [rulified]: |
621 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>" |
621 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>" |
622 apply (unfold exec_all_def) |
622 apply (unfold exec_all_def) |
623 apply (erule rtrancl_induct) |
623 apply (erule rtrancl_induct) |
624 apply simp |
624 apply simp |
625 apply (auto intro: BV_correct_1) |
625 apply (auto intro: BV_correct_1) |