Theory FJAux

(*  Title:       A theory of Featherweight Java in Isabelle/HOL
    Author:      Nate Foster <jnfoster at cis.upenn.edu>, 
                 Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>, 2006
    Maintainer:  Nate Foster <jnfoster at cis.upenn.edu>,
                 Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>
    License:     LGPL

  Auxiliary lemmas
*)

section ‹{\tt FJAux}: Auxiliary Lemmas›

theory FJAux imports FJDefs
begin 

subsection‹Non-FJ Lemmas›

subsubsection‹Lists›
lemma mem_ith: 
  assumes "ei ∈ set es" 
  shows "∃ el er. es = el@ei#er"
  using assms
proof(induct es)
  case Nil thus ?case by auto
next
  case (Cons esh est) 
  { assume "esh = ei" 
    with Cons have ?case by blast
  } moreover {
    assume "esh ≠ ei"
    with Cons have "ei ∈ set est" by auto    
    with Cons obtain el er where "esh # est = (esh#el) @ (ei#er)" by auto
    hence ?case by blast }
  ultimately show ?case by blast
qed

lemma ith_mem: "⋀i. ⟦ i < length es ⟧ ⟹ es!i ∈ set es"
proof(induct es)
  case Nil thus ?case by auto
next
  case (Cons h t) thus ?case by(cases "i", auto)
qed   

subsubsection‹Maps›

lemma map_shuffle: 
  assumes "length xs = length ys"
  shows "[xs[↦]ys,x↦y] = [(xs@[x])[↦](ys@[y])]"
  using assms
by (induct "xs" "ys" rule:list_induct2) (auto simp add:map_upds_append1)

lemma map_upds_index: 
  assumes "length xs = length As"
  and "[xs[↦]As]x = Some Ai"
  shows "∃i.(As!i = Ai) 
         ∧ (i < length As) 
         ∧ (∀(Bs::'c list).((length Bs = length As) 
                            ⟶ ([xs[↦]Bs] x = Some (Bs !i))))" 
  (is "∃i. ?P i xs As" 
   is "∃i.(?P1 i As) ∧ (?P2 i As) ∧ (∀Bs::('c list).(?P3 i xs As Bs))")
  using assms
proof(induct "xs" "As" rule:list_induct2)
  assume "[[][↦][]] x = Some Ai"
  moreover have "¬[[][↦][]] x = Some Ai" by auto
  ultimately show "∃i. ?P i [] []" by contradiction
next
  fix xa xs y ys 
  assume length_xs_ys: "length xs = length ys"
    and IH: "[xs [↦] ys] x = Some Ai ⟹ ∃i. ?P i xs ys"
    and map_eq_Some: "[xa # xs [↦] y # ys] x = Some Ai"
  then have map_decomp: "[xa#xs [↦] y#ys] = [xa↦y] ++ [xs[↦]ys]" by fastforce
  show "∃i. ?P i (xa#xs) (y # ys)"
  proof(cases "[xs[↦]ys]x")
    case(Some Ai')
    hence "([xa ↦y] ++ [xs[↦]ys]) x = Some Ai'" by(rule map_add_find_right)
    hence P: "[xs[↦]ys] x = Some Ai" using map_eq_Some Some by simp
    from IH[OF P] obtain i where 
      R1: "ys ! i = Ai" 
      and R2: "i < length ys" 
      and pre_r3: "∀(Bs::'c list). ?P3 i xs ys Bs" by fastforce
    { fix Bs::"'c list"
      assume length_Bs: "length Bs = length (y#ys)"
      then obtain n where "length (y#ys) = Suc n" by auto
      with length_Bs obtain b bs where Bs_def: "Bs = b#bs" by (auto simp add:length_Suc_conv)
      with length_Bs have "length ys = length bs" by simp
      with pre_r3 have "([xa↦b] ++ [xs[↦]bs]) x = Some (bs!i)" by(auto simp only:map_add_find_right)
      with pre_r3 Bs_def length_Bs have "?P3 (i+1) (xa#xs) (y#ys) Bs" by simp }
    with R1 R2 have "?P (i+1) (xa#xs) (y#ys)" by auto
    thus ?thesis ..
  next
    case None
    with map_decomp map_eq_Some have "[xa↦y] x = Some Ai" by (auto simp only:map_add_SomeD)
    hence ai_def: "y = Ai" and x_eq_xa:"x=xa" by (auto simp only:map_upd_Some_unfold)  
    { fix Bs::"'c list"
      assume length_Bs: "length Bs = length (y#ys)"
      then obtain n where "length (y#ys) = Suc n" by auto
      with length_Bs obtain b bs where Bs_def: "Bs = b#bs" by (auto simp add:length_Suc_conv)
      with length_Bs have "length ys = length bs" by simp
      hence "dom([xs[↦]ys]) = dom([xs[↦]bs])" by auto
      with None have "[xs[↦]bs] x = None" by (auto simp only:domIff)
      moreover from x_eq_xa have sing_map: "[xa↦b] x = Some b" by (auto simp only:map_upd_Some_unfold)
      ultimately have "([xa↦b] ++ [xs[↦]bs]) x = Some b" by (auto simp only:map_add_Some_iff)
      with Bs_def have "?P3 0 (xa#xs) (y#ys) Bs" by simp }
    with ai_def have "?P 0 (xa#xs) (y#ys)" by auto
    thus ?thesis ..
  qed
qed

subsection‹FJ Lemmas› 

subsubsection‹Substitution›

lemma subst_list1_eq_map_substs : 
  "∀σ. subst_list1 σ l = map (substs σ) l"
   by (induct l, simp_all)

lemma subst_list2_eq_map_substs : 
  "∀σ. subst_list2 σ l = map (substs σ) l"
   by (induct l, simp_all)

subsubsection‹Lookup›

lemma lookup_functional:
  assumes "lookup l f = o1"
  and "lookup l f = o2"
  shows "o1 = o2"
using assms by (induct l) auto

lemma lookup_true:
  "lookup l f = Some r ⟹ f r"
proof(induct l)
  case Nil thus ?case by simp
next
  case(Cons h t) thus ?case by(cases "f h") (auto simp add:lookup.simps)
qed

lemma lookup_hd:
  "⟦ length l > 0; f (l!0) ⟧ ⟹ lookup l f = Some (l!0)"
by (induct l) auto

lemma lookup_split: "lookup l f = None ∨ (∃h. lookup l f = Some h)"
by (induct l) simp_all

lemma lookup_index:
  assumes "lookup l1 f = Some e" 
  shows " ⋀l2. ∃i < (length l1). e = l1!i ∧ ((length l1 = length l2) ⟶ lookup2 l1 l2 f = Some (l2!i))"
  using assms
proof(induct l1)
  case Nil thus ?case by auto
next
  case (Cons h1 t1)
  { assume asm:"f h1"
    hence "0<length (h1 # t1) ∧ e = (h1 # t1) ! 0" 
      using Cons by (auto simp add:lookup.simps)
    moreover { 
      assume "length (h1 # t1) = length l2"  
      hence "length l2 = Suc (length t1)" by auto
      then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
      hence "lookup2 (h1 # t1) l2 f = Some (l2 ! 0)" using asm by(auto simp add: lookup2.simps)
    }
    ultimately have ?case by auto
  } moreover { 
    assume asm:"¬ (f h1)"
    hence "lookup t1 f = Some e" 
      using Cons by (auto simp add:lookup.simps)
    then obtain i where 
      "i<length t1" 
      and "e = t1 ! i" 
      and  ih:"(length t1 = length (tl l2) ⟶ lookup2 t1 (tl l2) f = Some ((tl l2) ! i))" 
      using Cons by blast
    hence "Suc i < length (h1#t1) ∧ e = (h1#t1)!(Suc i)" using Cons by auto
    moreover {
      assume "length (h1 # t1) = length l2"
      hence lens:"length l2 = Suc (length t1)" by auto
      then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
      hence "lookup2 t1 t2 f = Some (t2 ! i)" using ih l2_def lens by auto
      hence "lookup2 (h1 # t1) l2 f = Some (l2!(Suc i))" 
        using asm l2_def by(auto simp add: lookup2.simps)
    }
    ultimately have ?case by auto
  }
  ultimately show ?case by auto
qed

lemma lookup2_index:
  "⋀l2. ⟦ lookup2 l1 l2 f = Some e; 
  length l1 = length l2 ⟧ ⟹ ∃i < (length l2). e = (l2!i) ∧ lookup l1 f = Some (l1!i)"
proof(induct l1)
  case Nil thus ?case by auto
next
  case (Cons h1 t1) 
  hence "length l2 = Suc (length t1)" by auto
  then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
  { assume asm:"f h1"
    hence "e = h2" using Cons l2_def by (auto simp add:lookup2.simps)
    hence "0<length (h2#t2) ∧ e = (h2#t2) ! 0 ∧ lookup (h1 # t1) f = Some ((h1 # t1) ! 0)"
      using asm by (auto simp add:lookup.simps)
    hence ?case using l2_def by auto
  } moreover { 
    assume asm:"¬ (f h1)"
    hence "∃i<length t2. e = t2 ! i ∧ lookup t1 f = Some (t1 ! i)" using Cons l2_def by auto
    then obtain i where "i<length t2 ∧  e = t2 ! i ∧ lookup t1 f = Some (t1 ! i)" by auto
    hence "(Suc i) < length(h2#t2) ∧ e = ((h2#t2) ! (Suc i)) ∧ lookup (h1#t1) f = Some ((h1#t1) ! (Suc i))" 
      using asm by (force simp add: lookup.simps)
    hence ?case using l2_def by auto
  }
  ultimately show ?case by auto
qed

lemma lookup_append:
  assumes "lookup l f = Some r"
  shows "lookup (l@l') f = Some r"
  using assms by(induct l) auto

lemma method_typings_lookup:
  assumes lookup_eq_Some: "lookup M f = Some mDef"
  and M_ok: "CT ⊢+ M OK IN C"
  shows "CT ⊢ mDef OK IN C"
  using lookup_eq_Some M_ok 
proof(induct M)
  case Nil thus ?case by fastforce
next
  case (Cons h t) thus ?case by(cases "f h", auto elim:method_typings.cases simp add:lookup.simps)
qed

subsubsection‹Functional›

text ‹These lemmas prove that several relations are actually functions›

lemma mtype_functional:
  assumes "mtype(CT,m,C) = Cs → C0"
  and     "mtype(CT,m,C) = Ds → D0"
  shows "Ds=Cs ∧ D0=C0"
using assms by induct (auto elim:mtype.cases)

lemma mbody_functional:
  assumes mb1: "mbody(CT,m,C) = xs . e0"
  and     mb2: "mbody(CT,m,C) = ys . d0"
  shows "xs = ys ∧ e0 = d0"
using assms by induct (auto elim:mbody.cases)

lemma fields_functional:
  assumes "fields(CT,C) = Cf" 
  and "CT OK" 
  shows "⋀Cf'. ⟦ fields(CT,C) = Cf'⟧ ⟹ Cf = Cf'"
using assms
proof induct
  case (f_obj CT)
  hence "CT(Object) = None" by (auto elim: ct_typing.cases)
  thus ?case using f_obj by (auto elim: fields.cases)
next
  case (f_class CT C CDef D Cf Dg DgCf DgCf')
  hence f_class_inv: 
    "(CT C = Some CDef) ∧ (cSuper CDef = D) ∧ (cFields CDef = Cf)" 
    and "CT OK" by fastforce+
  hence c_not_obj:"C ≠ Object" by (force elim:ct_typing.cases)
  from f_class have flds:"fields(CT,C) = DgCf'" by fastforce
  then obtain Dg' where 
    "fields(CT,D) = Dg'"
    and "DgCf' = Dg' @ Cf" 
    using f_class_inv c_not_obj by (auto elim:fields.cases)
  hence "Dg' = Dg" using f_class by auto
  thus ?case using ‹DgCf = Dg @ Cf› and ‹DgCf' = Dg' @ Cf› by force
qed

subsubsection‹Subtyping and Typing›

lemma typings_lengths: assumes "CT;Γ ⊢+ es:Cs" shows "length es = length Cs" 
  using assms by(induct "es" "Cs") (auto elim:typings.cases)

lemma typings_index:
  assumes "CT;Γ ⊢+ es:Cs" 
  shows "⋀i. ⟦ i < length es ⟧ ⟹ CT;Γ ⊢ (es!i) : (Cs!i)" 
proof -
  have "length es = length Cs" using assms by (auto simp: typings_lengths)
  thus "⋀i. ⟦ i < length es ⟧ ⟹ CT;Γ ⊢ (es!i) : (Cs!i)" 
    using assms
  proof(induct es Cs rule:list_induct2)
    case Nil thus ?case by auto
  next
    case (Cons esh est hCs tCs i)
    thus ?case by(cases i) (auto elim:typings.cases)
  qed
qed


lemma subtypings_index:
  assumes "CT ⊢+ Cs <: Ds"
  shows "⋀i. ⟦ i < length Cs ⟧ ⟹ CT ⊢ (Cs!i) <: (Ds!i)"
  using assms
proof induct
  case ss_nil thus ?case by auto
next
  case (ss_cons hCs CT tCs hDs tDs i) 
  thus ?case by(cases "i", auto)
qed

lemma subtyping_append:
  assumes "CT ⊢+ Cs <: Ds"
  and "CT ⊢ C <: D"
  shows "CT ⊢+ (Cs@[C]) <: (Ds@[D])"
  using assms
  by (induct rule:subtypings.induct) (auto simp add:subtypings.intros elim:subtypings.cases)

lemma typings_append: 
  assumes "CT;Γ ⊢+ es : Cs"
  and "CT;Γ ⊢ e : C"
  shows "CT;Γ ⊢+ (es@[e]) : (Cs@[C])"
proof - 
  have "length es = length Cs" using assms by(simp_all add:typings_lengths)
  thus "CT;Γ ⊢+ (es@[e]) : (Cs@[C])" using assms
  proof(induct "es" "Cs" rule:list_induct2)
    have "CT;Γ ⊢+ []:[]" by(simp add:typings_typing.ts_nil)
    moreover from assms have "CT;Γ ⊢ e : C" by simp
    ultimately show "CT;Γ ⊢+ ([]@[e]) : ([]@[C])" by (auto simp add:typings_typing.ts_cons)
  next
    fix x xs y ys
    assume "length xs = length ys" 
      and IH: "⟦CT;Γ ⊢+ xs : ys; CT;Γ ⊢ e : C⟧ ⟹ CT;Γ ⊢+ (xs @ [e]) : (ys @ [C])"
      and x_xs_typs: "CT;Γ ⊢+ (x # xs) : (y # ys)"
      and e_typ: "CT;Γ ⊢ e : C"
    from x_xs_typs have x_typ: "CT;Γ ⊢ x : y" and "CT;Γ ⊢+ xs : ys" by(auto elim:typings.cases)
    with IH e_typ have "CT;Γ ⊢+ (xs@[e]) : (ys@[C])" by simp
    with x_typ have "CT;Γ ⊢+ ((x#xs)@[e]) : ((y#ys)@[C])" by (auto simp add:typings_typing.ts_cons)
    thus "CT;Γ ⊢+ ((x # xs) @ [e]) : ((y # ys) @ [C])" by(auto simp add:typings_typing.ts_cons)
  qed
qed

lemma ith_typing: "⋀Cs. ⟦ CT;Γ ⊢+ (es@(h#t)) : Cs ⟧ ⟹ CT;Γ ⊢ h : (Cs!(length es))"
proof(induct "es", auto elim:typings.cases)
qed

lemma ith_subtyping: "⋀Ds. ⟦ CT ⊢+ (Cs@(h#t)) <: Ds ⟧ ⟹ CT ⊢ h <: (Ds!(length Cs))"
proof(induct "Cs", auto elim:subtypings.cases)
qed

lemma subtypings_refl: "CT ⊢+ Cs <: Cs" 
by(induct "Cs", auto simp add: subtyping.s_refl subtypings.intros)

lemma subtypings_trans: "⋀Ds Es. ⟦ CT ⊢+ Cs <: Ds;  CT ⊢+ Ds <: Es ⟧ ⟹ CT ⊢+ Cs <: Es"
proof(induct "Cs")
  case Nil thus ?case 
    by (auto elim:subtypings.cases simp add:subtypings.ss_nil)
next
  case (Cons hCs tCs)
  then obtain hDs tDs
    where h1:"CT ⊢ hCs <: hDs" and t1:"CT ⊢+ tCs <: tDs" and "Ds = hDs#tDs"
    by (auto elim:subtypings.cases)
  then obtain hEs tEs
    where h2:"CT ⊢ hDs <: hEs" and t2:"CT ⊢+ tDs <: tEs" and "Es = hEs#tEs" 
    using Cons by (auto elim:subtypings.cases)
  moreover from subtyping.s_trans[OF h1 h2] have "CT ⊢ hCs <: hEs" by fastforce
  moreover with t1 t2 have "CT ⊢+ tCs <: tEs" using Cons by simp_all
  ultimately show ?case by (auto simp add:subtypings.intros)
qed

lemma ith_typing_sub: 
  "⋀Cs. ⟦ CT;Γ ⊢+ (es@(h#t)) : Cs; 
     CT;Γ ⊢ h' : Ci'; 
     CT ⊢ Ci' <: (Cs!(length es)) ⟧
  ⟹ ∃Cs'. (CT;Γ ⊢+ (es@(h'#t)) : Cs' ∧ CT ⊢+ Cs' <: Cs)"
proof(induct es)
case Nil
 then obtain hCs tCs 
   where ts: "CT;Γ ⊢+ t : tCs"
   and Cs_def: "Cs = hCs # tCs" by(auto elim:typings.cases)
 from Cs_def Nil have "CT ⊢ Ci' <: hCs" by auto
 with Cs_def have "CT ⊢+ (Ci'#tCs) <: Cs" by(auto simp add:subtypings.ss_cons subtypings_refl)
 moreover from ts Nil have "CT;Γ ⊢+ (h'#t) : (Ci'#tCs)" by(auto simp add:typings_typing.ts_cons)
 ultimately show ?case by auto
next
case (Cons eh et)
then obtain hCs tCs
  where "CT;Γ ⊢ eh : hCs" 
  and "CT;Γ ⊢+ (et@(h#t)) : tCs"
  and Cs_def: "Cs = hCs # tCs"
  by(auto elim:typings.cases)
moreover with Cons obtain tCs'
  where "CT;Γ ⊢+ (et@(h'#t)) : tCs'"
  and "CT ⊢+ tCs' <: tCs"
  by auto
ultimately have 
  "CT;Γ ⊢+ (eh#(et@(h'#t))) : (hCs#tCs')" 
  and "CT ⊢+ (hCs#tCs') <: Cs"
  by(auto simp add:typings_typing.ts_cons subtypings.ss_cons subtyping.s_refl)
thus ?case by auto
qed
   
lemma mem_typings: 
  "⋀Cs. ⟦ CT;Γ ⊢+ es:Cs; ei ∈ set es⟧ ⟹ ∃Ci. CT;Γ ⊢ ei:Ci"
proof(induct es)
  case Nil thus ?case by auto
next
  case (Cons eh et) thus ?case 
    by(cases "ei=eh", auto elim:typings.cases)
qed

lemma typings_proj: 
  assumes "CT;Γ ⊢+ ds : As"
      and "CT ⊢+ As <: Bs" 
      and "length ds = length As" 
      and "length ds = length Bs" 
      and "i < length ds" 
    shows "CT;Γ ⊢ ds!i : As!i" and "CT ⊢ As!i <: Bs!i"
  using assms by (auto simp add:typings_index subtypings_index)

lemma subtypings_length: 
  "CT ⊢+ As <: Bs ⟹ length As = length Bs" 
  by(induct rule:subtypings.induct) simp_all

lemma not_subtypes_aux: 
  assumes "CT ⊢ C <: Da" 
  and "C ≠ Da" 
  and "CT C = Some CDef" 
  and "cSuper CDef = D"
  shows "CT ⊢ D <: Da"
  using assms
by (induct rule:subtyping.induct) (auto intro:subtyping.intros) 

lemma not_subtypes:
  assumes "CT ⊢ A <: C"
  shows "⋀D. ⟦ CT ⊢ D ¬<: C;  CT ⊢ C ¬<: D⟧ ⟹ CT ⊢ A ¬<: D"
  using assms
proof(induct rule:subtyping.induct)
  case s_refl thus ?case by auto
next 
  case (s_trans CT C D E Da)
  have da_nsub_d:"CT ⊢ Da ¬<: D"
  proof(rule ccontr)
    assume "¬ CT ⊢ Da ¬<: D"
    hence da_sub_d:"CT ⊢ Da <: D" by auto
    have d_sub_e:"CT ⊢ D <: E" using s_trans by fastforce
    thus "False" using s_trans by (force simp add:subtyping.s_trans[OF da_sub_d d_sub_e])
  qed 
  have d_nsub_da:"CT ⊢ D ¬<: Da" using s_trans by auto
  from da_nsub_d d_nsub_da s_trans show "CT ⊢ C ¬<: Da" by auto
next
  case (s_super CT C CDef D Da)
  have "C ≠ Da" proof(rule ccontr)
    assume "¬ C ≠ Da"
    hence "C = Da" by auto 
    hence "CT ⊢ Da <: D" using s_super by(auto simp add: subtyping.s_super)
    thus "False" using s_super by auto
  qed
  thus ?case using s_super by (auto simp add: not_subtypes_aux)
qed

subsubsection‹Sub-Expressions›

lemma isubexpr_typing: 
  assumes "e1 ∈ isubexprs(e0)"
  shows "⋀C. ⟦ CT;Map.empty ⊢ e0 : C ⟧ ⟹ ∃D. CT;Map.empty ⊢ e1 : D"
using assms
  by (induct rule:isubexprs.induct) (auto elim:typing.cases simp add:mem_typings)

lemma subexpr_typing: 
  assumes "e1 ∈ subexprs(e0)"
  shows "⋀C. ⟦ CT;Map.empty ⊢ e0 : C ⟧ ⟹ ∃D. CT;Map.empty ⊢ e1 : D"
using assms
  by (induct rule:rtrancl.induct) (auto, force simp add:isubexpr_typing)

lemma isubexpr_reduct: 
  assumes "d1 ∈ isubexprs(e1)"
  shows "⋀d2. ⟦ CT ⊢ d1 → d2 ⟧ ⟹ ∃e2. CT ⊢ e1 → e2"
using assms mem_ith
  by induct
    (auto elim:isubexprs.cases intro:reduction.intros,
      force intro:reduction.intros, 
      force intro:reduction.intros)

lemma subexpr_reduct: 
  assumes "d1 ∈ subexprs(e1)"
  shows "⋀d2. ⟦ CT ⊢ d1 → d2 ⟧ ⟹ ∃e2. CT ⊢ e1 → e2"
using assms
  by (induct rule:rtrancl.induct) (auto, force simp add: isubexpr_reduct)

end