theory Horn_List
imports Horn_Inference
begin
locale horn_list_impl = horn +
fixes infer0_impl :: "'a list" and infer1_impl :: "'a ⇒ 'a list ⇒ 'a list"
begin
lemma saturate_fold_simp [simp]:
"fold (λxa. case_option None (f xa)) xs None = None"
by (induct xs) auto
lemma saturate_fold_mono [partial_function_mono]:
"option.mono_body (λf. fold (λx. case_option None (λy. f (x, y))) xs b)"
unfolding monotone_def fun_ord_def flat_ord_def
proof (intro allI impI, induct xs arbitrary: b)
case (Cons a xs)
show ?case
using Cons(1)[OF Cons(2), of "x (a, the b)"] Cons(2)[rule_format, of "(a, the b)"]
by (cases b) auto
qed auto
partial_function (option) saturate_rec :: "'a ⇒ 'a list ⇒ ('a list) option" where
"saturate_rec x bs = (if x ∈ set bs then Some bs else
fold (λx. case_option None (saturate_rec x)) (infer1_impl x bs) (Some (x # bs)))"
definition saturate_impl where
"saturate_impl = fold (λx. case_option None (saturate_rec x)) infer0_impl (Some [])"
end
locale horn_list = horn_list_impl +
assumes infer0: "infer0 = set infer0_impl"
and infer1: "⋀x bs. infer1 x (set bs) = set (infer1_impl x bs)"
begin
lemma saturate_rec_sound:
"saturate_rec x bs = Some bs' ⟹ ({x}, set bs) ⊢ ({}, set bs')"
proof (induct arbitrary: x bs bs' rule: saturate_rec.fixp_induct)
case 1 show ?case using option_admissible[of "λ(x, y) z. _ x y z"]
by fastforce
next
case (3 rec)
have [dest!]: "(set xs, set ys) ⊢ ({}, set bs')"
if "fold (λx a. case a of None ⇒ None | Some a ⇒ rec x a) xs (Some ys) = Some bs'"
for xs ys using that
proof (induct xs arbitrary: ys)
case (Cons a xs)
show ?case using trans[OF step_mono[OF 3(1)], of a ys _ "set xs" "{}" "set bs'"] Cons
by (cases "rec a ys") auto
qed (auto intro: refl)
show ?case using propagate[of x "{}" "set bs", unfolded infer1 Un_empty_left] 3(2)
by (auto split: if_splits intro: trans delete)
qed auto
lemma saturate_impl_sound:
assumes "saturate_impl = Some B'"
shows "set B' = saturate"
proof -
have "(set xs, set ys) ⊢ ({}, set bs')"
if "fold (λx a. case a of None ⇒ None | Some a ⇒ saturate_rec x a) xs (Some ys) = Some bs'"
for xs ys bs' using that
proof (induct xs arbitrary: ys)
case (Cons a xs)
show ?case
using trans[OF step_mono[OF saturate_rec_sound], of a ys _ "set xs" "{}" "set bs'"] Cons
by (cases "saturate_rec a ys") auto
qed (auto intro: refl)
from this[of infer0_impl "[]" B'] assms step_sound show ?thesis
by (auto simp: saturate_impl_def infer0)
qed
lemma saturate_impl_complete:
assumes "finite saturate"
shows "saturate_impl ≠ None"
proof -
have *: "fold (λx. case_option None (saturate_rec x)) ds (Some bs) ≠ None"
if "set bs ⊆ saturate" "set ds ⊆ saturate" for bs ds
using that
proof (induct "card (saturate - set bs)" arbitrary: bs ds rule: less_induct)
case less
show ?case using less(3)
proof (induct ds)
case (Cons d ds)
have "infer1 d (set bs) ⊆ saturate" using less(2) Cons(2)
unfolding infer1_def by (auto intro: saturate.infer)
moreover have "card (saturate - set (d # bs)) < card (saturate - set bs)" if "d ∉ set bs"
using card_insert[of "saturate - set bs" d] Cons(2) assms that
by (metis Diff_insert finite_Diff insert_Diff_if insert_absorb lessI list.set_intros(1) list.simps(15) set_mp)
ultimately show ?case using less(1)[of "d # bs" "infer1_impl d bs @ ds"] less(2) Cons assms
unfolding fold.simps comp_def option.simps
by (subst saturate_rec.simps) (auto split: if_splits simp: infer1)
qed simp
qed
show ?thesis using *[of "[]" "infer0_impl"] inv_start by (simp add: saturate_impl_def infer0)
qed
end
lemmas [code] = horn_list_impl.saturate_rec.simps horn_list_impl.saturate_impl_def
end