Theory Regular_Tree_Relations.Horn_Inference

theory Horn_Inference
  imports Main
begin

datatype 'a horn = horn "'a list" 'a (infix ‹→⇩h› 55)

locale horn =
  fixes ℋ :: "'a horn set"
begin

inductive_set saturate :: "'a set" where
  infer: "as →⇩h a ∈ ℋ ⟹ (⋀x. x ∈ set as ⟹ x ∈ saturate) ⟹ a ∈ saturate"

definition infer0 where
  "infer0 = {a. [] →⇩h a ∈ ℋ}"

definition infer1 where
  "infer1 x B = {a |as a. as →⇩h a ∈ ℋ ∧ x ∈ set as ∧ set as ⊆ B ∪ {x}}"

inductive step :: "'a set × 'a set ⇒ 'a set × 'a set ⇒ bool" (infix ‹⊢› 50) where
  delete: "x ∈ B ⟹ (insert x G, B) ⊢ (G, B)"
| propagate: "(insert x G, B) ⊢ (G ∪ infer1 x B, insert x B)"
| refl: "(G, B) ⊢ (G, B)"
| trans: "(G, B) ⊢ (G', B') ⟹ (G', B') ⊢ (G'', B'') ⟹ (G, B) ⊢ (G'', B'')"

lemma step_mono:
  "(G, B) ⊢ (G', B') ⟹ (H ∪ G, B) ⊢ (H ∪ G', B')"
  by (induction "(G, B)" "(G', B')" arbitrary: G B G' B' rule: step.induct)
    (auto intro: step.intros simp: Un_assoc[symmetric])

fun invariant where
  "invariant (G, B) ⟷ G ⊆ saturate ∧ B ⊆ saturate ∧ (∀a as. as →⇩h a ∈ ℋ ∧ set as ⊆ B ⟶ a ∈ G ∪ B)"

lemma inv_start:
  shows "invariant (infer0, {})"
  by (auto simp: infer0_def invariant.simps intro: infer)

lemma inv_step:
  assumes "invariant (G, B)" "(G, B) ⊢ (G', B')"
  shows "invariant (G', B')"
  using assms(2,1)
proof (induction "(G, B)" "(G', B')" arbitrary: G B G' B' rule: step.induct)
  case (propagate x G B)
  let ?G' = "G ∪ local.infer1 x B" and ?B' = "insert x B"
  have "?G' ⊆ saturate" "?B' ⊆ saturate"
    using assms(1) propagate by (auto 0 3 simp: infer1_def intro: saturate.infer)
  moreover have "as →⇩h a ∈ ℋ ⟹ set as ⊆ ?B' ⟹ a ∈ ?G' ∪ ?B'" for a as
    using assms(1) propagate by (fastforce simp: infer1_def)
  ultimately show ?case by auto
qed auto

lemma inv_end:
  assumes "invariant ({}, B)"
  shows "B = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) then show ?case using assms by auto
next
  case (rl x) then show ?case using assms
    by (induct x rule: saturate.induct) fastforce
qed

lemma step_sound:
  "(infer0, {}) ⊢ ({}, B) ⟹ B = saturate"
  by (metis inv_start inv_step inv_end)

end

lemma horn_infer0_union:
  "horn.infer0 (ℋ⇩1 ∪ ℋ⇩2) = horn.infer0 ℋ⇩1 ∪ horn.infer0 ℋ⇩2"
  by (auto simp: horn.infer0_def)

lemma horn_infer1_union:
  "horn.infer1 (ℋ⇩1 ∪ ℋ⇩2) x B = horn.infer1 ℋ⇩1 x B ∪ horn.infer1 ℋ⇩2 x B"
  by (auto simp: horn.infer1_def)

end