Theory JinjaDCI.ClassAdd

(*  Title: JinjaDCI/BV/ClassAdd.thy
    Author:     Susannah Mansky
    2019-20, UIUC
*)

section ‹ Property preservation under @{text "class_add"} ›

theory ClassAdd
imports BVConform
begin


lemma err_mono: "A ⊆ B ⟹ err A ⊆ err B"
 by(unfold err_def) auto

lemma opt_mono: "A ⊆ B ⟹ opt A ⊆ opt B"
 by(unfold opt_def) auto

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

― ‹ adding a class in the simplest way ›
abbreviation class_add :: "jvm_prog ⇒ jvm_method cdecl ⇒ jvm_prog" where
"class_add P cd ≡ cd#P"


subsection "Fields"

lemma class_add_has_fields:
assumes fs: "P ⊢ D has_fields FDTs" and nc: "¬is_class P C"
shows "class_add P (C, cdec) ⊢ D has_fields FDTs"
using assms
proof(induct rule: Fields.induct)
  case (has_fields_Object D fs ms FDTs)
  from has_fields_is_class_Object[OF fs] nc have "C ≠ Object" by fast
  with has_fields_Object show ?case
   by(auto simp: class_def fun_upd_apply intro!: TypeRel.has_fields_Object)
next
  case rec: (has_fields_rec C1 D fs ms FDTs FDTs')
  with has_fields_is_class have [simp]: "D ≠ C" by auto
  with rec have "C1 ≠ C" by(clarsimp simp: is_class_def)
  with rec show ?case
   by(auto simp: class_def fun_upd_apply intro: TypeRel.has_fields_rec)
qed

lemma class_add_has_fields_rev:
 "⟦ class_add P (C, cdec) ⊢ D has_fields FDTs; ¬P ⊢ D ≼⇧* C ⟧
 ⟹ P ⊢ D has_fields FDTs"
proof(induct rule: Fields.induct)
  case (has_fields_Object D fs ms FDTs)
  then show ?case by(auto simp: class_def fun_upd_apply intro!: TypeRel.has_fields_Object)
next
  case rec: (has_fields_rec C1 D fs ms FDTs FDTs')
  then have sub1: "P ⊢ C1 ≺⇧1 D"
   by(auto simp: class_def fun_upd_apply intro!: subcls1I split: if_split_asm)
  with rec.prems have cls: "¬ P ⊢ D ≼⇧* C" by (meson converse_rtrancl_into_rtrancl)
  with cls rec show ?case
   by(auto simp: class_def fun_upd_apply
           intro: TypeRel.has_fields_rec split: if_split_asm)
qed

lemma class_add_has_field:
assumes "P ⊢ C⇩0 has F,b:T in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊢ C⇩0 has F,b:T in D"
using assms by(auto simp: has_field_def dest!: class_add_has_fields[of P C⇩0])

lemma class_add_has_field_rev:
assumes has: "class_add P (C, cdec) ⊢ C⇩0 has F,b:T in D"
 and ncp: "⋀D'. P ⊢ C⇩0 ≼⇧* D' ⟹ D' ≠ C"
shows "P ⊢ C⇩0 has F,b:T in D"
using assms by(auto simp: has_field_def dest!: class_add_has_fields_rev)

lemma class_add_sees_field:
assumes "P ⊢ C⇩0 sees F,b:T in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊢ C⇩0 sees F,b:T in D"
using assms by(auto simp: sees_field_def dest!: class_add_has_fields[of P C⇩0])

lemma class_add_sees_field_rev:
assumes has: "class_add P (C, cdec) ⊢ C⇩0 sees F,b:T in D"
 and ncp: "⋀D'. P ⊢ C⇩0 ≼⇧* D' ⟹ D' ≠ C"
shows "P ⊢ C⇩0 sees F,b:T in D"
using assms by(auto simp: sees_field_def dest!: class_add_has_fields_rev)

lemma class_add_field:
assumes fd: "P ⊢ C⇩0 sees F,b:T in D" and "¬ is_class P C"
shows "field P C⇩0 F = field (class_add P (C, cdec)) C⇩0 F"
using class_add_sees_field[OF assms, of cdec] fd by simp

subsection "Methods"

lemma class_add_sees_methods:
assumes ms: "P ⊢ D sees_methods Mm" and nc: "¬is_class P C"
shows "class_add P (C, cdec) ⊢ D sees_methods Mm"
using assms
proof(induct rule: Methods.induct)
  case (sees_methods_Object D fs ms Mm)
  from sees_methods_is_class_Object[OF ms] nc have "C ≠ Object" by fast
  with sees_methods_Object show ?case
   by(auto simp: class_def fun_upd_apply intro!: TypeRel.sees_methods_Object)
next
  case rec: (sees_methods_rec C1 D fs ms Mm Mm')
  with sees_methods_is_class have [simp]: "D ≠ C" by auto
  with rec have "C1 ≠ C" by(clarsimp simp: is_class_def)
  with rec show ?case
   by(auto simp: class_def fun_upd_apply intro: TypeRel.sees_methods_rec)
qed

lemma class_add_sees_methods_rev:
 "⟦ class_add P (C, cdec) ⊢ D sees_methods Mm;
    ⋀D'. P ⊢ D ≼⇧* D' ⟹ D' ≠ C ⟧
 ⟹ P ⊢ D sees_methods Mm"
proof(induct rule: Methods.induct)
  case (sees_methods_Object D fs ms Mm)
  then show ?case
   by(auto simp: class_def fun_upd_apply intro!: TypeRel.sees_methods_Object)
next
  case rec: (sees_methods_rec C1 D fs ms Mm Mm')
  then have sub1: "P ⊢ C1 ≺⇧1 D"
   by(auto simp: class_def fun_upd_apply intro!: subcls1I)
  have cls: "⋀D'. P ⊢ D ≼⇧* D' ⟹ D' ≠ C"
  proof -
    fix D' assume "P ⊢ D ≼⇧* D'"
    with sub1 have "P ⊢ C1 ≼⇧* D'" by simp
    with rec.prems show "D' ≠ C" by simp
  qed
  with cls rec show ?case
   by(auto simp: class_def fun_upd_apply intro: TypeRel.sees_methods_rec)
qed

lemma class_add_sees_methods_Obj:
assumes "P ⊢ Object sees_methods Mm" and nObj: "C ≠ Object"
shows "class_add P (C, cdec) ⊢ Object sees_methods Mm"
proof -
  from assms obtain C' fs ms where cls: "class P Object = Some(C',fs,ms)"
     by(auto elim!: Methods.cases)
  with nObj have cls': "class (class_add P (C, cdec)) Object = Some(C',fs,ms)"
     by(simp add: class_def fun_upd_apply)
  from assms cls have "Mm = map_option (λm. (m, Object)) ∘ map_of ms" by(auto elim!: Methods.cases)
  with assms cls' show ?thesis
   by(auto simp: is_class_def fun_upd_apply intro!: sees_methods_Object)
qed

lemma class_add_sees_methods_rev_Obj:
assumes "class_add P (C, cdec) ⊢ Object sees_methods Mm" and nObj: "C ≠ Object"
shows "P ⊢ Object sees_methods Mm"
proof -
  from assms obtain C' fs ms where cls: "class (class_add P (C, cdec)) Object = Some(C',fs,ms)"
     by(auto elim!: Methods.cases)
  with nObj have cls': "class P Object = Some(C',fs,ms)"
     by(simp add: class_def fun_upd_apply)
  from assms cls have "Mm = map_option (λm. (m, Object)) ∘ map_of ms" by(auto elim!: Methods.cases)
  with assms cls' show ?thesis
   by(auto simp: is_class_def fun_upd_apply intro!: sees_methods_Object)
qed

lemma class_add_sees_method:
assumes "P ⊢ C⇩0 sees M⇩0, b : Ts→T = m in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊢ C⇩0 sees M⇩0, b : Ts→T = m in D"
using assms by(auto simp: Method_def dest!: class_add_sees_methods[of P C⇩0])

lemma class_add_method:
assumes md: "P ⊢ C⇩0 sees M⇩0, b : Ts→T = m in D" and "¬ is_class P C"
shows "method P C⇩0 M⇩0 = method (class_add P (C, cdec)) C⇩0 M⇩0"
using class_add_sees_method[OF assms, of cdec] md by simp

lemma class_add_sees_method_rev:
 "⟦ class_add P (C, cdec) ⊢ C⇩0 sees M⇩0, b : Ts→T = m in D;
    ¬ P ⊢ C⇩0 ≼⇧* C ⟧
  ⟹ P ⊢ C⇩0 sees M⇩0, b : Ts→T = m in D"
 by(auto simp: Method_def dest!: class_add_sees_methods_rev)

lemma class_add_sees_method_Obj:
 "⟦ P ⊢ Object sees M⇩0, b : Ts→T = m in D; C ≠ Object ⟧
  ⟹ class_add P (C, cdec) ⊢ Object sees M⇩0, b : Ts→T = m in D"
 by(auto simp: Method_def dest!: class_add_sees_methods_Obj[where P=P])

lemma class_add_sees_method_rev_Obj:
 "⟦ class_add P (C, cdec) ⊢ Object sees M⇩0, b : Ts→T = m in D; C ≠ Object ⟧
  ⟹ P ⊢ Object sees M⇩0, b : Ts→T = m in D"
 by(auto simp: Method_def dest!: class_add_sees_methods_rev_Obj[where P=P])

subsection "Types and states"

lemma class_add_is_type:
 "is_type P T ⟹ is_type (class_add P (C, cdec)) T"
 by(cases cdec, simp add: is_type_def is_class_def class_def fun_upd_apply split: ty.splits)

lemma class_add_types:
 "types P ⊆ types (class_add P (C, cdec))"
using class_add_is_type by(cases cdec, clarsimp)

lemma class_add_states:
 "states P mxs mxl ⊆ states (class_add P (C, cdec)) mxs mxl"
proof -
  let ?A = "types P" and ?B = "types (class_add P (C, cdec))"
  have ab: "?A ⊆ ?B" by(rule class_add_types)
  moreover have "⋀n. nlists n ?A ⊆ nlists n ?B" using ab by(rule nlists_mono)
  moreover have "nlists mxl (err ?A) ⊆ nlists mxl (err ?B)" using err_mono[OF ab] by(rule nlists_mono)
  ultimately show ?thesis by(auto simp: JVM_states_unfold intro!: err_mono opt_mono)
qed

lemma class_add_check_types:
 "check_types P mxs mxl τs ⟹ check_types (class_add P (C, cdec)) mxs mxl τs"
using class_add_states by(fastforce simp: check_types_def)

subsection "Subclasses and subtypes"

lemma class_add_subcls:
 "⟦ P ⊢ D ≼⇧* D'; ¬ is_class P C ⟧
 ⟹ class_add P (C, cdec) ⊢ D ≼⇧* D'"
proof(induct rule: rtrancl.induct)
  case (rtrancl_into_rtrancl a b c)
  then have "b ≠ C" by(clarsimp simp: is_class_def dest!: subcls1D)
  with rtrancl_into_rtrancl show ?case
   by(fastforce dest!: subcls1D simp: class_def fun_upd_apply
                intro!: rtrancl_trans[of a b] subcls1I)
qed(simp)

lemma class_add_subcls_rev:
 "⟦ class_add P (C, cdec) ⊢ D ≼⇧* D'; ¬P ⊢ D ≼⇧* C ⟧
 ⟹ P ⊢ D ≼⇧* D'"
proof(induct rule: rtrancl.induct)
  case (rtrancl_into_rtrancl a b c)
  then have "b ≠ C" by(clarsimp simp: is_class_def dest!: subcls1D)
  with rtrancl_into_rtrancl show ?case
   by(fastforce dest!: subcls1D simp: class_def fun_upd_apply
                intro!: rtrancl_trans[of a b] subcls1I)
qed(simp)

lemma class_add_subtype:
 "⟦ subtype P x y; ¬ is_class P C ⟧
 ⟹ subtype (class_add P (C, cdec)) x y"
proof(induct rule: widen.induct)
  case (widen_subcls C D)
  then show ?case using class_add_subcls by simp
qed(simp+)

lemma class_add_widens:
 "⟦ P ⊢ Ts [≤] Ts'; ¬ is_class P C ⟧
 ⟹ (class_add P (C, cdec)) ⊢ Ts [≤] Ts'"
using class_add_subtype by (metis (no_types) list_all2_mono)

lemma class_add_sup_ty_opt:
 "⟦ P ⊢ l1 ≤⇩⊤ l2; ¬ is_class P C ⟧
  ⟹ class_add P (C, cdec) ⊢ l1 ≤⇩⊤ l2"
using class_add_subtype by(auto simp: sup_ty_opt_def Err.le_def lesub_def split: err.splits)

lemma class_add_sup_loc:
"⟦ P ⊢ LT [≤⇩⊤] LT'; ¬ is_class P C ⟧
 ⟹ class_add P (C, cdec) ⊢ LT [≤⇩⊤] LT'"
using class_add_sup_ty_opt[where P=P and C=C] by (simp add: list.rel_mono_strong)

lemma class_add_sup_state:
 "⟦ P ⊢ τ ≤⇩i τ'; ¬ is_class P C ⟧
  ⟹ class_add P (C, cdec) ⊢ τ ≤⇩i τ'"
using class_add_subtype class_add_sup_ty_opt
 by(auto simp: sup_state_def Listn.le_def Product.le_def lesub_def class_add_widens
               class_add_sup_ty_opt list_all2_mono)

lemma class_add_sup_state_opt:
 "⟦ P ⊢ τ ≤' τ'; ¬ is_class P C ⟧
 ⟹ class_add P (C, cdec) ⊢ τ ≤' τ'"
 by(auto simp: sup_state_opt_def Opt.le_def lesub_def class_add_widens
               class_add_sup_ty_opt list_all2_mono)

subsection "Effect"

lemma class_add_is_relevant_class:
 "⟦ is_relevant_class i P C⇩0; ¬ is_class P C ⟧
  ⟹ is_relevant_class i (class_add P (C, cdec)) C⇩0"
  by(cases i, auto simp: class_add_subcls)

lemma class_add_is_relevant_class_rev:
assumes irc: "is_relevant_class i (class_add P (C, cdec)) C⇩0"
  and ncp: "⋀cd D'. cd ∈ set P ⟹ ¬P ⊢ fst cd ≼⇧* C"
  and wfxp: "wf_syscls P"
shows "is_relevant_class i P C⇩0"
using assms
proof(cases i)
  case (Getfield F D) with assms
  show ?thesis by(fastforce simp: wf_syscls_def sys_xcpts_def dest!: class_add_subcls_rev)
next
  case (Putfield F D) with assms
  show ?thesis by(fastforce simp: wf_syscls_def sys_xcpts_def dest!: class_add_subcls_rev)
next
  case (Checkcast D) with assms
  show ?thesis by(fastforce simp: wf_syscls_def sys_xcpts_def dest!: class_add_subcls_rev)
qed(simp_all)

lemma class_add_is_relevant_entry:
 "⟦ is_relevant_entry P i pc e; ¬ is_class P C ⟧
  ⟹ is_relevant_entry (class_add P (C, cdec)) i pc e"
 by(clarsimp simp: is_relevant_entry_def class_add_is_relevant_class)

lemma class_add_is_relevant_entry_rev:
 "⟦ is_relevant_entry (class_add P (C, cdec)) i pc e; 
    ⋀cd D'. cd ∈ set P ⟹ ¬P ⊢ fst cd ≼⇧* C;
    wf_syscls P ⟧
  ⟹ is_relevant_entry P i pc e"
 by(auto simp: is_relevant_entry_def dest!: class_add_is_relevant_class_rev)

lemma class_add_relevant_entries:
 "¬ is_class P C
  ⟹ set (relevant_entries P i pc xt) ⊆ set (relevant_entries (class_add P (C, cdec)) i pc xt)"
 by(clarsimp simp: relevant_entries_def class_add_is_relevant_entry)

lemma class_add_relevant_entries_eq:
assumes wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "relevant_entries P i pc xt = relevant_entries (class_add P (C, cdec)) i pc xt"
proof -
  have ncp: "⋀cd D'. cd ∈ set P ⟹ ¬P ⊢ fst cd ≼⇧* C"
   by(rule wf_subcls_nCls'[OF assms])
  moreover from wf have wfsys: "wf_syscls P" by(simp add: wf_prog_def)
  moreover
  note class_add_is_relevant_entry[OF _ nclass, of i pc _ cdec]
       class_add_is_relevant_entry_rev[OF _ ncp wfsys, of cdec i pc]
  ultimately show ?thesis by (metis filter_cong relevant_entries_def)
qed

lemma class_add_norm_eff_pc:
assumes ne: "∀(pc',τ') ∈ set (norm_eff i P pc τ). pc' < mpc"
shows "∀(pc',τ') ∈ set (norm_eff i (class_add P (C, cdec)) pc τ). pc' < mpc"
using assms by(cases i, auto simp: norm_eff_def)

lemma class_add_norm_eff_sup_state_opt:
assumes ne: "∀(pc',τ') ∈ set (norm_eff i P pc τ). P ⊢ τ' ≤' τs!pc'"
   and nclass: "¬ is_class P C" and app: "app⇩i (i, P, pc, mxs, T, τ)"
shows "∀(pc',τ') ∈ set (norm_eff i (class_add P (C, cdec)) pc τ). (class_add P (C, cdec)) ⊢ τ' ≤' τs!pc'"
proof -
  obtain ST LT where "τ = (ST,LT)" by(cases τ)
  with assms show ?thesis proof(cases i)
  qed(fastforce simp: norm_eff_def
                dest!: class_add_field[where cdec=cdec] class_add_method[where cdec=cdec]
                       class_add_sup_loc[OF _ nclass] class_add_subtype[OF _ nclass]
                       class_add_widens[OF _ nclass] class_add_sup_state_opt[OF _ nclass])+
qed

lemma class_add_xcpt_eff_eq:
assumes wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "xcpt_eff i P pc τ xt = xcpt_eff i (class_add P (C, cdec)) pc τ xt"
using class_add_relevant_entries_eq[OF assms, of i pc xt cdec] by(cases τ, simp add: xcpt_eff_def)

lemma class_add_eff_pc:
assumes eff: "∀(pc',τ') ∈ set (eff i P pc xt (Some τ)). pc' < mpc"
  and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "∀(pc',τ') ∈ set (eff i (class_add P (C, cdec)) pc xt (Some τ)). pc' < mpc"
using eff class_add_norm_eff_pc class_add_xcpt_eff_eq[OF wf nclass]
  by(auto simp: norm_eff_def eff_def)

lemma class_add_eff_sup_state_opt:
assumes eff: "∀(pc',τ') ∈ set (eff i P pc xt (Some τ)). P ⊢ τ' ≤' τs!pc'"
  and wf: "wf_prog wf_md P"and nclass: "¬ is_class P C"
  and app: "app⇩i (i, P, pc, mxs, T, τ)"
shows "∀(pc',τ') ∈ set (eff i (class_add P (C, cdec)) pc xt (Some τ)).
         (class_add P (C, cdec)) ⊢ τ' ≤' τs!pc'"
proof -
  from eff have ne: "∀(pc', τ')∈set (norm_eff i P pc τ). P ⊢ τ' ≤' τs ! pc'"
   by(simp add: norm_eff_def eff_def)
  from eff have "∀(pc', τ')∈set (xcpt_eff i P pc τ xt). P ⊢ τ' ≤' τs ! pc'"
   by(simp add: xcpt_eff_def eff_def)
  with class_add_norm_eff_sup_state_opt[OF ne nclass app]
       class_add_xcpt_eff_eq[OF wf nclass]class_add_sup_state_opt[OF _ nclass]
    show ?thesis by(cases cdec, auto simp: eff_def norm_eff_def xcpt_app_def)
qed


lemma class_add_app⇩i:
assumes "app⇩i (i, P, pc, mxs, T⇩r, ST, LT)" and "¬ is_class P C"
shows "app⇩i (i, class_add P (C, cdec), pc, mxs, T⇩r, ST, LT)"
using assms
proof(cases i)
  case New then show ?thesis using assms by(fastforce simp: is_class_def class_def fun_upd_apply)
next
  case Getfield then show ?thesis using assms
   by(auto simp: class_add_subtype dest!: class_add_sees_field[where P=P])
next
  case Getstatic then show ?thesis using assms by(auto dest!: class_add_sees_field[where P=P])
next
  case Putfield then show ?thesis using assms
   by(auto dest!: class_add_subtype[where P=P] class_add_sees_field[where P=P])
next
  case Putstatic then show ?thesis using assms
   by(auto dest!: class_add_subtype[where P=P] class_add_sees_field[where P=P])
next
  case Checkcast then show ?thesis using assms
   by(clarsimp simp: is_class_def class_def fun_upd_apply)
next
  case Invoke then show ?thesis using assms
    by(fastforce dest!: class_add_widens[where P=P] class_add_sees_method[where P=P])
next
  case Invokestatic then show ?thesis using assms
    by(fastforce dest!: class_add_widens[where P=P] class_add_sees_method[where P=P])
next
  case Return then show ?thesis using assms by(clarsimp simp: class_add_subtype)
qed(simp+)

lemma class_add_xcpt_app:
assumes xa: "xcpt_app i P pc mxs xt τ"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "xcpt_app i (class_add P (C, cdec)) pc mxs xt τ"
using xa class_add_relevant_entries_eq[OF wf nclass] nclass
 by(auto simp: xcpt_app_def is_class_def class_def fun_upd_apply) auto

lemma class_add_app:
assumes app: "app i P mxs T pc mpc xt t"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "app i (class_add P (C, cdec)) mxs T pc mpc xt t"
proof(cases t)
  case (Some τ)
  let ?P = "class_add P (C, cdec)"
  from assms Some have eff: "∀(pc', τ')∈set (eff i P pc xt ⌊τ⌋). pc' < mpc" by(simp add: app_def)
  from assms Some have app⇩i: "app⇩i (i,P,pc,mxs,T,τ)" by(simp add: app_def)
  with class_add_app⇩i[OF _ nclass] Some have "app⇩i (i,?P,pc,mxs,T,τ)" by(cases τ,simp)
  moreover
  from app class_add_xcpt_app[OF _ wf nclass] Some
  have "xcpt_app i ?P pc mxs xt τ" by(simp add: app_def del: xcpt_app_def)
  moreover
  from app class_add_eff_pc[OF eff wf nclass] Some
  have "∀(pc',τ') ∈ set (eff i ?P pc xt t). pc' < mpc" by auto
  moreover note app Some
  ultimately show ?thesis by(simp add: app_def)
qed(simp)

subsection "Well-formedness and well-typedness"

lemma class_add_wf_mdecl:
  "⟦ wf_mdecl wf_md P C⇩0 md;
     ⋀C⇩0 md. wf_md P C⇩0 md ⟹ wf_md (class_add P (C, cdec)) C⇩0 md ⟧
  ⟹ wf_mdecl wf_md (class_add P (C, cdec)) C⇩0 md"
 by(clarsimp simp: wf_mdecl_def class_add_is_type)

lemma class_add_wf_mdecl':
assumes wfd: "wf_mdecl wf_md P C⇩0 md"
  and ms: "(C⇩0,S,fs,ms) ∈ set P" and md: "md ∈ set ms"
  and wf_md': "⋀C⇩0 S fs ms m.⟦(C⇩0,S,fs,ms) ∈ set P; m ∈ set ms⟧ ⟹ wf_md' (class_add P (C, cdec)) C⇩0 m"
shows "wf_mdecl wf_md' (class_add P (C, cdec)) C⇩0 md"
using assms by(clarsimp simp: wf_mdecl_def class_add_is_type)

lemma class_add_wf_cdecl:
assumes wfcd: "wf_cdecl wf_md P cd" and cdP: "cd ∈ set P"
 and ncp: "¬ P ⊢ fst cd ≼⇧* C" and dist: "distinct_fst P"
 and wfmd: "⋀C⇩0 md. wf_md P C⇩0 md ⟹ wf_md (class_add P (C, cdec)) C⇩0 md"
 and nclass: "¬ is_class P C"
shows "wf_cdecl wf_md (class_add P (C, cdec)) cd"
proof -
  let ?P = "class_add P (C, cdec)"
  obtain C1 D fs ms where [simp]: "cd = (C1,(D,fs,ms))" by(cases cd)
  from wfcd
  have "∀f∈set fs. wf_fdecl ?P f" by(auto simp: wf_cdecl_def wf_fdecl_def class_add_is_type)
  moreover
  from wfcd wfmd class_add_wf_mdecl
  have "∀m∈set ms. wf_mdecl wf_md ?P C1 m" by(auto simp: wf_cdecl_def)
  moreover
  have "C1 ≠ Object ⟹ is_class ?P D ∧ ¬ ?P ⊢ D ≼⇧* C1
    ∧ (∀(M,b,Ts,T,m)∈set ms.
        ∀D' b' Ts' T' m'. ?P ⊢ D sees M,b':Ts' → T' = m' in D' ⟶
                       b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T')"
  proof -
    assume nObj[simp]: "C1 ≠ Object"
    with cdP dist have sub1: "P ⊢ C1 ≺⇧1 D" by(auto simp: class_def intro!: subcls1I map_of_SomeI)
    with ncp have ncp': "¬ P ⊢ D ≼⇧* C" by(auto simp: converse_rtrancl_into_rtrancl)
    with wfcd
    have clsD: "is_class ?P D"
     by(auto simp: wf_cdecl_def is_class_def class_def fun_upd_apply)
    moreover
    from wfcd sub1
    have "¬ ?P ⊢ D ≼⇧* C1" by(auto simp: wf_cdecl_def dest!: class_add_subcls_rev[OF _ ncp'])
    moreover
    have "⋀M b Ts T m D' b' Ts' T' m'. (M,b,Ts,T,m) ∈ set ms
            ⟹ ?P ⊢ D sees M,b':Ts' → T' = m' in D'
            ⟹ b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T'"
    proof -
      fix M b Ts T m D' b' Ts' T' m'
      assume ms: "(M,b,Ts,T,m) ∈ set ms" and meth': "?P ⊢ D sees M,b':Ts' → T' = m' in D'"
      with sub1
      have "P ⊢ D sees M,b':Ts' → T' = m' in D'"
       by(fastforce dest!: class_add_sees_method_rev[OF _ ncp'])
      moreover
      with wfcd ms meth'
      have "b = b' ∧ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T'"
       by(cases m', fastforce simp: wf_cdecl_def elim!: ballE[where x="(M,b,Ts,T,m)"])
      ultimately show "b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T'"
       by(auto dest!: class_add_subtype[OF _ nclass] class_add_widens[OF _ nclass])
    qed
    ultimately show ?thesis by clarsimp
  qed
  moreover note wfcd
  ultimately show ?thesis by(simp add: wf_cdecl_def)
qed

lemma class_add_wf_cdecl':
assumes wfcd: "wf_cdecl wf_md P cd" and cdP: "cd ∈ set P"
 and ncp: "¬P ⊢ fst cd ≼⇧* C" and dist: "distinct_fst P"
 and wfmd: "⋀C⇩0 S fs ms m.⟦(C⇩0,S,fs,ms) ∈ set P; m ∈ set ms⟧ ⟹ wf_md' (class_add P (C, cdec)) C⇩0 m"
 and nclass: "¬ is_class P C"
shows "wf_cdecl wf_md' (class_add P (C, cdec)) cd"
proof -
  let ?P = "class_add P (C, cdec)"
  obtain C1 D fs ms where [simp]: "cd = (C1,(D,fs,ms))" by(cases cd)
  from wfcd
  have "∀f∈set fs. wf_fdecl ?P f" by(auto simp: wf_cdecl_def wf_fdecl_def class_add_is_type)
  moreover
  from cdP wfcd wfmd
  have "∀m∈set ms. wf_mdecl wf_md' ?P C1 m"
    by(auto simp: wf_cdecl_def wf_mdecl_def class_add_is_type)
  moreover
  have "C1 ≠ Object ⟹ is_class ?P D ∧ ¬ ?P ⊢ D ≼⇧* C1
    ∧ (∀(M,b,Ts,T,m)∈set ms.
        ∀D' b' Ts' T' m'. ?P ⊢ D sees M,b':Ts' → T' = m' in D' ⟶
                       b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T')"
  proof -
    assume nObj[simp]: "C1 ≠ Object"
    with cdP dist have sub1: "P ⊢ C1 ≺⇧1 D" by(auto simp: class_def intro!: subcls1I map_of_SomeI)
    with ncp have ncp': "¬ P ⊢ D ≼⇧* C" by(auto simp: converse_rtrancl_into_rtrancl)
    with wfcd
    have clsD: "is_class ?P D"
     by(auto simp: wf_cdecl_def is_class_def class_def fun_upd_apply)
    moreover
    from wfcd sub1
    have "¬ ?P ⊢ D ≼⇧* C1" by(auto simp: wf_cdecl_def dest!: class_add_subcls_rev[OF _ ncp'])
    moreover
    have "⋀M b Ts T m D' b' Ts' T' m'. (M,b,Ts,T,m) ∈ set ms
            ⟹ ?P ⊢ D sees M,b':Ts' → T' = m' in D'
            ⟹ b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T'"
    proof -
      fix M b Ts T m D' b' Ts' T' m'
      assume ms: "(M,b,Ts,T,m) ∈ set ms" and meth': "?P ⊢ D sees M,b':Ts' → T' = m' in D'"
      with sub1
      have "P ⊢ D sees M,b':Ts' → T' = m' in D'"
       by(fastforce dest!: class_add_sees_method_rev[OF _ ncp'])
      moreover
      with wfcd ms meth'
      have "b = b' ∧ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T'"
       by(cases m', fastforce simp: wf_cdecl_def elim!: ballE[where x="(M,b,Ts,T,m)"])
      ultimately show "b = b' ∧ ?P ⊢ Ts' [≤] Ts ∧ ?P ⊢ T ≤ T'"
       by(auto dest!: class_add_subtype[OF _ nclass] class_add_widens[OF _ nclass])
    qed
    ultimately show ?thesis by clarsimp
  qed
  moreover note wfcd
  ultimately show ?thesis by(simp add: wf_cdecl_def)
qed

lemma class_add_wt_start:
 "⟦ wt_start P C⇩0 b Ts mxl τs; ¬ is_class P C ⟧
 ⟹ wt_start (class_add P (C, cdec)) C⇩0 b Ts mxl τs"
using class_add_sup_state_opt by(clarsimp simp: wt_start_def split: staticb.splits)

lemma class_add_wt_instr:
assumes wti: "P,T,mxs,mpc,xt ⊢ i,pc :: τs"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "class_add P (C, cdec),T,mxs,mpc,xt ⊢ i,pc :: τs"
proof -
  let ?P = "class_add P (C, cdec)"
  from wti have eff: "∀(pc', τ')∈set (eff i P pc xt (τs ! pc)). P ⊢ τ' ≤' τs ! pc'"
   by(simp add: wt_instr_def)
  from wti have app⇩i: "τs!pc ≠ None ⟹ app⇩i (i,P,pc,mxs,T,the (τs!pc))"
   by(simp add: wt_instr_def app_def)
  from wti class_add_app[OF _ wf nclass]
  have "app i ?P mxs T pc mpc xt (τs!pc)" by(simp add: wt_instr_def)
  moreover
  have "∀(pc',τ') ∈ set (eff i ?P pc xt (τs!pc)). ?P ⊢ τ' ≤' τs!pc'"
  proof(cases "τs!pc")
    case Some with eff class_add_eff_sup_state_opt[OF _ wf nclass app⇩i] show ?thesis by auto
  qed(simp add: eff_def)
  moreover note wti
  ultimately show ?thesis by(clarsimp simp: wt_instr_def)
qed

lemma class_add_wt_method:
assumes wtm: "wt_method P C⇩0 b Ts T⇩r mxs mxl⇩0 is xt (Φ C⇩0 M⇩0)"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "wt_method (class_add P (C, cdec)) C⇩0 b Ts T⇩r mxs mxl⇩0 is xt (Φ C⇩0 M⇩0)"
proof -
  let ?P = "class_add P (C, cdec)"
  let ?τs = "Φ C⇩0 M⇩0"
  from wtm class_add_check_types
  have "check_types ?P mxs ((case b of Static ⇒ 0 | NonStatic ⇒ 1)+size Ts+mxl⇩0) (map OK ?τs)"
   by(simp add: wt_method_def)
  moreover
  from wtm class_add_wt_start nclass
  have "wt_start ?P C⇩0 b Ts mxl⇩0 ?τs" by(simp add: wt_method_def)
  moreover
  from wtm class_add_wt_instr[OF _ wf nclass]
  have "∀pc < size is. ?P,T⇩r,mxs,size is,xt ⊢ is!pc,pc :: ?τs" by(clarsimp simp: wt_method_def)
  moreover note wtm
  ultimately
  show ?thesis by(clarsimp simp: wt_method_def)
qed

lemma class_add_wt_method':
 "⟦ (λP C (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)). wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M)) P C⇩0 md;
    wf_prog wf_md P; ¬ is_class P C ⟧
    ⟹ (λP C (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)). wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M))
            (class_add P (C, cdec)) C⇩0 md"
 by(clarsimp simp: class_add_wt_method)

subsection ‹ @{text "distinct_fst"} ›

lemma class_add_distinct_fst:
"⟦ distinct_fst P; ¬ is_class P C ⟧
  ⟹ distinct_fst (class_add P (C, cdec))"
 by(clarsimp simp: distinct_fst_def is_class_def class_def)

subsection "Conformance"

lemma class_add_conf:
 "⟦ P,h ⊢ v :≤ T; ¬ is_class P C ⟧
 ⟹ class_add P (C, cdec),h ⊢ v :≤ T"
 by(clarsimp simp: conf_def class_add_subtype)

lemma class_add_oconf:
fixes obj::obj
assumes oc: "P,h ⊢ obj √" and ns: "¬ is_class P C"
  and ncp: "⋀D'. P ⊢ fst(obj) ≼⇧* D' ⟹ D' ≠ C"
shows "(class_add P (C, cdec)),h ⊢ obj √"
proof -
  obtain C⇩0 fs where [simp]: "obj=(C⇩0,fs)" by(cases obj)
  from oc have
    oc': "⋀F D T. P ⊢ C⇩0 has F,NonStatic:T in D ⟹ (∃v. fs (F, D) = ⌊v⌋ ∧ P,h ⊢ v :≤ T)"
    by(simp add: oconf_def)
  have "⋀F D T. class_add P (C, cdec) ⊢ C⇩0 has F,NonStatic:T in D
                       ⟹ ∃v. fs(F,D) = Some v ∧ class_add P (C, cdec),h ⊢ v :≤ T"
  proof -
    fix F D T assume "class_add P (C, cdec) ⊢ C⇩0 has F,NonStatic:T in D"
    with class_add_has_field_rev[OF _ ncp] have meth: "P ⊢ C⇩0 has F,NonStatic:T in D" by simp
    then show "∃v. fs(F,D) = Some v ∧ class_add P (C, cdec),h ⊢ v :≤ T"
    using oc'[OF meth] class_add_conf[OF _ ns] by(fastforce simp: oconf_def)
  qed
  then show ?thesis by(simp add: oconf_def)
qed

lemma class_add_soconf:
assumes soc: "P,h,C⇩0 ⊢⇩s sfs √" and ns: "¬ is_class P C"
  and ncp: "⋀D'. P ⊢ C⇩0 ≼⇧* D' ⟹ D' ≠ C"
shows "(class_add P (C, cdec)),h,C⇩0 ⊢⇩s sfs √"
proof -
  from soc have
    oc': "⋀F T. P ⊢ C⇩0 has F,Static:T in C⇩0 ⟹ (∃v. sfs F = ⌊v⌋ ∧ P,h ⊢ v :≤ T)"
    by(simp add: soconf_def)
  have "⋀F T. class_add P (C, cdec) ⊢ C⇩0 has F,Static:T in C⇩0
                       ⟹ ∃v. sfs F = Some v ∧ class_add P (C, cdec),h ⊢ v :≤ T"
  proof -
    fix F T assume "class_add P (C, cdec) ⊢ C⇩0 has F,Static:T in C⇩0"
    with class_add_has_field_rev[OF _ ncp] have meth: "P ⊢ C⇩0 has F,Static:T in C⇩0" by simp
    then show "∃v. sfs F = Some v ∧ class_add P (C, cdec),h ⊢ v :≤ T"
    using oc'[OF meth] class_add_conf[OF _ ns] by(fastforce simp: soconf_def)
  qed
  then show ?thesis by(simp add: soconf_def)
qed

lemma class_add_hconf:
assumes "P ⊢ h √" and "¬ is_class P C"
 and "⋀a obj D'. h a = Some obj ⟹ P ⊢ fst(obj) ≼⇧* D' ⟹ D' ≠ C"
shows "class_add P (C, cdec) ⊢ h √"
using assms by(auto simp: hconf_def intro!: class_add_oconf)

lemma class_add_hconf_wf:
assumes wf: "wf_prog wf_md P" and "P ⊢ h √" and "¬ is_class P C"
 and "⋀a obj. h a = Some obj ⟹ fst(obj) ≠ C"
shows "class_add P (C, cdec) ⊢ h √"
using wf_subcls_nCls[OF wf] assms by(fastforce simp: hconf_def intro!: class_add_oconf)

lemma class_add_shconf:
assumes "P,h ⊢⇩s sh √" and ns: "¬ is_class P C"
 and "⋀C sobj D'. sh C = Some sobj ⟹ P ⊢ C ≼⇧* D' ⟹ D' ≠ C"
shows "class_add P (C, cdec),h ⊢⇩s sh √"
using assms by(fastforce simp: shconf_def)

lemma class_add_shconf_wf:
assumes wf: "wf_prog wf_md P" and "P,h ⊢⇩s sh √" and "¬ is_class P C"
 and "⋀C sobj. sh C = Some sobj ⟹ C ≠ C"
shows "class_add P (C, cdec),h ⊢⇩s sh √"
using wf_subcls_nCls[OF wf] assms by(fastforce simp: shconf_def)


end