Theory LemmasComp

(*  Title:      HOL/MicroJava/Comp/LemmasComp.thy
    Author:     Martin Strecker
*)

(* Lemmas for compiler correctness proof *)

theory LemmasComp
imports TranslComp
begin


context
begin

declare split_paired_All [simp del]
declare split_paired_Ex [simp del]


(**********************************************************************)
(* misc lemmas *)

lemma c_hupd_conv: 
  "c_hupd h' (xo, (h,l)) = (xo, (if xo = None then h' else h),l)"
  by (simp add: c_hupd_def)

lemma gl_c_hupd [simp]: "(gl (c_hupd h xs)) = (gl xs)"
  by (simp add: gl_def c_hupd_def split_beta)

lemma c_hupd_xcpt_invariant [simp]: "gx (c_hupd h' (xo, st)) = xo"
  by (cases st) (simp only: c_hupd_conv gx_conv)

(* not added to simpset because of interference with c_hupd_conv *)
lemma c_hupd_hp_invariant: "gh (c_hupd hp (None, st)) = hp"
  by (cases st) (simp add: c_hupd_conv gh_def)


lemma unique_map_fst [rule_format]: "(∀ x ∈ set xs. (fst x = fst (f x) )) ⟶
  unique (map f xs) = unique xs"
proof (induct xs)
  case Nil show ?case by simp
next
  case (Cons a list)
  show ?case
  proof
    assume fst_eq: "∀x∈set (a # list). fst x = fst (f x)"

    have fst_set: "(fst a ∈ fst ` set list) = (fst (f a) ∈ fst ` f ` set list)" 
    proof 
      assume as: "fst a ∈ fst ` set list" 
      then obtain x where fst_a_x: "x∈set list ∧ fst a = fst x" 
        by (auto simp add: image_iff)
      then have "fst (f a) = fst (f x)" by (simp add: fst_eq)
      with as show "(fst (f a) ∈ fst ` f ` set list)" by (simp add: fst_a_x)
    next
      assume as: "fst (f a) ∈ fst ` f ` set list"
      then obtain x where fst_a_x: "x∈set list ∧ fst (f a) = fst (f x)"
        by (auto simp add: image_iff)
      then have "fst a = fst x" by (simp add: fst_eq)
      with as show "fst a ∈ fst ` set list" by (simp add: fst_a_x)
    qed

    with fst_eq Cons 
    show "unique (map f (a # list)) = unique (a # list)"
      by (simp add: unique_def fst_set image_comp)
  qed
qed

lemma comp_unique: "unique (comp G) = unique G"
  apply (simp add: comp_def)
  apply (rule unique_map_fst)
  apply (simp add: compClass_def split_beta)
  done


(**********************************************************************)
(* invariance of properties under compilation *)

lemma comp_class_imp:
  "(class G C = Some(D, fs, ms)) ⟹ 
  (class (comp G) C = Some(D, fs, map (compMethod G C) ms))"
  apply (simp add: class_def comp_def compClass_def)
  apply (rule trans)
   apply (rule map_of_map2)
   apply auto
  done

lemma comp_class_None: 
"(class G C = None) = (class (comp G) C = None)"
  apply (simp add: class_def comp_def compClass_def)
  apply (simp add: map_of_in_set)
  apply (simp add: image_comp [symmetric] o_def split_beta)
  done

lemma comp_is_class: "is_class (comp G) C = is_class G C"
  by (cases "class G C") (auto simp: is_class_def comp_class_None dest: comp_class_imp)


lemma comp_is_type: "is_type (comp G) T = is_type G T"
  apply (cases T, simp)
  apply (induct G)
   apply simp
   apply (simp only: comp_is_class)
  apply (simp add: comp_is_class)
  apply (simp only: comp_is_class)
  done

lemma comp_classname:
  "is_class G C ⟹ fst (the (class G C)) = fst (the (class (comp G) C))"
  by (cases "class G C") (auto simp: is_class_def dest: comp_class_imp)

lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
  by (auto simp add: subcls1_def2 comp_classname comp_is_class)

lemma comp_widen: "widen (comp G) = widen G"
  apply (simp add: fun_eq_iff)
  apply (intro allI iffI)
   apply (erule widen.cases)
     apply (simp_all add: comp_subcls1 widen.null)
  apply (erule widen.cases)
    apply (simp_all add: comp_subcls1 widen.null)
  done

lemma comp_cast: "cast (comp G) = cast G"
  apply (simp add: fun_eq_iff)
  apply (intro allI iffI)
   apply (erule cast.cases)
    apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   apply (rule cast.widen)
   apply (simp add: comp_widen)
  apply (erule cast.cases)
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
  apply (rule cast.widen)
  apply (simp add: comp_widen)
  done

lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
  by (simp add: fun_eq_iff cast_ok_def comp_widen)


lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
  by (simp add: compClass_def split_beta)

lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))"
  by (simp add: compClass_def split_beta)

lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))"
  by (simp add: compClass_def split_beta)

lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd"
  by (cases fd) (simp add: wf_fdecl_def comp_is_type)


lemma compClass_forall [simp]:
  "(∀x∈set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
  (∀x∈set (snd (snd (snd C))). P (fst x) (fst (snd x)))"
  by (simp add: compClass_def compMethod_def split_beta)

lemma comp_wf_mhead: "wf_mhead (comp G) S rT =  wf_mhead G S rT"
  by (simp add: wf_mhead_def split_beta comp_is_type)

lemma comp_ws_cdecl:
  "ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
  apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
  apply (simp (no_asm_simp) add: comp_wf_mhead)
  apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
  done


lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
  apply (simp add: wf_syscls_def comp_def compClass_def split_beta cong: image_cong_simp)
  apply (simp add: image_comp cong: image_cong_simp)
  done


lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G"
  apply (rule sym)
  apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
  apply (simp add: comp_wf_syscls)
  apply (auto simp add: comp_ws_cdecl [symmetric] TranslComp.comp_def)
  done


lemma comp_class_rec: 
  "wf ((subcls1 G)¯) ⟹ 
  class_rec (comp G) C t f =
  class_rec G C t (λ C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
  apply (rule_tac a = C in  wf_induct)
   apply assumption
  apply (subgoal_tac "wf ((subcls1 (comp G))¯)")
   apply (subgoal_tac "(class G x = None) ∨ (∃ D fs ms. (class G x = Some (D, fs, ms)))")
    apply (erule disjE)

     (* case class G x = None *)
     apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 
                                    wfrec [where R="(subcls1 G)¯", simplified])
     apply (simp add: comp_class_None)

    (* case ∃ D fs ms. (class G x = Some (D, fs, ms)) *)
    apply (erule exE)+
    apply (frule comp_class_imp)
    apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma)
     apply assumption
    apply (frule_tac G=G and C=x and t=t
                 and f="(λC' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma)
     apply assumption
    apply (simp only:)
    apply (case_tac "x = Object")
     apply simp
    apply (frule subcls1I, assumption)
    apply (drule_tac x=D in spec, drule mp, simp)
    apply simp

   (* subgoals *)
   apply (case_tac "class G x")
    apply auto
  apply (simp add: comp_subcls1)
  done

lemma comp_fields: "wf ((subcls1 G)¯) ⟹ 
  fields (comp G,C) = fields (G,C)" 
  by (simp add: fields_def comp_class_rec)

lemma comp_field: "wf ((subcls1 G)¯) ⟹ 
  field (comp G,C) = field (G,C)" 
  by (simp add: TypeRel.field_def comp_fields)


lemma class_rec_relation [rule_format (no_asm)]: "⟦  ws_prog G;
  ∀fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
   ∀C fs ms r1 r2. (R r1 r2) ⟶ (R (f1 C fs ms r1) (f2 C fs ms r2)) ⟧
  ⟹ ((class G C) ≠ None) ⟶  R (class_rec G C t1 f1) (class_rec G C t2 f2)"
  apply (frule wf_subcls1) (* establish wf ((subcls1 G)¯) *)
  apply (rule_tac a = C in wf_induct)
   apply assumption
  apply (intro strip)
  apply (subgoal_tac "(∃D rT mb. class G x = Some (D, rT, mb))")
   apply (erule exE)+
   apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma)
    apply assumption
   apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma)
    apply assumption
   apply (simp only:)

   apply (case_tac "x = Object")
    apply simp
   apply (frule subcls1I, assumption)
   apply (drule_tac x=D in spec, drule mp, simp)
   apply simp
   apply (subgoal_tac "(∃D' rT' mb'. class G D = Some (D', rT', mb'))")
    apply blast

   (* subgoals *)
   apply (frule class_wf_struct, assumption)
   apply (simp add: ws_cdecl_def is_class_def)
   apply (simp add: subcls1_def2 is_class_def)
   apply auto
  done


abbreviation (input)
  "mtd_mb == snd o snd"

lemma map_of_map:
  "map_of (map (λ(k, v). (k, f v)) xs) k = map_option f (map_of xs k)"
  by (simp add: map_of_map)

lemma map_of_map_fst:
  "⟦ inj f; ∀x∈set xs. fst (f x) = fst x; ∀x∈set xs. fst (g x) = fst x ⟧
  ⟹  map_of (map g xs) k = map_option (λ e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
  apply (induct xs)
   apply simp
  apply simp
  apply (case_tac "k = fst a")
   apply simp
   apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
   apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
   apply (erule conjE)+
   apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
   apply simp
  apply (simp add: surjective_pairing)
  done

lemma comp_method [rule_format (no_asm)]:
  "⟦ ws_prog G; is_class G C⟧ ⟹ 
  ((method (comp G, C) S) = 
   map_option (λ (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
              (method (G, C) S))"
  apply (simp add: method_def)
  apply (frule wf_subcls1)
  apply (simp add: comp_class_rec)
  apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
  apply (rule_tac R="λx y. ((x S) = (map_option (λ(D, rT, b).
                           (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))"
                  in class_rec_relation)
     apply assumption

    apply (intro strip)
    apply simp
    apply (rule trans)

     apply (rule_tac f="(λ(s, m). (s, Object, m))" and
                     g="(Fun.comp (λ(s, m). (s, Object, m)) (compMethod G Object))"
                  in map_of_map_fst)
       defer  (* inj … *)
       apply (simp add: inj_on_def split_beta)
      apply (simp add: split_beta compMethod_def)
     apply (simp add: map_of_map [symmetric])
     apply (simp add: split_beta)
     apply (simp add: Fun.comp_def split_beta)
     apply (subgoal_tac "(λx::(vname list × fdecl list × stmt × expr) mdecl.
                        (fst x, Object,
                         snd (compMethod G Object
                         (inv (λ(s::sig, m::ty × vname list × fdecl list × stmt × expr).
                           (s, Object, m))
                           (S, Object, snd x)))))
                        = (λx. (fst x, Object, fst (snd x),
                                snd (snd (compMethod G Object (S, snd x)))))")
      apply (simp only:)
     apply (simp add: fun_eq_iff)
     apply (intro strip)
     apply (subgoal_tac "(inv (λ(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
      apply (simp only:)
      apply (simp add: compMethod_def split_beta)
     apply (rule inv_f_eq)
      defer
      defer

      apply (intro strip)
      apply (simp add: map_add_Some_iff map_of_map)
      apply (simp add: map_add_def)
      apply (subgoal_tac "inj (λ(s, m). (s, Ca, m))")
       apply (drule_tac g="(Fun.comp (λ(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
                    and k=S in map_of_map_fst)
         apply (simp add: split_beta)
        apply (simp add: compMethod_def split_beta)
       apply (case_tac "(map_of (map (λ(s, m). (s, Ca, m)) ms) S)")
        apply simp
       apply (simp add: split_beta map_of_map)
       apply (elim exE conjE)
       apply (drule_tac t=a in sym)
       apply (subgoal_tac "(inv (λ(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
        apply simp
        apply (subgoal_tac "∀x∈set ms. fst ((Fun.comp (λ(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
         prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
        apply (simp add: map_of_map2)
        apply (simp (no_asm_simp) add: compMethod_def split_beta)

       ― ‹remaining subgoals›
       apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
  done



lemma comp_wf_mrT: "⟦ ws_prog G; is_class G D⟧ ⟹ 
  wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) =
  wf_mrT G (C, D, fs, ms)"
  apply (simp add: wf_mrT_def compMethod_def split_beta)
  apply (simp add: comp_widen)
  apply (rule iffI)
   apply (intro strip)
   apply simp
   apply (drule (1) bspec)
   apply (drule_tac x=D' in spec)
   apply (drule_tac x=rT' in spec)
   apply (drule mp)
    prefer 2 apply assumption
   apply (simp add: comp_method [of G D])
   apply (erule exE)+
   apply (simp add: split_paired_all)
  apply (auto simp: comp_method)
  done


(**********************************************************************)
  (* DIVERSE OTHER LEMMAS *)
(**********************************************************************)

lemma max_spec_preserves_length:
  "max_spec G C (mn, pTs) = {((md,rT),pTs')} ⟹ length pTs = length pTs'"
  apply (frule max_spec2mheads)
  apply (clarsimp simp: list_all2_iff)
  done


lemma ty_exprs_length [simp]: "(E⊢es[::]Ts ⟶ length es = length Ts)"
  apply (subgoal_tac "(E⊢e::T ⟶ True) ∧ (E⊢es[::]Ts ⟶ length es = length Ts) ∧ (E⊢s√ ⟶ True)")
   apply blast
  apply (rule ty_expr_ty_exprs_wt_stmt.induct, auto)
  done


lemma max_spec_preserves_method_rT [simp]:
  "max_spec G C (mn, pTs) = {((md,rT),pTs')}
  ⟹ method_rT (the (method (G, C) (mn, pTs'))) = rT"
  apply (frule max_spec2mheads)
  apply (clarsimp simp: method_rT_def)
  done

  (**********************************************************************************)

end (* context *)

declare compClass_fst [simp del]
declare compClass_fst_snd [simp del]
declare compClass_fst_snd_snd [simp del]

end