--- 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