Theory Place_Framework

theory Place_Framework
  imports HereditarilyFinite.HF MLSS_Extras MLSS_Decision_Proc.MLSS_Realisation
begin

definition places :: "'a set ⇒ ('a ⇒ bool) set" where
  "places V ≡ (λα. (λv. v ∈ α)) ` Pow V"

lemma places_domain:"π ∈ places V ⟹ x ∉ V ⟹ ¬ π x"
  unfolding places_def by blast

fun place_membership :: "'a pset_fm set ⇒ ('a ⇒ bool) set ⇒ (('a ⇒ bool) × ('a ⇒ bool)) set" where
  "place_membership 𝒞 PI = {(π⇩1, π⇩2) |π⇩1 π⇩2. π⇩1 ∈ PI ∧ π⇩2 ∈ PI ∧ (∃x y. AT (Var x =⇩s Single (Var y)) ∈ 𝒞 ∧ π⇩1 y ∧ π⇩2 x)}"

fun place_mem_graph :: "'a pset_fm set ⇒ ('a ⇒ bool) set ⇒ ('a ⇒ bool, ('a ⇒ bool) × ('a ⇒ bool)) pre_digraph" where
  "place_mem_graph 𝒞 PI = ⦇ verts = PI, arcs = place_membership 𝒞 PI, tail = fst, head = snd ⦈"

lemma place_mem_graph_wf_digraph: "wf_digraph (place_mem_graph 𝒞 PI)"
proof
  fix e assume "e ∈ arcs (place_mem_graph 𝒞 PI)"
  then have "e ∈ place_membership 𝒞 PI" by simp
  have "tail (place_mem_graph 𝒞 PI) e = fst e" by simp
  also have "... ∈ PI" using ‹e ∈ place_membership 𝒞 PI› by auto
  also have "... = verts (place_mem_graph 𝒞 PI)" by simp
  finally show "tail (place_mem_graph 𝒞 PI) e ∈ verts (place_mem_graph 𝒞 PI)" by simp
next
  fix e assume "e ∈ arcs (place_mem_graph 𝒞 PI)"
  then have "e ∈ place_membership 𝒞 PI" by simp
  have "head (place_mem_graph 𝒞 PI) e = snd e" by simp
  also have "... ∈ PI" using ‹e ∈ place_membership 𝒞 PI› by auto
  also have "... = verts (place_mem_graph 𝒞 PI)" by simp
  finally show "head (place_mem_graph 𝒞 PI) e ∈ verts (place_mem_graph 𝒞 PI)" by simp
qed

locale adequate_place_framework =
  normalized_MLSS_clause 𝒞 for 𝒞 +
    fixes PI :: "('a ⇒ bool) set"
  assumes PI_subset_places_V: "PI ⊆ places V"

    fixes at⇩p :: "('a × ('a ⇒ bool)) set"
  assumes dom_at⇩p: "Domain at⇩p = W"
      and range_at⇩p: "Range at⇩p ⊆ PI"
      and single_valued_at⇩p: "single_valued at⇩p"
    ― ‹dom_at_p together with single_valued_at_p and the definition of W are also part of C5.1 in the original paper›

  assumes membership_irreflexive: "(π, π) ∉ place_membership 𝒞 PI" (* Otherwise 𝒞 cannot hold *)
      and C6: "dag (place_mem_graph 𝒞 PI)"

  assumes C1_1: "∃n. AT (Var x =⇩s ∅ n) ∈ 𝒞 ⟹ ∀π ∈ PI. ¬ π x"
      and C1_2: "AT (Var x =⇩s Var y) ∈ 𝒞 ⟹ ∀π ∈ PI. π x ⟷ π y"
      and C2: "AT (Var x =⇩s Var y ⊔⇩s Var z) ∈ 𝒞 ⟹ ∀π ∈ PI. π x ⟷ π y ∨ π z"
      and C3: "AT (Var x =⇩s Var y -⇩s Var z) ∈ 𝒞 ⟹ ∀π ∈ PI. π x ⟷ π y ∧ ¬ π z"
      and C4: "AF (Var x =⇩s Var y) ∈ 𝒞 ⟹ ∃π ∈ PI. π x ⟷ ¬ π y"
      and C5_1: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞 ⟹ ∃π. (y, π) ∈ at⇩p ∧ π x ∧ (∀π' ∈ PI. π' ≠ π ⟶ ¬ π' x)"
      and C5_2: "⟦y ∈ W; z ∈ W; ∃π. (y, π) ∈ at⇩p ∧ (z, π) ∈ at⇩p⟧ ⟹
                 ∀π ∈ PI. π y ⟷ π z"
      and C5_3: "⟦y ∈ W; y' ∈ W; ∀π ∈ PI. π y' ⟷ π y⟧ ⟹ ∃π. (y, π) ∈ at⇩p ∧ (y', π) ∈ at⇩p"

      and C7: "⟦π⇩1 ∈ Range at⇩p - Range (place_membership 𝒞 PI);
                π⇩2 ∈ Range at⇩p - Range (place_membership 𝒞 PI)⟧ ⟹ π⇩1 = π⇩2"
begin

lemma finite_PI: "finite PI"
proof -
  from finite_𝒞 have "finite V" by (simp add: finite_vars_fm)
  then have "finite (places V)" unfolding places_def by simp
  then show ?thesis using PI_subset_places_V
    by (simp add: finite_subset)
qed

end

end