# HG changeset patch
# User kleing
# Date 976206144 -3600
# Node ID 4ea7f3e8e4710bd0f351ab98b5da59edd0b35c67
# Parent  dc3eff1b755621ed7ba438ad7f459d7e660d8e63
fixed and cleaned up wt[l]_jvm_prog proofs

diff -r dc3eff1b7556 -r 4ea7f3e8e471 src/HOL/MicroJava/BV/LBVComplete.thy
--- 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
diff -r dc3eff1b7556 -r 4ea7f3e8e471 src/HOL/MicroJava/BV/LBVCorrect.thy
--- 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
diff -r dc3eff1b7556 -r 4ea7f3e8e471 src/HOL/MicroJava/BV/LBVSpec.thy
--- 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