# 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
```