src/HOL/MicroJava/BV/LBVCorrect.thy

new ADD instruction

(*  Title:      HOL/MicroJava/BV/BVLcorrect.thy
    ID:         $Id$
    Author:     Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* Correctness of the LBV *}

theory LBVCorrect = LBVSpec:;

constdefs
fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool" 
"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow> 
                   wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow> 
                   wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow> 
                      ((cert!(pc+length a)      = None   \\<longrightarrow> phi!(pc+length a) = s1) \\<and> 
                       (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
  
fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert";

lemma fitsD: 
"fits phi is G rT s0 s2 cert \\<Longrightarrow>
 (a@(i#b) = is) \\<Longrightarrow>
 wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\<Longrightarrow>
 wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\<Longrightarrow>
 ((cert!(0+length a)     = None   \\<longrightarrow> phi!(0+length a) = s1) \\<and> 
 (\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))";
by (unfold fits_def fits_partial_def) blast;

lemma exists_list: "\\<exists>l. n < length l" (is "?Q n");
proof (induct "n"); 
  fix n;  assume "?Q n";
  thus "?Q (Suc n)";
  proof elim; 
    fix l; assume "n < length (l::'a list)";
    hence "Suc n < length (a#l)"; by simp;
    thus ?thesis; ..;
  qed;
qed auto;

lemma exists_phi:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> 
 \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi";
proof -;
  assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
  have "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc 
     \\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)"
    (is "?P is");
  proof (induct "?P" "is");
    case Nil; 
    show "?P []"; by (simp add: fits_partial_def exists_list);
    case Cons;
    show "?P (a#list)";
    proof (intro allI impI);
      fix s0 pc;
      assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc";
      thus "\\<exists>phi. pc + length (a # list) < length phi \\<and> 
                  fits_partial phi pc (a # list) G rT s0 s2 cert";
        obtain s1 where 
          opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and
          wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)";
          by auto; 
        with Cons;
        show ?thesis; 
          obtain phi where fits:   "fits_partial phi (Suc pc) list G rT s1 s2 cert" 
                       and length: "(Suc pc) + length list < length phi"; by blast;
          let "?A phi pc x s1'" = 
              "(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
               (\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)";          
          show ?thesis; 
          proof (cases "cert!pc");
            case None;            
            have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert"; 
            proof (unfold fits_partial_def, intro allI impI);
              fix x i y s1'; 
              assume * : 
                "x @ i # y = a # list"
                "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
                "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
              show "?A (phi[pc:= s0]) pc x s1'"; 
              proof (cases "x");
                assume "x = []";
                with * length None;
                show ?thesis; by simp;
              next;
                fix b l; assume Cons: "x = b#l";
                with fits *;
                have "?A (phi[pc:= s0]) (Suc pc) l s1'"; 
                proof (unfold fits_partial_def, elim allE impE);
                  from * Cons;
                  show "l @ i # y = list"; by simp; 
                  from Cons opt *; 
                  show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"; 
                    by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
                qed simp+;
                with Cons length;
                show ?thesis; by auto;
              qed;
            qed;
            with length;
            show ?thesis; by intro auto;
          next;
            fix c; assume Some: "cert!pc = Some c";
            have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert";
            proof (unfold fits_partial_def, intro allI impI);
              fix x i y s1'; 
              assume * : 
                "x @ i # y = a # list"
                "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
                "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
              show "?A (phi[pc:= c]) pc x s1'";
              proof (cases "x");
                assume "x = []";
                with length Some;
                show ?thesis; by simp;
              next;
                fix b l; assume Cons: "x = b#l";
                with fits *;
                have "?A (phi[pc:= c]) (Suc pc) l s1'"; 
                proof (unfold fits_partial_def, elim allE impE);
                  from * Cons;
                  show "l @ i # y = list"; by simp; 
                  from Cons opt *; 
                  show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"; 
                    by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
                qed simp+;
                with Cons length;
                show ?thesis; by auto;
              qed;
            qed;
            with length;
            show ?thesis; by intro auto;
          qed; 
        qed; 
      qed; 
    qed; 
  qed;  
  with all; 
  show ?thesis;  
  proof (elim exE allE impE conjE); 
    show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0"; by simp; 
  qed (auto simp add: fits_def);  
qed; 


lemma fits_lemma1:
"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow> 
  \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
proof intro;
  fix pc t;
  assume wtl:  "wtl_inst_list is G rT s0 s3 cert (length is) 0";
  assume fits: "fits phi is G rT s0 s3 cert";
  assume pc:   "pc < length is";
  assume cert: "cert ! pc = Some t";
  from pc;
  have "is \\<noteq> []"; by auto;
  hence cons: "\\<exists>i y. is = i#y"; by (simp add: neq_Nil_conv);
  from wtl pc;
  have "\\<exists>a b s1. a@b = is \\<and> length a = pc \\<and> 
                 wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<and> 
                 wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
    (is "\\<exists>a b s1. ?A a b \\<and> ?L a \\<and> ?W1 a s1 \\<and> ?W2 a b s1");
  by (rule wtl_partial [rulify]);
  with cons;
  show "phi ! pc = t";
  proof (elim exE conjE);
    fix a b s1 i y;
    assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y";
    with pc;
    have "b \\<noteq> []"; by auto;
    hence "\\<exists>b' bs. b = b'#bs"; by (simp add: neq_Nil_conv);
    thus ?thesis;
    proof (elim exE);
      fix b' bs; assume Cons: "b=b'#bs";
      with * fits cert;     
      show ?thesis; 
      proof (unfold fits_def fits_partial_def, elim allE impE); 
        from * Cons; show "a@b'#bs=is"; by simp;
      qed simp+;
    qed;
  qed;
qed;

lemma fits_lemma2:
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
  wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
  fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None; 
  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> 
 \\<Longrightarrow>  phi!(length a) = s1";
proof (unfold fits_def fits_partial_def, elim allE impE);
qed (auto simp del: split_paired_Ex);



lemma wtl_suc_pc:
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; 
  wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); 
  wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a)); 
  fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow> 
  b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
proof;
  assume f: "fits phi (a@i#b) G rT s0 s3 cert";
  assume "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
         "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
  and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
  hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append);
  assume "b \\<noteq> []";
  thus "G \\<turnstile> s2 <=s phi ! Suc (length a)";
    obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
    hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
    with f;
    show ?thesis;
    proof (rule fitsD [elimify]); 
      from Cons w;       
      show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
        by simp;
      from a; 
      show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;

      assume cert:
        "(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
         (\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
      show ?thesis;
      proof (cases "cert ! Suc (length a)");
        assume "cert ! Suc (length a) = None";
        with cert;
        have "s2 = phi ! Suc (length a)"; by simp; 
        thus ?thesis; by simp;
      next;
        fix t; assume "cert ! Suc (length a) = Some t";
        with cert;
        have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
        with cert Cons w;
        show ?thesis;  by (auto simp add: wtl_inst_option_def);
      qed;            
    qed;
  qed;
qed;

lemma wtl_lemma: 
"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
  wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1);
  wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1));
  fits phi (i1@i#i2) G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
  wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i");
proof -;
  assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1);
  assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)";
  assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))";
  assume f:  "fits phi (i1@i#i2) G rT s0 s3 cert";

  from w1 wo w2;
  have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0"; 
    by (rule wtl_cons_appendl);

  with f;  
  have c1: "\\<forall>t. cert ! (length i1) = Some t \\<longrightarrow> phi ! (length i1) = t";
    by intro (rule fits_lemma1 [rulify], auto);

  from w1 wo w2 f;
  have c2: "cert ! (length i1) = None \\<Longrightarrow> phi ! (length i1) = s1";
    by - (rule fits_lemma2);

  from wtl f;
  have c3: "\\<forall>pc t. pc < length(i1@i#i2) \\<longrightarrow> cert ! pc = Some t \\<longrightarrow> phi ! pc = t";
    by (rule fits_lemma1);

  from w1 wo w2 f;
  have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)"; 
    by (rule wtl_suc_pc [rulify]); 

  show ?thesis;
  proof (cases "i");
    case LS;    
    with wo suc;
    show ?thesis;
     by - (cases "load_and_store", 
        (cases "cert ! (length i1)",
         clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
         clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);      
  next;
    case CO;
    with wo suc;
    show ?thesis; 
     by - (cases "create_object" , 
           cases "cert ! (length i1)",
           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
  next;
    case MO;
    with wo suc;
    show ?thesis;
     by - (cases "manipulate_object" , 
           (cases "cert ! (length i1)",
            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
  next;
    case CH;
    with wo suc;
    show ?thesis;
     by - (cases "check_object" , cases "cert ! (length i1)",
           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
  next;
    case MI; 
    with wo suc;
    show ?thesis; 
     by - (cases "meth_inv", cases "cert ! (length i1)",
           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
           intro exI conjI, rule refl, simp, force,
           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def,
           intro exI conjI, rule refl, simp, force);
  next;
    case MR;
    with wo suc;
    show ?thesis;
      by - (cases "meth_ret" , cases "cert ! (length i1)",
            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
  next;
    case OS;
    with wo suc;
    show ?thesis;
     by - (cases "op_stack" , 
           (cases "cert ! (length i1)",
            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
  next;
    case BR;
    with wo suc;
    show ?thesis;
      by - (cases "branch", 
            (cases "cert ! (length i1)",
             clarsimp_tac simp add: c2 c3 wt_instr_def wtl_inst_option_def split_beta,
             clarsimp_tac simp add: c1 c3 wt_instr_def wtl_inst_option_def)+);
  qed;
qed;

lemma wtl_fits_wt:
"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> 
 \\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
proof intro;
  assume fits: "fits phi is G rT s0 s3 cert";

  fix pc;
  assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
     and pc:  "pc < length is";

  thus "wt_instr (is ! pc) G rT phi (length is) pc"; 
    obtain i1 i2' s1 where l: "i1 @ i2' = is" "length i1 = pc" and
      w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and 
      w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)"; 
      by (rule wtl_partial [rulify, elimify]) (elim, rule that);
    from l pc;
    have "i2' \\<noteq> []"; by auto;
    thus ?thesis; 
      obtain i i2 where c: "i2' = i#i2"; by (simp add: neq_Nil_conv) (elim, rule that);
      with w2 l;
      show ?thesis;
        obtain s2 where w3:
          "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
          "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"; by auto;
      
        from w1 l c;
        have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0"; by simp;

        from l c fits;
        have "fits phi (i1@i#i2) G rT s0 s3 cert"; by simp;
        with w4 w3;
        have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)"; by (rule wtl_lemma);
        with l c;
        show ?thesis; by (auto simp add: nth_append);
      qed;
    qed;
  qed;
qed;
    
lemma wtl_inst_list_correct:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> 
 \\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
proof -;
  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
  thus ?thesis;
    obtain phi where "fits phi is G rT s0 s2 cert";
      by (rule exists_phi [elimify]) blast;
    with wtl;
    show ?thesis;
     by (rule wtl_fits_wt [elimify]) blast;
  qed;
qed;
    
lemma fits_first:
"\\<lbrakk>is \\<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0; 
 fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
proof -;
  assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
  assume fits: "fits phi is G rT s0 s2 cert";
  assume "is \\<noteq> []";
  thus ?thesis; 
    obtain y ys where cons: "is = y#ys"; by (simp add: neq_Nil_conv) (elim, rule that); 
    from fits;
    show ?thesis; 
    proof (rule fitsD [elimify]);
      from cons; show "[]@y#ys = is"; by simp;
      from cons wtl; 
      show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])"; 
        by simp;

      assume cert:
        "(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
         (\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)";

      show ?thesis;
      proof (cases "cert!0");
        assume "cert!0 = None";
        with cert;
        show ?thesis; by simp;
      next;
        fix t; assume "cert!0 = Some t";
        with cert; 
        have "phi!0 = t"; by (simp del: split_paired_All);
        with cert cons wtl;
        show ?thesis; by (auto simp add: wtl_inst_option_def);
      qed;
    qed simp;
  qed; 
qed;
  
lemma wtl_method_correct:
"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi";
proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE);
  let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)";
  fix s2;
  assume neqNil: "ins \\<noteq> []";
  assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0";
  thus ?thesis;
    obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi";
      by (rule exists_phi [elimify]) blast; 
    with wtl;
    have allpc:
      "\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc";
      by elim (rule wtl_fits_wt [elimify]);
    from neqNil wtl fits;
    have "wt_start G C pTs mxl phi"; 
     by (elim conjE, unfold wt_start_def) (rule fits_first);
    with neqNil allpc fits;
    show ?thesis; by (auto simp add: wt_method_def);
  qed;
qed;

lemma unique_set:
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
  by (induct "l") auto;

lemma unique_epsilon:
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
  by (auto simp add: unique_set);

theorem wtl_correct:
"wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
proof (clarsimp_tac 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);

  show "\\<exists>Phi. Ball (set G) (wf_cdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
    (is "\\<exists>Phi. ?Q Phi");
  proof (intro exI);
    let "?Phi" = 
        "\\<lambda> C sig. let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
                   let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in\
                     \\<epsilon> phi. wt_method G C (snd sig) rT maxl b phi";
    from wtl_prog;
    show "?Q ?Phi";
    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,maxl,b). wt_method G C (snd sig) rT 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>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
               "unique bb";
        with 1 uniqueG;
        show "(\\<lambda>(sig,rT,mb).
          wf_mhead G sig rT \\<and>
          (\\<lambda>(maxl,b).
              wt_method G a (snd sig) rT maxl b 
               ((\\<lambda>(C,x,y,mdecls).
                    (\\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
                     (\\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \\<in> set mdecls \\<and> sg = sig))
                 (\\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\<in> set G \\<and> Cl = a))) mb) m";
          by - (drule bspec, assumption, 
                clarsimp_tac elim: wtl_method_correct [elimify],
                clarsimp_tac intro: selectI simp add: unique_epsilon); 
      qed;
    qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
  qed;
qed;
    

end;