(*  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 ≺¹ 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₀ has F,b:T in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊨ C₀ has F,b:T in D"
using assms by(auto simp: has_field_def dest!: class_add_has_fields[of P C₀])

lemma class_add_has_field_rev:
assumes has: "class_add P (C, cdec) ⊨ C₀ has F,b:T in D"
 and ncp: "∧D'. P ⊨ C₀ ⪯^* D' ==> D' ≠ C"
shows "P ⊨ C₀ 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₀ sees F,b:T in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊨ C₀ sees F,b:T in D"
using assms by(auto simp: sees_field_def dest!: class_add_has_fields[of P C₀])

lemma class_add_sees_field_rev:
assumes has: "class_add P (C, cdec) ⊨ C₀ sees F,b:T in D"
 and ncp: "∧D'. P ⊨ C₀ ⪯^* D' ==> D' ≠ C"
shows "P ⊨ C₀ 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₀ sees F,b:T in D" and "¬ is_class P C"
shows "field P C₀ F = field (class_add P (C, cdec)) C₀ 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 ≺¹ 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₀ sees M₀, b : Ts→T = m in D" and "¬ is_class P C"
shows "class_add P (C, cdec) ⊨ C₀ sees M₀, b : Ts→T = m in D"
using assms by(auto simp: Method_def dest!: class_add_sees_methods[of P C₀])

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

lemma class_add_sees_method_rev:
 "[ class_add P (C, cdec) ⊨ C₀ sees M₀, b : Ts→T = m in D;
    ¬ P ⊨ C₀ ⪯^* C ]
  ==> P ⊨ C₀ sees M₀, 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₀, b : Ts→T = m in D; C ≠ Object ]
  ==> class_add P (C, cdec) ⊨ Object sees M₀, 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₀, b : Ts→T = m in D; C ≠ Object ]
  ==> P ⊨ Object sees M₀, 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 ≤_\<top> l2; ¬ is_class P C ]
  ==> class_add P (C, cdec) ⊨ l1 ≤_\<top> 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 [≤_\<top>] LT'; ¬ is_class P C ]
 ==> class_add P (C, cdec) ⊨ LT [≤_\<top>] 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₀; ¬ is_class P C ]
  ==> is_relevant_class i (class_add P (C, cdec)) C₀"
  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₀"
  and ncp: "∧cd D'. cd ∈ set P ==> ¬P ⊨ fst cd ⪯^* C"
  and wfxp: "wf_syscls P"
shows "is_relevant_class i P C₀"
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₀ md;
     ∧C₀ md. wf_md P C₀ md ==> wf_md (class_add P (C, cdec)) C₀ md ]
  ==> wf_mdecl wf_md (class_add P (C, cdec)) C₀ md"
 by(clarsimp simp: wf_mdecl_def class_add_is_type)

lemma class_add_wf_mdecl':
assumes wfd: "wf_mdecl wf_md P C₀ md"
  and ms: "(C₀,S,fs,ms) ∈ set P" and md: "md ∈ set ms"
  and wf_md': "∧C₀ S fs ms m.[(C₀,S,fs,ms) ∈ set P; m ∈ set ms] ==> wf_md' (class_add P (C, cdec)) C₀ m"
shows "wf_mdecl wf_md' (class_add P (C, cdec)) C₀ 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₀ md. wf_md P C₀ md ==> wf_md (class_add P (C, cdec)) C₀ 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 ≺¹ 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₀ S fs ms m.[(C₀,S,fs,ms) ∈ set P; m ∈ set ms] ==> wf_md' (class_add P (C, cdec)) C₀ 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 ≺¹ 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₀ b Ts mxl τs; ¬ is_class P C ]
 ==> wt_start (class_add P (C, cdec)) C₀ 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₀ b Ts T_r mxs mxl₀ is xt (Φ C₀ M₀)"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "wt_method (class_add P (C, cdec)) C₀ b Ts T_r mxs mxl₀ is xt (Φ C₀ M₀)"
proof -
  let ?P = "class_add P (C, cdec)"
  let ?τs = "Φ C₀ M₀"
  from wtm class_add_check_types
  have "check_types ?P mxs ((case b of Static → 0 | NonStatic → 1)+size Ts+mxl₀) (map OK ?τs)"
   by(simp add: wt_method_def)
  moreover
  from wtm class_add_wt_start nclass
  have "wt_start ?P C₀ b Ts mxl₀ ?τ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₀,is,xt)). wt_method P C b Ts T_r mxs mxl₀ is xt (Φ C M)) P C₀ md;
    wf_prog wf_md P; ¬ is_class P C ]
    ==> (λP C (M,b,Ts,T_r,(mxs,mxl₀,is,xt)). wt_method P C b Ts T_r mxs mxl₀ is xt (Φ C M))
            (class_add P (C, cdec)) C₀ 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₀ fs where [simp]: "obj=(C₀,fs)" by(cases obj)
  from oc have
    oc': "∧F D T. P ⊨ C₀ 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₀ 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₀ has F,NonStatic:T in D"
    with class_add_has_field_rev[OF _ ncp] have meth: "P ⊨ C₀ 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₀ ⊨_s sfs √" and ns: "¬ is_class P C"
  and ncp: "∧D'. P ⊨ C₀ ⪯^* D' ==> D' ≠ C"
shows "(class_add P (C, cdec)),h,C₀ ⊨_s sfs √"
proof -
  from soc have
    oc': "∧F T. P ⊨ C₀ has F,Static:T in C₀ ==> (∃v. sfs F = ⌊v⌋ ∧ P,h ⊨ v :≤ T)"
    by(simp add: soconf_def)
  have "∧F T. class_add P (C, cdec) ⊨ C₀ has F,Static:T in C₀
                       ==> ∃v. sfs F = Some v ∧ class_add P (C, cdec),h ⊨ v :≤ T"
  proof -
    fix F T assume "class_add P (C, cdec) ⊨ C₀ has F,Static:T in C₀"
    with class_add_has_field_rev[OF _ ncp] have meth: "P ⊨ C₀ has F,Static:T in C₀" 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