Theory Correctness1

(*  Title:      Jinja/Compiler/Correctness1.thy
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

section ‹Correctness of Stage 1›

theory Correctness1
imports J1WellForm Compiler1
begin

subsection‹Correctness of program compilation›

primrec unmod :: "expr1  nat  bool"
  and unmods :: "expr1 list  nat  bool" where
"unmod (new C) i = True" |
"unmod (Cast C e) i = unmod e i" |
"unmod (Val v) i = True" |
"unmod (e1 «bop» e2) i = (unmod e1 i  unmod e2 i)" |
"unmod (Var i) j = True" |
"unmod (i:=e) j = (i  j  unmod e j)" |
"unmod (eF{D}) i = unmod e i" |
"unmod (e1F{D}:=e2) i = (unmod e1 i  unmod e2 i)" |
"unmod (eM(es)) i = (unmod e i  unmods es i)" |
"unmod {j:T; e} i = unmod e i" |
"unmod (e1;;e2) i = (unmod e1 i   unmod e2 i)" |
"unmod (if (e) e1 else e2) i = (unmod e i  unmod e1 i  unmod e2 i)" |
"unmod (while (e) c) i = (unmod e i  unmod c i)" |
"unmod (throw e) i = unmod e i" |
"unmod (try e1 catch(C i) e2) j = (unmod e1 j  (if i=j then False else unmod e2 j))" |

"unmods ([]) i = True" |
"unmods (e#es) i = (unmod e i  unmods es i)"

lemma hidden_unmod: "Vs. hidden Vs i  unmod (compE1 Vs e) i" and
 "Vs. hidden Vs i  unmods (compEs1 Vs es) i"
(*<*)
proof(induct e and es rule: compE1.induct compEs1.induct)
  case TryCatch
  then show ?case by(simp add:hidden_inacc)(auto simp add:hidden_def)
qed (simp_all add:hidden_inacc)
(*>*)


lemma eval1_preserves_unmod:
  " P 1 e,(h,ls)  e',(h',ls'); unmod e i; i < size ls 
   ls ! i = ls' ! i"
and " P 1 es,(h,ls) [⇒] es',(h',ls'); unmods es i; i < size ls 
       ls ! i = ls' ! i"
(*<*)
proof(induct rule:eval1_evals1_inducts)
qed(auto dest!:eval1_preserves_len evals1_preserves_len split:if_split_asm)
(*>*)


lemma LAss_lem:
  "x  set xs; size xs  size ys 
   m1 m m2(xs[↦]ys)  m1(xy) m m2(xs[↦]ys[last_index xs x := y])"
(*<*)
by(simp add:map_le_def fun_upds_apply eq_sym_conv)
(*>*)
lemma Block_lem:
fixes l :: "'a  'b"
assumes 0: "l m [Vs [↦] ls]"
    and 1: "l' m [Vs [↦] ls', Vv]"
    and hidden: "V  set Vs  ls ! last_index Vs V = ls' ! last_index Vs V"
    and size: "size ls = size ls'"    "size Vs < size ls'"
shows "l'(V := l V) m [Vs [↦] ls']"
(*<*)
proof -
  have "l'(V := l V) m [Vs [↦] ls', Vv](V := l V)"
    using 1 by(rule map_le_upd)
  also have " = [Vs [↦] ls'](V := l V)" by simp
  also have " m [Vs [↦] ls']"
  proof (cases "l V")
    case None thus ?thesis by simp
  next
    case (Some w)
    hence "[Vs [↦] ls] V = Some w"
      using 0 by(force simp add: map_le_def split:if_splits)
    hence VinVs: "V  set Vs" and w: "w = ls ! last_index Vs V"
      using size by(auto simp add:fun_upds_apply split:if_splits)
    hence "w = ls' ! last_index Vs V" using hidden[OF VinVs] by simp
    hence "[Vs [↦] ls'](V := l V) = [Vs [↦] ls']" using Some size VinVs
      by(simp add: map_upds_upd_conv_last_index)
    thus ?thesis by simp
  qed
  finally show ?thesis .
qed
(*>*)

(*<*)
declare fun_upd_apply[simp del]
(*>*)


text‹\noindent The main theorem:›

theorem assumes wf: "wwf_J_prog P"
shows eval1_eval: "P  e,(h,l)  e',(h',l')
   (Vs ls.  fv e  set Vs;  l m [Vs[↦]ls]; size Vs + max_vars e  size ls 
        ls'. compP1 P 1 compE1 Vs e,(h,ls)  fin1 e',(h',ls')  l' m [Vs[↦]ls'])"
(*<*)
  (is "_  (Vs ls. PROP ?P e h l e' h' l' Vs ls)"
   is "_  (Vs ls.  _; _; _   ls'. ?Post e h l e' h' l' Vs ls ls')")
(*>*)

and evals1_evals: "P  es,(h,l) [⇒] es',(h',l')
     (Vs ls.  fvs es  set Vs;  l m [Vs[↦]ls]; size Vs + max_varss es  size ls 
          ls'. compP1 P 1 compEs1 Vs es,(h,ls) [⇒] compEs1 Vs es',(h',ls') 
                      l' m [Vs[↦]ls'])"
(*<*)
  (is "_  (Vs ls. PROP ?Ps es h l es' h' l' Vs ls)"
   is "_  (Vs ls.  _; _; _  ls'. ?Posts es h l es' h' l' Vs ls ls')")
proof (induct rule:eval_evals_inducts)
  case Nil thus ?case by(fastforce intro!:Nil1)
next
  case (Cons e h l v h' l' es es' h2 l2)
  have "PROP ?P e h l (Val v) h' l' Vs ls" by fact
  with Cons.prems
  obtain ls' where 1: "?Post e h l (Val v) h' l' Vs ls ls'"
    "size ls = size ls'" by(auto intro!:eval1_preserves_len)
  have "PROP ?Ps es h' l' es' h2 l2 Vs ls'" by fact
  with 1 Cons.prems
  obtain ls2 where 2: "?Posts es h' l' es' h2 l2 Vs ls' ls2" by(auto)
  from 1 2 Cons show ?case by(auto intro!:Cons1)
next
  case ConsThrow thus ?case
    by(fastforce intro!:ConsThrow1 dest: eval_final)
next
  case (Block e h l V e' h' l' T)
  let ?Vs = "Vs @ [V]"
  have IH:
  "fv e  set ?Vs; l(V := None) m [?Vs [↦] ls];
    size ?Vs + max_vars e  size ls
    ls'. compP1 P 1 compE1 ?Vs e,(h,ls)  fin1 e',(h', ls') 
             l' m [?Vs [↦] ls']" and
  fv: "fv {V:T; e}  set Vs" and rel: "l m [Vs [↦] ls]" and
  len: "length Vs + max_vars {V:T; e}  length ls" by fact+
  have len': "length Vs < length ls" using len by auto
  have "fv e  set ?Vs" using fv by auto
  moreover have "l(V := None) m [?Vs [↦] ls]" using rel len' by simp
  moreover have "size ?Vs + max_vars e  size ls" using len by simp
  ultimately obtain ls' where
   1: "compP1 P 1 compE1 ?Vs e,(h,ls)  fin1 e',(h',ls')"
   and rel': "l' m [?Vs [↦] ls']" using IH by blast
  have [simp]: "length ls = length ls'" by(rule eval1_preserves_len[OF 1])
  show "ls'. compP1 P 1 compE1 Vs {V:T; e},(h,ls)  fin1 e',(h',ls')
               l'(V := l V) m [Vs [↦] ls']" (is "ls'. ?R ls'")
  proof
    show "?R ls'"
    proof
      show "compP1 P 1 compE1 Vs {V:T; e},(h,ls)  fin1 e',(h',ls')"
        using 1 by(simp add:Block1)
    next
      show "l'(V := l V) m [Vs [↦] ls']"
      proof -
        have "l' m [Vs [↦] ls', V  ls' ! length Vs]"
          using len' rel' by simp
        moreover
        { assume VinVs: "V  set Vs"
          hence "hidden (Vs @ [V]) (last_index Vs V)"
            by(rule hidden_last_index)
          hence "unmod (compE1 (Vs @ [V]) e) (last_index Vs V)"
            by(rule hidden_unmod)
          moreover have "last_index Vs V < length ls"
            using len' VinVs by simp
          ultimately have "ls ! last_index Vs V = ls' ! last_index Vs V"
            by(rule eval1_preserves_unmod[OF 1])
        }
        ultimately show ?thesis using Block_lem[OF rel] len' by auto
      qed
    qed
  qed
next
  case (TryThrow e' h l a h' l' D fs C V e2)
  have "PROP ?P e' h l (Throw a) h' l' Vs ls" by fact
  with TryThrow.prems
  obtain ls' where 1: "?Post e' h l (Throw a) h' l' Vs ls ls'"  by(auto)
  show ?case using 1 TryThrow.hyps by(auto intro!:eval1_evals1.TryThrow1)
next
  case (TryCatch e1 h l a h1 l1 D fs C e2 V e' h2 l2)
  let ?e = "try e1 catch(C V) e2"
  have IH1: "fv e1  set Vs; l m [Vs [↦] ls];
              size Vs + max_vars e1  length ls
           ls1. compP1 P 1 compE1 Vs e1,(h,ls) 
                                fin1 (Throw a),(h1,ls1) 
                    l1 m [Vs [↦] ls1]" and
    fv: "fv ?e  set Vs" and
    rel: "l m [Vs [↦] ls]" and
    len: "length Vs + max_vars ?e  length ls" by fact+
  have "fv e1  set Vs" using fv by auto
  moreover have "length Vs + max_vars e1  length ls" using len by(auto)
  ultimately obtain ls1 where
    1: "compP1 P 1 compE1 Vs e1,(h,ls)  Throw a,(h1,ls1)"
    and rel1: "l1 m [Vs [↦] ls1]" using IH1 rel by fastforce
  from 1 have [simp]: "size ls = size ls1" by(rule eval1_preserves_len)
  let ?Vs = "Vs @ [V]" let ?ls = "(ls1[size Vs:=Addr a])"
  have IH2: "fv e2  set ?Vs; l1(V  Addr a) m [?Vs [↦] ?ls];
              length ?Vs + max_vars e2  length ?ls  ls2.
       compP1 P 1 compE1 ?Vs e2,(h1,?ls)  fin1 e',(h2, ls2) 
       l2 m [?Vs [↦] ls2]" by fact
  have len1: "size Vs < size ls1" using len by(auto)
  have "fv e2  set ?Vs" using fv by auto
  moreover have "l1(V  Addr a) m [?Vs [↦] ?ls]" using rel1 len1 by simp
  moreover have "length ?Vs + max_vars e2  length ?ls" using len by(auto)
  ultimately obtain ls2 where
    2: "compP1 P 1 compE1 ?Vs e2,(h1,?ls)  fin1 e',(h2, ls2)"
    and rel2: "l2 m [?Vs [↦] ls2]"  using IH2 by blast
  from 2 have [simp]: "size ls1 = size ls2"
    by(fastforce dest: eval1_preserves_len)
  show "ls2. compP1 P 1 compE1 Vs ?e,(h,ls)  fin1 e',(h2,ls2) 
              l2(V := l1 V) m [Vs [↦] ls2]"  (is "ls2. ?R ls2")
  proof
    show "?R ls2"
    proof
      have hp: "h1 a = Some (D, fs)" by fact
      have "P  D * C" by fact hence caught: "compP1 P  D * C" by simp
      from TryCatch1[OF 1 _ caught len1 2, OF hp]
      show "compP1 P 1 compE1 Vs ?e,(h,ls)  fin1 e',(h2,ls2)" by simp
    next
      show "l2(V := l1 V) m [Vs [↦] ls2]"
      proof -
        have "l2 m [Vs [↦] ls2, V  ls2 ! length Vs]"
          using len1 rel2 by simp
        moreover
        { assume VinVs: "V  set Vs"
          hence "hidden (Vs @ [V]) (last_index Vs V)" by(rule hidden_last_index)
          hence "unmod (compE1 (Vs @ [V]) e2) (last_index Vs V)"
            by(rule hidden_unmod)
          moreover have "last_index Vs V < length ?ls"
            using len1 VinVs by simp
          ultimately have "?ls ! last_index Vs V = ls2 ! last_index Vs V"
            by(rule eval1_preserves_unmod[OF 2])
          moreover have "last_index Vs V < size Vs" using VinVs by simp
          ultimately have "ls1 ! last_index Vs V = ls2 ! last_index Vs V"
            using len1 by(simp del:size_last_index_conv)
        }
        ultimately show ?thesis using Block_lem[OF rel1] len1  by simp
      qed
    qed
  qed
next
  case Try thus ?case by(fastforce intro!:Try1)
next
  case Throw thus ?case by(fastforce intro!:Throw1)
next
  case ThrowNull thus ?case by(fastforce intro!:ThrowNull1)
next
  case ThrowThrow thus ?case  by(fastforce intro!:ThrowThrow1)
next
  case (CondT e h l h1 l1 e1 e' h2 l2 e2)
  have "PROP ?P e h l true h1 l1 Vs ls" by fact
  with CondT.prems
  obtain ls1 where 1: "?Post e h l true h1 l1 Vs ls ls1"
    "size ls = size ls1"  by(auto intro!:eval1_preserves_len)
  have "PROP ?P e1 h1 l1 e' h2 l2 Vs ls1" by fact
  with 1 CondT.prems
  obtain ls2 where 2: "?Post e1 h1 l1 e' h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 show ?case by(auto intro!:CondT1)
next
  case (CondF e h l h1 l1 e2 e' h2 l2 e1 Vs ls)
  have "PROP ?P e h l false h1 l1 Vs ls" by fact
  with CondF.prems
  obtain ls1 where 1: "?Post e h l false h1 l1 Vs ls ls1"
    "size ls = size ls1"  by(auto intro!:eval1_preserves_len)
  have "PROP ?P e2 h1 l1 e' h2 l2 Vs ls1" by fact
  with 1 CondF.prems
  obtain ls2 where 2: "?Post e2 h1 l1 e' h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 show ?case by(auto intro!:CondF1)
next
  case CondThrow thus ?case by(fastforce intro!:CondThrow1)
next
  case (Seq e h l v h1 l1 e1 e' h2 l2)
  have "PROP ?P e h l (Val v) h1 l1 Vs ls" by fact
  with Seq.prems
  obtain ls1 where 1: "?Post e h l (Val v) h1 l1 Vs ls ls1"
    "size ls = size ls1"  by(auto intro!:eval1_preserves_len)
  have "PROP ?P e1 h1 l1 e' h2 l2 Vs ls1" by fact
  with 1 Seq.prems
  obtain ls2 where 2: "?Post e1 h1 l1 e' h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 Seq show ?case by(auto intro!:Seq1)
next
  case SeqThrow thus ?case by(fastforce intro!:SeqThrow1)
next
  case WhileF thus ?case by(fastforce intro!:eval1_evals1.intros)
next
  case (WhileT e h l h1 l1 c v h2 l2 e' h3 l3)
  have "PROP ?P e h l true h1 l1 Vs ls" by fact
  with WhileT.prems
  obtain ls1 where 1: "?Post e h l true h1 l1 Vs ls ls1"
    "size ls = size ls1"   by(auto intro!:eval1_preserves_len)
  have "PROP ?P c h1 l1 (Val v) h2 l2 Vs ls1" by fact
  with 1 WhileT.prems
  obtain ls2 where 2: "?Post c h1 l1 (Val v) h2 l2 Vs ls1 ls2"
    "size ls1 = size ls2"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P (While (e) c) h2 l2 e' h3 l3 Vs ls2" by fact
  with 1 2 WhileT.prems
  obtain ls3 where 3: "?Post (While (e) c) h2 l2 e' h3 l3 Vs ls2 ls3" by(auto)
  from 1 2 3 show ?case by(auto intro!:WhileT1)
next
  case (WhileBodyThrow e h l h1 l1 c e' h2 l2)
  have "PROP ?P e h l true h1 l1 Vs ls" by fact
  with WhileBodyThrow.prems
  obtain ls1 where 1: "?Post e h l true h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P c h1 l1 (throw e') h2 l2 Vs ls1" by fact
  with 1 WhileBodyThrow.prems
  obtain ls2 where 2: "?Post c h1 l1 (throw e') h2 l2 Vs ls1 ls2" by auto
  from 1 2 show ?case by(auto intro!:WhileBodyThrow1)
next
  case WhileCondThrow thus ?case by(fastforce intro!:WhileCondThrow1)
next
  case New thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case NewFail thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case Cast thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case CastNull thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case CastThrow thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case (CastFail e h l a h1 l1 D fs C)
  have "PROP ?P e h l (addr a) h1 l1 Vs ls" by fact
  with CastFail.prems
  obtain ls1 where 1: "?Post e h l (addr a) h1 l1 Vs ls ls1" by auto
  show ?case using 1 CastFail.hyps
    by(auto intro!:CastFail1[where D=D])
next
  case Val thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case (BinOp e h l v1 h1 l1 e1 v2 h2 l2 bop v)
  have "PROP ?P e h l (Val v1) h1 l1 Vs ls" by fact
  with BinOp.prems
  obtain ls1 where 1: "?Post e h l (Val v1) h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P e1 h1 l1 (Val v2) h2 l2 Vs ls1" by fact
  with 1 BinOp.prems
  obtain ls2 where 2: "?Post e1 h1 l1 (Val v2) h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 BinOp show ?case by(auto intro!:BinOp1)
next
  case (BinOpThrow2 e0 h l v1 h1 l1 e1 e h2 l2 bop)
  have "PROP ?P e0 h l (Val v1) h1 l1 Vs ls" by fact
  with BinOpThrow2.prems
  obtain ls1 where 1: "?Post e0 h l (Val v1) h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P e1 h1 l1 (throw e) h2 l2 Vs ls1" by fact
  with 1 BinOpThrow2.prems
  obtain ls2 where 2: "?Post e1 h1 l1 (throw e) h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 BinOpThrow2 show ?case by(auto intro!:BinOpThrow21)
next
  case BinOpThrow1 thus ?case  by(fastforce intro!:eval1_evals1.intros)
next
  case Var thus ?case
    by(force intro!:Var1 simp add: map_le_def fun_upds_apply)
next
  case LAss thus ?case
    by(fastforce simp add: LAss_lem intro:eval1_evals1.intros
                dest:eval1_preserves_len)
next
  case LAssThrow thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case FAcc thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case FAccNull thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case FAccThrow thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case (FAss e1 h l a h1 l1 e2 v h2 l2 C fs fs' F D h2')
  have "PROP ?P e1 h l (addr a) h1 l1 Vs ls" by fact
  with FAss.prems
  obtain ls1 where 1: "?Post e1 h l (addr a) h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P e2 h1 l1 (Val v) h2 l2 Vs ls1" by fact
  with 1 FAss.prems
  obtain ls2 where 2: "?Post e2 h1 l1 (Val v) h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 FAss show ?case by(auto intro!:FAss1)
next
  case (FAssNull e1 h l h1 l1 e2 v h2 l2 F D)
  have "PROP ?P e1 h l null h1 l1 Vs ls" by fact
  with FAssNull.prems
  obtain ls1 where 1: "?Post e1 h l null h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?P e2 h1 l1 (Val v) h2 l2 Vs ls1" by fact
  with 1 FAssNull.prems
  obtain ls2 where 2: "?Post e2 h1 l1 (Val v) h2 l2 Vs ls1 ls2" by(auto)
  from 1 2 FAssNull show ?case by(auto intro!:FAssNull1)
next
  case FAssThrow1 thus ?case by(fastforce intro:eval1_evals1.intros)
next
  case (FAssThrow2 e1 h l v h1 l1 e2 e h2 l2 F D)
  have "PROP ?P e1 h l (Val v) h1 l1 Vs ls" by fact
  with FAssThrow2.prems
  obtain ls1 where 1: "?Post e1 h l (Val v) h1 l1 Vs ls ls1"
    "size ls = size ls1"   by(auto intro!:eval1_preserves_len)
  have "PROP ?P e2 h1 l1 (throw e) h2 l2 Vs ls1" by fact
  with 1 FAssThrow2.prems
  obtain ls2 where 2: "?Post e2 h1 l1 (throw e) h2 l2 Vs ls1 ls2"  by(auto)
  from 1 2 FAssThrow2 show ?case by(auto intro!:FAssThrow21)
next
  case (CallNull e h l h1 l1 es vs h2 l2 M)
  have "PROP ?P e h l null h1 l1 Vs ls" by fact
  with CallNull.prems
  obtain ls1 where 1: "?Post e h l null h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?Ps es h1 l1 (map Val vs) h2 l2 Vs ls1" by fact
  with 1 CallNull.prems
  obtain ls2 where 2: "?Posts es h1 l1 (map Val vs) h2 l2 Vs ls1 ls2" by(auto)
  from 1 2 CallNull show ?case
    by (auto simp add: comp_def elim!: CallNull1)
next
  case CallObjThrow thus ?case  by(fastforce intro:eval1_evals1.intros)
next
  case (CallParamsThrow e h l v h1 l1 es vs ex es' h2 l2 M)
  have "PROP ?P e h l (Val v) h1 l1 Vs ls" by fact
  with CallParamsThrow.prems
  obtain ls1 where 1: "?Post e h l (Val v) h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?Ps es h1 l1 (map Val vs @ throw ex # es') h2 l2 Vs ls1" by fact
  with 1 CallParamsThrow.prems
  obtain ls2 where 2: "?Posts es h1 l1 (map Val vs @ throw ex # es') h2 l2 Vs ls1 ls2" by(auto)
  from 1 2 CallParamsThrow show ?case
    by (auto simp add: comp_def
             elim!: CallParamsThrow1 dest!:evals_final)
next
  case (Call e h l a h1 l1 es vs h2 l2 C fs M Ts T pns body D l2' b' h3 l3)
  have "PROP ?P e h l (addr a) h1 l1 Vs ls" by fact
  with Call.prems
  obtain ls1 where 1: "?Post e h l (addr a) h1 l1 Vs ls ls1"
    "size ls = size ls1"    by(auto intro!:eval1_preserves_len)
  have "PROP ?Ps es h1 l1 (map Val vs) h2 l2 Vs ls1" by fact
  with 1 Call.prems
  obtain ls2 where 2: "?Posts es h1 l1 (map Val vs) h2 l2 Vs ls1 ls2"
    "size ls1 = size ls2"    by(auto intro!:evals1_preserves_len)
  let ?Vs = "this#pns"
  let ?ls = "Addr a # vs @ replicate (max_vars body) undefined"
  have mdecl: "P  C sees M: TsT = (pns, body) in D" by fact
  have fv_body: "fv body  set ?Vs" and wf_size: "size Ts = size pns"
    using wf mdecl by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
  have mdecl1: "compP1 P  C sees M: TsT = (compE1 ?Vs body) in D"
    using sees_method_compP[OF mdecl, of "λ(pns,e). compE1 (this#pns) e"]
    by(simp)
  have [simp]: "l2' = [this  Addr a, pns [↦] vs]" by fact
  have Call_size: "size vs = size pns" by fact
  have "PROP ?P body h2 l2' b' h3 l3 ?Vs ?ls" by fact
  with 1 2 fv_body Call_size Call.prems
  obtain ls3 where 3: "?Post body h2 l2' b' h3 l3 ?Vs ?ls ls3"  by(auto)
  have hp: "h2 a = Some (C, fs)" by fact
  from 1 2 3 hp mdecl1 wf_size Call_size show ?case
    by(fastforce simp add: comp_def
                intro!: Call1 dest!:evals_final)
qed
(*>*)


subsection‹Preservation of well-formedness›

text‹The compiler preserves well-formedness. Is less trivial than it
may appear. We start with two simple properties: preservation of
well-typedness›

lemma compE1_pres_wt: "Vs Ts U.
   P,[Vs[↦]Ts]  e :: U; size Ts = size Vs 
   compP f P,Ts 1 compE1 Vs e :: U"
and  "Vs Ts Us.
   P,[Vs[↦]Ts]  es [::] Us; size Ts = size Vs 
   compP f P,Ts 1 compEs1 Vs es [::] Us"
(*<*)
proof(induct e and es rule: compE1.induct compEs1.induct)
  case Var then show ?case
    by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
next
  case LAss then show ?case
    by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
next
  case Call then show ?case
    by (fastforce dest!: sees_method_compP[where f = f])
next
  case Block then show ?case by (fastforce simp:nth_append)
next
  case TryCatch then show ?case by (fastforce simp:nth_append)
qed fastforce+
(*>*)

text‹\noindent and the correct block numbering:›

lemma : "Vs n. size Vs = n   (compE1 Vs e) n"
and ℬs: "Vs n. size Vs = n  ℬs (compEs1 Vs es) n"
(*<*)by (induct e and es rule: ℬ.induct ℬs.induct)
        (force | simp,metis length_append_singleton)+(*>*)

text‹The main complication is preservation of definite assignment
@{term"𝒟"}.›

lemma image_last_index: "A  set(xs@[x])  last_index (xs @ [x]) ` A =
  (if x  A then insert (size xs) (last_index xs ` (A-{x})) else last_index xs ` A)"
(*<*)
by(auto simp:image_def)
(*>*)


lemma A_compE1_None[simp]:
      "Vs. 𝒜 e = None  𝒜 (compE1 Vs e) = None"
and "Vs. 𝒜s es = None  𝒜s (compEs1 Vs es) = None"
(*<*)by(induct e and es rule: compE1.induct compEs1.induct)(auto simp:hyperset_defs)(*>*)


lemma A_compE1:
      "A Vs.  𝒜 e = A; fv e  set Vs   𝒜 (compE1 Vs e) = last_index Vs ` A"
and "A Vs.  𝒜s es = A; fvs es  set Vs   𝒜s (compEs1 Vs es) = last_index Vs ` A"
(*<*)
proof(induct e and es rule: fv.induct fvs.induct)
  case (Block V' T e)
  hence "fv e  set (Vs@[V'])" by fastforce
  moreover obtain B where "𝒜 e = B"
    using Block.prems by(simp add: hyperset_defs)
  moreover from calculation have "B  set (Vs@[V'])" by(auto dest!:A_fv)
  ultimately show ?case using Block
    by(auto simp add: hyperset_defs image_last_index last_index_size_conv)
next
  case (TryCatch e1 C V' e2)
  hence fve2: "fv e2  set (Vs@[V'])" by auto
  show ?case
  proof (cases "𝒜 e1")
    assume A1: "𝒜 e1 = None"
    then obtain A2 where A2: "𝒜 e2 = A2" using TryCatch
      by(simp add:hyperset_defs)
    hence "A2  set (Vs@[V'])" using TryCatch.prems A_fv[OF A2] by simp blast
    thus ?thesis using TryCatch fve2 A1 A2
      by(auto simp add:hyperset_defs image_last_index last_index_size_conv)
  next
    fix A1 assume A1: "𝒜 e1 =  A1"
    show ?thesis
    proof (cases  "𝒜 e2")
      assume A2: "𝒜 e2 = None"
      then show ?case using TryCatch A1 by(simp add:hyperset_defs)
    next
      fix A2 assume A2: "𝒜 e2 = A2"
      have "A1  set Vs" using TryCatch.prems A_fv[OF A1] by simp blast
      moreover
      have "A2  set (Vs@[V'])" using TryCatch.prems A_fv[OF A2] by simp blast
      ultimately show ?thesis using TryCatch A1 A2
        by (auto simp add: Diff_subset_conv last_index_size_conv subsetD hyperset_defs dest!: sym [of _ A])
    qed
  qed
next
  case (Cond e e1 e2)
  { assume "𝒜 e = None  𝒜 e1 = None  𝒜 e2 = None"
    hence ?case using Cond by (auto simp add: hyperset_defs)
  }
  moreover
  { fix A A1 A2
    assume "𝒜 e = A" and A1: "𝒜 e1 = A1" and A2: "𝒜 e2 = A2"
    moreover
    have "A1  set Vs" using Cond.prems A_fv[OF A1] by simp blast
    moreover
    have "A2  set Vs" using Cond.prems A_fv[OF A2] by simp blast
    ultimately have ?case using Cond
      by(auto simp add:hyperset_defs image_Un
          inj_on_image_Int[OF inj_on_last_index])
  }
  ultimately show ?case by fastforce
qed (auto simp add:hyperset_defs)
(*>*)


lemma D_None[iff]: "𝒟 (e::'a exp) None" and [iff]: "𝒟s (es::'a exp list) None"
(*<*)by(induct e and es rule: 𝒟.induct 𝒟s.induct)(simp_all)(*>*)


lemma D_last_index_compE1:
      "A Vs.  A  set Vs; fv e  set Vs  
                𝒟 e A  𝒟 (compE1 Vs e) last_index Vs ` A"
and "A Vs.  A  set Vs; fvs es  set Vs  
                𝒟s es A  𝒟s (compEs1 Vs es) last_index Vs ` A"
(*<*)
proof(induct e and es rule: 𝒟.induct 𝒟s.induct)
  case (BinOp e1 bop e2)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using BinOp by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] BinOp.prems  by auto
    have "A  A1  set Vs" using BinOp.prems A_fv[OF Some] by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` (A  A1)" using BinOp Some by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
next
  case (FAss e1 F D e2)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using FAss by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] FAss.prems  by auto
    have "A  A1  set Vs" using FAss.prems A_fv[OF Some] by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` (A  A1)" using FAss Some by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
next
  case (Call e1 M es)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using Call by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] Call.prems  by auto
    have "A  A1  set Vs" using Call.prems A_fv[OF Some] by auto
    hence "𝒟s (compEs1 Vs es) last_index Vs ` (A  A1)" using Call Some by auto
    hence "𝒟s (compEs1 Vs es) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
next
  case (TryCatch e1 C V e2)
  have " A{V}  set(Vs@[V]); fv e2  set(Vs@[V]); 𝒟 e2 A{V} 
        𝒟 (compE1 (Vs@[V]) e2) last_index (Vs@[V]) ` (A{V})" by fact
  hence "𝒟 (compE1 (Vs@[V]) e2) last_index (Vs@[V]) ` (A{V})"
    using TryCatch.prems by(simp add:Diff_subset_conv)
  moreover have "last_index (Vs@[V]) ` A  last_index Vs ` A  {size Vs}"
    using TryCatch.prems by(auto simp add: image_last_index split:if_split_asm)
  ultimately show ?case using TryCatch
    by(auto simp:hyperset_defs elim!:D_mono')
next
  case (Seq e1 e2)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using Seq by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] Seq.prems  by auto
    have "A  A1  set Vs" using Seq.prems A_fv[OF Some] by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` (A  A1)" using Seq Some by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
next
  case (Cond e e1 e2)
  hence IH1: "𝒟 (compE1 Vs e) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e")
    case None thus ?thesis using Cond by simp
  next
    case (Some B)
    have indexB: "𝒜 (compE1 Vs e) = last_index Vs ` B"
      using A_compE1[OF Some] Cond.prems  by auto
    have "A  B  set Vs" using Cond.prems A_fv[OF Some] by auto
    hence "𝒟 (compE1 Vs e1) last_index Vs ` (A  B)"
      and "𝒟 (compE1 Vs e2) last_index Vs ` (A  B)"
      using Cond Some by auto
    hence "𝒟 (compE1 Vs e1) last_index Vs ` A  last_index Vs ` B"
      and "𝒟 (compE1 Vs e2) last_index Vs ` A  last_index Vs ` B"
      by(simp add: image_Un)+
    thus ?thesis using IH1 indexB by auto
  qed
next
  case (While e1 e2)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using While by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] While.prems  by auto
    have "A  A1  set Vs" using While.prems A_fv[OF Some] by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` (A  A1)" using While Some by auto
    hence "𝒟 (compE1 Vs e2) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
next
  case (Block V T e)
  have " A-{V}  set(Vs@[V]); fv e  set(Vs@[V]); 𝒟 e A-{V}  
        𝒟 (compE1 (Vs@[V]) e) last_index (Vs@[V]) ` (A-{V})" by fact
  hence "𝒟 (compE1 (Vs@[V]) e) last_index (Vs@[V]) ` (A-{V})"
    using Block.prems by(simp add:Diff_subset_conv)
  moreover have "size Vs  last_index Vs ` A"
    using Block.prems by(auto simp add:image_def size_last_index_conv)
  ultimately show ?case using Block
    by(auto simp add: image_last_index Diff_subset_conv hyperset_defs elim!: D_mono')
next
  case (Cons_exp e1 es)
  hence IH1: "𝒟 (compE1 Vs e1) last_index Vs ` A" by simp
  show ?case
  proof (cases "𝒜 e1")
    case None thus ?thesis using Cons_exp by simp
  next
    case (Some A1)
    have indexA1: "𝒜 (compE1 Vs e1) = last_index Vs ` A1"
      using A_compE1[OF Some] Cons_exp.prems  by auto
    have "A  A1  set Vs" using Cons_exp.prems A_fv[OF Some] by auto
    hence "𝒟s (compEs1 Vs es) last_index Vs ` (A  A1)" using Cons_exp Some by auto
    hence "𝒟s (compEs1 Vs es) last_index Vs ` A  last_index Vs ` A1"
      by(simp add: image_Un)
    thus ?thesis using IH1 indexA1 by auto
  qed
qed (simp_all add:hyperset_defs)
(*>*)


lemma last_index_image_set: "distinct xs  last_index xs ` set xs = {..<size xs}"
(*<*)by(induct xs rule:rev_induct) (auto simp add: image_last_index)(*>*)


lemma D_compE1:
  " 𝒟 e set Vs; fv e  set Vs; distinct Vs   𝒟 (compE1 Vs e) {..<length Vs}"
(*<*)by(fastforce dest!: D_last_index_compE1[OF subset_refl] simp add:last_index_image_set)(*>*)


lemma D_compE1':
assumes "𝒟 e set(V#Vs)" and "fv e  set(V#Vs)" and "distinct(V#Vs)"
shows "𝒟 (compE1 (V#Vs) e) {..length Vs}"
(*<*)
proof -
  have "{..size Vs} = {..<size(V#Vs)}" by auto
  thus ?thesis using assms by (simp only:)(rule D_compE1)
qed
(*>*)


lemma compP1_pres_wf: "wf_J_prog P  wf_J1_prog (compP1 P)"
(*<*)
proof -
  assume wf: "wf_J_prog P"
  let ?f = "(λ(pns, body). compE1 (this # pns) body)"
  let ?wf2 = "wf_J1_mdecl"

  { fix C M b Ts T m
    assume cM: "P  C sees M :  TsT = m in C"
      and wfm: "wf_mdecl wf_J_mdecl P C (M, Ts, T, m)"
    obtain pns body where [simp]: "m = (pns, body)" by(cases m) simp
    let ?E = "[pns [↦] Ts, this  Class C]"
    obtain T' where WT: "P,?E  body :: T'" and subT: "P  T'  T"
      using wfm by(auto simp: wf_mdecl_def)
    have fv: "fv body  dom ?E" by(rule WT_fv[OF WT])
    have "wf_mdecl ?wf2 (compP ?f P) C (M, Ts, T, ?f m)" using cM wfm fv
      by(clarsimp simp add:wf_mdecl_def wf_J1_mdecl_def)
        (fastforce intro!: compE1_pres_wt D_compE1' )
  }
  then show ?thesis by simp (rule wf_prog_compPI[OF _ wf])
qed
(*>*)


end