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