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

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

lemma class_add_sees_field_rev:
assumes has: "class_add P (C, cdec)  C0 sees F,b:T in D"
 and ncp: "D'. P  C0 * D'  D'  C"
shows "P  C0 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  C0 sees F,b:T in D" and "¬ is_class P C"
shows "field P C0 F = field (class_add P (C, cdec)) C0 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  C0 sees M0, b : TsT = m in D" and "¬ is_class P C"
shows "class_add P (C, cdec)  C0 sees M0, b : TsT = m in D"
using assms by(auto simp: Method_def dest!: class_add_sees_methods[of P C0])

lemma class_add_method:
assumes md: "P  C0 sees M0, b : TsT = m in D" and "¬ is_class P C"
shows "method P C0 M0 = method (class_add P (C, cdec)) C0 M0"
using class_add_sees_method[OF assms, of cdec] md by simp

lemma class_add_sees_method_rev:
 " class_add P (C, cdec)  C0 sees M0, b : TsT = m in D;
    ¬ P  C0 * C 
   P  C0 sees M0, b : TsT = m in D"
 by(auto simp: Method_def dest!: class_add_sees_methods_rev)

lemma class_add_sees_method_Obj:
 " P  Object sees M0, b : TsT = m in D; C  Object 
   class_add P (C, cdec)  Object sees M0, b : TsT = 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 M0, b : TsT = m in D; C  Object 
   P  Object sees M0, b : TsT = 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 C0; ¬ is_class P C 
   is_relevant_class i (class_add P (C, cdec)) C0"
  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)) C0"
  and ncp: "cd D'. cd  set P  ¬P  fst cd * C"
  and wfxp: "wf_syscls P"
shows "is_relevant_class i P C0"
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: "appi (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: "appi (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_appi:
assumes "appi (i, P, pc, mxs, Tr, ST, LT)" and "¬ is_class P C"
shows "appi (i, class_add P (C, cdec), pc, mxs, Tr, 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 appi: "appi (i,P,pc,mxs,T,τ)" by(simp add: app_def)
  with class_add_appi[OF _ nclass] Some have "appi (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 C0 md;
     C0 md. wf_md P C0 md  wf_md (class_add P (C, cdec)) C0 md 
   wf_mdecl wf_md (class_add P (C, cdec)) C0 md"
 by(clarsimp simp: wf_mdecl_def class_add_is_type)

lemma class_add_wf_mdecl':
assumes wfd: "wf_mdecl wf_md P C0 md"
  and ms: "(C0,S,fs,ms)  set P" and md: "md  set ms"
  and wf_md': "C0 S fs ms m.(C0,S,fs,ms)  set P; m  set ms  wf_md' (class_add P (C, cdec)) C0 m"
shows "wf_mdecl wf_md' (class_add P (C, cdec)) C0 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: "C0 md. wf_md P C0 md  wf_md (class_add P (C, cdec)) C0 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 "fset 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 "mset 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: "C0 S fs ms m.(C0,S,fs,ms)  set P; m  set ms  wf_md' (class_add P (C, cdec)) C0 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 "fset fs. wf_fdecl ?P f" by(auto simp: wf_cdecl_def wf_fdecl_def class_add_is_type)
  moreover
  from cdP wfcd wfmd
  have "mset 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 C0 b Ts mxl τs; ¬ is_class P C 
  wt_start (class_add P (C, cdec)) C0 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 appi: "τs!pc  None  appi (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 appi] 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 C0 b Ts Tr mxs mxl0 is xt (Φ C0 M0)"
 and wf: "wf_prog wf_md P" and nclass: "¬ is_class P C"
shows "wt_method (class_add P (C, cdec)) C0 b Ts Tr mxs mxl0 is xt (Φ C0 M0)"
proof -
  let ?P = "class_add P (C, cdec)"
  let ?τs = "Φ C0 M0"
  from wtm class_add_check_types
  have "check_types ?P mxs ((case b of Static  0 | NonStatic  1)+size Ts+mxl0) (map OK ?τs)"
   by(simp add: wt_method_def)
  moreover
  from wtm class_add_wt_start nclass
  have "wt_start ?P C0 b Ts mxl0 ?τs" by(simp add: wt_method_def)
  moreover
  from wtm class_add_wt_instr[OF _ wf nclass]
  have "pc < size is. ?P,Tr,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,Tr,(mxs,mxl0,is,xt)). wt_method P C b Ts Tr mxs mxl0 is xt (Φ C M)) P C0 md;
    wf_prog wf_md P; ¬ is_class P C 
     (λP C (M,b,Ts,Tr,(mxs,mxl0,is,xt)). wt_method P C b Ts Tr mxs mxl0 is xt (Φ C M))
            (class_add P (C, cdec)) C0 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 C0 fs where [simp]: "obj=(C0,fs)" by(cases obj)
  from oc have
    oc': "F D T. P  C0 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)  C0 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)  C0 has F,NonStatic:T in D"
    with class_add_has_field_rev[OF _ ncp] have meth: "P  C0 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,C0 s sfs " and ns: "¬ is_class P C"
  and ncp: "D'. P  C0 * D'  D'  C"
shows "(class_add P (C, cdec)),h,C0 s sfs "
proof -
  from soc have
    oc': "F T. P  C0 has F,Static:T in C0  (v. sfs F = v  P,h  v :≤ T)"
    by(simp add: soconf_def)
  have "F T. class_add P (C, cdec)  C0 has F,Static:T in C0
                        v. sfs F = Some v  class_add P (C, cdec),h  v :≤ T"
  proof -
    fix F T assume "class_add P (C, cdec)  C0 has F,Static:T in C0"
    with class_add_has_field_rev[OF _ ncp] have meth: "P  C0 has F,Static:T in C0" 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