--- a/src/HOL/MicroJava/BV/LBVComplete.thy Thu Dec 07 17:09:15 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Thu Dec 07 17:22:24 2000 +0100
@@ -30,10 +30,8 @@
map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
- "make_Cert G Phi == \<lambda> C sig.
- let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,mxs,mxl,b) = SOME (sg,rT,mxs,mxl,b). (sg,rT,mxs,mxl,b) \<in> set mdecls \<and> sg = sig
- in make_cert b (Phi C sig)"
+ "make_Cert G Phi == \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
+ in make_cert b (Phi C sig)"
lemmas [simp del] = split_paired_Ex
@@ -420,53 +418,33 @@
qed
-theorem wtl_complete:
+theorem wtl_complete:
"wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
-proof (unfold wt_jvm_prog_def)
-
- assume wfprog:
- "wf_prog (\<lambda>G C (sig,rT,mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) G"
-
- thus ?thesis (* DvO: braucht ewig :-( *)
- proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
- fix a aa ab b ac ba ad ae af bb
- assume 1 : "\<forall>(C,D,fs,ms)\<in>set G.
- Ball (set fs) (wf_fdecl G) \<and> unique fs \<and>
- (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and>
- (\<lambda>(mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) mb) \<and>
- unique ms \<and>
- (C \<noteq> Object \<longrightarrow>
- is_class G D \<and>
- (D, C) \<notin> (subcls1 G)^* \<and>
- (\<forall>(sig,rT,b)\<in>set ms.
- \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\<turnstile>rT\<preceq>rT'))"
- "(a, aa, ab, b) \<in> set G"
+proof -
+ assume wt: "wt_jvm_prog G Phi"
+
+ { fix C S fs mdecls sig rT code
+ assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
+ moreover
+ from wt obtain wf_mb where "wf_prog wf_mb G"
+ by (blast dest: wt_jvm_progD)
+ ultimately
+ have "method (G,C) sig = Some (C,rT,code)"
+ by (simp add: methd)
+ } note this [simp]
+
+ from wt
+ show ?thesis
+ apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
+ apply (drule bspec, assumption)
+ apply (clarsimp simp add: wf_mdecl_def)
+ apply (drule bspec, assumption)
+ apply (clarsimp simp add: make_Cert_def)
+ apply (clarsimp dest!: wtl_method_complete)
+ done
- assume uG : "unique G"
- assume b : "((ac, ba), ad, ae, af, bb) \<in> set b"
-
- from 1
- show "wtl_method G a ba ad ae af bb (make_Cert G Phi a (ac, ba))"
- proof (rule bspec [elim_format], clarsimp)
- assume ub : "unique b"
- assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and>
- (\<lambda>(mxs,mxl,b). wt_method G a (snd sig) rT mxs mxl b (Phi a sig)) mb"
- from m b
- show ?thesis
- proof (rule bspec [elim_format], clarsimp)
- assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))"
- with wfprog uG ub b 1
- show ?thesis
- by - (rule wtl_method_complete [elim_format], assumption+,
- simp add: make_Cert_def unique_epsilon unique_epsilon')
- qed
-oops
-(*
- qed
- qed
-qed
-*)
-
+qed
+
lemmas [simp] = split_paired_Ex
end
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Dec 07 17:09:15 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Dec 07 17:22:24 2000 +0100
@@ -281,58 +281,36 @@
theorem wtl_correct:
-"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
-(*
-proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
-
- assume wtl_prog: "wtl_jvm_prog G cert"
- thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def)
-
- from wtl_prog
- show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
+ "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
+proof -
+
+ assume wtl: "wtl_jvm_prog G cert"
- show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxs,maxl,b).
- wt_method G C (snd sig) rT maxs maxl b (Phi C sig)) G)"
- (is "\<exists>Phi. ?Q Phi")
- proof (intro exI)
- let "?Phi" = "\<lambda> C sig.
- let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,maxs,maxl,b) = SOME (sg,rT,maxs,maxl,b). (sg,rT,maxs,maxl,b) \<in> set mdecls \<and> sg = sig
- in SOME phi. wt_method G C (snd sig) rT maxs maxl b phi"
- from wtl_prog
- show "?Q ?Phi"
-*)
-sorry
-(*
-DvO: hier beginnt die Maschine wie blöd zu swappen
- proof (unfold wf_cdecl_def, intro)
- fix x a b aa ba ab bb m
- assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
- with wtl_prog
- show "wf_mdecl (\<lambda>G C (sig,rT,maxs,maxl,b).
- wt_method G C (snd sig) rT maxs maxl b (?Phi C sig)) G a m"
- proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def,
- elim conjE)
- apply_end (drule bspec, assumption, simp, elim conjE)
- assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and>
- (\<lambda>(maxs,maxl,b). wtl_method G a (snd sig) rT maxs maxl b (cert a sig)) mb"
- "unique bb"
- with 1 uniqueG
- show "(\<lambda>(sig,rT,mb).
- wf_mhead G sig rT \<and>
- (\<lambda>(maxs,maxl,b).
- wt_method G a (snd sig) rT maxs maxl b
- ((\<lambda>(C,x,y,mdecls).
- (\<lambda>(sig,rT,maxs,maxl,b). Eps (wt_method G C (snd sig) rT maxs maxl b))
- (SOME (sg,rT,maxs,maxl,b). (sg, rT, maxs, maxl, b) \<in> set mdecls \<and> sg = sig))
- (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
- by - (drule bspec, assumption,
- clarsimp dest!: wtl_method_correct,
- clarsimp intro!: someI simp add: unique_epsilon unique_epsilon')
- qed
- qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
- qed
-qed
-*)
+ let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in
+ SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi"
+
+ { fix C S fs mdecls sig rT code
+ assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
+ moreover
+ from wtl obtain wf_mb where "wf_prog wf_mb G"
+ by (auto simp add: wtl_jvm_prog_def)
+ ultimately
+ have "method (G,C) sig = Some (C,rT,code)"
+ by (simp add: methd)
+ } note this [simp]
+
+ from wtl
+ have "wt_jvm_prog G ?Phi"
+ apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
+ apply (drule bspec, assumption)
+ apply (clarsimp simp add: wf_mdecl_def)
+ apply (drule bspec, assumption)
+ apply (clarsimp dest!: wtl_method_correct)
+ apply (rule someI, assumption)
+ done
-end
+ thus ?thesis
+ by blast
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Thu Dec 07 17:09:15 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Dec 07 17:22:24 2000 +0100
@@ -26,7 +26,7 @@
"wtl_inst i G rT s cert maxs max_pc pc ==
if app i G maxs rT s \<and> check_cert i G s cert pc max_pc then
if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1))
- else Err";
+ else Err"
constdefs
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
@@ -45,7 +45,7 @@
"wtl_inst_list [] G rT cert maxs max_pc pc s = OK s"
"wtl_inst_list (i#is) G rT cert maxs max_pc pc s =
(let s' = wtl_cert i G rT s cert maxs max_pc pc in
- strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')";
+ strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')"
constdefs
@@ -68,7 +68,7 @@
(app i G maxs rT s \<and> (\<forall>pc' \<in> set (succs i pc).
pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and>
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
- by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
+ by (auto simp add: wtl_inst_def check_cert_def set_mem_eq)
lemma strict_Some [simp]:
"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
@@ -190,24 +190,41 @@
by (auto simp add: wtl_append min_def)
qed
-lemma unique_set:
-"(a,b,c,d)\<in>set l --> unique l --> (a',b',c',d') \<in> set l -->
- a = a' --> b=b' \<and> c=c' \<and> d=d'"
- by (induct "l") auto
-lemma unique_epsilon:
- "(a,b,c,d)\<in>set l --> unique l -->
- (SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
- by (auto simp add: unique_set)
+lemma methd:
+ "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
+ ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
+proof -
+ assume wf: "wf_prog wf_mb G"
+ assume C: "(C,S,fs,mdecls) \<in> set G"
-lemma unique_set':
-"(a,b,c,d,e)\<in>set l --> unique l --> (a',b',c',d',e') \<in> set l -->
- a = a' --> b=b' \<and> c=c' \<and> d=d' \<and> e=e'"
- by (induct "l") auto
+ assume m: "(sig,rT,code) \<in> set mdecls"
+ moreover
+ from wf
+ have "class G Object = Some (arbitrary, [], [])"
+ by simp
+ moreover
+ from wf C
+ have c: "class G C = Some (S,fs,mdecls)"
+ by (auto simp add: wf_prog_def intro: map_of_SomeI)
+ ultimately
+ have O: "C \<noteq> Object"
+ by auto
+
+ from wf C
+ have "unique mdecls"
+ by (unfold wf_prog_def wf_cdecl_def) auto
-lemma unique_epsilon':
- "(a,b,c,d,e)\<in>set l --> unique l -->
- (SOME (a',b',c',d',e'). (a',b',c',d',e') \<in> set l \<and> a'=a) = (a,b,c,d,e)"
- by (auto simp add: unique_set')
+ hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
+ by - (induct mdecls, auto)
+
+ with m
+ have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+ by (force intro: map_of_SomeI)
+
+ with wf C m c O
+ show ?thesis
+ by (auto dest: method_rec [of _ _ C])
+qed
end