Theory Correctness1

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

header {* \isaheader{Correctness of Stage 1} *}

theory Correctness1
imports J1WellForm Compiler1
begin

section{*Correctness of program compilation *}

primrec unmod :: "expr⇣1 => nat => bool"
  and unmods :: "expr⇣1 list => nat => bool" where
"unmod (new C) i = True" |
"unmod (Cast C e) i = unmod e i" |
"unmod (Val v) i = True" |
"unmod (e⇣1 «bop» e⇣2) i = (unmod e⇣1 i ∧ unmod e⇣2 i)" |
"unmod (Var i) j = True" |
"unmod (i:=e) j = (i ≠ j ∧ unmod e j)" |
"unmod (e•F{D}) i = unmod e i" |
"unmod (e⇣1•F{D}:=e⇣2) i = (unmod e⇣1 i ∧ unmod e⇣2 i)" |
"unmod (e•M(es)) i = (unmod e i ∧ unmods es i)" |
"unmod {j:T; e} i = unmod e i" |
"unmod (e⇣1;;e⇣2) i = (unmod e⇣1 i ∧  unmod e⇣2 i)" |
"unmod (if (e) e⇣1 else e⇣2) i = (unmod e i ∧ unmod e⇣1 i ∧ unmod e⇣2 i)" |
"unmod (while (e) c) i = (unmod e i ∧ unmod c i)" |
"unmod (throw e) i = unmod e i" |
"unmod (try e⇣1 catch(C i) e⇣2) j = (unmod e⇣1 j ∧ (if i=j then False else unmod e⇣2 j))" |

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

lemma hidden_unmod: "!!Vs. hidden Vs i ==> unmod (compE⇣1 Vs e) i" and
 "!!Vs. hidden Vs i ==> unmods (compEs⇣1 Vs es) i"
(*<*)
apply(induct e and es)
apply (simp_all add:hidden_inacc)
apply(auto simp add:hidden_def)
done
(*>*)


lemma eval⇣1_preserves_unmod:
  "[| P \<turnstile>⇩1 ⟨e,(h,ls)⟩ => ⟨e',(h',ls')⟩; unmod e i; i < size ls |]
  ==> ls ! i = ls' ! i"
and "[| P \<turnstile>⇩1 ⟨es,(h,ls)⟩ [=>] ⟨es',(h',ls')⟩; unmods es i; i < size ls |]
      ==> ls ! i = ls' ! i"
(*<*)
apply(induct rule:eval⇣1_evals⇣1_inducts)
apply(auto dest!:eval⇣1_preserves_len split:split_if_asm)
done
(*>*)


lemma LAss_lem:
  "[|x ∈ set xs; size xs ≤ size ys |]
  ==> m⇣1 ⊆⇩m m⇣2(xs[\<mapsto>]ys) ==> m⇣1(x\<mapsto>y) ⊆⇩m m⇣2(xs[\<mapsto>]ys[last_index xs x := y])"
(*<*)
by(simp add:map_le_def fun_upds_apply eq_sym_conv)
(*>*)
lemma Block_lem:
fixes l :: "'a \<rightharpoonup> 'b"
assumes 0: "l ⊆⇩m [Vs [\<mapsto>] ls]"
    and 1: "l' ⊆⇩m [Vs [\<mapsto>] ls', V\<mapsto>v]"
    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 [\<mapsto>] ls']"
(*<*)
proof -
  have "l'(V := l V) ⊆⇩m [Vs [\<mapsto>] ls', V\<mapsto>v](V := l V)"
    using 1 by(rule map_le_upd)
  also have "… = [Vs [\<mapsto>] ls'](V := l V)" by simp
  also have "… ⊆⇩m [Vs [\<mapsto>] ls']"
  proof (cases "l V")
    case None thus ?thesis by simp
  next
    case (Some w)
    hence "[Vs [\<mapsto>] 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 [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] 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 eval⇣1_eval: "P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩
  ==> (!!Vs ls. [| fv e ⊆ set Vs;  l ⊆⇩m [Vs[\<mapsto>]ls]; size Vs + max_vars e ≤ size ls |]
       ==> ∃ls'. compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs e,(h,ls)⟩ => ⟨fin⇣1 e',(h',ls')⟩ ∧ l' ⊆⇩m [Vs[\<mapsto>]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 evals⇣1_evals: "P \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩
    ==> (!!Vs ls. [| fvs es ⊆ set Vs;  l ⊆⇩m [Vs[\<mapsto>]ls]; size Vs + max_varss es ≤ size ls |]
         ==> ∃ls'. compP⇣1 P \<turnstile>⇩1 ⟨compEs⇣1 Vs es,(h,ls)⟩ [=>] ⟨compEs⇣1 Vs es',(h',ls')⟩ ∧
                      l' ⊆⇩m [Vs[\<mapsto>]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!:Nil⇣1)
next
  case (Cons e h l v h' l' es es' h⇣2 l⇣2)
  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!:eval⇣1_preserves_len)
  have "PROP ?Ps es h' l' es' h⇣2 l⇣2 Vs ls'" by fact
  with 1 Cons.prems
  obtain ls⇣2 where 2: "?Posts es h' l' es' h⇣2 l⇣2 Vs ls' ls⇣2" by(auto)
  from 1 2 Cons show ?case by(auto intro!:Cons⇣1)
next
  case ConsThrow thus ?case
    by(fastforce intro!:ConsThrow⇣1 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 [\<mapsto>] ls];
    size ?Vs + max_vars e ≤ size ls|]
   ==> ∃ls'. compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 ?Vs e,(h,ls)⟩ => ⟨fin⇣1 e',(h', ls')⟩ ∧
             l' ⊆⇩m [?Vs [\<mapsto>] ls']" and
  fv: "fv {V:T; e} ⊆ set Vs" and rel: "l ⊆⇩m [Vs [\<mapsto>] 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 [\<mapsto>] ls]" using rel len' by simp
  moreover have "size ?Vs + max_vars e ≤ size ls" using len by simp
  ultimately obtain ls' where
   1: "compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 ?Vs e,(h,ls)⟩ => ⟨fin⇣1 e',(h',ls')⟩"
   and rel': "l' ⊆⇩m [?Vs [\<mapsto>] ls']" using IH by blast
  have [simp]: "length ls = length ls'" by(rule eval⇣1_preserves_len[OF 1])
  show "∃ls'. compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs {V:T; e},(h,ls)⟩ => ⟨fin⇣1 e',(h',ls')⟩
              ∧ l'(V := l V) ⊆⇩m [Vs [\<mapsto>] ls']" (is "∃ls'. ?R ls'")
  proof
    show "?R ls'"
    proof
      show "compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs {V:T; e},(h,ls)⟩ => ⟨fin⇣1 e',(h',ls')⟩"
        using 1 by(simp add:Block⇣1)
    next
      show "l'(V := l V) ⊆⇩m [Vs [\<mapsto>] ls']"
      proof -
        have "l' ⊆⇩m [Vs [\<mapsto>] ls', V \<mapsto> 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 (compE⇣1 (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 eval⇣1_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 e⇣2)
  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!:eval⇣1_evals⇣1.TryThrow⇣1)
next
  case (TryCatch e⇣1 h l a h⇣1 l⇣1 D fs C e⇣2 V e' h⇣2 l⇣2)
  let ?e = "try e⇣1 catch(C V) e⇣2"
  have IH⇣1: "[|fv e⇣1 ⊆ set Vs; l ⊆⇩m [Vs [\<mapsto>] ls];
              size Vs + max_vars e⇣1 ≤ length ls|]
          ==> ∃ls⇣1. compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs e⇣1,(h,ls)⟩ =>
                                ⟨fin⇣1 (Throw a),(h⇣1,ls⇣1)⟩ ∧
                    l⇣1 ⊆⇩m [Vs [\<mapsto>] ls⇣1]" and
    fv: "fv ?e ⊆ set Vs" and
    rel: "l ⊆⇩m [Vs [\<mapsto>] ls]" and
    len: "length Vs + max_vars ?e ≤ length ls" by fact+
  have "fv e⇣1 ⊆ set Vs" using fv by auto
  moreover have "length Vs + max_vars e⇣1 ≤ length ls" using len by(auto)
  ultimately obtain ls⇣1 where
    1: "compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs e⇣1,(h,ls)⟩ => ⟨Throw a,(h⇣1,ls⇣1)⟩"
    and rel⇣1: "l⇣1 ⊆⇩m [Vs [\<mapsto>] ls⇣1]" using IH⇣1 rel by fastforce
  from 1 have [simp]: "size ls = size ls⇣1" by(rule eval⇣1_preserves_len)
  let ?Vs = "Vs @ [V]" let ?ls = "(ls⇣1[size Vs:=Addr a])"
  have IH⇣2: "[|fv e⇣2 ⊆ set ?Vs; l⇣1(V \<mapsto> Addr a) ⊆⇩m [?Vs [\<mapsto>] ?ls];
              length ?Vs + max_vars e⇣2 ≤ length ?ls|] ==> ∃ls⇣2.
       compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 ?Vs e⇣2,(h⇣1,?ls)⟩ => ⟨fin⇣1 e',(h⇣2, ls⇣2)⟩ ∧
       l⇣2 ⊆⇩m [?Vs [\<mapsto>] ls⇣2]" by fact
  have len⇣1: "size Vs < size ls⇣1" using len by(auto)
  have "fv e⇣2 ⊆ set ?Vs" using fv by auto
  moreover have "l⇣1(V \<mapsto> Addr a) ⊆⇩m [?Vs [\<mapsto>] ?ls]" using rel⇣1 len⇣1 by simp
  moreover have "length ?Vs + max_vars e⇣2 ≤ length ?ls" using len by(auto)
  ultimately obtain ls⇣2 where
    2: "compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 ?Vs e⇣2,(h⇣1,?ls)⟩ => ⟨fin⇣1 e',(h⇣2, ls⇣2)⟩"
    and rel⇣2: "l⇣2 ⊆⇩m [?Vs [\<mapsto>] ls⇣2]"  using IH⇣2 by blast
  from 2 have [simp]: "size ls⇣1 = size ls⇣2"
    by(fastforce dest: eval⇣1_preserves_len)
  show "∃ls⇣2. compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs ?e,(h,ls)⟩ => ⟨fin⇣1 e',(h⇣2,ls⇣2)⟩ ∧
              l⇣2(V := l⇣1 V) ⊆⇩m [Vs [\<mapsto>] ls⇣2]"  (is "∃ls⇣2. ?R ls⇣2")
  proof
    show "?R ls⇣2"
    proof
      have hp: "h⇣1 a = Some (D, fs)" by fact
      have "P \<turnstile> D \<preceq>⇧* C" by fact hence caught: "compP⇣1 P \<turnstile> D \<preceq>⇧* C" by simp
      from TryCatch⇣1[OF 1 _ caught len⇣1 2, OF hp]
      show "compP⇣1 P \<turnstile>⇩1 ⟨compE⇣1 Vs ?e,(h,ls)⟩ => ⟨fin⇣1 e',(h⇣2,ls⇣2)⟩" by simp
    next
      show "l⇣2(V := l⇣1 V) ⊆⇩m [Vs [\<mapsto>] ls⇣2]"
      proof -
        have "l⇣2 ⊆⇩m [Vs [\<mapsto>] ls⇣2, V \<mapsto> ls⇣2 ! length Vs]"
          using len⇣1 rel⇣2 by simp
        moreover
        { assume VinVs: "V ∈ set Vs"
          hence "hidden (Vs @ [V]) (last_index Vs V)" by(rule hidden_last_index)
          hence "unmod (compE⇣1 (Vs @ [V]) e⇣2) (last_index Vs V)"
            by(rule hidden_unmod)
          moreover have "last_index Vs V < length ?ls"
            using len⇣1 VinVs by simp
          ultimately have "?ls ! last_index Vs V = ls⇣2 ! last_index Vs V"
            by(rule eval⇣1_preserves_unmod[OF 2])
          moreover have "last_index Vs V < size Vs" using VinVs by simp
          ultimately have "ls⇣1 ! last_index Vs V = ls⇣2 ! last_index Vs V"
            using len⇣1 by(simp del:size_last_index_conv)
        }
        ultimately show ?thesis using Block_lem[OF rel⇣1] len⇣1  by simp
      qed
    qed
  qed
next
  case Try thus ?case by(fastforce intro!:Try⇣1)
next
  case Throw thus ?case by(fastforce intro!:Throw⇣1)
next
  case ThrowNull thus ?case by(fastforce intro!:ThrowNull⇣1)
next
  case ThrowThrow thus ?case  by(fastforce intro!:ThrowThrow⇣1)
next
  case (CondT e h l h⇣1 l⇣1 e⇣1 e' h⇣2 l⇣2 e⇣2)
  have "PROP ?P e h l true h⇣1 l⇣1 Vs ls" by fact
  with CondT.prems
  obtain ls⇣1 where 1: "?Post e h l true h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"  by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣1 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 CondT.prems
  obtain ls⇣2 where 2: "?Post e⇣1 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 show ?case by(auto intro!:CondT⇣1)
next
  case (CondF e h l h⇣1 l⇣1 e⇣2 e' h⇣2 l⇣2 e⇣1 Vs ls)
  have "PROP ?P e h l false h⇣1 l⇣1 Vs ls" by fact
  with CondF.prems
  obtain ls⇣1 where 1: "?Post e h l false h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"  by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣2 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 CondF.prems
  obtain ls⇣2 where 2: "?Post e⇣2 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 show ?case by(auto intro!:CondF⇣1)
next
  case CondThrow thus ?case by(fastforce intro!:CondThrow⇣1)
next
  case (Seq e h l v h⇣1 l⇣1 e⇣1 e' h⇣2 l⇣2)
  have "PROP ?P e h l (Val v) h⇣1 l⇣1 Vs ls" by fact
  with Seq.prems
  obtain ls⇣1 where 1: "?Post e h l (Val v) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"  by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣1 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 Seq.prems
  obtain ls⇣2 where 2: "?Post e⇣1 h⇣1 l⇣1 e' h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 Seq show ?case by(auto intro!:Seq⇣1)
next
  case SeqThrow thus ?case by(fastforce intro!:SeqThrow⇣1)
next
  case WhileF thus ?case by(fastforce intro!:eval⇣1_evals⇣1.intros)
next
  case (WhileT e h l h⇣1 l⇣1 c v h⇣2 l⇣2 e' h⇣3 l⇣3)
  have "PROP ?P e h l true h⇣1 l⇣1 Vs ls" by fact
  with WhileT.prems
  obtain ls⇣1 where 1: "?Post e h l true h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"   by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P c h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 WhileT.prems
  obtain ls⇣2 where 2: "?Post c h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"
    "size ls⇣1 = size ls⇣2"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P (While (e) c) h⇣2 l⇣2 e' h⇣3 l⇣3 Vs ls⇣2" by fact
  with 1 2 WhileT.prems
  obtain ls⇣3 where 3: "?Post (While (e) c) h⇣2 l⇣2 e' h⇣3 l⇣3 Vs ls⇣2 ls⇣3" by(auto)
  from 1 2 3 show ?case by(auto intro!:WhileT⇣1)
next
  case (WhileBodyThrow e h l h⇣1 l⇣1 c e' h⇣2 l⇣2)
  have "PROP ?P e h l true h⇣1 l⇣1 Vs ls" by fact
  with WhileBodyThrow.prems
  obtain ls⇣1 where 1: "?Post e h l true h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P c h⇣1 l⇣1 (throw e') h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 WhileBodyThrow.prems
  obtain ls⇣2 where 2: "?Post c h⇣1 l⇣1 (throw e') h⇣2 l⇣2 Vs ls⇣1 ls⇣2" by auto
  from 1 2 show ?case by(auto intro!:WhileBodyThrow⇣1)
next
  case WhileCondThrow thus ?case by(fastforce intro!:WhileCondThrow⇣1)
next
  case New thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case NewFail thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case Cast thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case CastNull thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case CastThrow thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case (CastFail e h l a h⇣1 l⇣1 D fs C)
  have "PROP ?P e h l (addr a) h⇣1 l⇣1 Vs ls" by fact
  with CastFail.prems
  obtain ls⇣1 where 1: "?Post e h l (addr a) h⇣1 l⇣1 Vs ls ls⇣1" by auto
  show ?case using 1 CastFail.hyps
    by(auto intro!:CastFail⇣1[where D=D])
next
  case Val thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case (BinOp e h l v⇣1 h⇣1 l⇣1 e⇣1 v⇣2 h⇣2 l⇣2 bop v)
  have "PROP ?P e h l (Val v⇣1) h⇣1 l⇣1 Vs ls" by fact
  with BinOp.prems
  obtain ls⇣1 where 1: "?Post e h l (Val v⇣1) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣1 h⇣1 l⇣1 (Val v⇣2) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 BinOp.prems
  obtain ls⇣2 where 2: "?Post e⇣1 h⇣1 l⇣1 (Val v⇣2) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 BinOp show ?case by(auto intro!:BinOp⇣1)
next
  case (BinOpThrow2 e⇣0 h l v⇣1 h⇣1 l⇣1 e⇣1 e h⇣2 l⇣2 bop)
  have "PROP ?P e⇣0 h l (Val v⇣1) h⇣1 l⇣1 Vs ls" by fact
  with BinOpThrow2.prems
  obtain ls⇣1 where 1: "?Post e⇣0 h l (Val v⇣1) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣1 h⇣1 l⇣1 (throw e) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 BinOpThrow2.prems
  obtain ls⇣2 where 2: "?Post e⇣1 h⇣1 l⇣1 (throw e) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 BinOpThrow2 show ?case by(auto intro!:BinOpThrow⇣2⇣1)
next
  case BinOpThrow1 thus ?case  by(fastforce intro!:eval⇣1_evals⇣1.intros)
next
  case Var thus ?case
    by(force intro!:Var⇣1 simp add: map_le_def fun_upds_apply)
next
  case LAss thus ?case
    by(fastforce simp add: LAss_lem intro:eval⇣1_evals⇣1.intros
                dest:eval⇣1_preserves_len)
next
  case LAssThrow thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case FAcc thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case FAccNull thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case FAccThrow thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case (FAss e⇣1 h l a h⇣1 l⇣1 e⇣2 v h⇣2 l⇣2 C fs fs' F D h⇣2')
  have "PROP ?P e⇣1 h l (addr a) h⇣1 l⇣1 Vs ls" by fact
  with FAss.prems
  obtain ls⇣1 where 1: "?Post e⇣1 h l (addr a) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣2 h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 FAss.prems
  obtain ls⇣2 where 2: "?Post e⇣2 h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 FAss show ?case by(auto intro!:FAss⇣1)
next
  case (FAssNull e⇣1 h l h⇣1 l⇣1 e⇣2 v h⇣2 l⇣2 F D)
  have "PROP ?P e⇣1 h l null h⇣1 l⇣1 Vs ls" by fact
  with FAssNull.prems
  obtain ls⇣1 where 1: "?Post e⇣1 h l null h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣2 h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 FAssNull.prems
  obtain ls⇣2 where 2: "?Post e⇣2 h⇣1 l⇣1 (Val v) h⇣2 l⇣2 Vs ls⇣1 ls⇣2" by(auto)
  from 1 2 FAssNull show ?case by(auto intro!:FAssNull⇣1)
next
  case FAssThrow1 thus ?case by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case (FAssThrow2 e⇣1 h l v h⇣1 l⇣1 e⇣2 e h⇣2 l⇣2 F D)
  have "PROP ?P e⇣1 h l (Val v) h⇣1 l⇣1 Vs ls" by fact
  with FAssThrow2.prems
  obtain ls⇣1 where 1: "?Post e⇣1 h l (Val v) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"   by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?P e⇣2 h⇣1 l⇣1 (throw e) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 FAssThrow2.prems
  obtain ls⇣2 where 2: "?Post e⇣2 h⇣1 l⇣1 (throw e) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"  by(auto)
  from 1 2 FAssThrow2 show ?case by(auto intro!:FAssThrow⇣2⇣1)
next
  case (CallNull e h l h⇣1 l⇣1 es vs h⇣2 l⇣2 M)
  have "PROP ?P e h l null h⇣1 l⇣1 Vs ls" by fact
  with CallNull.prems
  obtain ls⇣1 where 1: "?Post e h l null h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?Ps es h⇣1 l⇣1 (map Val vs) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 CallNull.prems
  obtain ls⇣2 where 2: "?Posts es h⇣1 l⇣1 (map Val vs) h⇣2 l⇣2 Vs ls⇣1 ls⇣2" by(auto)
  from 1 2 CallNull show ?case
    by (auto simp add: comp_def elim!: CallNull⇣1)
next
  case CallObjThrow thus ?case  by(fastforce intro:eval⇣1_evals⇣1.intros)
next
  case (CallParamsThrow e h l v h⇣1 l⇣1 es vs ex es' h⇣2 l⇣2 M)
  have "PROP ?P e h l (Val v) h⇣1 l⇣1 Vs ls" by fact
  with CallParamsThrow.prems
  obtain ls⇣1 where 1: "?Post e h l (Val v) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?Ps es h⇣1 l⇣1 (map Val vs @ throw ex # es') h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 CallParamsThrow.prems
  obtain ls⇣2 where 2: "?Posts es h⇣1 l⇣1 (map Val vs @ throw ex # es') h⇣2 l⇣2 Vs ls⇣1 ls⇣2" by(auto)
  from 1 2 CallParamsThrow show ?case
    by (auto simp add: comp_def
             elim!: CallParamsThrow⇣1 dest!:evals_final)
next
  case (Call e h l a h⇣1 l⇣1 es vs h⇣2 l⇣2 C fs M Ts T pns body D l⇣2' b' h⇣3 l⇣3)
  have "PROP ?P e h l (addr a) h⇣1 l⇣1 Vs ls" by fact
  with Call.prems
  obtain ls⇣1 where 1: "?Post e h l (addr a) h⇣1 l⇣1 Vs ls ls⇣1"
    "size ls = size ls⇣1"    by(auto intro!:eval⇣1_preserves_len)
  have "PROP ?Ps es h⇣1 l⇣1 (map Val vs) h⇣2 l⇣2 Vs ls⇣1" by fact
  with 1 Call.prems
  obtain ls⇣2 where 2: "?Posts es h⇣1 l⇣1 (map Val vs) h⇣2 l⇣2 Vs ls⇣1 ls⇣2"
    "size ls⇣1 = size ls⇣2"    by(auto intro!:evals⇣1_preserves_len)
  let ?Vs = "this#pns"
  let ?ls = "Addr a # vs @ replicate (max_vars body) undefined"
  have mdecl: "P \<turnstile> C sees M: Ts->T = (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 mdecl⇣1: "compP⇣1 P \<turnstile> C sees M: Ts->T = (compE⇣1 ?Vs body) in D"
    using sees_method_compP[OF mdecl, of "λ(pns,e). compE⇣1 (this#pns) e"]
    by(simp)
  have [simp]: "l⇣2' = [this \<mapsto> Addr a, pns [\<mapsto>] vs]" by fact
  have Call_size: "size vs = size pns" by fact
  have "PROP ?P body h⇣2 l⇣2' b' h⇣3 l⇣3 ?Vs ?ls" by fact
  with 1 2 fv_body Call_size Call.prems
  obtain ls⇣3 where 3: "?Post body h⇣2 l⇣2' b' h⇣3 l⇣3 ?Vs ?ls ls⇣3"  by(auto)
  have hp: "h⇣2 a = Some (C, fs)" by fact
  from 1 2 3 hp mdecl⇣1 wf_size Call_size show ?case
    by(fastforce simp add: comp_def
                intro!: Call⇣1 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 compE⇣1_pres_wt: "!!Vs Ts U.
  [| P,[Vs[\<mapsto>]Ts] \<turnstile> e :: U; size Ts = size Vs |]
  ==> compP f P,Ts \<turnstile>⇩1 compE⇣1 Vs e :: U"
and  "!!Vs Ts Us.
  [| P,[Vs[\<mapsto>]Ts] \<turnstile> es [::] Us; size Ts = size Vs |]
  ==> compP f P,Ts \<turnstile>⇩1 compEs⇣1 Vs es [::] Us"
(*<*)
apply(induct e and es)
apply clarsimp
apply(fastforce)
apply clarsimp
apply(fastforce split:bop.splits)
apply (fastforce simp:map_upds_apply_eq_Some split:split_if_asm)
apply (fastforce simp:map_upds_apply_eq_Some split:split_if_asm)
apply (fastforce)
apply (fastforce)
apply (fastforce dest!: sees_method_compP[where f = f])
apply (fastforce simp:nth_append)
apply (fastforce)
apply (fastforce)
apply (fastforce)
apply (fastforce)
apply (fastforce simp:nth_append)
apply simp
apply (fastforce)
done
(*>*)

text{*\noindent and the correct block numbering: *}

lemma \<B>: "!!Vs n. size Vs = n ==> \<B> (compE⇣1 Vs e) n"
and \<B>s: "!!Vs n. size Vs = n ==> \<B>s (compEs⇣1 Vs es) n"
(*<*)by(induct e and es) simp_all(*>*)

text{* The main complication is preservation of definite assignment
@{term"\<D>"}. *}

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_compE⇣1_None[simp]:
      "!!Vs. \<A> e = None ==> \<A> (compE⇣1 Vs e) = None"
and "!!Vs. \<A>s es = None ==> \<A>s (compEs⇣1 Vs es) = None"
(*<*)by(induct e and es)(auto simp:hyperset_defs)(*>*)


lemma A_compE⇣1:
      "!!A Vs. [| \<A> e = ⌊A⌋; fv e ⊆ set Vs |] ==> \<A> (compE⇣1 Vs e) = ⌊last_index Vs ` A⌋"
and "!!A Vs. [| \<A>s es = ⌊A⌋; fvs es ⊆ set Vs |] ==> \<A>s (compEs⇣1 Vs es) = ⌊last_index Vs ` A⌋"
(*<*)
proof(induct e and es)
  case (Block V' T e)
  hence "fv e ⊆ set (Vs@[V'])" by fastforce
  moreover obtain B where "\<A> 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 e⇣1 C V' e⇣2)
  hence fve⇣2: "fv e⇣2 ⊆ set (Vs@[V'])" by auto
  show ?case
  proof (cases "\<A> e⇣1")
    assume A⇣1: "\<A> e⇣1 = None"
    then obtain A⇣2 where A⇣2: "\<A> e⇣2 = ⌊A⇣2⌋" using TryCatch
      by(simp add:hyperset_defs)
    hence "A⇣2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A⇣2] by simp blast
    thus ?thesis using TryCatch fve⇣2 A⇣1 A⇣2
      by(auto simp add:hyperset_defs image_last_index last_index_size_conv)
  next
    fix A⇣1 assume A⇣1: "\<A> e⇣1 =  ⌊A⇣1⌋"
    show ?thesis
    proof (cases  "\<A> e⇣2")
      assume A⇣2: "\<A> e⇣2 = None"
      then show ?case using TryCatch A⇣1 by(simp add:hyperset_defs)
    next
      fix A⇣2 assume A⇣2: "\<A> e⇣2 = ⌊A⇣2⌋"
      have "A⇣1 ⊆ set Vs" using TryCatch.prems A_fv[OF A⇣1] by simp blast
      moreover
      have "A⇣2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A⇣2] by simp blast
      ultimately show ?thesis using TryCatch A⇣1 A⇣2
        by(fastforce simp add: hyperset_defs image_last_index last_index_size_conv
          Diff_subset_conv inj_on_image_Int[OF inj_on_last_index])
    qed
  qed
next
  case (Cond e e⇣1 e⇣2)
  { assume "\<A> e = None ∨ \<A> e⇣1 = None ∨ \<A> e⇣2 = None"
    hence ?case using Cond by(auto simp add:hyperset_defs image_Un)
  }
  moreover
  { fix A A⇣1 A⇣2
    assume "\<A> e = ⌊A⌋" and A⇣1: "\<A> e⇣1 = ⌊A⇣1⌋" and A⇣2: "\<A> e⇣2 = ⌊A⇣2⌋"
    moreover
    have "A⇣1 ⊆ set Vs" using Cond.prems A_fv[OF A⇣1] by simp blast
    moreover
    have "A⇣2 ⊆ set Vs" using Cond.prems A_fv[OF A⇣2] 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]: "\<D> (e::'a exp) None" and [iff]: "\<D>s (es::'a exp list) None"
(*<*)by(induct e and es)(simp_all)(*>*)


lemma D_last_index_compE⇣1:
      "!!A Vs. [| A ⊆ set Vs; fv e ⊆ set Vs |] ==>
                \<D> e ⌊A⌋ ==> \<D> (compE⇣1 Vs e) ⌊last_index Vs ` A⌋"
and "!!A Vs. [| A ⊆ set Vs; fvs es ⊆ set Vs |] ==>
                \<D>s es ⌊A⌋ ==> \<D>s (compEs⇣1 Vs es) ⌊last_index Vs ` A⌋"
(*<*)
proof(induct e and es)
  case (BinOp e⇣1 bop e⇣2)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using BinOp by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] BinOp.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using BinOp.prems A_fv[OF Some] by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using BinOp Some by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 by auto
  qed
next
  case (FAss e⇣1 F D e⇣2)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using FAss by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] FAss.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using FAss.prems A_fv[OF Some] by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using FAss Some by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 by auto
  qed
next
  case (Call e⇣1 M es)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using Call by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] Call.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using Call.prems A_fv[OF Some] by auto
    hence "\<D>s (compEs⇣1 Vs es) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using Call Some by auto
    hence "\<D>s (compEs⇣1 Vs es) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 by auto
  qed
next
  case (TryCatch e⇣1 C V e⇣2)
  have "[| A∪{V} ⊆ set(Vs@[V]); fv e⇣2 ⊆ set(Vs@[V]); \<D> e⇣2 ⌊A∪{V}⌋|] ==>
        \<D> (compE⇣1 (Vs@[V]) e⇣2) ⌊last_index (Vs@[V]) ` (A∪{V})⌋" by fact
  hence "\<D> (compE⇣1 (Vs@[V]) e⇣2) ⌊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:split_if_asm)
  ultimately show ?case using TryCatch
    by(auto simp:hyperset_defs elim!:D_mono')
next
  case (Seq e⇣1 e⇣2)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using Seq by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] Seq.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using Seq.prems A_fv[OF Some] by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using Seq Some by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 by auto
  qed
next
  case (Cond e e⇣1 e⇣2)
  hence IH⇣1: "\<D> (compE⇣1 Vs e) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e")
    case None thus ?thesis using Cond by simp
  next
    case (Some B)
    have indexB: "\<A> (compE⇣1 Vs e) = ⌊last_index Vs ` B⌋"
      using A_compE⇣1[OF Some] Cond.prems  by auto
    have "A ∪ B ⊆ set Vs" using Cond.prems A_fv[OF Some] by auto
    hence "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` (A ∪ B)⌋"
      and "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` (A ∪ B)⌋"
      using Cond Some by auto
    hence "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A ∪ last_index Vs ` B⌋"
      and "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` A ∪ last_index Vs ` B⌋"
      by(simp add: image_Un)+
    thus ?thesis using IH⇣1 indexB by auto
  qed
next
  case (While e⇣1 e⇣2)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using While by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] While.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using While.prems A_fv[OF Some] by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using While Some by auto
    hence "\<D> (compE⇣1 Vs e⇣2) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 by auto
  qed
next
  case (Block V T e)
  have "[| A-{V} ⊆ set(Vs@[V]); fv e ⊆ set(Vs@[V]); \<D> e ⌊A-{V}⌋ |] ==>
        \<D> (compE⇣1 (Vs@[V]) e) ⌊last_index (Vs@[V]) ` (A-{V})⌋" by fact
  hence "\<D> (compE⇣1 (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 e⇣1 es)
  hence IH⇣1: "\<D> (compE⇣1 Vs e⇣1) ⌊last_index Vs ` A⌋" by simp
  show ?case
  proof (cases "\<A> e⇣1")
    case None thus ?thesis using Cons_exp by simp
  next
    case (Some A⇣1)
    have indexA⇣1: "\<A> (compE⇣1 Vs e⇣1) = ⌊last_index Vs ` A⇣1⌋"
      using A_compE⇣1[OF Some] Cons_exp.prems  by auto
    have "A ∪ A⇣1 ⊆ set Vs" using Cons_exp.prems A_fv[OF Some] by auto
    hence "\<D>s (compEs⇣1 Vs es) ⌊last_index Vs ` (A ∪ A⇣1)⌋" using Cons_exp Some by auto
    hence "\<D>s (compEs⇣1 Vs es) ⌊last_index Vs ` A ∪ last_index Vs ` A⇣1⌋"
      by(simp add: image_Un)
    thus ?thesis using IH⇣1 indexA⇣1 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_compE⇣1:
  "[| \<D> e ⌊set Vs⌋; fv e ⊆ set Vs; distinct Vs |] ==> \<D> (compE⇣1 Vs e) ⌊{..<length Vs}⌋"
(*<*)by(fastforce dest!: D_last_index_compE⇣1[OF subset_refl] simp add:last_index_image_set)(*>*)


lemma D_compE⇣1':
assumes "\<D> e ⌊set(V#Vs)⌋" and "fv e ⊆ set(V#Vs)" and "distinct(V#Vs)"
shows "\<D> (compE⇣1 (V#Vs) e) ⌊{..length Vs}⌋"
(*<*)
proof -
  have "{..size Vs} = {..<size(V#Vs)}" by auto
  thus ?thesis using assms by (simp only:)(rule D_compE⇣1)
qed
(*>*)


lemma compP⇣1_pres_wf: "wf_J_prog P ==> wf_J⇣1_prog (compP⇣1 P)"
(*<*)
apply simp
apply(rule wf_prog_compPI)
 prefer 2 apply assumption
apply(case_tac m)
apply(simp add:wf_mdecl_def wf_J⇣1_mdecl_def wf_J_mdecl)
apply(clarify)
apply(frule WT_fv)
apply(fastforce intro!: compE⇣1_pres_wt D_compE⇣1' \<B>)
done
(*>*)


end