--- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Aug 08 16:57:44 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Aug 09 11:53:00 2000 +0200
@@ -36,6 +36,8 @@
wf_prog (\\<lambda>G C (sig,rT,maxl,b).
wt_method G C (snd sig) rT maxl b (phi C sig)) G"
+
+
lemma wt_jvm_progD:
"wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Tue Aug 08 16:57:44 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 09 11:53:00 2000 +0200
@@ -6,11 +6,7 @@
header {* Completeness of the LBV *}
-theory LBVComplete = BVSpec + LBVSpec:
-
-
-ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
-ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
+theory LBVComplete = BVSpec + LBVSpec + StepMono:
constdefs
@@ -66,52 +62,60 @@
make_cert b (Phi C sig)"
-lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l"
+lemmas [simp del] = split_paired_Ex
+
+lemma length_ofn [rulify]: "\\<forall>n. length (option_filter_n l P n) = length l"
by (induct l) auto
-lemma is_approx_option_filter_n:
-"\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
-proof (induct a)
- show "?P []" by (auto simp add: is_approx_def)
- fix l ls
- assume Cons: "?P ls"
-
- show "?P (l#ls)"
- proof (unfold is_approx_def, intro allI conjI impI)
- fix n
- show "length (option_filter_n (l # ls) P n) = length (l # ls)"
- by (simp only: length_ofn)
+lemma is_approx_option_filter: "is_approx (option_filter l P) l"
+proof -
+ {
+ fix a n
+ have "\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
+ proof (induct a)
+ show "?P []" by (auto simp add: is_approx_def)
+
+ fix l ls
+ assume Cons: "?P ls"
- fix m
- assume "m < length (option_filter_n (l # ls) P n)"
- hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
-
- show "option_filter_n (l # ls) P n ! m = None \\<or>
- option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)"
- proof (cases "m")
- assume "m = 0"
- with m show ?thesis by simp
- next
- fix m' assume Suc: "m = Suc m'"
- from Cons
- show ?thesis
- proof (unfold is_approx_def, elim allE impE conjE)
- from m Suc
- show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
-
- assume "option_filter_n ls P (Suc n) ! m' = None \\<or>
- option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
- with m Suc
- show ?thesis by auto
+ show "?P (l#ls)"
+ proof (unfold is_approx_def, intro allI conjI impI)
+ fix n
+ show "length (option_filter_n (l # ls) P n) = length (l # ls)"
+ by (simp only: length_ofn)
+
+ fix m
+ assume "m < length (option_filter_n (l # ls) P n)"
+ hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
+
+ show "option_filter_n (l # ls) P n ! m = None \\<or>
+ option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)"
+ proof (cases "m")
+ assume "m = 0"
+ with m show ?thesis by simp
+ next
+ fix m' assume Suc: "m = Suc m'"
+ from Cons
+ show ?thesis
+ proof (unfold is_approx_def, elim allE impE conjE)
+ from m Suc
+ show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
+
+ assume "option_filter_n ls P (Suc n) ! m' = None \\<or>
+ option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
+ with m Suc
+ show ?thesis by auto
+ qed
+ qed
qed
qed
- qed
+ }
+
+ thus ?thesis
+ by (auto simp add: option_filter_def)
qed
-lemma is_approx_option_filter: "is_approx (option_filter l P) l"
- by (simp add: option_filter_def is_approx_option_filter_n)
-
lemma option_filter_Some:
"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
proof -
@@ -200,11 +204,8 @@
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
-
-lemmas [trans] = sup_state_trans
-
lemma wtl_inst_mono:
-"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G;
+"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
\\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
proof -
@@ -270,6 +271,42 @@
with pc show ?thesis by simp
qed
+
+lemma wtl_option_mono:
+"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi;
+ pc < length ins; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
+ \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+proof -
+ assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and
+ fits: "fits ins cert phi" "pc < length ins"
+ "G \\<turnstile> s2 <=s s1" "i = ins!pc"
+
+ show ?thesis
+ proof (cases "cert!pc")
+ case None
+ with wtl fits;
+ show ?thesis;
+ by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
+ next
+ case Some
+ with wtl fits;
+
+ have G: "G \\<turnstile> s2 <=s a"
+ by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
+
+ from Some wtl
+ have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
+
+ with G fits
+ have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+ by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
+
+ with Some G;
+ show ?thesis; by (simp add: wtl_inst_option_def);
+ qed
+qed
+
+
lemma wt_instr_imp_wtl_inst:
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
@@ -296,7 +333,7 @@
from wt fits pc
have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk>
\\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
- by (auto dest: fitsD simp add: wt_instr_def simp del: split_paired_Ex)
+ by (auto dest: fitsD simp add: wt_instr_def)
show ?thesis
proof (cases "pc+1 \\<in> succs (ins!pc) pc")
@@ -358,143 +395,87 @@
qed
-lemma wtl_option_mono:
-"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
- wf_prog wf_mb G; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
-proof -
- assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and
- fits: "fits ins cert phi" "pc < length ins"
- "wf_prog wf_mb G" "G \\<turnstile> s2 <=s s1" "i = ins!pc"
-
- show ?thesis
- proof (cases "cert!pc")
- case None
- with wtl fits;
- show ?thesis;
- by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
- next
- case Some
- with wtl fits;
-
- have G: "G \\<turnstile> s2 <=s a"
- by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
-
- from Some wtl
- have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
+text {*
+ \medskip
+ Main induction over the instruction list.
+*}
- with G fits
- have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
- by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
-
- with Some G;
- show ?thesis; by (simp add: wtl_inst_option_def);
- qed
-qed
-
-
-(* main induction over instruction list *)
theorem wt_imp_wtl_inst_list:
-"\\<forall> pc. (\\<forall>pc'. pc' < length ins \\<longrightarrow> wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\<longrightarrow>
- wf_prog wf_mb G \\<longrightarrow>
- fits all_ins cert phi \\<longrightarrow> (\\<exists> l. pc = length l \\<and> all_ins=l@ins) \\<longrightarrow> pc < length all_ins \\<longrightarrow>
+"\\<forall> pc. (\\<forall>pc'. pc' < length all_ins \\<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\<longrightarrow>
+ fits all_ins cert phi \\<longrightarrow>
+ (\\<exists>l. pc = length l \\<and> all_ins = l@ins) \\<longrightarrow>
+ pc < length all_ins \\<longrightarrow>
(\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow>
- (\\<exists>s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))"
-(is "\\<forall>pc. ?C pc ins" is "?P ins");
-proof (induct "?P" "ins");
- case Nil;
- show "?P []"; by simp;
-next;
- case Cons;
+ (\\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))"
+(is "\\<forall>pc. ?wt \\<longrightarrow> ?fits \\<longrightarrow> ?l pc ins \\<longrightarrow> ?len pc \\<longrightarrow> ?wtl pc ins" is "\\<forall>pc. ?C pc ins" is "?P ins")
+proof (induct "?P" "ins")
+ case Nil
+ show "?P []" by simp
+next
+ fix i ins'
+ assume Cons: "?P ins'"
- show "?P (a#list)";
- proof (intro allI impI, elim exE conjE);
- fix pc s l;
- assume 1: "wf_prog wf_mb G" "fits all_ins cert phi";
- assume 2: "pc < length all_ins" "G \\<turnstile> s <=s phi ! pc"
- "all_ins = l @ a # list" "pc = length l";
+ show "?P (i#ins')"
+ proof (intro allI impI, elim exE conjE)
+ fix pc s l
+ assume wt : "\\<forall>pc'. pc' < length all_ins \\<longrightarrow>
+ wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
+ assume fits: "fits all_ins cert phi"
+ assume G : "G \\<turnstile> s <=s phi ! pc"
+ assume l : "pc < length all_ins"
- from Cons;
- have IH: "?C (Suc pc) list"; by blast;
+ assume pc : "all_ins = l@i#ins'" "pc = length l"
+ hence i : "all_ins ! pc = i"
+ by (simp add: nth_append)
- assume 3: "\\<forall>pc'. pc' < length (a # list) \\<longrightarrow>
- wt_instr ((a # list) ! pc') G rT phi (pc + length (a # list)) (pc + pc')";
- hence 4: "\\<forall>pc'. pc' < length list \\<longrightarrow>
- wt_instr (list ! pc') G rT phi (Suc pc + length list) (Suc pc + pc')"; by auto;
+ from l wt
+ have "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast
- from 2;
- have 5: "a = all_ins ! pc"; by (simp add: nth_append);
-
-
- show "\\<exists>s'. wtl_inst_list (a # list) G rT s s' cert (pc + length (a # list)) pc";
- proof (cases list);
- case Nil;
-
- with 1 2 3 5;
- have "\\<exists>s'. wtl_inst_option a G rT (phi ! pc) s' cert (Suc (length l)) pc";
- by - (rule wt_instr_imp_wtl_option [elimify], force+);
+ with fits l
+ obtain s1 where
+ "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and
+ s1: "G \\<turnstile> s1 <=s phi ! (Suc pc)"
+ by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp)
+
+ with fits l
+ obtain s2 where
+ o: "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc"
+ and "G \\<turnstile> s2 <=s s1"
+ by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that)
- with Nil 1 2 5;
- have "\\<exists>s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc";
- by elim (rule wtl_option_mono [elimify], force+);
-
- with Nil 2;
- show ?thesis; by auto;
- next;
- fix i' ins';
- assume Cons2: "list = i' # ins'";
-
- with IH 1 2 3;
- have * : "\\<forall> s. (G \\<turnstile> s <=s (phi!(Suc pc))) \\<longrightarrow>
- (\\<exists>s'. wtl_inst_list list G rT s s' cert ((Suc pc)+length list) (Suc pc))";
- by (elim impE) force+;
+ with s1
+ have G': "G \\<turnstile> s2 <=s phi ! (Suc pc)"
+ by - (rule sup_state_trans, auto)
- from 3;
- have "wt_instr a G rT phi (pc + length (a # list)) pc"; by auto;
-
- with 1 2 5;
- have "\\<exists>s1'. wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc \\<and> G \\<turnstile> s1' <=s phi ! Suc pc";
- by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+);
-
- hence "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
- (G \\<turnstile> s1 <=s (phi ! (Suc pc)))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
- proof elim;
- fix s1';
- assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and
- a :"G \\<turnstile> s1' <=s phi ! Suc pc";
- with 1 2 5;
- have "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
- ((G \\<turnstile> s1 <=s s1'))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
- by - (rule wtl_option_mono [elimify], simp+);
+ from Cons
+ have "?C (Suc pc) ins'" by blast
+ with wt fits pc
+ have IH: "?len (Suc pc) \\<longrightarrow> ?wtl (Suc pc) ins'" by auto
- with a;
- show ?thesis;
- proof (elim, intro);
- fix s1;
- assume "G \\<turnstile> s1 <=s s1'" "G \\<turnstile> s1' <=s phi ! Suc pc";
- show "G \\<turnstile> s1 <=s phi ! Suc pc"; by (rule sup_state_trans);
- qed auto;
- qed
-
- thus ?thesis
- proof (elim exE conjE);
- fix s1;
- assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc";
- assume Gs1: "G \\<turnstile> s1 <=s phi ! Suc pc" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s)"; *)
-
- with *
- have "\\<exists>s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)"; by blast
-
- with wto;
- show ?thesis; by (auto simp del: split_paired_Ex);
- qed
+ show "\\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
+ proof (cases "?len (Suc pc)")
+ case False
+ with pc
+ have "ins' = []" by simp
+ with i o
+ show ?thesis by auto
+ next
+ case True
+ with IH
+ have "?wtl (Suc pc) ins'" by blast
+ with G'
+ obtain s' where
+ "wtl_inst_list ins' G rT s2 s' cert (length all_ins) (Suc pc)"
+ by - (elim allE impE, auto)
+ with i o
+ show ?thesis by auto
qed
qed
qed
-
+
lemma fits_imp_wtl_method_complete:
-"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert";
+"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
(rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex);
@@ -560,5 +541,6 @@
qed;
qed
+lemmas [simp] = split_paired_Ex
end
--- a/src/HOL/MicroJava/BV/Step.thy Tue Aug 08 16:57:44 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Wed Aug 09 11:53:00 2000 +0200
@@ -10,7 +10,7 @@
theory Step = Convert :
-(* effect of instruction on the state type *)
+text "Effect of instruction on the state type"
consts
step :: "instr \\<times> jvm_prog \\<times> state_type \\<Rightarrow> state_type option"
@@ -39,7 +39,7 @@
"step (i,G,s) = None"
-(* conditions under which step is applicable *)
+text "Conditions under which step is applicable"
consts
app :: "instr \\<times> jvm_prog \\<times> ty \\<times> state_type \\<Rightarrow> bool"
@@ -84,7 +84,8 @@
"app (i,G,rT,s) = False"
-(* p_count of successor instructions *)
+text {* \isa{p_count} of successor instructions *}
+
consts
succs :: "instr \\<Rightarrow> p_count \\<Rightarrow> p_count set"
@@ -131,15 +132,21 @@
with * show ?thesis by (auto dest: 0)
qed
+text {*
+\mdeskip
+simp rules for \isa{app} without patterns, better suited for proofs
+\medskip
+*}
+
lemma appStore[simp]:
-"app (Store idx, G, rT, s) = (\\<exists> ts ST LT. s = (ts#ST,LT) \\<and> idx < length LT)" (is "?app s = ?P s")
+"app (Store idx, G, rT, s) = (\\<exists> ts ST LT. s = (ts#ST,LT) \\<and> idx < length LT)"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appGetField[simp]:
"app (Getfield F C, G, rT, s) = (\\<exists> oT ST LT. s = (oT#ST, LT) \\<and> is_class G C \\<and>
fst (the (field (G,C) F)) = C \\<and>
- field (G,C) F \\<noteq> None \\<and> G \\<turnstile> oT \\<preceq> (Class C))" (is "?app s = ?P s")
+ field (G,C) F \\<noteq> None \\<and> G \\<turnstile> oT \\<preceq> (Class C))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
@@ -147,36 +154,36 @@
"app (Putfield F C, G, rT, s) = (\\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \\<and> is_class G C \\<and>
field (G,C) F \\<noteq> None \\<and> fst (the (field (G,C) F)) = C \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))" (is "?app s = ?P s")
+ G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appCheckcast[simp]:
-"app (Checkcast C, G, rT, s) = (\\<exists>rT ST LT. s = (RefT rT#ST,LT) \\<and> is_class G C)" (is "?app s = ?P s")
+"app (Checkcast C, G, rT, s) = (\\<exists>rT ST LT. s = (RefT rT#ST,LT) \\<and> is_class G C)"
by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
lemma appPop[simp]:
-"app (Pop, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s")
+"app (Pop, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup[simp]:
-"app (Dup, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s")
+"app (Dup, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup_x1[simp]:
-"app (Dup_x1, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s")
+"app (Dup_x1, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup_x2[simp]:
-"app (Dup_x2, G, rT, s) = (\\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"(is "?app s = ?P s")
+"app (Dup_x2, G, rT, s) = (\\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appSwap[simp]:
-"app (Swap, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s")
+"app (Swap, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
@@ -250,469 +257,5 @@
qed
lemmas [simp del] = app_invoke
-lemmas [trans] = sup_loc_trans
-
-ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
-ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
-
-
-
-lemma app_step_some:
-"\\<lbrakk>app (i,G,rT,s); succs i pc \\<noteq> {} \\<rbrakk> \\<Longrightarrow> step (i,G,s) \\<noteq> None";
-by (cases s, cases i, auto)
-
-lemma sup_state_length:
-"G \\<turnstile> s2 <=s s1 \\<Longrightarrow> length (fst s2) = length (fst s1) \\<and> length (snd s2) = length (snd s1)"
- by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
-
-lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
-proof
- show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p" by blast
-
- show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p"
- proof (cases xb)
- fix prim
- assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p"
- thus ?thesis by simp
- next
- fix ref
- assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref"
- thus ?thesis by simp (rule widen_RefT [elimify], auto)
- qed
-qed
-
-lemma sup_loc_some [rulify]:
-"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct "?P" b)
- show "?P []" by simp
-
- case Cons
- show "?P (a#list)"
- proof (clarsimp simp add: list_all2_Cons1 sup_loc_def)
- fix z zs n
- assume * :
- "G \\<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
- "n < Suc (length zs)" "(z # zs) ! n = Some t"
-
- show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t"
- proof (cases n)
- case 0
- with * show ?thesis by (simp add: sup_ty_opt_some)
- next
- case Suc
- with Cons *
- show ?thesis by (simp add: sup_loc_def)
- qed
- qed
-qed
-
-
-lemma all_widen_is_sup_loc:
-"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
- (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a")
-proof (induct "a")
- show "?P []" by simp
-
- fix l ls assume Cons: "?P ls"
-
- show "?P (l#ls)"
- proof (intro allI impI)
- fix b
- assume "length (l # ls) = length (b::ty list)"
- with Cons
- show "?Q (l # ls) b" by - (cases b, auto)
- qed
-qed
-
-
-lemma append_length_n: "\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x")
-proof (induct "?P" "x")
- show "?P []" by simp
-
- fix l ls assume Cons: "?P ls"
-
- show "?P (l#ls)"
- proof (intro allI impI)
- fix n
- assume l: "n \\<le> length (l # ls)"
-
- show "\\<exists>a b. l # ls = a @ b \\<and> length a = n"
- proof (cases n)
- assume "n=0" thus ?thesis by simp
- next
- fix "n'" assume s: "n = Suc n'"
- with l
- have "n' \\<le> length ls" by simp
- hence "\\<exists>a b. ls = a @ b \\<and> length a = n'" by (rule Cons [rulify])
- thus ?thesis
- proof elim
- fix a b
- assume "ls = a @ b" "length a = n'"
- with s
- have "l # ls = (l#a) @ b \\<and> length (l#a) = n" by simp
- thus ?thesis by blast
- qed
- qed
- qed
-qed
-
-
-
-lemma rev_append_cons:
-"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n"
-proof -
- assume n: "n < length x"
- hence "n \\<le> length x" by simp
- hence "\\<exists>a b. x = a @ b \\<and> length a = n" by (rule append_length_n [rulify])
- thus ?thesis
- proof elim
- fix r d assume x: "x = r@d" "length r = n"
- with n
- have "\\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
-
- thus ?thesis
- proof elim
- fix b c
- assume "d = b#c"
- with x
- have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n" by simp
- thus ?thesis by blast
- qed
- qed
-qed
-
-
-lemma app_mono:
-"\\<lbrakk>G \\<turnstile> s2 <=s s1; app (i, G, rT, s1)\\<rbrakk> \\<Longrightarrow> app (i, G, rT, s2)";
-proof -
- assume G: "G \\<turnstile> s2 <=s s1"
- assume app: "app (i, G, rT, s1)"
-
- show ?thesis
- proof (cases i)
- case Load
-
- from G
- have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
-
- from G Load app
- have "G \\<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
-
- with G Load app l
- show ?thesis by clarsimp (drule sup_loc_some, simp+)
- next
- case Store
- with G app
- show ?thesis
- by - (cases s2,
- auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
- next
- case Bipush
- thus ?thesis by simp
- next
- case Aconst_null
- thus ?thesis by simp
- next
- case New
- with app
- show ?thesis by simp
- next
- case Getfield
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
- next
- case Putfield
-
- with app
- obtain vT oT ST LT b
- where s1: "s1 = (vT # oT # ST, LT)" and
- "field (G, cname) vname = Some (cname, b)"
- "is_class G cname" and
- oT: "G\\<turnstile> oT\\<preceq> (Class cname)" and
- vT: "G\\<turnstile> vT\\<preceq> b"
- by simp (elim exE conjE, simp, rule that)
- moreover
- from s1 G
- obtain vT' oT' ST' LT'
- where s2: "s2 = (vT' # oT' # ST', LT')" and
- oT': "G\\<turnstile> oT' \\<preceq> oT" and
- vT': "G\\<turnstile> vT' \\<preceq> vT"
- by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
- moreover
- from vT' vT
- have "G \\<turnstile> vT' \\<preceq> b" by (rule widen_trans)
- moreover
- from oT' oT
- have "G\\<turnstile> oT' \\<preceq> (Class cname)" by (rule widen_trans)
- ultimately
- show ?thesis
- by (auto simp add: Putfield)
- next
- case Checkcast
- with app G
- show ?thesis
- by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2)
- next
- case Return
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
- next
- case Pop
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
- next
- case Dup
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
- next
- case Dup_x1
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
- next
- case Dup_x2
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
- next
- case Swap
- with app G
- show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
- next
- case IAdd
- with app G
- show ?thesis
- by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
- next
- case Goto
- with app
- show ?thesis by simp
- next
- case Ifcmpeq
- with app G
- show ?thesis
- by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
- next
- case Invoke
-
- with app
- obtain apTs X ST LT where
- s1: "s1 = (rev apTs @ X # ST, LT)" and
- l: "length apTs = length list" and
- C: "G \\<turnstile> X \\<preceq> Class cname" and
- w: "\\<forall>x \\<in> set (zip apTs list). x \\<in> widen G" and
- m: "method (G, cname) (mname, list) \\<noteq> None"
- by (simp del: not_None_eq, elim exE conjE) (rule that)
-
- obtain apTs' X' ST' LT' where
- s2: "s2 = (rev apTs' @ X' # ST', LT')" and
- l': "length apTs' = length list"
- proof -
- from l s1 G
- have "length list < length (fst s2)"
- by (simp add: sup_state_length)
- hence "\\<exists>a b c. (fst s2) = rev a @ b # c \\<and> length a = length list"
- by (rule rev_append_cons [rulify])
- thus ?thesis
- by - (cases s2, elim exE conjE, simp, rule that)
- qed
-
- from l l'
- have "length (rev apTs') = length (rev apTs)" by simp
-
- from this s1 s2 G
- obtain
- G': "G \\<turnstile> (apTs',LT') <=s (apTs,LT)"
- "G \\<turnstile> X' \\<preceq> X" "G \\<turnstile> (ST',LT') <=s (ST,LT)"
- by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
-
- with C
- have C': "G \\<turnstile> X' \\<preceq> Class cname"
- by - (rule widen_trans, auto)
-
- from G'
- have "G \\<turnstile> map Some apTs' <=l map Some apTs"
- by (simp add: sup_state_def)
- also
- from l w
- have "G \\<turnstile> map Some apTs <=l map Some list"
- by (simp add: all_widen_is_sup_loc)
- finally
- have "G \\<turnstile> map Some apTs' <=l map Some list" .
-
- with l'
- have w': "\\<forall>x \\<in> set (zip apTs' list). x \\<in> widen G"
- by (simp add: all_widen_is_sup_loc)
-
- from Invoke s2 l' w' C' m
- show ?thesis
- by simp blast
- qed
-qed
-
-
-lemma step_mono:
-"\\<lbrakk>succs i pc \\<noteq> {}; app (i,G,rT,s2); G \\<turnstile> s1 <=s s2\\<rbrakk> \\<Longrightarrow>
- G \\<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
-proof (cases s1, cases s2)
- fix a1 b1 a2 b2
- assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
- assume succs: "succs i pc \\<noteq> {}"
- assume app2: "app (i,G,rT,s2)"
- assume G: "G \\<turnstile> s1 <=s s2"
-
- from G app2
- have app1: "app (i,G,rT,s1)" by (rule app_mono)
-
- from app1 app2 succs
- obtain a1' b1' a2' b2'
- where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
- by (auto dest: app_step_some);
-
- have "G \\<turnstile> (a1',b1') <=s (a2',b2')"
- proof (cases i)
- case Load
-
- with s app1
- obtain y where
- y: "nat < length b1" "b1 ! nat = Some y" by clarsimp
-
- from Load s app2
- obtain y' where
- y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
-
- from G s
- have "G \\<turnstile> b1 <=l b2" by (simp add: sup_state_def)
-
- with y y'
- have "G \\<turnstile> y \\<preceq> y'"
- by - (drule sup_loc_some, simp+)
-
- with Load G y y' s step app1 app2
- show ?thesis by (clarsimp simp add: sup_state_def)
- next
- case Store
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_def sup_loc_update)
- next
- case Bipush
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case New
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Aconst_null
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Getfield
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Putfield
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Checkcast
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Invoke
-
- with s app1
- obtain a X ST where
- s1: "s1 = (a @ X # ST, b1)" and
- l: "length a = length list"
- by (simp, elim exE conjE, simp)
-
- from Invoke s app2
- obtain a' X' ST' where
- s2: "s2 = (a' @ X' # ST', b2)" and
- l': "length a' = length list"
- by (simp, elim exE conjE, simp)
-
- from l l'
- have lr: "length a = length a'" by simp
-
- from lr G s s1 s2
- have "G \\<turnstile> (ST, b1) <=s (ST', b2)"
- by (simp add: sup_state_append_fst sup_state_Cons1)
-
- moreover
-
- from Invoke G s step app1 app2
- have "b1 = b1' \\<and> b2 = b2'" by simp
-
- ultimately
-
- have "G \\<turnstile> (ST, b1') <=s (ST', b2')" by simp
-
- with Invoke G s step app1 app2 s1 s2 l l'
- show ?thesis
- by (clarsimp simp add: sup_state_def)
- next
- case Return
- with succs have "False" by simp
- thus ?thesis by blast
- next
- case Pop
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Dup
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Dup_x1
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Dup_x2
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Swap
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case IAdd
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
- case Goto
- with G s step app1 app2
- show ?thesis by simp
- next
- case Ifcmpeq
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- qed
-
- with step
- show ?thesis by auto
-qed
-
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/StepMono.thy Wed Aug 09 11:53:00 2000 +0200
@@ -0,0 +1,480 @@
+(* Title: HOL/MicroJava/BV/Step.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 Technische Universitaet Muenchen
+*)
+
+header {* Monotonicity of \isa{step} and \isa{app} *}
+
+theory StepMono = Step :
+
+
+lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
+
+ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
+ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
+
+
+lemma app_step_some:
+"\\<lbrakk>app (i,G,rT,s); succs i pc \\<noteq> {} \\<rbrakk> \\<Longrightarrow> step (i,G,s) \\<noteq> None";
+by (cases s, cases i, auto)
+
+
+lemma sup_state_length:
+"G \\<turnstile> s2 <=s s1 \\<Longrightarrow> length (fst s2) = length (fst s1) \\<and> length (snd s2) = length (snd s1)"
+ by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
+
+
+lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
+proof
+ show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p" by blast
+
+ show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p"
+ proof (cases xb)
+ fix prim
+ assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p"
+ thus ?thesis by simp
+ next
+ fix ref
+ assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref"
+ thus ?thesis by simp (rule widen_RefT [elimify], auto)
+ qed
+qed
+
+
+lemma sup_loc_some [rulify]:
+"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b")
+proof (induct "?P" b)
+ show "?P []" by simp
+
+ case Cons
+ show "?P (a#list)"
+ proof (clarsimp simp add: list_all2_Cons1 sup_loc_def)
+ fix z zs n
+ assume * :
+ "G \\<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
+ "n < Suc (length zs)" "(z # zs) ! n = Some t"
+
+ show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t"
+ proof (cases n)
+ case 0
+ with * show ?thesis by (simp add: sup_ty_opt_some)
+ next
+ case Suc
+ with Cons *
+ show ?thesis by (simp add: sup_loc_def)
+ qed
+ qed
+qed
+
+
+lemma all_widen_is_sup_loc:
+"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
+ (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a")
+proof (induct "a")
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix b
+ assume "length (l # ls) = length (b::ty list)"
+ with Cons
+ show "?Q (l # ls) b" by - (cases b, auto)
+ qed
+qed
+
+
+lemma append_length_n [rulify]:
+"\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x")
+proof (induct "?P" "x")
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix n
+ assume l: "n \\<le> length (l # ls)"
+
+ show "\\<exists>a b. l # ls = a @ b \\<and> length a = n"
+ proof (cases n)
+ assume "n=0" thus ?thesis by simp
+ next
+ fix "n'" assume s: "n = Suc n'"
+ with l
+ have "n' \\<le> length ls" by simp
+ hence "\\<exists>a b. ls = a @ b \\<and> length a = n'" by (rule Cons [rulify])
+ thus ?thesis
+ proof elim
+ fix a b
+ assume "ls = a @ b" "length a = n'"
+ with s
+ have "l # ls = (l#a) @ b \\<and> length (l#a) = n" by simp
+ thus ?thesis by blast
+ qed
+ qed
+ qed
+qed
+
+
+
+lemma rev_append_cons:
+"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n"
+proof -
+ assume n: "n < length x"
+ hence "n \\<le> length x" by simp
+ hence "\\<exists>a b. x = a @ b \\<and> length a = n" by (rule append_length_n)
+ thus ?thesis
+ proof elim
+ fix r d assume x: "x = r@d" "length r = n"
+ with n
+ have "\\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
+
+ thus ?thesis
+ proof elim
+ fix b c
+ assume "d = b#c"
+ with x
+ have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n" by simp
+ thus ?thesis by blast
+ qed
+ qed
+qed
+
+
+lemma app_mono:
+"\\<lbrakk>G \\<turnstile> s2 <=s s1; app (i, G, rT, s1)\\<rbrakk> \\<Longrightarrow> app (i, G, rT, s2)";
+proof -
+ assume G: "G \\<turnstile> s2 <=s s1"
+ assume app: "app (i, G, rT, s1)"
+
+ show ?thesis
+ proof (cases i)
+ case Load
+
+ from G
+ have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
+
+ from G Load app
+ have "G \\<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
+
+ with G Load app l
+ show ?thesis by clarsimp (drule sup_loc_some, simp+)
+ next
+ case Store
+ with G app
+ show ?thesis
+ by - (cases s2,
+ auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
+ next
+ case Bipush
+ thus ?thesis by simp
+ next
+ case Aconst_null
+ thus ?thesis by simp
+ next
+ case New
+ with app
+ show ?thesis by simp
+ next
+ case Getfield
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+ next
+ case Putfield
+
+ with app
+ obtain vT oT ST LT b
+ where s1: "s1 = (vT # oT # ST, LT)" and
+ "field (G, cname) vname = Some (cname, b)"
+ "is_class G cname" and
+ oT: "G\\<turnstile> oT\\<preceq> (Class cname)" and
+ vT: "G\\<turnstile> vT\\<preceq> b"
+ by simp (elim exE conjE, simp, rule that)
+ moreover
+ from s1 G
+ obtain vT' oT' ST' LT'
+ where s2: "s2 = (vT' # oT' # ST', LT')" and
+ oT': "G\\<turnstile> oT' \\<preceq> oT" and
+ vT': "G\\<turnstile> vT' \\<preceq> vT"
+ by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+ moreover
+ from vT' vT
+ have "G \\<turnstile> vT' \\<preceq> b" by (rule widen_trans)
+ moreover
+ from oT' oT
+ have "G\\<turnstile> oT' \\<preceq> (Class cname)" by (rule widen_trans)
+ ultimately
+ show ?thesis
+ by (auto simp add: Putfield)
+ next
+ case Checkcast
+ with app G
+ show ?thesis
+ by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2)
+ next
+ case Return
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+ next
+ case Pop
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup_x1
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup_x2
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Swap
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case IAdd
+ with app G
+ show ?thesis
+ by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
+ next
+ case Goto
+ with app
+ show ?thesis by simp
+ next
+ case Ifcmpeq
+ with app G
+ show ?thesis
+ by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
+ next
+ case Invoke
+
+ with app
+ obtain apTs X ST LT where
+ s1: "s1 = (rev apTs @ X # ST, LT)" and
+ l: "length apTs = length list" and
+ C: "G \\<turnstile> X \\<preceq> Class cname" and
+ w: "\\<forall>x \\<in> set (zip apTs list). x \\<in> widen G" and
+ m: "method (G, cname) (mname, list) \\<noteq> None"
+ by (simp del: not_None_eq, elim exE conjE) (rule that)
+
+ obtain apTs' X' ST' LT' where
+ s2: "s2 = (rev apTs' @ X' # ST', LT')" and
+ l': "length apTs' = length list"
+ proof -
+ from l s1 G
+ have "length list < length (fst s2)"
+ by (simp add: sup_state_length)
+ hence "\\<exists>a b c. (fst s2) = rev a @ b # c \\<and> length a = length list"
+ by (rule rev_append_cons [rulify])
+ thus ?thesis
+ by - (cases s2, elim exE conjE, simp, rule that)
+ qed
+
+ from l l'
+ have "length (rev apTs') = length (rev apTs)" by simp
+
+ from this s1 s2 G
+ obtain
+ G': "G \\<turnstile> (apTs',LT') <=s (apTs,LT)" and
+ X : "G \\<turnstile> X' \\<preceq> X" and "G \\<turnstile> (ST',LT') <=s (ST,LT)"
+ by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
+
+ with C
+ have C': "G \\<turnstile> X' \\<preceq> Class cname"
+ by - (rule widen_trans, auto)
+
+ from G'
+ have "G \\<turnstile> map Some apTs' <=l map Some apTs"
+ by (simp add: sup_state_def)
+ also
+ from l w
+ have "G \\<turnstile> map Some apTs <=l map Some list"
+ by (simp add: all_widen_is_sup_loc)
+ finally
+ have "G \\<turnstile> map Some apTs' <=l map Some list" .
+
+ with l'
+ have w': "\\<forall>x \\<in> set (zip apTs' list). x \\<in> widen G"
+ by (simp add: all_widen_is_sup_loc)
+
+ from Invoke s2 l' w' C' m
+ show ?thesis
+ by simp blast
+ qed
+qed
+
+
+lemma step_mono:
+"\\<lbrakk>succs i pc \\<noteq> {}; app (i,G,rT,s2); G \\<turnstile> s1 <=s s2\\<rbrakk> \\<Longrightarrow>
+ G \\<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
+proof (cases s1, cases s2)
+ fix a1 b1 a2 b2
+ assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
+ assume succs: "succs i pc \\<noteq> {}"
+ assume app2: "app (i,G,rT,s2)"
+ assume G: "G \\<turnstile> s1 <=s s2"
+
+ from G app2
+ have app1: "app (i,G,rT,s1)" by (rule app_mono)
+
+ from app1 app2 succs
+ obtain a1' b1' a2' b2'
+ where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
+ by (auto dest: app_step_some);
+
+ have "G \\<turnstile> (a1',b1') <=s (a2',b2')"
+ proof (cases i)
+ case Load
+
+ with s app1
+ obtain y where
+ y: "nat < length b1" "b1 ! nat = Some y" by clarsimp
+
+ from Load s app2
+ obtain y' where
+ y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
+
+ from G s
+ have "G \\<turnstile> b1 <=l b2" by (simp add: sup_state_def)
+
+ with y y'
+ have "G \\<turnstile> y \\<preceq> y'"
+ by - (drule sup_loc_some, simp+)
+
+ with Load G y y' s step app1 app2
+ show ?thesis by (clarsimp simp add: sup_state_def)
+ next
+ case Store
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_def sup_loc_update)
+ next
+ case Bipush
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case New
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Aconst_null
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Getfield
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Putfield
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Checkcast
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Invoke
+
+ with s app1
+ obtain a X ST where
+ s1: "s1 = (a @ X # ST, b1)" and
+ l: "length a = length list"
+ by (simp, elim exE conjE, simp)
+
+ from Invoke s app2
+ obtain a' X' ST' where
+ s2: "s2 = (a' @ X' # ST', b2)" and
+ l': "length a' = length list"
+ by (simp, elim exE conjE, simp)
+
+ from l l'
+ have lr: "length a = length a'" by simp
+
+ from lr G s s1 s2
+ have "G \\<turnstile> (ST, b1) <=s (ST', b2)"
+ by (simp add: sup_state_append_fst sup_state_Cons1)
+
+ moreover
+
+ from Invoke G s step app1 app2
+ have "b1 = b1' \\<and> b2 = b2'" by simp
+
+ ultimately
+
+ have "G \\<turnstile> (ST, b1') <=s (ST', b2')" by simp
+
+ with Invoke G s step app1 app2 s1 s2 l l'
+ show ?thesis
+ by (clarsimp simp add: sup_state_def)
+ next
+ case Return
+ with succs have "False" by simp
+ thus ?thesis by blast
+ next
+ case Pop
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x1
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x2
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Swap
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case IAdd
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Goto
+ with G s step app1 app2
+ show ?thesis by simp
+ next
+ case Ifcmpeq
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ qed
+
+ with step
+ show ?thesis by auto
+qed
+
+
+
+end