Theory Subcls

(*  Title:      RTS/JinjaSuppl/Subcls.thy
    Author:    Susannah Mansky, UIUC 2020
    Description:  Theory for the subcls relation
*)

section "@{term subcls} theory"

theory Subcls
imports JinjaDCI.TypeRel
begin

lemma subcls_class_ex: "⟦ P ⊢ C ≼⇧^* C'; C ≠ C' ⟧
 ⟹ ∃D' fs ms. class P C = ⌊(D', fs, ms)⌋"
proof(induct rule: converse_rtrancl_induct)
  case (step y z) then show ?case by(auto dest: subcls1D)
qed(simp)

lemma class_subcls1:
 "⟦ class P y = class P' y; P ⊢ y ≺⇧¹ z ⟧ ⟹ P' ⊢ y ≺⇧¹ z"
 by(auto dest!: subcls1D intro!: subcls1I intro: sym)


lemma subcls1_single_valued: "single_valued (subcls1 P)"
by (clarsimp simp: single_valued_def subcls1.simps)

lemma subcls_confluent:
  "⟦ P ⊢ C ≼⇧^* C'; P ⊢ C ≼⇧^* C'' ⟧ ⟹ P ⊢ C' ≼⇧^* C'' ∨ P ⊢ C'' ≼⇧^* C'"
 by (simp add: single_valued_confluent subcls1_single_valued)

lemma subcls1_confluent: "⟦ P ⊢ a ≺⇧¹ b; P ⊢ a ≼⇧^* c; a ≠ c ⟧ ⟹ P ⊢ b ≼⇧^* c"
using subcls1_single_valued
 by (auto elim!: converse_rtranclE[where x=a] simp: single_valued_def)


lemma subcls_self_superclass: "⟦ P ⊢ C ≺⇧¹ C; P ⊢ C ≼⇧^* D ⟧ ⟹ D = C"
using subcls1_single_valued
 by (auto elim!: rtrancl_induct[where b=D] simp: single_valued_def)

lemma subcls_of_Obj_acyclic:
 "⟦ P ⊢ C ≼⇧^* Object; C ≠ D⟧ ⟹ ¬(P ⊢ C ≼⇧^* D ∧ P ⊢ D ≼⇧^* C)"
proof(induct arbitrary: D rule: converse_rtrancl_induct)
  case base then show ?case by simp
next
  case (step y z) show ?case
  proof(cases "y=z")
    case True with step show ?thesis by simp
  next
    case False show ?thesis
    proof(cases "z = D")
      case True with False step.hyps(3)[of y] show ?thesis by clarsimp
    next
      case neq: False
      with step.hyps(3) have "¬(P ⊢ z ≼⇧^* D ∧ P ⊢ D ≼⇧^* z)" by simp
      moreover from step.hyps(1)
      have "P ⊢ D ≼⇧^* y ⟹ P ⊢ D ≼⇧^* z" by(simp add: rtrancl_into_rtrancl)
      moreover from step.hyps(1) step.prems(1)
      have "P ⊢ y ≼⇧^* D ⟹ P ⊢ z ≼⇧^* D" by(simp add: subcls1_confluent)
      ultimately show ?thesis by clarsimp
    qed
  qed
qed

lemma subcls_of_Obj: "⟦ P ⊢ C ≼⇧^* Object; P ⊢ C ≼⇧^* D ⟧ ⟹ P ⊢ D ≼⇧^* Object"
 by(auto dest: subcls_confluent)

end