Theory MLSS_Realisation

theory MLSS_Realisation
  imports HereditarilyFinite.Finitary Graph_Theory.Graph_Theory
begin

section ‹The Realisation Function›
text ‹
  This theory contains an abstract formulation of a model
  for membership relations.
›

abbreviation parents :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a set"
  where "parents G s ≡ {u. u →⇘G⇙ s}"

abbreviation ancestors :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a set"
  where "ancestors G s ≡ {u. u →⇧+⇘G⇙ s}"

lemma (in fin_digraph) parents_subs_verts: "parents G s ⊆ verts G"
  using reachable_in_verts by blast

lemma (in fin_digraph) finite_parents[intro]: "finite (parents G s)"
  using finite_subset[OF parents_subs_verts finite_verts] .

lemma (in fin_digraph) finite_ancestors[intro]: "finite (ancestors G s)"
  using reachable_in_verts
  by (auto intro: rev_finite_subset[where ?A="ancestors G s", OF finite_verts])

lemma (in wf_digraph) in_ancestors_if_dominates[simp, intro]:
  assumes "s →⇘G⇙ t"
  shows "s ∈ ancestors G t"
  using assms by blast

lemma (in wf_digraph) ancestors_mono:
  assumes "s ∈ ancestors G t"
  shows "ancestors G s ⊆ ancestors G t"
  using assms by fastforce

locale dag = digraph G for G +
  assumes acyclic: "∄c. cycle c"
begin

lemma ancestors_asym:
  assumes "s ∈ ancestors G t"
  shows "t ∉ ancestors G s"
proof
  assume "t ∈ ancestors G s"
  then obtain p1 p2 where "awalk t p1 s" "p1 ≠ []" "awalk s p2 t" "p2 ≠ []"
    using assms reachable1_awalk by auto
  then have "closed_w (p1 @ p2)"
    unfolding closed_w_def by auto
  with closed_w_imp_cycle acyclic show False
    by blast
qed

lemma ancestors_strict_mono:
  assumes "s ∈ ancestors G t"
  shows "ancestors G s ⊂ ancestors G t"
  using assms ancestors_mono ancestors_asym by blast

lemma card_ancestors_strict_mono:
  assumes "s →⇘G⇙ t"
  shows "card (ancestors G s) < card (ancestors G t)"
  using assms finite_ancestors ancestors_strict_mono
  by (metis in_ancestors_if_dominates psubset_card_mono)

end

text ‹
  The realisation assumes that the terms can be split into
  a set of base terms ‹B› that are realised with the function ‹I›
  and set terms ‹T› that are realised according to the structure
  of the membership relation (represented as a graph ‹G›).
›
locale realisation = dag G for G +
  fixes B T :: "'a set"
  fixes I :: "'a ⇒ hf"
  fixes eq :: "'a rel"
  assumes B_T_partition_verts: "B ∩ T = {}" "verts G = B ∪ T"
  assumes P_urelems: "⋀p t. p ∈ B ⟹ ¬ t →⇘G⇙ p"
begin

lemma
  shows finite_B: "finite B"
    and finite_T: "finite T"
    and finite_B_un_T: "finite (B ∪ T)"
  using finite_verts B_T_partition_verts by auto

abbreviation "eq_class x ≡ eq `` {x}"

function realise :: "'a ⇒ hf" where
  "x ∈ B ⟹ realise x = HF (realise ` parents G x) ⊔ HF (I ` eq_class x)"
| "t ∈ T ⟹ realise t = HF (realise ` parents G t)"
| "x ∉ B ∪ T ⟹ realise x = 0"
  using B_T_partition_verts by auto
termination
  by (relation "measure (λt. card (ancestors G t))") (simp_all add: card_ancestors_strict_mono)

lemma finite_realisation_parents[simp, intro!]: "finite (realise ` parents G t)"
  by auto
 
function height :: "'a ⇒ nat" where
  "∀s. ¬ s →⇘G⇙ t ⟹ height t = 0"
| "s →⇘G⇙ t ⟹ height t = Max (height ` parents G t) + 1"
  using P_urelems by force+
termination
  by (relation "measure (λt. card (ancestors G t))") (simp_all add: card_ancestors_strict_mono)

lemma height_cases':
  obtains
      (Zero) "height t = 0"
    | (Suc_Max) s where "s →⇘G⇙ t" "height t = height s + 1"
  apply(cases t rule: height.cases)
  using Max_in[OF finite_imageI[where ?h=height, OF finite_parents]]
  by auto

lemma lemma1_1:
  assumes "s →⇘G⇙ t"
  shows "height s < height t"
proof(cases t rule: height_cases')
  case Zero
  with assms show ?thesis by simp
next
  case (Suc_Max s')
  note finite_imageI[where ?h=height, OF finite_parents]
  note Max_ge[OF this, of "height s" t]
  with assms Suc_Max show ?thesis
    by simp
qed

lemma dominates_if_mem_realisation:
  assumes "⋀x y. I x ≠ realise y"
  assumes "realise s ❙∈ realise t"
  obtains s' where "s' →⇘G⇙ t" "realise s = realise s'"
  using assms(2-)
proof(induction t rule: realise.induct)
  case (1 x)
  with assms(1) show ?case
    by simp (metis (no_types, lifting) image_iff mem_Collect_eq)
qed auto

lemma (in -) Max_le_if_All_Ex_le:
  assumes "finite A" "finite B"
      and "A ≠ {}"
      and "∀a ∈ A. ∃b ∈ B. a ≤ b"
    shows "Max A ≤ Max B"
  using assms
proof(induction rule: finite_induct)
  case (insert a A)
  then obtain b B' where "B = insert b B'"
    by (metis equals0I insert_absorb)
  with insert show ?case
    by (meson Max_ge_iff Max_in finite.insertI insert_not_empty)
qed blast

lemma lemma1_2':
  assumes "⋀x y. I x ≠ realise y"
  assumes "t1 ∈ B ∪ T" "t2 ∈ B ∪ T" "realise t1 = realise t2"
  shows "height t1 ≤ height t2"
  using assms(2-)
proof(induction "height t1" arbitrary: t1 t2 rule: less_induct)
  case less
  then show ?case
  proof(cases "height t1")
    case (Suc h)
    then obtain s1 where "s1 →⇘G⇙ t1"
      by (cases t1 rule: height.cases) auto
    have Ex_approx: "∃v. v →⇘G⇙ t2 ∧ realise w = realise v" if "w →⇘G⇙ t1" for w
    proof -
      from that less(2) have "realise w ❙∈ realise t1"
        by (induction t1 rule: realise.induct) auto
      with "less.prems" have "realise w ❙∈ realise t2"
        by metis
      with dominates_if_mem_realisation assms(1) obtain v
        where "v →⇘G⇙ t2" "realise w = realise v"
        by blast
      with less.prems show ?thesis
        by auto
    qed
    moreover
    have "height w ≤ height v"
      if "w →⇘G⇙ t1" "v ∈ B ∪ T" "realise w = realise v" for w v
    proof -
      have "w ∈ B ∪ T"
        using adj_in_verts[OF that(1)] B_T_partition_verts(2) by blast
      from "less.hyps"[OF lemma1_1, OF that(1) this that(2,3)] show ?thesis .
    qed
    ultimately have IH': "∃v ∈ parents G t2. height w ≤ height v"
      if "w ∈ parents G t1" for w
      by (metis that adj_in_verts(1) mem_Collect_eq B_T_partition_verts(2))
    then have Max_le: "Max (height ` parents G t1) ≤ Max (height ` parents G t2)"
    proof -
      have "finite (height ` parents G t1)"
           "finite (height ` parents G t2)"
           "height ` parents G t1 ≠ {}"
        using finite_parents ‹s1 →⇘G⇙ t1› by blast+
      with Max_le_if_All_Ex_le[OF this] IH' show ?thesis by blast
    qed
    show ?thesis 
    proof -
      note s1 = ‹s1 →⇘G⇙ t1›
      with Ex_approx obtain s2 where "s2 →⇘G⇙ t2"
        by blast
      with s1 Max_le show ?thesis by simp
    qed
  qed simp
qed

lemma lemma1_2:
  assumes "⋀x y. I x ≠ realise y"
  assumes "t1 ∈ B ∪ T" "t2 ∈ B ∪ T" "realise t1 = realise t2"
  shows "height t1 = height t2"
  using assms lemma1_2' le_antisym by metis

lemma lemma1_3:
  assumes "⋀x y. I x ≠ realise y"
  assumes "s ∈ B ∪ T" "t ∈ B ∪ T" "realise s ❙∈ realise t"
  shows "height s < height t"
proof -
  from dominates_if_mem_realisation[OF assms(1,4)] obtain s'
    where "s' →⇘G⇙ t" "realise s' = realise s"
    by metis
  then have "height s = height s'"
    using lemma1_2[OF assms(1,2)]
    by (metis adj_in_verts(1) B_T_partition_verts(2))
  also have "… < height t"
    using ‹s' →⇘G⇙ t› lemma1_1 by blast
  finally show ?thesis .
qed

end

end