Theory ClassesAbove

(*  Title:      RTS/JinjaSuppl/ClassesAbove.thy
    Author:    Susannah Mansky, UIUC 2020
*)

section "@{term classes_above} theory"

text "This section contains theory around the classes above
 (superclasses of) a class in the class structure, in particular
 noting that if their contents have not changed, then much of what
 that class sees (methods, fields) stays the same."

theory ClassesAbove
imports ClassesChanged Subcls JinjaDCI.Exceptions
begin

abbreviation classes_above :: "'m prog ⇒ cname ⇒ cname set" where
"classes_above P c ≡ { cn. P ⊢ c ≼⇧* cn }"

abbreviation classes_between :: "'m prog ⇒ cname ⇒ cname ⇒ cname set" where
"classes_between P c d ≡ { cn. (P ⊢ c ≼⇧* cn ∧ P ⊢ cn ≼⇧* d) }"

abbreviation classes_above_xcpts :: "'m prog ⇒ cname set" where
"classes_above_xcpts P ≡ ⋃x∈sys_xcpts. classes_above P x"

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

lemma classes_above_def2:
 "P ⊢ C ≺⇧1 D ⟹ classes_above P C = {C} ∪ classes_above P D"
using subcls1_confluent by auto

lemma classes_above_class:
 "⟦ classes_above P C ∩ classes_changed P P' = {}; P ⊢ C ≼⇧* C' ⟧
  ⟹ class P C' = class P' C'"
 by (drule classes_changed_class_set, simp)

lemma classes_above_subset:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "classes_above P C ⊆ classes_above P' C"
proof -
  have ind: "⋀x. P ⊢ C ≼⇧* x ⟹ P' ⊢ C ≼⇧* x"
  proof -
    fix x assume sub: "P ⊢ C ≼⇧* x"
    then show "P' ⊢ C ≼⇧* x"
    proof(induct rule: rtrancl_induct)
      case base then show ?case by simp
    next
      case (step y z)
      have "P' ⊢ y ≺⇧1 z" by(rule class_subcls1[OF classes_above_class[OF assms step(1)] step(2)])
      then show ?case using step(3) by simp
    qed
  qed
  with classes_changed_class_set[OF assms] show ?thesis by clarsimp
qed

lemma classes_above_subcls:
 "⟦ classes_above P C ∩ classes_changed P P' = {}; P ⊢ C ≼⇧* C' ⟧
   ⟹ P' ⊢ C ≼⇧* C'"
 by (fastforce dest: classes_above_subset)

lemma classes_above_subset2:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "classes_above P' C ⊆ classes_above P C"
proof -
  have ind: "⋀x. P' ⊢ C ≼⇧* x ⟹ P ⊢ C ≼⇧* x"
  proof -
    fix x assume sub: "P' ⊢ C ≼⇧* x"
    then show "P ⊢ C ≼⇧* x"
    proof(induct rule: rtrancl_induct)
      case base then show ?case by simp
    next
      case (step y z)
      with class_subcls1 classes_above_class[OF assms] rtrancl_into_rtrancl show ?case by metis
    qed
  qed
  with classes_changed_class_set[OF assms] show ?thesis by clarsimp
qed

lemma classes_above_subcls2:
 "⟦ classes_above P C ∩ classes_changed P P' = {}; P' ⊢ C ≼⇧* C' ⟧
   ⟹ P ⊢ C ≼⇧* C'"
 by (fastforce dest: classes_above_subset2)

lemma classes_above_set:
 "⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
  ⟹ classes_above P C = classes_above P' C"
 by(fastforce dest: classes_above_subset classes_above_subset2)

lemma classes_above_classes_changed_sym:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "classes_above P' C ∩ classes_changed P' P = {}"
proof -
  have "classes_above P C = classes_above P' C" by(rule classes_above_set[OF assms])
  with classes_changed_sym[where P=P] assms show ?thesis by simp
qed

lemma classes_above_sub_classes_between_eq:
 "P ⊢ C ≼⇧* D ⟹ classes_above P C = (classes_between P C D - {D}) ∪ classes_above P D"
using subcls_confluent by auto

lemma classes_above_subcls_subset:
 "⟦ P ⊢ C ≼⇧* C' ⟧ ⟹ classes_above P C' ⊆ classes_above P C"
 by auto

(************************************************************)
subsection "Methods"

lemma classes_above_sees_methods:
assumes int: "classes_above P C ∩ classes_changed P P' = {}" and ms: "P ⊢ C sees_methods Mm"
shows "P' ⊢ C sees_methods Mm"
proof -
  have cls: "∀C'∈classes_above P C. class P C' = class P' C'"
   by(rule classes_changed_class_set[OF int])

  have "⋀C Mm. P ⊢ C sees_methods Mm ⟹
               ∀C'∈classes_above P C. class P C' = class P' C' ⟹ P' ⊢ C sees_methods Mm"
  proof -
    fix C Mm assume "P ⊢ C sees_methods Mm" and "∀C'∈classes_above P C. class P C' = class P' C'"
    then show "P' ⊢ C sees_methods Mm"
    proof(induct rule: Methods.induct)
      case Obj: (sees_methods_Object D fs ms Mm)
      with cls have "class P' Object = ⌊(D, fs, ms)⌋" by simp
      with Obj show ?case by(auto intro!: sees_methods_Object)
    next
      case rec: (sees_methods_rec C D fs ms Mm Mm')
      then have "P ⊢ C ≼⇧* D" by (simp add: r_into_rtrancl[OF subcls1I])
      with converse_rtrancl_into_rtrancl have "⋀x. P ⊢ D ≼⇧* x ⟹ P ⊢ C ≼⇧* x" by simp
      with rec.prems(1) have "∀C'∈classes_above P D. class P C' = class P' C'" by simp
      with rec show ?case by(auto intro: sees_methods_rec)
    qed
  qed
  with ms cls show ?thesis by simp
qed

lemma classes_above_sees_method:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
     P ⊢ C sees M,b: Ts→T = m in C' ⟧
  ⟹ P' ⊢ C sees M,b: Ts→T = m in C'"
 by (auto dest: classes_above_sees_methods simp: Method_def)

lemma classes_above_sees_method2:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
     P' ⊢ C sees M,b: Ts→T = m in C' ⟧
  ⟹ P ⊢ C sees M,b: Ts→T = m in C'"
 by (auto dest: classes_above_classes_changed_sym intro: classes_above_sees_method)

lemma classes_above_method:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "method P C M = method P' C M"
proof(cases "∃Ts T m D b. P ⊢ C sees M,b :  Ts→T = m in D")
  case True
  with assms show ?thesis by (auto dest: classes_above_sees_method)
next
  case False
  with assms have "¬(∃Ts T m D b. P' ⊢ C sees M,b :  Ts→T = m in D)"
    by (auto dest: classes_above_sees_method2)
  with False show ?thesis by(simp add: method_def)
qed

(*********************************************)
subsection "Fields"

lemma classes_above_has_fields:
assumes int: "classes_above P C ∩ classes_changed P P' = {}" and fs: "P ⊢ C has_fields FDTs"
shows "P' ⊢ C has_fields FDTs"
proof -
  have cls: "∀C'∈classes_above P C. class P C' = class P' C'"
   by(rule classes_changed_class_set[OF int])

  have "⋀C Mm. P ⊢ C has_fields FDTs ⟹
               ∀C'∈classes_above P C. class P C' = class P' C' ⟹ P' ⊢ C has_fields FDTs"
  proof -
    fix C Mm assume "P ⊢ C has_fields FDTs" and "∀C'∈classes_above P C. class P C' = class P' C'"
    then show "P' ⊢ C has_fields FDTs"
    proof(induct rule: Fields.induct)
      case Obj: (has_fields_Object D fs ms FDTs)
      with cls have "class P' Object = ⌊(D, fs, ms)⌋" by simp
      with Obj show ?case by(auto intro!: has_fields_Object)
    next
      case rec: (has_fields_rec C D fs ms FDTs FDTs')
      then have "P ⊢ C ≼⇧* D" by (simp add: r_into_rtrancl[OF subcls1I])
      with converse_rtrancl_into_rtrancl have "⋀x. P ⊢ D ≼⇧* x ⟹ P ⊢ C ≼⇧* x" by simp
      with rec.prems(1) have "∀x. P ⊢ D ≼⇧* x ⟶ class P x = class P' x" by simp
      with rec show ?case by(auto intro: has_fields_rec)
    qed
  qed
  with fs cls show ?thesis by simp
qed

lemma classes_above_has_fields_dne:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "(∀FDTs. ¬ P ⊢ C has_fields FDTs) = (∀FDTs. ¬ P' ⊢ C has_fields FDTs)"
proof(rule iffI)
  assume asm: "∀FDTs. ¬ P ⊢ C has_fields FDTs"
  from assms classes_changed_sym[where P=P] classes_above_set[OF assms]
   have int': "classes_above P' C ∩ classes_changed P' P = {}" by simp
  from asm classes_above_has_fields[OF int'] show "∀FDTs. ¬ P' ⊢ C has_fields FDTs" by auto
next
  assume "∀FDTs. ¬ P' ⊢ C has_fields FDTs"
  with assms show "∀FDTs. ¬ P ⊢ C has_fields FDTs" by(auto dest: classes_above_has_fields)
qed

lemma classes_above_has_field:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
    P ⊢ C has F,b:t in C' ⟧
   ⟹ P' ⊢ C has F,b:t in C'"
 by(auto dest: classes_above_has_fields simp: has_field_def)

lemma classes_above_has_field2:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
     P' ⊢ C has F,b:t in C' ⟧
  ⟹ P ⊢ C has F,b:t in C'"
 by(auto intro: classes_above_has_field dest: classes_above_classes_changed_sym)

lemma classes_above_sees_field:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
    P ⊢ C sees F,b:t in C' ⟧
   ⟹ P' ⊢ C sees F,b:t in C'"
 by(auto dest: classes_above_has_fields simp: sees_field_def)

lemma classes_above_sees_field2:
 "⟦ classes_above P C ∩ classes_changed P P' = {};
     P' ⊢ C sees F,b:t in C' ⟧
  ⟹ P ⊢ C sees F,b:t in C'"
 by (auto intro: classes_above_sees_field dest: classes_above_classes_changed_sym)

lemma classes_above_field:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "field P C F = field P' C F"
proof(cases "∃T D b. P ⊢ C sees F,b : T in D")
  case True
  with assms show ?thesis by (auto dest: classes_above_sees_field)
next
  case False
  with assms have "¬(∃T D b. P' ⊢ C sees F,b : T in D)"
    by (auto dest: classes_above_sees_field2)
  with False show ?thesis by(simp add: field_def)
qed

lemma classes_above_fields:
assumes "classes_above P C ∩ classes_changed P P' = {}"
shows "fields P C = fields P' C"
proof(cases "∃FDTs. P ⊢ C has_fields FDTs")
  case True
  with assms show ?thesis by(auto dest: classes_above_has_fields)
next
  case False
  with assms show ?thesis by (auto dest: classes_above_has_fields_dne simp: fields_def)
qed

lemma classes_above_ifields:
 "⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
 ⟹
  ifields P C = ifields P' C"
 by (simp add: ifields_def classes_above_fields)


lemma classes_above_blank:
 "⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
 ⟹
  blank P C = blank P' C"
 by (simp add: blank_def classes_above_ifields)

lemma classes_above_isfields:
 "⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
 ⟹
  isfields P C = isfields P' C"
 by (simp add: isfields_def classes_above_fields)

lemma classes_above_sblank:
 "⟦ classes_above P C ∩ classes_changed P P' = {} ⟧
 ⟹
  sblank P C = sblank P' C"
 by (simp add: sblank_def classes_above_isfields)

(******************************************)
subsection "Other"

lemma classes_above_start_heap:
assumes "classes_above_xcpts P ∩ classes_changed P P' = {}"
shows "start_heap P = start_heap P'"
proof -
  from assms have "∀C ∈ sys_xcpts. blank P C = blank P' C" by (auto intro: classes_above_blank)
  then show ?thesis by(simp add: start_heap_def)
qed

end