Theory MLSS_Proc
theory MLSS_Proc
imports MLSS_Realisation MLSS_HF_Extras MLSS_Semantics MLSS_Typing
begin
section ‹A Decision Procedure for MLSS›
text ‹
This theory proves the soundness and completeness of the
tableau calculus defined in 🗏‹./MLSS_Calculus.thy›
It then lifts those properties to a recursive procedure
that applies the rules of the calculus exhaustively.
To obtain a decision procedure, we also prove termination.
›
subsection ‹Basic Definitions›
definition "lin_sat b ≡ ∀b'. lexpands b' b ⟶ set b' ⊆ set b"
lemma lin_satD:
assumes "lin_sat b"
assumes "lexpands b' b"
assumes "x ∈ set b'"
shows "x ∈ set b"
using assms unfolding lin_sat_def by auto
lemma not_lin_satD: "¬ lin_sat b ⟹ ∃b'. lexpands b' b ∧ set b ⊂ set (b' @ b)"
unfolding lin_sat_def by auto
definition "sat b ≡ lin_sat b ∧ (∄bs'. bexpands bs' b)"
lemma satD:
assumes "sat b"
shows "lin_sat b" "∄bs'. bexpands bs' b"
using assms unfolding sat_def by auto
definition wits :: "'a branch ⇒ 'a set" where
"wits b ≡ vars b - vars (last b)"
definition pwits :: "'a branch ⇒ 'a set" where
"pwits b ≡ {c ∈ wits b. ∀t ∈ subterms (last b).
AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b}"
lemma wits_singleton[simp]: "wits [φ] = {}"
unfolding wits_def vars_branch_simps by simp
lemma pwits_singleton[simp]: "pwits [φ] = {}"
unfolding pwits_def by auto
lemma pwitsD:
assumes "c ∈ pwits b"
shows "c ∈ wits b"
"t ∈ subterms (last b) ⟹ AT (Var c =⇩s t) ∉ set b"
"t ∈ subterms (last b) ⟹ AT (t =⇩s Var c) ∉ set b"
using assms unfolding pwits_def by auto
lemma pwitsI:
assumes "c ∈ wits b"
assumes "⋀t. t ∈ subterms (last b) ⟹ AT (Var c =⇩s t) ∉ set b"
assumes "⋀t. t ∈ subterms (last b) ⟹ AT (t =⇩s Var c) ∉ set b"
shows "c ∈ pwits b"
using assms unfolding pwits_def by blast
lemma finite_wits: "finite (wits b)"
unfolding wits_def using finite_vars_branch by auto
lemma finite_pwits: "finite (pwits b)"
proof -
have "pwits b ⊆ wits b"
unfolding pwits_def by simp
then show ?thesis using finite_wits finite_subset by blast
qed
lemma lexpands_subterms_branch_eq:
"lexpands b' b ⟹ b ≠ [] ⟹ subterms (b' @ b) = subterms b"
proof(induction rule: lexpands.induct)
case (1 b' b)
then show ?case
apply(induction rule: lexpands_fm.induct)
apply(auto simp: subterms_branch_def)
done
next
case (2 b' b)
then show ?case
apply(induction rule: lexpands_un.induct)
using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
apply(auto simp: subterms_branch_simps
intro: subterms_term_subterms_branch_trans
dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
done
next
case (3 b' b)
then show ?case
apply(induction rule: lexpands_int.induct)
using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
apply(auto simp: subterms_branch_simps
intro: subterms_term_subterms_branch_trans
dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
done
next
case (4 b' b)
then show ?case
apply(induction rule: lexpands_diff.induct)
using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
apply(auto simp: subterms_branch_simps
intro: subterms_term_subterms_branch_trans
dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
done
next
case (5 b' b)
then show ?case
proof(induction rule: lexpands_single.induct)
case (1 t1 b)
then show ?case
using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
apply(auto simp: subterms_branch_simps
dest: subterms_fmD intro: subterms_term_subterms_branch_trans)
done
qed (auto simp: subterms_branch_simps subterms_term_subterms_atom_Atom_trans
dest: subterms_branchD AF_mem_subterms_branchD
intro: subterms_term_subterms_branch_trans)
next
case (6 b' b)
have *: "subterms_atom (subst_tlvl t1 t2 a) ⊆ subterms t2 ∪ subterms_atom a"
for t1 t2 and a :: "'a pset_atom"
by (cases "(t1, t2, a)" rule: subst_tlvl.cases) auto
from 6 show ?case
by (induction rule: lexpands_eq.induct)
(auto simp: subterms_branch_def subterms_term_subterms_atom_Atom_trans
dest!: subsetD[OF *])
qed
lemma lexpands_vars_branch_eq:
"lexpands b' b ⟹ b ≠ [] ⟹ vars (b' @ b) = vars b"
using lexpands_subterms_branch_eq subterms_branch_eq_if_vars_branch_eq by metis
lemma bexpands_nowit_subterms_branch_eq:
"bexpands_nowit bs' b ⟹ b' ∈ bs' ⟹ b ≠ [] ⟹ subterms (b' @ b) = subterms b"
proof(induction rule: bexpands_nowit.induct)
case (3 s t1 t2 b)
then show ?case
by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
next
case (4 s t1 b t2)
then show ?case
using subterms_branch_subterms_subterms_fm_trans[OF _ _ "4"(2)]
by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
next
case (5 s t1 b t2)
then show ?case
using subterms_branch_subterms_subterms_fm_trans[OF _ _ "5"(2)]
by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
qed (use subterms_branch_def in ‹(fastforce simp: subterms_branch_simps)+›)
lemma bexpands_nowit_vars_branch_eq:
"bexpands_nowit bs' b ⟹ b' ∈ bs' ⟹ b ≠ [] ⟹ vars (b' @ b) = vars b"
using bexpands_nowit_subterms_branch_eq subterms_branch_eq_if_vars_branch_eq by metis
lemma lexpands_wits_eq:
"lexpands b' b ⟹ b ≠ [] ⟹ wits (b' @ b) = wits b"
using lexpands_vars_branch_eq unfolding wits_def by force
lemma bexpands_nowit_wits_eq:
assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
shows "wits (b' @ b) = wits b"
using bexpands_nowit_vars_branch_eq[OF assms] assms(3)
unfolding wits_def by simp
lemma bexpands_wit_vars_branch_eq:
assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
shows "vars (b' @ b) = insert x (vars b)"
using assms bexpands_witD[OF assms(1)]
by (auto simp: mem_vars_fm_if_mem_subterms_fm vars_branch_simps vars_fm_vars_branchI)
lemma bexpands_wit_wits_eq:
assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
shows "wits (b' @ b) = insert x (wits b)"
using assms bexpands_witD[OF assms(1)]
unfolding wits_def
by (auto simp: mem_vars_fm_if_mem_subterms_fm vars_branch_simps vars_branch_def)
lemma lexpands_pwits_subs:
assumes "lexpands b' b" "b ≠ []"
shows "pwits (b' @ b) ⊆ pwits b"
using assms lexpands_wits_eq[OF assms]
by (induction rule: lexpands_induct) (auto simp: pwits_def)
subsubsection ‹‹no_new_subterms››
definition "no_new_subterms b ≡
∀t ∈ subterms b. t ∉ Var ` wits b ⟶ t ∈ subterms (last b)"
lemma no_new_subtermsI:
assumes "⋀t. t ∈ subterms b ⟹ t ∉ Var ` wits b ⟹ t ∈ subterms (last b)"
shows "no_new_subterms b"
using assms unfolding no_new_subterms_def by blast
lemma Var_mem_subterms_branch_and_not_in_wits:
assumes "Var v ∈ subterms b" "v ∉ wits b"
shows "v ∈ vars (last b)"
using assms unfolding wits_def no_new_subterms_def
by (auto simp: image_set_diff[unfolded inj_on_def] image_UN
Un_vars_term_subterms_branch_eq_vars_branch[symmetric])
lemma subterms_branch_cases:
assumes "t ∈ subterms b" "t ∉ Var ` wits b"
obtains
(Empty) n where "t = ∅ n"
| (Union) t1 t2 where "t = t1 ⊔⇩s t2"
| (Inter) t1 t2 where "t = t1 ⊓⇩s t2"
| (Diff) t1 t2 where "t = t1 -⇩s t2"
| (Single) t1 where "t = Single t1"
| (Var) v where "t = Var v" "v ∈ vars (last b)"
proof(cases t)
case (Var x)
with assms have "x ∈ vars (last b)"
using Var_mem_subterms_branch_and_not_in_wits by (metis imageI)
with Var that show ?thesis by blast
qed (use assms that in auto)
lemma no_new_subterms_casesI[case_names Empty Union Inter Diff Single]:
assumes "⋀n. ∅ n ∈ subterms b ⟹ ∅ n ∈ subterms (last b)"
assumes "⋀t1 t2. t1 ⊔⇩s t2 ∈ subterms b ⟹ t1 ⊔⇩s t2 ∈ subterms (last b)"
assumes "⋀t1 t2. t1 ⊓⇩s t2 ∈ subterms b ⟹ t1 ⊓⇩s t2 ∈ subterms (last b)"
assumes "⋀t1 t2. t1 -⇩s t2 ∈ subterms b ⟹ t1 -⇩s t2 ∈ subterms (last b)"
assumes "⋀t. Single t ∈ subterms b ⟹ Single t ∈ subterms (last b)"
shows "no_new_subterms b"
proof(intro no_new_subtermsI)
fix t assume "t ∈ subterms b" "t ∉ Var ` wits b"
with this assms show "t ∈ subterms (last b)"
by (cases t rule: subterms_branch_cases) (auto simp: vars_fm_subs_subterms_fm)
qed
lemma no_new_subtermsD:
assumes "no_new_subterms b"
shows "⋀n. ∅ n ∈ subterms b ⟹ ∅ n ∈ subterms (last b)"
"⋀t1 t2. t1 ⊔⇩s t2 ∈ subterms b ⟹ t1 ⊔⇩s t2 ∈ subterms (last b)"
"⋀t1 t2. t1 ⊓⇩s t2 ∈ subterms b ⟹ t1 ⊓⇩s t2 ∈ subterms (last b)"
"⋀t1 t2. t1 -⇩s t2 ∈ subterms b ⟹ t1 -⇩s t2 ∈ subterms (last b)"
"⋀t. Single t ∈ subterms b ⟹ Single t ∈ subterms (last b)"
using assms unfolding no_new_subterms_def by auto
lemma lexpands_no_new_subterms:
assumes "lexpands b' b" "b ≠ []"
assumes "no_new_subterms b"
shows "no_new_subterms (b' @ b)"
using assms unfolding no_new_subterms_def
by (simp add: lexpands_wits_eq lexpands_subterms_branch_eq[OF assms(1,2)])
lemma subterms_branch_subterms_atomI:
assumes "Atom l ∈ set b" "t ∈ subterms_atom l"
shows "t ∈ subterms_branch b"
using assms unfolding subterms_branch_def
apply (cases l rule: subterms_atom.cases)
apply (metis subterms_branch_def subterms_term_subterms_atom_Atom_trans subterms_refl)+
done
lemma bexpands_nowit_no_new_subterms:
assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
assumes "no_new_subterms b"
shows "no_new_subterms (b' @ b)"
using assms unfolding no_new_subterms_def
by (simp add: bexpands_nowit_wits_eq bexpands_nowit_subterms_branch_eq[OF assms(1,2)])
lemma bexpands_wit_no_new_subterms:
assumes "bexpands_wit t1 t2 x bs' b" "b ≠ []" "b' ∈ bs'"
assumes "no_new_subterms b"
shows "no_new_subterms (b' @ b)"
using assms
apply(induction rule: bexpands_wit.induct)
apply(auto simp: subterms_branch_simps
subterms_term_subterms_atom_trans subterms_term_subterms_fm_trans
elim: no_new_subtermsD
intro!: no_new_subterms_casesI)
done
lemma bexpands_no_new_subterms:
assumes "bexpands bs' b" "b ≠ []" "b' ∈ bs'"
assumes "no_new_subterms b"
shows "no_new_subterms (b' @ b)"
using assms
apply(cases rule: bexpands.cases)
using bexpands_nowit_no_new_subterms bexpands_wit_no_new_subterms by metis+
lemma expandss_no_new_subterms:
assumes "expandss b' b" "b ≠ []" "no_new_subterms b"
shows "no_new_subterms b'"
using assms
apply(induction b' b rule: expandss.induct)
using expandss_suffix suffix_bot.extremum_uniqueI
using lexpands_no_new_subterms bexpands_no_new_subterms
by blast+
lemmas subterms_branch_subterms_fm_lastI =
subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
subsubsection ‹‹wits_subterms››
definition wits_subterms :: "'a branch ⇒ 'a pset_term set" where
"wits_subterms b ≡ Var ` wits b ∪ subterms (last b)"
lemma subterms_branch_eq_if_no_new_subterms:
assumes "no_new_subterms b" "b ≠ []"
shows "subterms_branch b = wits_subterms b"
using assms no_new_subtermsD[OF assms(1)]
proof -
note simps = wits_def no_new_subterms_def wits_subterms_def
subterms_branch_simps vars_branch_simps
with assms show ?thesis
by (auto simp: simps vars_fm_subs_subterms_fm
vars_branch_subs_subterms_branch[unfolded image_subset_iff]
intro: subterms_branch_subterms_fm_lastI)
qed
lemma wits_subterms_last_disjnt: "Var ` wits b ∩ subterms (last b) = {}"
by (auto simp: wits_def intro!: mem_vars_fm_if_mem_subterms_fm)
subsection ‹Completeness of the Calculus›
subsubsection ‹Proof of Lemma 2›
fun is_literal :: "'a fm ⇒ bool" where
"is_literal (Atom _) = True"
| "is_literal (Neg (Atom _)) = True"
| "is_literal _ = False"
lemma lexpands_no_wits_if_not_literal:
defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
assumes "lexpands b' b" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-) lexpands_wits_eq[OF assms(2,3)]
by (induction rule: lexpands_induct) (auto simp: disjoint_iff P_def)
lemma bexpands_nowit_no_wits_if_not_literal:
defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-)
by (induction rule: bexpands_nowit.induct)
(auto simp: Int_def P_def wits_def vars_fm_vars_branchI)
lemma bexpands_wit_no_wits_if_not_literal:
defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-)
by (induction rule: bexpands_wit.induct)
(auto simp: Int_def P_def wits_def vars_fm_vars_branchI)
lemma bexpands_no_wits_if_not_literal:
defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
assumes "bexpands bs' b" "b' ∈ bs'" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-)
apply(cases bs' b rule: bexpands_cases)
using bexpands_wit_no_wits_if_not_literal bexpands_nowit_no_wits_if_not_literal
using P_def by fast+
lemma expandss_no_wits_if_not_literal:
defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
assumes "expandss b' b" "b ≠ []"
assumes "P b"
shows "P b'"
using assms(2-)
apply (induction rule: expandss.induct)
using lexpands_no_wits_if_not_literal bexpands_no_wits_if_not_literal
apply (metis P_def expandss_suffix suffix_bot.extremum_uniqueI)+
done
lemma lexpands_fm_pwits_eq:
assumes "lexpands_fm b' b" "b ≠ []"
assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
shows "pwits (b' @ b) = pwits b"
using assms
apply(induction rule: lexpands_fm.induct)
apply(fastforce simp: pwits_def wits_def vars_branch_def)+
done
lemma lexpands_un_pwits_eq:
assumes "lexpands_un b' b" "b ≠ []"
assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
shows "pwits (b' @ b) = pwits b"
proof -
note lexpands.intros(2)[OF assms(1)]
note lexpands_wits_eq[OF this ‹b ≠ []›]
from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
using that
by (induction rule: lexpands_un.induct)
(auto simp: wits_subterms_def pwitsD intro!: pwitsI)
with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
by auto
qed
lemma lexpands_int_pwits_eq:
assumes "lexpands_int b' b" "b ≠ []"
assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
shows "pwits (b' @ b) = pwits b"
proof -
note lexpands.intros(3)[OF assms(1)]
note lexpands_wits_eq[OF this ‹b ≠ []›]
from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
using that
by (induction rule: lexpands_int.induct)
(auto simp: wits_subterms_def pwitsD intro!: pwitsI)
with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
by auto
qed
lemma lexpands_diff_pwits_eq:
assumes "lexpands_diff b' b" "b ≠ []"
assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
shows "pwits (b' @ b) = pwits b"
proof -
note lexpands.intros(4)[OF assms(1)]
note lexpands_wits_eq[OF this ‹b ≠ []›]
from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
using that
by (induction rule: lexpands_diff.induct)
(auto simp: wits_subterms_def pwitsD intro!: pwitsI)
with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
by auto
qed
lemma bexpands_nowit_pwits_eq:
assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
shows "pwits (b' @ b) = pwits b"
using assms
proof -
from assms have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
using that bexpands_nowit_wits_eq[OF assms(1-3)]
by (induction rule: bexpands_nowit.induct)
(intro pwitsI; fastforce simp: pwitsD)+
moreover from assms have "pwits (b' @ b) ⊆ pwits b"
unfolding pwits_def
using bexpands_nowit_wits_eq by fastforce
ultimately show ?thesis by blast
qed
lemma bexpands_wit_pwits_eq:
assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
shows "pwits (b' @ b) = insert x (pwits b)"
using assms(2,3) bexpands_witD[OF assms(1)]
unfolding pwits_def bexpands_wit_wits_eq[OF assms]
by (auto simp: vars_fm_vars_branchI)
lemma lemma_2_lexpands:
defines "P ≡ (λb c t. AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b)"
assumes "lexpands b' b" "b ≠ []"
assumes "no_new_subterms b"
assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b. P b c t"
shows "∀c ∈ pwits (b' @ b). ∀t ∈ wits_subterms (b' @ b). P (b' @ b) c t"
using assms(2-6)
using lexpands_wits_eq[OF assms(2,3)]
lexpands_pwits_subs[OF assms(2,3)]
proof(induction rule: lexpands.induct)
case (1 b' b)
have "P (b' @ b) c t"
if "∀φ ∈ set b'. vars φ ∩ wits (b' @ b) = {}"
and "c ∈ pwits b" "t ∈ wits_subterms (b' @ b)" for c t
proof -
from that "1.prems"(5)
have "∀φ ∈ set b'. φ ≠ AT (Var c =⇩s t) ∧ φ ≠ AT (t =⇩s Var c) ∧ φ ≠ AT (t ∈⇩s Var c)"
by (auto simp: pwits_def disjoint_iff)
with 1 that show ?thesis
unfolding P_def wits_subterms_def
by (metis Un_iff last_appendR set_append)
qed
moreover from "1"(1,4,6) have "∀φ ∈ set b'. vars φ ∩ wits (b' @ b) = {}"
by (induction rule: lexpands_fm.induct) (auto simp: disjoint_iff)
ultimately show ?case
using 1 lexpands_fm_pwits_eq by blast
next
case (2 b' b)
then show ?case
using lexpands_un_pwits_eq[OF "2"(1,2,5)[unfolded P_def]]
proof(induction rule: lexpands_un.induct)
case (4 s t1 t2 b)
then have "t1 ⊔⇩s t2 ∈ subterms b"
unfolding subterms_branch_def
by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
with ‹no_new_subterms b› have "t1 ⊔⇩s t2 ∈ subterms (last b)"
using no_new_subtermsD by blast
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 4 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
next
case (5 s t1 t2 b)
then have "t1 ⊔⇩s t2 ∈ subterms b"
unfolding subterms_branch_def
by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
with ‹no_new_subterms b› have "t1 ⊔⇩s t2 ∈ subterms (last b)"
using no_new_subtermsD by blast
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 5 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
qed (auto simp: wits_subterms_def P_def)
next
case (3 b' b)
then show ?case
using lexpands_int_pwits_eq[OF "3"(1,2,5)[unfolded P_def]]
proof(induction rule: lexpands_int.induct)
case (1 s t1 t2 b)
then have "t1 ⊓⇩s t2 ∈ subterms b"
unfolding subterms_branch_def
by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
with ‹no_new_subterms b› have "t1 ⊓⇩s t2 ∈ subterms (last b)"
using no_new_subtermsD by blast
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 1 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
next
case (6 s t1 b t2)
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 6 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
qed (auto simp: wits_subterms_def P_def)
next
case (4 b' b)
then show ?case
using lexpands_diff_pwits_eq[OF "4"(1,2,5)[unfolded P_def]]
proof(induction rule: lexpands_diff.induct)
case (1 s t1 t2 b)
then have "t1 -⇩s t2 ∈ subterms b"
unfolding subterms_branch_def
by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
with ‹no_new_subterms b› have "t1 -⇩s t2 ∈ subterms (last b)"
using no_new_subtermsD by blast
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 1 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps dest: pwitsD(1))
next
case (4 s t1 t2 b)
then have "t1 -⇩s t2 ∈ subterms b"
unfolding subterms_branch_def
by (metis AF_mem_subterms_branchD(2) subterms_branch_def)
with ‹no_new_subterms b› have "t1 -⇩s t2 ∈ subterms (last b)"
using no_new_subtermsD by blast
then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 4 show ?case
by (auto simp: wits_subterms_def P_def subterms_branch_simps dest: pwitsD(1))
qed (auto simp: wits_subterms_def P_def)
next
case (5 b' b)
then show ?case
proof(induction rule: lexpands_single.induct)
case (2 s t b)
then have "Single t ∈ subterms b"
by (auto intro: subterms_branch_subterms_atomI)
with 2 have "t ∈ subterms (last b)"
by (metis subterms_fmD(7) no_new_subtermsD(5))
then have "∀c ∈ pwits b. Var c ≠ t"
unfolding pwits_def wits_def
using wits_def wits_subterms_last_disjnt by fastforce
with ‹t ∈ subterms (last b)› show ?case
using 2
unfolding P_def
by (auto simp: wits_subterms_last_disjnt[unfolded disjoint_iff] wits_subterms_def subsetD
dest: pwitsD(2))
qed (auto simp: wits_subterms_def P_def)
next
case (6 b' b)
then have "no_new_subterms (b' @ b)" "b' @ b ≠ []"
using lexpands_no_new_subterms[OF lexpands.intros(6)] by blast+
note subterms_branch_eq_if_no_new_subterms[OF this]
with 6 show ?case
proof(induction rule: lexpands_eq_induct')
case (subst t1 t2 t1' t2' p l b)
then have "t1' ∈ subterms b"
using AT_eq_subterms_branchD by blast
then show ?case unfolding P_def
proof(safe, goal_cases)
case (1 c x)
with subst have [simp]: "p"
by (cases p) (simp add: P_def wits_subterms_def; blast)+
from 1 subst have "(Var c =⇩s x) = subst_tlvl t1' t2' l"
by (simp add: P_def wits_subterms_def; blast)
with 1 subst consider
(refl) "l = (t1' =⇩s t1')" "t2' = Var c" "x = Var c"
| (t1'_left) "l = (Var c =⇩s t1')" "t2' = x"
| (t1'_right) "l = (t1' =⇩s x)" "t2' = Var c"
apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
by (auto split: if_splits)
then show ?case
apply(cases)
by (use 1 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
next
case (2 c x)
with subst have [simp]: "p"
by (cases p) (simp add: P_def wits_subterms_def; blast)+
from 2 subst have "(x =⇩s Var c) = subst_tlvl t1' t2' l"
by (simp add: P_def wits_subterms_def; blast)
with 2 subst consider
(refl) "l = (t1' =⇩s t1')" "t2' = Var c" "x = Var c"
| (t1_left) "l = (t1' =⇩s Var c)" "t2' = x"
| (t1_right) "l = (x =⇩s t1')" "t2' = Var c"
apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
by (auto split: if_splits)
then show ?case
apply(cases)
by (use 2 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
next
case (3 c x)
with subst have [simp]: "p"
by (cases p) (simp add: P_def wits_subterms_def; blast)+
from 3 subst have "(x ∈⇩s Var c) = subst_tlvl t1' t2' l"
by (simp add: P_def wits_subterms_def; blast)
with 3 subst consider
(refl) "l = (t1' ∈⇩s t1')" "t2' = Var c" "x = Var c"
| (t1_left) "l = (t1' ∈⇩s Var c)" "t2' = x"
| (t1_right) "l = (x ∈⇩s t1')" "t2' = Var c"
apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
by (auto split: if_splits)
then show ?case
apply(cases)
by (use 3 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
qed
next
case (neq s t s' b)
then show ?case
using P_def by (simp add: wits_subterms_def) blast
qed
qed
lemma lemma_2_bexpands:
defines "P ≡ (λb c t. AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b
∧ AT (t ∈⇩s Var c) ∉ set b)"
assumes "bexpands bs' b" "b' ∈ bs'" "b ≠ []"
assumes "no_new_subterms b"
assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b. P b c t"
shows "∀c ∈ pwits (b' @ b). ∀t ∈ wits_subterms (b' @ b). P (b' @ b) c t"
using assms(2-) bexpands_no_new_subterms[OF assms(2,4,3,5)]
proof(induction rule: bexpands.induct)
case (1 bs' b)
then show ?case
using bexpands_nowit_wits_eq[OF "1"(1-3)] bexpands_nowit_pwits_eq[OF "1"(1-3,5)]
proof(induction rule: bexpands_nowit.induct)
case (1 p q b)
then show ?case
unfolding P_def wits_subterms_def
by (fastforce dest: pwitsD)
next
case (2 p q b)
then show ?case
unfolding P_def wits_subterms_def
by (fastforce dest: pwitsD)
next
case (3 s t1 t2 b)
then have "t1 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 3 show ?case
unfolding P_def wits_subterms_def
by (fastforce simp: vars_branch_simps dest: pwitsD)
next
case (4 s t1 b t2)
then have "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 4 show ?case
unfolding P_def wits_subterms_def
by (fastforce simp: vars_branch_simps dest: pwitsD)
next
case (5 s t1 b t2)
then have "t2 ∉ Var ` wits b"
by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
with 5 show ?case
unfolding P_def wits_subterms_def
by (fastforce simp: vars_branch_simps dest: pwitsD)
qed
next
case (2 t1 t2 x bs b)
from bexpands_witD[OF "2"(1)] have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
by (meson disjoint_iff_not_equal wits_subterms_last_disjnt)+
then have not_in_pwits: "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
unfolding pwits_def by auto
with bexpands_witD[OF "2"(1)] "2"(2-) show ?case
unfolding P_def wits_subterms_def
unfolding bexpands_wit_pwits_eq[OF "2"(1-3)] bexpands_wit_wits_eq[OF "2"(1-3)]
by safe (auto simp: vars_fm_vars_branchI[where ?x=x and ?b=b])
qed
lemma subterms_branch_eq_if_wf_branch:
assumes "wf_branch b"
shows "subterms_branch b = wits_subterms b"
proof -
from assms obtain φ where "expandss b [φ]"
unfolding wf_branch_def by blast
then have "no_new_subterms [φ]"
unfolding no_new_subterms_def wits_def
by (simp add: subterms_branch_simps)
with ‹expandss b [φ]› have "no_new_subterms b"
using expandss_no_new_subterms by blast
with ‹expandss b [φ]› assms show ?thesis
by (intro subterms_branch_eq_if_no_new_subterms) simp_all
qed
lemma
assumes "wf_branch b"
shows no_new_subterms_if_wf_branch: "no_new_subterms b"
and no_wits_if_not_literal_if_wf_branch:
"∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
proof -
from assms obtain φ where "expandss b [φ]"
unfolding wf_branch_def by blast
then have "no_new_subterms [φ]"
by (auto simp: no_new_subterms_def wits_def vars_branch_simps subterms_branch_simps)
from expandss_no_new_subterms[OF ‹expandss b [φ]› _ this] show "no_new_subterms b"
by simp
from expandss_no_wits_if_not_literal[OF ‹expandss b [φ]›]
show "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
unfolding wits_def by simp
qed
lemma lemma_2:
assumes "wf_branch b"
assumes "c ∈ pwits b"
shows "AT (Var c =⇩s t) ∉ set b" "AT (t =⇩s Var c) ∉ set b" "AT (t ∈⇩s Var c) ∉ set b"
proof -
from ‹wf_branch b› obtain φ where "expandss b [φ]"
using wf_branch_def by blast
have no_wits_if_not_literal: "∀φ ∈ set b'. ¬ is_literal φ ⟶ vars φ ∩ wits b' = {}"
if "expandss b' [φ]" for b'
using no_wits_if_not_literal_if_wf_branch that unfolding wf_branch_def by blast
have no_new_subterms: "no_new_subterms b'" if "expandss b' [φ]" for b'
using no_new_subterms_if_wf_branch that unfolding wf_branch_def by blast
have "AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
using ‹expandss b [φ]› assms(2)
proof(induction b "[φ]" arbitrary: c t rule: expandss.induct)
case 1
then show ?case by simp
next
case (2 b1 b2)
note lemma_2_lexpands[OF this(1) _
no_new_subterms[OF this(3)] no_wits_if_not_literal[OF this(3)]]
with 2 show ?case
using wf_branch_def wf_branch_not_Nil subterms_branch_eq_if_wf_branch
by (metis AT_eq_subterms_branchD(1,2) AT_mem_subterms_branchD(1) expandss.intros(2))
next
case (3 bs b2 b1)
note lemma_2_bexpands[OF "3"(1) _ _
no_new_subterms[OF "3"(3)] no_wits_if_not_literal[OF "3"(3)]]
with 3 show ?case
using wf_branch_def wf_branch_not_Nil subterms_branch_eq_if_wf_branch
by (metis AT_eq_subterms_branchD(1,2) AT_mem_subterms_branchD(1) expandss.intros(3))
qed
then show "AT (Var c =⇩s t) ∉ set b" "AT (t =⇩s Var c) ∉ set b" "AT (t ∈⇩s Var c) ∉ set b"
by safe
qed
subsubsection ‹Urelements›
definition "urelems b ≡ {x ∈ subterms b. ∃v. ∀φ ∈ set b. urelem' v φ x}"
lemma finite_urelems: "finite (urelems b)"
proof -
have "urelems b ⊆ subterms b"
unfolding urelems_def urelem_def by blast
with finite_subset finite_subterms_branch show ?thesis
by blast
qed
lemma urelems_subs_subterms: "urelems b ⊆ subterms b"
unfolding urelems_def by blast
lemma is_Var_if_mem_urelems: "t ∈ urelems b ⟹ is_Var t"
unfolding urelems_def subterms_branch_def
using is_Var_if_urelem' by auto
lemma urelems_subs_vars: "urelems b ⊆ Var ` vars b"
proof
fix t assume "t ∈ urelems b"
with urelems_subs_subterms have "t ∈ subterms b"
by blast
moreover note is_Var_if_mem_urelems[OF ‹t ∈ urelems b›]
then obtain x where "t = Var x"
by (meson is_Var_def)
ultimately have "x ∈ vars b"
unfolding Un_vars_term_subterms_branch_eq_vars_branch[symmetric]
by force
with ‹t = Var x› show "t ∈ Var ` vars b"
by blast
qed
lemma types_term_inf:
includes Set_member_no_ascii_notation
assumes "v1 ⊢ t : l1" "v2 ⊢ t : l2"
shows "inf v1 v2 ⊢ t : inf l1 l2"
using assms
apply(induction t arbitrary: l1 l2)
apply(auto simp: inf_min elim!: types_pset_term_cases
intro: types_pset_term_intros' types_pset_term.intros(4-))
done
lemma types_pset_atom_inf:
fixes a :: "'a pset_atom"
assumes "v1 ⊢ a" "v2 ⊢ a"
shows "inf v1 v2 ⊢ a"
using assms
by (auto simp: types_pset_atom.simps) (metis inf_min min_Suc_Suc types_term_inf)+
lemma types_pset_fm_inf:
fixes φ :: "'a pset_fm"
assumes "v1 ⊢ φ" "v2 ⊢ φ"
shows "inf v1 v2 ⊢ φ"
using assms types_pset_atom_inf
unfolding types_pset_fm_def by blast
lemma types_urelems:
includes Set_member_no_ascii_notation
fixes b :: "'a branch"
assumes "wf_branch b" "v ⊢ last b"
obtains v' where "∀φ ∈ set b. v' ⊢ φ" "∀u ∈ urelems b. v' ⊢ u : 0"
proof -
from assms have "expandss b [last b]"
unfolding wf_branch_def by force
define V where "V ≡ {v. (∀φ ∈ set b. v ⊢ φ) ∧ (∀x. x ∉ vars b ⟶ v x = 0)}"
have "V ≠ {}"
proof -
from types_expandss[OF ‹expandss b [last b]›, simplified] ‹v ⊢ last b›
obtain v where v: "∀φ ∈ set b. v ⊢ φ"
unfolding vars_branch_simps by metis
define v' where "v' ≡ λx. if x ∈ vars b then v x else 0"
have "v' ⊢ φ ⟷ v ⊢ φ" if "φ ∈ set b" for φ :: "'a pset_fm"
apply(intro types_pset_fm_if_on_vars_eq)
using that vars_fm_vars_branchI unfolding v'_def by metis
with v have "∀φ ∈ set b. v' ⊢ φ"
by blast
then have "v' ∈ V"
unfolding V_def v'_def by simp
then show ?thesis
by blast
qed
define m_x where "m_x ≡ λx. ARG_MIN (λv. v x) v. v ∈ V"
with ‹V ≠ {}› have m_x: "∀v ∈ V. m_x x x ≤ v x" "m_x x ∈ V" for x
using arg_min_nat_le arg_min_natI by (metis ex_in_conv)+
define M where "M ≡ Finite_Set.fold inf (SOME v. v ∈ V) (m_x ` vars b)"
note finite_imageI[where ?h=m_x, OF finite_vars_branch[of b]]
note M_inf_eq = Inf_fin.eq_fold[symmetric, OF this, of "SOME v. v ∈ V"]
have M_leq: "M x ≤ v x" if "x ∈ vars b" "v ∈ V" for x v
proof -
from that have "m_x x ∈ m_x ` vars b"
by blast
then have "M = inf (m_x x) (⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` vars b))"
unfolding M_def M_inf_eq
by (simp add: Inf_fin.in_idem finite_vars_branch)
with m_x that show ?thesis
by (simp add: inf.coboundedI1)
qed
moreover have "M ∈ V"
unfolding M_def M_inf_eq using finite_vars_branch[of b]
proof(induction rule: finite_induct)
case empty
with ‹V ≠ {}› show ?case
by (simp add: some_in_eq)
next
case (insert x F)
then have M'_eq: "⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` insert x F)
= inf (m_x x) (⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` F))" (is "_ = ?M'")
by (simp add: insert_commute)
from types_pset_fm_inf insert have "∀φ ∈ set b. ?M' ⊢ φ"
using V_def m_x(2) by blast
moreover have "(inf w v) x = 0" if "x ∉ vars b" "w ∈ V" "v ∈ V" for w v
using that by (simp add: V_def)
with "insert.IH" m_x(2) have "∀x. x ∉ vars b ⟶ ?M' x = 0"
by (simp add: V_def)
ultimately have "?M' ∈ V"
using V_def by blast
with M'_eq show ?case
by metis
qed
moreover have "M ⊢ u : 0" if "u ∈ urelems b" for u
proof -
from that obtain v where v: "∀φ ∈ set b. urelem' v φ u"
unfolding urelems_def by blast
define v' where "v' ≡ λx. if x ∈ vars b then v x else 0"
have "v' ⊢ φ ⟷ v ⊢ φ" if "φ ∈ set b" for φ :: "'a pset_fm"
apply(intro types_pset_fm_if_on_vars_eq)
using that vars_fm_vars_branchI unfolding v'_def by metis
with v have "∀φ ∈ set b. v' ⊢ φ"
by blast
then have "v' ∈ V"
unfolding V_def v'_def by auto
moreover obtain uv where uv: "u = Var uv"
using v is_Var_if_urelem' wf_branch_not_Nil[OF ‹wf_branch b›]
by (metis is_Var_def last_in_set)
then have "v' ⊢ u : 0"
using v wf_branch_not_Nil[OF ‹wf_branch b›, THEN last_in_set]
unfolding v'_def
by (auto elim!: types_pset_term_cases(2) intro!: types_pset_term_intros'(2))
ultimately show "M ⊢ u : 0"
using M_leq[where ?v=v'] ‹M ∈ V›[unfolded V_def] unfolding uv
by (fastforce elim!: types_pset_term_cases(2) intro!: types_pset_term_intros'(2))
qed
ultimately show ?thesis
using that unfolding V_def by auto
qed
lemma mem_urelems_if_urelem_last:
assumes "wf_branch b"
assumes "urelem (last b) x" "x ∈ subterms (last b)"
shows "x ∈ urelems b"
proof -
from assms have "x ∈ subterms b"
unfolding subterms_branch_def by auto
moreover note urelem_invar_if_wf_branch[OF assms]
ultimately show ?thesis
unfolding urelems_def urelem_def by blast
qed
lemma not_urelem_comps_if_compound:
assumes "f t1 t2 ∈ subterms b" "f ∈ {(⊓⇩s), (⊔⇩s), (-⇩s)}"
shows "t1 ∉ urelems b" "t2 ∉ urelems b"
proof -
from assms obtain φ where "φ ∈ set b" "f t1 t2 ∈ subterms φ"
unfolding subterms_branch_def by auto
note not_urelem_comps_if_compound[of f t1 t2, OF this(2) assms(2)]
with ‹φ ∈ set b› show "t1 ∉ urelems b" "t2 ∉ urelems b"
unfolding urelems_def urelem_def by auto
qed
subsubsection ‹Realization of an Open Branch›
definition "base_vars b ≡ Var ` pwits b ∪ urelems b"
lemma finite_base_vars: "finite (base_vars b)"
unfolding base_vars_def finite_Un
using finite_pwits[THEN finite_imageI] finite_urelems by blast
lemma pwits_subs_base_vars:
shows "Var ` pwits b ⊆ base_vars b"
unfolding base_vars_def
by blast
lemma base_vars_subs_vars: "base_vars b ⊆ Var ` vars b"
unfolding base_vars_def pwits_def wits_def
using urelems_subs_vars by blast
definition subterms' :: "'a branch ⇒ 'a pset_term set" where
"subterms' b ≡ subterms b - base_vars b"
definition bgraph :: "'a branch ⇒ ('a pset_term, 'a pset_term × 'a pset_term) pre_digraph" where
"bgraph b ≡
let
vs = base_vars b ∪ subterms' b
in
⦇ verts = vs,
arcs = {(s, t). AT (s ∈⇩s t) ∈ set b},
tail = fst,
head = snd ⦈"
lemma base_vars_Un_subterms'_eq_subterms:
"base_vars b ∪ subterms' b = subterms b"
unfolding subterms'_def
using base_vars_subs_vars vars_branch_subs_subterms_branch by fastforce
lemma finite_base_vars_Un_subterms': "finite (base_vars b ∪ subterms' b)"
unfolding base_vars_Un_subterms'_eq_subterms
using finite_subterms_branch .
lemma verts_bgraph: "verts (bgraph b) = base_vars b ∪ subterms' b"
unfolding bgraph_def Let_def by simp
lemma verts_bgraph_eq_subterms: "verts (bgraph b) = subterms b"
unfolding verts_bgraph base_vars_Un_subterms'_eq_subterms ..
lemma finite_subterms': "finite (subterms' b)"
unfolding subterms'_def using finite_base_vars finite_subterms_branch
by auto
lemma base_vars_subterms'_disjnt: "base_vars b ∩ subterms' b = {}"
unfolding subterms'_def by fastforce
lemma wits_subterms_eq_base_vars_Un_subterms':
assumes "wf_branch b"
shows "wits_subterms b = base_vars b ∪ subterms' b"
unfolding subterms_branch_eq_if_wf_branch[OF assms, symmetric] subterms'_def
using base_vars_subs_vars vars_branch_subs_subterms_branch
by fastforce
lemma in_subterms'_if_AT_mem_in_branch:
assumes "wf_branch b"
assumes "AT (s ∈⇩s t) ∈ set b"
shows "s ∈ base_vars b ∪ subterms' b"
and "t ∈ base_vars b ∪ subterms' b"
using assms
using wits_subterms_eq_base_vars_Un_subterms' AT_mem_subterms_branchD
using subterms_branch_eq_if_wf_branch
by blast+
lemma in_subterms'_if_AF_mem_in_branch:
assumes "wf_branch b"
assumes "AF (s ∈⇩s t) ∈ set b"
shows "s ∈ base_vars b ∪ subterms' b"
and "t ∈ base_vars b ∪ subterms' b"
using assms
using wits_subterms_eq_base_vars_Un_subterms' AF_mem_subterms_branchD
using subterms_branch_eq_if_wf_branch
by blast+
lemma in_subterms'_if_AT_eq_in_branch:
assumes "wf_branch b"
assumes "AT (s =⇩s t) ∈ set b"
shows "s ∈ base_vars b ∪ subterms' b"
and "t ∈ base_vars b ∪ subterms' b"
using assms
using wits_subterms_eq_base_vars_Un_subterms' AT_eq_subterms_branchD
using subterms_branch_eq_if_wf_branch
by blast+
lemma in_subterms'_if_AF_eq_in_branch:
assumes "wf_branch b"
assumes "AF (s =⇩s t) ∈ set b"
shows "s ∈ base_vars b ∪ subterms' b"
and "t ∈ base_vars b ∪ subterms' b"
using assms
using wits_subterms_eq_base_vars_Un_subterms' AF_eq_subterms_branchD
using subterms_branch_eq_if_wf_branch
by blast+
lemma mem_subterms_fm_last_if_mem_subterms_branch:
assumes "wf_branch b"
assumes "t ∈ subterms b" "¬ is_Var t"
shows "t ∈ subterms (last b)"
using assms
unfolding subterms_branch_eq_if_wf_branch[OF ‹wf_branch b›]
unfolding subterms'_def wits_subterms_def by force
locale open_branch =
fixes b :: "'a branch"
assumes wf_branch: "wf_branch b" and bopen: "bopen b" and types: "∃v. v ⊢ last b"
and infinite_vars: "infinite (UNIV :: 'a set)"
begin
sublocale fin_digraph_bgraph: fin_digraph "bgraph b"
proof
show "finite (verts (bgraph b))"
using finite_base_vars finite_subterms'
by (auto simp: bgraph_def Let_def)
show "finite (arcs (bgraph b))"
using [[simproc add: finite_Collect]]
by (auto simp: bgraph_def Let_def inj_on_def intro!: finite_vimageI)
qed (use in_subterms'_if_AT_mem_in_branch[OF wf_branch]
in ‹(fastforce simp: bgraph_def Let_def)+›)
lemma member_seq_if_cas:
"fin_digraph_bgraph.cas t1 is t2
⟹ member_seq t1 (map (λe. tail (bgraph b) e ∈⇩s head (bgraph b) e) is) t2"
by (induction "is" arbitrary: t1 t2) auto
lemma member_cycle_if_cycle:
"fin_digraph_bgraph.cycle c
⟹ member_cycle (map (λe. tail (bgraph b) e ∈⇩s head (bgraph b) e) c)"
unfolding pre_digraph.cycle_def
by (cases c) (auto simp: member_seq_if_cas)
sublocale dag_bgraph: dag "bgraph b"
proof(unfold_locales, goal_cases)
case (1 e)
show ?case
proof
assume "tail (bgraph b) e = head (bgraph b) e"
then obtain t where "AT (t ∈⇩s t) ∈ set b"
using 1 unfolding bgraph_def Let_def by auto
then have "member_cycle [(t ∈⇩s t)]" "(t ∈⇩s t) ∈ Atoms (set b)"
by (auto simp: Atoms_def)
then have "bclosed b"
using memberCycle by (metis empty_iff empty_set set_ConsD subsetI)
with bopen show "False"
by blast
qed
next
case (2 e1 e2)
then show ?case
by (auto simp: bgraph_def Let_def arc_to_ends_def)
next
case 3
show ?case
proof
assume "∃c. fin_digraph_bgraph.cycle c"
then obtain c where "fin_digraph_bgraph.cycle c"
by blast
then have "member_cycle (map (λe. (tail (bgraph b) e ∈⇩s head (bgraph b) e)) c)"
using member_cycle_if_cycle by blast
moreover
from ‹fin_digraph_bgraph.cycle c› have "set c ⊆ arcs (bgraph b)"
by (meson fin_digraph_bgraph.cycle_def pre_digraph.awalk_def)
then have "set (map (λe. (tail (bgraph b) e ∈⇩s head (bgraph b) e)) c) ⊆ Atoms (set b)"
unfolding bgraph_def Let_def Atoms_def by auto
ultimately have "bclosed b"
using memberCycle by blast
with bopen show False by blast
qed
qed
definition I :: "'a pset_term ⇒ hf" where
"I ≡ SOME f. inj_on f (subterms b)
∧ (∀p. hcard (f p) > 2 * card (base_vars b ∪ subterms' b))"
lemma (in -) Ex_set_family:
assumes "finite P"
shows "∃I. inj_on I P ∧ (∀p. hcard (I p) ≥ n)"
proof -
from ‹finite P› obtain ip where ip: "bij_betw ip P {..<card P}"
using to_nat_on_finite by blast
let ?I = "ord_of o ((+) n) o ip"
from ip have "inj_on ?I P"
by (auto simp: inj_on_def bij_betw_def)
moreover have "hcard (?I p) ≥ n" for p
by simp
ultimately show ?thesis
by auto
qed
lemma
shows inj_on_I: "inj_on I (subterms b)"
and card_I: "hcard (I p) > 2 * card (base_vars b ∪ subterms' b)"
proof -
have "∃f. inj_on f (subterms b)
∧ (∀p. hcard (f p) > 2 * card (base_vars b ∪ subterms' b))"
using Ex_set_family finite_subterms_branch by (metis less_eq_Suc_le)
from someI_ex[OF this]
show "inj_on I (subterms b)"
"hcard (I p) > 2 * card (base_vars b ∪ subterms' b)"
unfolding I_def by blast+
qed
lemma
shows inj_on_base_vars_I: "inj_on I (base_vars b)"
and inj_on_subterms'_I: "inj_on I (subterms' b)"
proof -
from base_vars_Un_subterms'_eq_subterms have
"base_vars b ⊆ subterms b" "subterms' b ⊆ subterms b"
using wf_branch_not_Nil[OF wf_branch] by blast+
with inj_on_I show "inj_on I (base_vars b)" "inj_on I (subterms' b)"
unfolding inj_on_def by blast+
qed
definition "eq ≡ symcl ({(s, t). AT (s =⇩s t) ∈ set b}⇧=)"
lemma refl_eq: "refl eq"
unfolding eq_def symcl_def refl_on_def by auto
lemma trans_eq:
assumes "lin_sat b" shows "trans eq"
proof
fix s t u assume assms: "(s, t) ∈ eq" "(t, u) ∈ eq"
have "(s, u) ∈ eq" if "s ≠ t" "t ≠ u"
proof -
from that assms have
s_t: "AT (s =⇩s t) ∈ set b ∨ AT (t =⇩s s) ∈ set b" and
t_u: "AT (t =⇩s u) ∈ set b ∨ AT (u =⇩s t) ∈ set b"
unfolding eq_def symcl_def by fastforce+
note intros = lexpands_eq.intros(1,3)[
THEN lexpands.intros(6), THEN ‹lin_sat b›[THEN lin_satD]]
note intros' = intros[where ?x="AT (s =⇩s u)"] intros[where ?x="AT (u =⇩s s)"]
from s_t t_u that have "AT (s =⇩s u) ∈ set b ∨ AT (u =⇩s s) ∈ set b"
by safe (simp_all add: intros')
then show ?thesis
unfolding eq_def symcl_def by auto
qed
with assms show "(s, u) ∈ eq"
by (cases "s ≠ t ∧ t ≠ u") (auto simp: eq_def)
qed
lemma sym_eq: "sym eq"
unfolding eq_def symcl_def sym_def by auto
lemma equiv_eq: "lin_sat b ⟹ equiv UNIV eq"
by (rule equivI) (use refl_eq trans_eq sym_eq in safe)
lemma not_dominated_if_pwits:
assumes "x ∈ Var ` pwits b" shows "¬ s →⇘bgraph b⇙ x"
proof -
from assms obtain x' where "x = Var x'" "x' ∈ pwits b"
by blast
from lemma_2(3)[OF wf_branch this(2)] this(1) show "¬ s →⇘bgraph b⇙ x"
unfolding arcs_ends_def arc_to_ends_def by (auto simp: bgraph_def)
qed
lemma parents_empty_if_pwits:
assumes "x ∈ Var ` pwits b" shows "parents (bgraph b) x = {}"
using not_dominated_if_pwits[OF assms] unfolding bgraph_def by simp
lemma not_AT_mem_if_urelem:
assumes "t ∈ urelems b"
shows "AT (s ∈⇩s t) ∉ set b"
proof
assume "AT (s ∈⇩s t) ∈ set b"
with assms urelem_invar_if_wf_branch[OF wf_branch] have "urelem (AT (s ∈⇩s t)) t"
by (meson types types_urelems urelem_def wf_branch)
then show False
unfolding urelem_def
by (auto dest!: types_fmD simp: types_pset_atom.simps dest: types_term_unique)
qed
lemma not_dominated_if_urelems:
assumes "t ∈ urelems b"
shows "¬ s →⇘bgraph b⇙ t"
using not_AT_mem_if_urelem[OF assms] unfolding bgraph_def by auto
lemma parents_empty_if_urelems:
assumes "t ∈ urelems b"
shows "parents (bgraph b) t = {}"
using not_dominated_if_urelems[OF assms] by simp
lemma not_dominated_if_base_vars:
assumes "x ∈ base_vars b"
shows "¬ s →⇘bgraph b⇙ x"
using assms not_dominated_if_urelems not_dominated_if_pwits
unfolding base_vars_def by blast
lemma parents_empty_if_base_vars:
assumes "x ∈ base_vars b"
shows "parents (bgraph b) x = {}"
using not_dominated_if_base_vars[OF assms] by blast
lemma eq_class_subs_subterms: "eq `` {t} ⊆ {t} ∪ subterms b"
proof -
have "eq - Id ⊆ subterms b × subterms b"
by (auto simp: AT_eq_subterms_branchD eq_def symcl_def)
then show "eq `` {t} ⊆ {t} ∪ subterms b"
by blast
qed
lemma finite_eq_class: "finite (eq `` {x})"
using eq_class_subs_subterms finite_subterms_branch
using finite_subset by fastforce
lemma finite_I_image_eq_class: "finite (I ` eq `` {x})"
using finite_eq_class by blast
context
begin
interpretation realisation "bgraph b" "base_vars b" "subterms' b" I eq
proof(unfold_locales)
from base_vars_subterms'_disjnt show "base_vars b ∩ subterms' b = {}" .
show "verts (bgraph b) = base_vars b ∪ subterms' b"
unfolding bgraph_def by simp
from not_dominated_if_base_vars show "⋀p t. p ∈ base_vars b ⟹ ¬ t →⇘bgraph b⇙ p" .
qed
lemmas realisation = realisation_axioms
lemma card_realisation:
"hcard (realise t) ≤ 2 * card (subterms b)"
proof(induction t rule: realise.induct)
case (1 x)
then have "hcard (realise x) = card (realise ` parents (bgraph b) x ∪ I ` eq_class x)"
using hcard_HF Zero_hf_def parents_empty_if_base_vars
using finite_I_image_eq_class by force
also have "… ≤ card (realise ` parents (bgraph b) x) + card (I ` eq_class x)"
using card_Un_le by blast
also have "… ≤ card (parents (bgraph b) x) + card (eq_class x)"
using card_image_le[OF fin_digraph_bgraph.finite_parents]
using card_image_le[OF finite_eq_class]
by (metis add_le_mono)
also have "… ≤ card (subterms b) + card (eq_class x)"
using fin_digraph_bgraph.parents_subs_verts[unfolded verts_bgraph_eq_subterms]
using card_mono[OF finite_subterms_branch]
by (simp add: "1.hyps" not_dominated_if_base_vars)
also have "… ≤ card (subterms b) + card ({x} ∪ subterms b)"
apply (intro add_le_mono card_mono[where ?B="{x} ∪ subterms b"])
using eq_class_subs_subterms finite_subterms_branch by auto
also have "… ≤ 2 * card (subterms b)"
proof -
from 1 have "x ∈ subterms b"
using "1.prems" verts_bgraph verts_bgraph_eq_subterms wf_branch_not_Nil[OF wf_branch]
by blast
then show ?thesis
unfolding mult_2 by (metis insert_absorb insert_is_Un order_refl)
qed
finally show ?case .
next
case (2 t)
then have "hcard (realise t) = card (realise ` parents (bgraph b) t)"
using hcard_HF[OF finite_realisation_parents] by simp
also have "… ≤ card (parents (bgraph b) t)"
using card_image_le by blast
also have "… ≤ card (subterms b)"
using fin_digraph_bgraph.parents_subs_verts wf_branch_not_Nil[OF wf_branch]
unfolding verts_bgraph_eq_subterms
by (metis card_mono fin_digraph_bgraph.finite_verts verts_bgraph_eq_subterms)
finally show ?case
unfolding base_vars_Un_subterms'_eq_subterms by auto
next
case (3 t)
then show ?case by simp
qed
lemma I_neq_realise: "I x ≠ realise y"
proof -
note card_realisation[of y]
moreover have "hcard (I x) > 2 * card (subterms b)"
using card_I wf_branch
by (simp add: subterms_branch_eq_if_wf_branch wits_subterms_eq_base_vars_Un_subterms')
ultimately show ?thesis
by (metis linorder_not_le)
qed
end
sublocale realisation "bgraph b" "base_vars b" "subterms' b" I eq
rewrites "(⋀x y. I x ≠ realise y) ≡ Trueprop True"
and "⋀P. (True ⟹ P) ≡ Trueprop P"
and "⋀P Q. (True ⟹ PROP P ⟹ PROP Q) ≡ (PROP P ⟹ True ⟹ PROP Q)"
using realisation I_neq_realise by simp_all
lemma eq_class_singleton_if_pwits:
assumes "x ∈ Var ` pwits b" shows "eq_class x = {x}"
proof -
from assms obtain x' where "x = Var x'" "x' ∈ pwits b"
by blast
have False if "eq_class x ≠ {x}"
proof -
have "x ∈ eq_class x"
by (simp add: eq_def symcl_def)
with that obtain y where "y ∈ eq_class x" "y ≠ x"
by auto
then have "AT (y =⇩s x) ∈ set b ∨ AT (x =⇩s y) ∈ set b"
unfolding eq_def symcl_def by auto
with lemma_2(1,2)[OF wf_branch ‹x' ∈ pwits b›] ‹x = Var x'› show False
by blast
qed
with assms show ?thesis by blast
qed
lemma realise_pwits:
"x ∈ Var ` pwits b ⟹ realise x = HF {I x}"
unfolding realise.simps(1)[OF pwits_subs_base_vars[THEN subsetD]]
by (auto simp: eq_class_singleton_if_pwits parents_empty_if_pwits)
lemma I_in_realise_if_base_vars[simp]:
"s ∈ base_vars b ⟹ I s ❙∈ realise s"
using refl_eq by (simp add: finite_I_image_eq_class refl_on_def)
lemma realise_neq_if_base_vars_and_subterms':
assumes "s ∈ base_vars b" "t ∈ subterms' b"
shows "realise s ≠ realise t"
proof -
from assms have "I s ❙∉ realise t"
using I_neq_realise by auto
with I_in_realise_if_base_vars assms(1) show ?thesis
by metis
qed
lemma AT_mem_branch_wits_subtermsD:
assumes "AT (s ∈⇩s t) ∈ set b"
shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
using assms AT_mem_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+
lemma AF_mem_branch_wits_subtermsD:
assumes "AF (s ∈⇩s t) ∈ set b"
shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
using assms AF_mem_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+
lemma AT_eq_branch_wits_subtermsD:
assumes "AT (s =⇩s t) ∈ set b"
shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
using assms AT_eq_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+
lemma AF_eq_branch_wits_subtermsD:
assumes "AF (s =⇩s t) ∈ set b"
shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
using assms AF_eq_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+
lemma realisation_if_AT_mem:
assumes "AT (s ∈⇩s t) ∈ set b"
shows "realise s ❙∈ realise t"
proof -
from assms have "t ∈ base_vars b ∪ subterms' b"
using in_subterms'_if_AT_mem_in_branch(2) wf_branch by blast
moreover from assms have "s →⇘bgraph b⇙ t"
unfolding arcs_ends_def arc_to_ends_def by (simp add: bgraph_def)
ultimately show ?thesis
by (cases t rule: realise.cases) auto
qed
lemma AT_eq_urelems_subterms'_cases:
includes Set_member_no_ascii_notation
assumes "AT (s =⇩s t) ∈ set b"
obtains (urelems) "s ∈ urelems b" "t ∈ urelems b" |
(subterms') "s ∈ subterms' b" "t ∈ subterms' b"
proof -
from types obtain v where "v ⊢ last b"
by blast
with types_urelems wf_branch obtain v'
where v': "∀φ ∈ set b. v' ⊢ φ" "∀u ∈ urelems b. v' ⊢ u : 0"
by blast
with assms have "v' ⊢ AT (s =⇩s t)"
by blast
then obtain lst where lst: "v' ⊢ s : lst" "v' ⊢ t : lst"
by (auto dest!: types_fmD(6) simp: types_pset_atom.simps)
note mem_subterms = AT_eq_subterms_branchD[OF assms]
with v' have "t ∈ urelems b" if "s ∈ urelems b"
using that lst types_term_unique urelems_def by fastforce
moreover from assms have "s ∉ Var ` pwits b" "t ∉ Var ` pwits b"
using lemma_2(1,2)[OF wf_branch] by blast+
moreover have "t ∈ subterms' b" if "s ∈ subterms' b"
proof -
have "s ∉ urelems b"
using that B_T_partition_verts(1) unfolding base_vars_def by blast
with v'(1) mem_subterms(1) have "¬ v' ⊢ s : 0"
using urelems_def by blast
with lst v'(2) have "t ∉ urelems b"
using types_term_unique by metis
with ‹t ∉ Var ` pwits b› ‹t ∈ subterms b› show "t ∈ subterms' b"
by (simp add: base_vars_def subterms'_def)
qed
ultimately show ?thesis
using that mem_subterms
by (cases "s ∈ subterms' b") (auto simp: base_vars_def subterms'_def)
qed
lemma realisation_if_AT_eq:
assumes "lin_sat b"
assumes "AT (s =⇩s t) ∈ set b"
shows "realise s = realise t"
proof -
from assms(2) show ?thesis
proof(cases rule: AT_eq_urelems_subterms'_cases)
case urelems
then have "s ∈ base_vars b" "t ∈ base_vars b"
by (simp_all add: base_vars_def)
moreover from assms have "(s, t) ∈ eq"
unfolding eq_def symcl_def by blast
then have "I ` eq_class s = I ` eq_class t"
using equiv_eq[OF assms(1)] by (simp add: equiv_class_eq_iff)
ultimately show ?thesis
using urelems by (simp add: parents_empty_if_urelems)
next
case subterms'
have "False" if "realise s ≠ realise t"
proof -
from that have "hfset (realise s) ≠ hfset (realise t)"
by (metis HF_hfset)
then obtain a s' t' where
a: "a ∈ realise ` parents (bgraph b) s'"
"a ∉ realise ` parents (bgraph b) t'"
and s'_t': "s' = s ∧ t' = t ∨ s' = t ∧ t' = s"
using subterms' by auto blast+
with subterms' have "s' ∈ subterms' b" "t' ∈ subterms' b"
by auto
with a obtain u where u: "a = realise u" "u →⇘bgraph b⇙ s'"
using subterms' dominates_if_mem_realisation by auto
then have "u ≠ s'"
using dag_bgraph.adj_not_same by blast
from u have "AT (u ∈⇩s s') ∈ set b"
unfolding bgraph_def Let_def using dag_bgraph.adj_not_same by auto
note lexpands_eq.intros(1,3)[OF assms(2) this, THEN lexpands.intros(6)]
with ‹lin_sat b› s'_t' ‹u ≠ s'› have "AT (u ∈⇩s t') ∈ set b"
unfolding lin_sat_def by (auto split: if_splits)
from realisation_if_AT_mem[OF this] ‹a = realise u› have "a ❙∈ realise t'"
by blast
with a show False
using ‹t' ∈ subterms' b› by simp
qed
then show ?thesis by blast
qed
qed
lemma realise_base_vars_if_AF_eq:
assumes "sat b"
assumes "AF (x =⇩s y) ∈ set b"
assumes "x ∈ base_vars b ∨ y ∈ base_vars b"
shows "realise x ≠ realise y"
proof(cases "x ∈ base_vars b ∧ y ∈ base_vars b")
case False
with assms(3) show ?thesis
using realise_neq_if_base_vars_and_subterms' I_in_realise_if_base_vars
by (metis hempty_iff realise.elims)
next
case True
from assms bopen have "x ≠ y"
using neqSelf by blast
moreover from assms bopen have "AT (x =⇩s y) ∉ set b"
using contr by blast
moreover have "AT (y =⇩s x) ∉ set b"
proof
assume "AT (y =⇩s x) ∈ set b"
note lexpands_eq.intros(2)[OF this assms(2), THEN lexpands.intros(6)]
with ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (x =⇩s x) ∈ set b"
by auto
with bopen neqSelf show False
by blast
qed
ultimately have "(x, y) ∉ eq"
unfolding eq_def symcl_def by auto
then have "x ∉ eq_class y"
by (meson Image_singleton_iff symE sym_eq)
then have "I x ∉ I ` eq_class y"
using inj_on_I AF_eq_subterms_branchD[OF assms(2)]
using eq_class_subs_subterms inj_onD by fastforce
then have "I ` eq_class x ≠ I ` eq_class y"
using refl_eq
by (metis Image_singleton_iff UNIV_I imageI refl_onD)
with ‹x ∈ base_vars b ∧ y ∈ base_vars b› show "realise x ≠ realise y"
using hunion_hempty_left[unfolded Zero_hf_def]
using inj_on_HF[THEN inj_onD] finite_I_image_eq_class
by (force simp: parents_empty_if_base_vars)
qed
lemma Ex_AT_eq_mem_subterms_last_if_subterms':
assumes "t ∈ subterms' b"
obtains "t ∈ subterms (last b) - base_vars b"
| t' where "t' ∈ subterms (last b) - base_vars b"
"AT (t =⇩s t') ∈ set b ∨ AT (t' =⇩s t) ∈ set b"
proof(cases "t ∈ subterms (last b) - base_vars b")
case False
from assms have "t ∈ subterms b"
using base_vars_Un_subterms'_eq_subterms by auto
with False consider (t_base_vars) "t ∈ base_vars b" | (t_wits) "t ∈ Var ` wits b"
using no_new_subterms_if_wf_branch[OF wf_branch]
by (meson DiffI no_new_subterms_def)
then show ?thesis
proof cases
case t_wits
with ‹t ∈ subterms' b› have "t ∉ Var ` pwits b"
unfolding subterms'_def base_vars_def by blast
with t_wits obtain t' where t': "t' ∈ subterms (last b)"
"AT (t =⇩s t') ∈ set b ∨ AT (t' =⇩s t) ∈ set b"
unfolding pwits_def by blast
with ‹t ∈ subterms' b› have "t' ∉ base_vars b"
using AT_eq_urelems_subterms'_cases B_T_partition_verts(1)
by (metis Un_iff base_vars_def disjoint_iff)
with t' that show ?thesis
by blast
qed (use assms[unfolded subterms'_def] in blast)
qed
lemma realisation_if_AF_eq:
assumes "sat b"
assumes "AF (t1 =⇩s t2) ∈ set b"
shows "realise t1 ≠ realise t2"
proof -
note AF_eq_branch_wits_subtermsD[OF assms(2)]
then consider
(t1_base_vars) "t1 ∈ base_vars b" |
(t2_base_vars) "t2 ∈ base_vars b" "t1 ∈ base_vars b ∪ subterms' b" |
(subterms) "t1 ∈ subterms' b" "t2 ∈ subterms' b"
by (metis UnE wf_branch wits_subterms_eq_base_vars_Un_subterms')
then show ?thesis
proof cases
case t1_base_vars
with assms show ?thesis
using realise_base_vars_if_AF_eq by blast
next
case t2_base_vars
with assms show ?thesis
using realise_base_vars_if_AF_eq by blast
next
case subterms
define Δ where "Δ ≡ {(t1, t2) ∈ subterms' b × subterms' b.
AF (t1 =⇩s t2) ∈ set b ∧ realise t1 = realise t2}"
have "finite Δ"
proof -
have "Δ ⊆ subterms' b × subterms' b"
unfolding Δ_def by auto
moreover note finite_cartesian_product[OF finite_subterms' finite_subterms']
ultimately show ?thesis
using finite_subset by blast
qed
let ?h = "λ(t1, t2). min (height t1) (height t2)"
have False if "Δ ≠ {}"
proof -
obtain t1 t2 where t1_t2: "(t1, t2) = arg_min_on ?h Δ"
by (metis surj_pair)
have "(t1, t2) ∈ Δ" "?h (t1, t2) = Min (?h ` Δ)"
proof -
from arg_min_if_finite(1)[OF ‹finite Δ› that] t1_t2 show "(t1, t2) ∈ Δ"
by metis
have "f (arg_min_on f S) = Min (f ` S)" if "finite S" "S ≠ {}"
for f :: "('a pset_term × 'a pset_term) ⇒ nat" and S
using arg_min_least[OF that] that
by (auto intro!: Min_eqI[symmetric] intro: arg_min_if_finite(1)[OF that])
from this[OF ‹finite Δ› that] t1_t2 show "?h (t1, t2) = Min (?h ` Δ)"
by auto
qed
then have *: "t1 ∈ subterms' b" "t2 ∈ subterms' b"
"AF (t1 =⇩s t2) ∈ set b" "realise t1 = realise t2"
unfolding Δ_def by auto
obtain t1' t2' where t1'_t2':
"t1' ∈ subterms (last b) - base_vars b" "t2' ∈ subterms (last b) - base_vars b"
"AF (t1' =⇩s t2') ∈ set b"
"realise t1' = realise t1" "realise t2' = realise t2"
proof -
note Ex_AT_eq_mem_subterms_last_if_subterms'[OF ‹t1 ∈ subterms' b›]
then obtain t1'' where
"t1'' ∈ subterms (last b) - base_vars b" "AF (t1'' =⇩s t2) ∈ set b"
"realise t1'' = realise t1"
proof cases
case (2 t1')
from bopen neqSelf ‹AF (t1 =⇩s t2) ∈ set b› have "t1 ≠ t2"
by blast
with 2 ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (t1' =⇩s t2) ∈ set b"
using lexpands_eq.intros(2,4)[OF _ ‹AF (t1 =⇩s t2) ∈ set b›, THEN lexpands.intros(6)]
by fastforce
with that[OF _ this] "2"(1) ‹sat b›[unfolded sat_def] show ?thesis
using realisation_if_AT_eq 2 by metis
qed (use * that[of t1] in blast)
moreover
note Ex_AT_eq_mem_subterms_last_if_subterms'[OF ‹t2 ∈ subterms' b›]
then obtain t2'' where
"t2'' ∈ subterms (last b) - base_vars b" "AF (t1'' =⇩s t2'') ∈ set b"
"realise t2'' = realise t2"
proof cases
case (2 t2')
from bopen neqSelf ‹AF (t1'' =⇩s t2) ∈ set b› have "t1'' ≠ t2"
by blast
with 2 ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (t1'' =⇩s t2') ∈ set b"
using lexpands_eq.intros(2,4)[OF _ ‹AF (t1'' =⇩s t2) ∈ set b›, THEN lexpands.intros(6)]
by fastforce
with that[OF _ this] "2"(1) ‹sat b›[unfolded sat_def] show ?thesis
using realisation_if_AT_eq 2 by metis
qed (use ‹AF (t1'' =⇩s t2) ∈ set b› that[of t2] in blast)
ultimately show ?thesis
using that * by metis
qed
with ‹realise t1 = realise t2› have "(t1', t2') ∈ Δ"
unfolding Δ_def subterms'_def
by (simp add: AF_eq_subterms_branchD(1,2))
then have t1'_t2'_subterms: "t1' ∈ subterms' b" "t2' ∈ subterms' b"
unfolding Δ_def by blast+
from t1'_t2' lemma1_2 "*"(3) have "?h (t1', t2') = ?h (t1, t2)"
by (metis in_subterms'_if_AF_eq_in_branch(1,2)[OF wf_branch] case_prod_conv)
from mem_urelems_if_urelem_last[OF wf_branch] t1'_t2'(1,2)
have not_urelem: "¬ urelem (last b) t1'" "¬ urelem (last b) t2'"
unfolding base_vars_def by auto
from finite_vars_branch infinite_vars obtain x where "x ∉ vars b"
using ex_new_if_finite by blast
from bexpands_wit.intros[OF t1'_t2'(3) _ _ _ _ this not_urelem]
t1'_t2'(1,2) ‹sat b›[unfolded sat_def] consider
s1 where "AT (s1 ∈⇩s t1') ∈ set b" "AF (s1 ∈⇩s t2') ∈ set b" |
s2 where "AF (s2 ∈⇩s t1') ∈ set b" "AT (s2 ∈⇩s t2') ∈ set b"
using bexpands.intros(2-) by (metis Diff_iff)
then show ?thesis
proof cases
case 1
then have "realise s1 ❙∈ realise t2'"
using realisation_if_AT_mem
by (metis "*"(4) t1'_t2'(4) t1'_t2'(5))
with 1 t1'_t2'(3,4) obtain s2 where
"s2 →⇘bgraph b⇙ t2'" "realise s1 = realise s2"
using dominates_if_mem_realisation in_subterms'_if_AT_mem_in_branch(1)[OF wf_branch]
by metis
then have "AT (s2 ∈⇩s t2') ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹AF (s1 ∈⇩s t2') ∈ set b› ‹sat b›[THEN satD(1), THEN lin_satD]
have "AF (s2 =⇩s s1) ∈ set b"
using lexpands_eq.intros(5)[THEN lexpands.intros(6)] by fastforce
then have "s1 ≠ s2"
using neqSelf bopen by blast
from realise_base_vars_if_AF_eq[OF ‹sat b› ‹AF (s2 =⇩s s1) ∈ set b›]
‹realise s1 = realise s2›
have "s1 ∈ subterms' b" "s2 ∈ subterms' b"
by (metis Un_iff ‹AF (s2 =⇩s s1) ∈ set b› in_subterms'_if_AF_eq_in_branch wf_branch)+
with ‹realise s1 = realise s2› have "(s2, s1) ∈ Δ"
unfolding Δ_def using ‹AF (s2 =⇩s s1) ∈ set b› by auto
moreover
have "realise s1 ❙∈ realise t1'" "realise s2 ❙∈ realise t1'"
"realise s1 ❙∈ realise t2'" "realise s2 ❙∈ realise t2'"
using ‹realise s1 ❙∈ realise t2'› ‹realise s1 = realise s2›
using "*"(4) t1'_t2'(4,5) by auto
with lemma1_3 have "?h (s2, s1) < ?h (t1', t2')"
using ‹s1 ∈ subterms' b› ‹s2 ∈ subterms' b› t1'_t2'_subterms
by (auto simp: min_def)
ultimately show ?thesis
using arg_min_least[OF ‹finite Δ› ‹Δ ≠ {}›]
using ‹(t1', t2') ∈ Δ› ‹?h (t1', t2') = ?h (t1, t2)› t1_t2
by (metis (mono_tags, lifting) le_antisym le_eq_less_or_eq nat_neq_iff)
next
case 2
then have "realise s2 ❙∈ realise t1'"
using realisation_if_AT_mem
by (metis "*"(4) t1'_t2'(4) t1'_t2'(5))
with 2 t1'_t2'(3,4) obtain s1 where
"s1 →⇘bgraph b⇙ t1'" "realise s1 = realise s2"
using dominates_if_mem_realisation by metis
then have "AT (s1 ∈⇩s t1') ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹AF (s2 ∈⇩s t1') ∈ set b› ‹sat b›[unfolded sat_def]
have "AF (s1 =⇩s s2) ∈ set b"
using lexpands_eq.intros(5)[THEN lexpands.intros(6)]
using lin_satD by fastforce
then have "s1 ≠ s2"
using neqSelf bopen by blast
from realise_base_vars_if_AF_eq[OF ‹sat b› ‹AF (s1 =⇩s s2) ∈ set b›]
‹realise s1 = realise s2›
have "s1 ∈ subterms' b" "s2 ∈ subterms' b"
by (metis Un_iff ‹AF (s1 =⇩s s2) ∈ set b› in_subterms'_if_AF_eq_in_branch wf_branch)+
with ‹realise s1 = realise s2› have "(s1, s2) ∈ Δ"
unfolding Δ_def using ‹AF (s1 =⇩s s2) ∈ set b› by auto
moreover
have "realise s1 ❙∈ realise t1'" "realise s2 ❙∈ realise t1'"
"realise s1 ❙∈ realise t2'" "realise s2 ❙∈ realise t2'"
using ‹realise s2 ❙∈ realise t1'› ‹realise s1 = realise s2›
using "*"(4) t1'_t2'(4,5) by auto
with lemma1_3 have "?h (s1, s2) < ?h (t1', t2')"
using ‹s1 ∈ subterms' b› ‹s2 ∈ subterms' b› t1'_t2'_subterms
by (auto simp: min_def)
ultimately show ?thesis
using arg_min_least[OF ‹finite Δ› ‹Δ ≠ {}›]
using ‹(t1', t2') ∈ Δ› ‹?h (t1', t2') = ?h (t1, t2)› t1_t2
by (metis (mono_tags, lifting) le_antisym le_eq_less_or_eq nat_neq_iff)
qed
qed
with assms subterms show ?thesis
unfolding Δ_def by blast
qed
qed
lemma realisation_if_AF_mem:
assumes "sat b"
assumes "AF (s ∈⇩s t) ∈ set b"
shows "realise s ❙∉ realise t"
proof
assume "realise s ❙∈ realise t"
from assms have "s ∈ base_vars b ∪ subterms' b"
"t ∈ base_vars b ∪ subterms' b"
using in_subterms'_if_AF_mem_in_branch[OF wf_branch] by blast+
from dominates_if_mem_realisation[OF ‹realise s ❙∈ realise t›]
obtain s' where "s' →⇘bgraph b⇙ t" "realise s = realise s'"
by blast
then have "AT (s' ∈⇩s t) ∈ set b"
unfolding bgraph_def Let_def by auto
with assms lexpands_eq.intros(5)[THEN lexpands.intros(6)] have "AF (s' =⇩s s) ∈ set b"
unfolding sat_def using lin_satD by fastforce
from realisation_if_AF_eq[OF ‹sat b› this] ‹realise s = realise s'› show False
by simp
qed
lemma realisation_Empty: "realise (∅ n) = 0"
proof -
from bopen have "AT (s ∈⇩s ∅ n) ∉ set b" for s
using bclosed.intros by blast
then have "parents (bgraph b) (∅ n) = {}"
unfolding bgraph_def Let_def by auto
moreover
have "(∅ n) ∉ base_vars b"
proof -
have "(∅ n) ∉ Var ` pwits b"
using pwits_def wits_def by blast
moreover have "(∅ n) ∉ urelems b"
unfolding urelems_def using wf_branch[THEN wf_branch_not_Nil] last_in_set
using is_Var_if_urelem' by fastforce
ultimately show ?thesis
unfolding base_vars_def by blast
qed
then have "(∅ n) ∈ subterms' b ∨ (∅ n) ∉ verts (bgraph b)"
by (simp add: verts_bgraph)
ultimately show "realise (∅ n) = 0"
by (auto simp: verts_bgraph)
qed
lemma realisation_Union:
assumes "sat b"
assumes "t1 ⊔⇩s t2 ∈ subterms b"
shows "realise (t1 ⊔⇩s t2) = realise t1 ⊔ realise t2"
using assms
proof -
from assms have mem_subterms_last: "t1 ⊔⇩s t2 ∈ subterms (last b)"
using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
by simp
note not_urelem_comps_if_compound[where ?f="(⊔⇩s)", OF assms(2), simplified]
moreover note subterms_fmD(1,2)[OF mem_subterms_last]
then have "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
unfolding pwits_def wits_def
using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
ultimately have "t1 ∈ subterms' b" "t2 ∈ subterms' b"
unfolding subterms'_def base_vars_def
using assms(2) by (auto dest: subterms_branchD)
from assms(2) have "t1 ⊔⇩s t2 ∈ subterms' b"
using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast
have "realise (t1 ⊔⇩s t2) ≤ realise t1 ⊔ realise t2"
proof
fix e assume "e ❙∈ realise (t1 ⊔⇩s t2)"
then obtain s where s: "e = realise s" "s →⇘bgraph b⇙ (t1 ⊔⇩s t2)"
using dominates_if_mem_realisation ‹t1 ⊔⇩s t2 ∈ subterms' b›
by auto
then have "AT (s ∈⇩s t1 ⊔⇩s t2) ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹sat b› consider "AT (s ∈⇩s t1) ∈ set b" | "AF (s ∈⇩s t1) ∈ set b"
unfolding sat_def using bexpands_nowit.intros(3)[OF _ mem_subterms_last, THEN bexpands.intros(1)]
by blast
then show "e ❙∈ realise t1 ⊔ realise t2"
proof(cases)
case 1
with s show ?thesis using realisation_if_AT_mem by auto
next
case 2
from ‹sat b› lexpands_un.intros(4)[OF ‹AT (s ∈⇩s t1 ⊔⇩s t2) ∈ set b› this]
have "AT (s ∈⇩s t2) ∈ set b"
unfolding sat_def using lin_satD lexpands.intros(2) by force
with s show ?thesis using realisation_if_AT_mem by auto
qed
qed
moreover have "realise t1 ⊔ realise t2 ≤ realise (t1 ⊔⇩s t2)"
proof
fix e assume "e ❙∈ realise t1 ⊔ realise t2"
with ‹t1 ∈ subterms' b› ‹t2 ∈ subterms' b› consider
s1 where "e = realise s1" "s1 →⇘bgraph b⇙ t1" |
s2 where "e = realise s2" "s2 →⇘bgraph b⇙ t2"
using dominates_if_mem_realisation by force
then show "e ❙∈ realise (t1 ⊔⇩s t2)"
proof(cases)
case 1
then have "AT (s1 ∈⇩s t1) ∈ set b"
unfolding bgraph_def Let_def by auto
from ‹sat b› lexpands_un.intros(2)[OF this mem_subterms_last, THEN lexpands.intros(2)]
have "AT (s1 ∈⇩s t1 ⊔⇩s t2) ∈ set b"
unfolding sat_def using lin_satD by force
with 1 realisation_if_AT_mem[OF this] show ?thesis
by blast
next
case 2
then have "AT (s2 ∈⇩s t2) ∈ set b"
unfolding bgraph_def Let_def by auto
from ‹sat b› lexpands_un.intros(3)[OF this mem_subterms_last, THEN lexpands.intros(2)]
have "AT (s2 ∈⇩s t1 ⊔⇩s t2) ∈ set b"
unfolding sat_def using lin_satD by force
with 2 realisation_if_AT_mem[OF this] show ?thesis
by blast
qed
qed
ultimately show ?thesis by blast
qed
lemma realisation_Inter:
assumes "sat b"
assumes "t1 ⊓⇩s t2 ∈ subterms b"
shows "realise (t1 ⊓⇩s t2) = realise t1 ⊓ realise t2"
using assms
proof -
from assms have mem_subterms_last: "t1 ⊓⇩s t2 ∈ subterms (last b)"
using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
by simp
note not_urelem_comps_if_compound[where ?f="(⊓⇩s)", OF assms(2), simplified]
moreover note subterms_fmD(3,4)[OF mem_subterms_last]
then have "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
unfolding pwits_def wits_def
using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
ultimately have t1_t2_subterms': "t1 ∈ subterms' b" "t2 ∈ subterms' b"
unfolding subterms'_def base_vars_def
using assms(2) by (auto dest: subterms_branchD)
from assms(2) have "t1 ⊓⇩s t2 ∈ subterms' b"
using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast
have "realise (t1 ⊓⇩s t2) ≤ realise t1 ⊓ realise t2"
proof
fix e assume "e ❙∈ realise (t1 ⊓⇩s t2)"
with ‹t1 ⊓⇩s t2 ∈ subterms' b› obtain s
where s: "e = realise s" "s →⇘bgraph b⇙ (t1 ⊓⇩s t2)"
using dominates_if_mem_realisation by auto
then have "AT (s ∈⇩s t1 ⊓⇩s t2) ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹sat b› lexpands_int.intros(1)[OF this, THEN lexpands.intros(3)]
have "AT (s ∈⇩s t1) ∈ set b" "AT (s ∈⇩s t2) ∈ set b"
unfolding sat_def using lin_satD by force+
from this[THEN realisation_if_AT_mem] s show "e ❙∈ realise t1 ⊓ realise t2"
by auto
qed
moreover have "realise t1 ⊓ realise t2 ≤ realise (t1 ⊓⇩s t2)"
proof
fix e assume "e ❙∈ realise t1 ⊓ realise t2"
with ‹t1 ∈ subterms' b› ‹t2 ∈ subterms' b› obtain s1 s2 where s1_s2:
"e = realise s1" "s1 →⇘bgraph b⇙ t1"
"e = realise s2" "s2 →⇘bgraph b⇙ t2"
using dominates_if_mem_realisation by auto metis
then have "AT (s1 ∈⇩s t1) ∈ set b" "AT (s2 ∈⇩s t2) ∈ set b"
unfolding bgraph_def Let_def by auto
moreover have "AT (s1 ∈⇩s t2) ∈ set b"
proof -
from ‹sat b› have "AT (s1 ∈⇩s t2) ∈ set b ∨ AF (s1 ∈⇩s t2) ∈ set b"
unfolding sat_def
using bexpands_nowit.intros(4)[OF ‹AT (s1 ∈⇩s t1) ∈ set b› mem_subterms_last]
using bexpands.intros(1) by blast
moreover from ‹sat b› s1_s2 have False if "AF (s1 ∈⇩s t2) ∈ set b"
proof -
note lexpands_eq.intros(5)[OF ‹AT (s2 ∈⇩s t2) ∈ set b› that, THEN lexpands.intros(6)]
with realisation_if_AF_eq[OF ‹sat b›, of s2 s1] have "realise s2 ≠ realise s1"
using ‹sat b› by (auto simp: sat_def lin_satD)
with ‹e = realise s1› ‹e = realise s2› show False by simp
qed
ultimately show "AT (s1 ∈⇩s t2) ∈ set b" by blast
qed
ultimately have "AT (s1 ∈⇩s t1 ⊓⇩s t2) ∈ set b"
using ‹sat b› lexpands_int.intros(6)[OF _ _ mem_subterms_last, THEN lexpands.intros(3)]
unfolding sat_def by (fastforce simp: lin_satD)
from realisation_if_AT_mem[OF this] show "e ❙∈ realise (t1 ⊓⇩s t2)"
unfolding ‹e = realise s1›
by simp
qed
ultimately show ?thesis by blast
qed
lemma realisation_Diff:
assumes "sat b"
assumes "s -⇩s t ∈ subterms b"
shows "realise (s -⇩s t) = realise s - realise t"
using assms
proof -
from assms have mem_subterms_last: "s -⇩s t ∈ subterms (last b)"
using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
by simp
note not_urelem_comps_if_compound[where ?f="(-⇩s)", OF assms(2), simplified]
moreover note subterms_fmD(5,6)[OF mem_subterms_last]
then have "s ∉ Var ` pwits b" "t ∉ Var ` pwits b"
unfolding pwits_def wits_def
using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
ultimately have "s ∈ subterms' b" "t ∈ subterms' b"
unfolding subterms'_def base_vars_def
using assms(2) by (auto dest: subterms_branchD)
from assms(2) have "s -⇩s t ∈ subterms' b"
using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast
have "realise (s -⇩s t) ≤ realise s - realise t"
proof
fix e assume "e ❙∈ realise (s -⇩s t)"
then obtain u where u: "e = realise u" "u →⇘bgraph b⇙ (s -⇩s t)"
using dominates_if_mem_realisation ‹s -⇩s t ∈ subterms' b› by auto
then have "AT (u ∈⇩s s -⇩s t) ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹sat b› lexpands_diff.intros(1)[OF this, THEN lexpands.intros(4)]
have "AT (u ∈⇩s s) ∈ set b" "AF (u ∈⇩s t) ∈ set b"
unfolding sat_def using lin_satD by force+
with u show "e ❙∈ realise s - realise t"
using ‹sat b› realisation_if_AT_mem realisation_if_AF_mem
by auto
qed
moreover have "realise s - realise t ≤ realise (s -⇩s t)"
proof
fix e assume "e ❙∈ realise s - realise t"
then obtain u where u:
"e = realise u" "u →⇘bgraph b⇙ s" "¬ u →⇘bgraph b⇙ t"
using dominates_if_mem_realisation ‹s ∈ subterms' b› ‹t ∈ subterms' b› by auto
then have "AT (u ∈⇩s s) ∈ set b"
unfolding bgraph_def Let_def by auto
moreover have "AF (u ∈⇩s t) ∈ set b"
proof -
from ‹sat b› have "AT (u ∈⇩s t) ∈ set b ∨ AF (u ∈⇩s t) ∈ set b"
unfolding sat_def using bexpands_nowit.intros(5)[OF ‹AT (u ∈⇩s s) ∈ set b› mem_subterms_last]
using bexpands.intros(1) by blast
moreover from u(3) have False if "AT (u ∈⇩s t) ∈ set b"
using that unfolding Let_def bgraph_def by (auto simp: arcs_ends_def arc_to_ends_def)
ultimately show "AF (u ∈⇩s t) ∈ set b"
by blast
qed
ultimately have "AT (u ∈⇩s s -⇩s t) ∈ set b"
using ‹sat b› lexpands_diff.intros(6)[OF _ _ mem_subterms_last, THEN lexpands.intros(4)]
unfolding sat_def by (fastforce simp: lin_satD)
from realisation_if_AT_mem[OF this] show "e ❙∈ realise (s -⇩s t)"
unfolding ‹e = realise u›
by simp
qed
ultimately show ?thesis by blast
qed
lemma realisation_Single:
assumes "sat b"
assumes "Single t ∈ subterms b"
shows "realise (Single t) = HF {realise t}"
using assms
proof -
from assms have mem_subterms_last: "Single t ∈ subterms (last b)"
using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
by simp
have "Single t ∈ subterms' b"
proof -
from urelems_subs_vars have "Single t ∉ base_vars b"
unfolding base_vars_def by blast
then show ?thesis
by (simp add: assms(2) subterms'_def)
qed
have "realise (Single t) ≤ HF {realise t}"
proof
fix e assume "e ❙∈ realise (Single t)"
then obtain s where s: "e = realise s" "s →⇘bgraph b⇙ Single t"
using dominates_if_mem_realisation ‹Single t ∈ subterms' b› by auto
then have "AT (s ∈⇩s Single t) ∈ set b"
unfolding bgraph_def Let_def by auto
with ‹sat b› lexpands_single.intros(2)[OF this, THEN lexpands.intros(5)]
have "AT (s =⇩s t) ∈ set b"
unfolding sat_def using lin_satD by fastforce
with s show "e ❙∈ HF {realise t}"
using realisation_if_AT_eq ‹sat b›[unfolded sat_def]
by auto
qed
moreover have "HF {realise t} ≤ realise (Single t)"
proof
fix e assume "e ❙∈ HF {realise t}"
then have "e = realise t"
by simp
from lexpands_single.intros(1)[OF mem_subterms_last, THEN lexpands.intros(5)] ‹sat b›
have "AT (t ∈⇩s Single t) ∈ set b"
unfolding sat_def using lin_satD by fastforce
from realisation_if_AT_mem[OF this] ‹e = realise t›
show "e ❙∈ realise (Single t)"
by simp
qed
ultimately show ?thesis by blast
qed
lemmas realisation_simps =
realisation_Empty realisation_Union realisation_Inter realisation_Diff realisation_Single
end
subsubsection ‹Coherence›
lemma (in open_branch) I⇩s⇩t_realisation_eq_realisation:
assumes "sat b" "t ∈ subterms b"
shows "I⇩s⇩t (λx. realise (Var x)) t = realise t"
using assms
by (induction t) (force simp: realisation_simps dest: subterms_branchD)+
lemma (in open_branch) coherence:
assumes "sat b" "φ ∈ set b"
shows "interp I⇩s⇩a (λx. realise (Var x)) φ"
using assms
proof(induction "size φ" arbitrary: φ rule: less_induct)
case less
then show ?case
proof(cases φ)
case (Atom a)
then show ?thesis
proof(cases a)
case (Elem s t)
with Atom less have "s ∈ subterms b" "t ∈ subterms b"
using AT_mem_subterms_branchD by blast+
with Atom Elem less show ?thesis
using I⇩s⇩t_realisation_eq_realisation[OF ‹sat b›] realisation_if_AT_mem by auto
next
case (Equal s t)
with Atom less have "s ∈ subterms b" "t ∈ subterms b"
using AT_eq_subterms_branchD by blast+
with Atom Equal less satD(1)[OF ‹sat b›] show ?thesis
using I⇩s⇩t_realisation_eq_realisation[OF ‹sat b›] realisation_if_AT_eq by auto
qed
next
case (And φ1 φ2)
with ‹φ ∈ set b› ‹sat b›[THEN satD(1), THEN lin_satD] have "φ1 ∈ set b" "φ2 ∈ set b"
using lexpands_fm.intros(1)[THEN lexpands.intros(1)] by fastforce+
with And less show ?thesis by simp
next
case (Or φ1 φ2)
with ‹φ ∈ set b› ‹sat b›[THEN satD(2)] have "φ1 ∈ set b ∨ Neg φ1 ∈ set b"
using bexpands_nowit.intros(1)[THEN bexpands.intros(1)]
by blast
with less Or ‹sat b›[THEN satD(1), THEN lin_satD] have "φ1 ∈ set b ∨ φ2 ∈ set b"
using lexpands_fm.intros(3)[THEN lexpands.intros(1)] by fastforce
with Or less show ?thesis
by force
next
case (Neg φ')
show ?thesis
proof(cases φ')
case (Atom a)
then show ?thesis
proof(cases a)
case (Elem s t)
with Atom Neg less have "s ∈ subterms b" "t ∈ subterms b"
using AF_mem_subterms_branchD by blast+
with Neg Atom Elem less show ?thesis
using I⇩s⇩t_realisation_eq_realisation realisation_if_AF_mem ‹sat b› by auto
next
case (Equal s t)
with Atom Neg less have "s ∈ subterms b" "t ∈ subterms b"
using AF_eq_subterms_branchD by blast+
with Neg Atom Equal less show ?thesis
using I⇩s⇩t_realisation_eq_realisation realisation_if_AF_eq ‹sat b› by auto
qed
next
case (And φ1 φ2)
with Neg ‹sat b›[THEN satD(2)] less have "φ1 ∈ set b ∨ Neg φ1 ∈ set b"
using bexpands_nowit.intros(2)[THEN bexpands.intros(1)] by blast
with ‹sat b›[THEN satD(1), THEN lin_satD] Neg And less
have "Neg φ2 ∈ set b ∨ Neg φ1 ∈ set b"
using lexpands_fm.intros(5)[THEN lexpands.intros(1)] by fastforce
with Neg And less show ?thesis by force
next
case (Or φ1 φ2)
with ‹φ ∈ set b› Neg ‹sat b›[THEN satD(1), THEN lin_satD]
have "Neg φ1 ∈ set b" "Neg φ2 ∈ set b"
using lexpands_fm.intros(2)[THEN lexpands.intros(1)] by fastforce+
moreover have "size (Neg φ1) < size φ" "size (Neg φ2) < size φ"
using Neg Or by simp_all
ultimately show ?thesis using Neg Or less by force
next
case Neg': (Neg φ'')
with ‹φ ∈ set b› Neg ‹sat b›[THEN satD(1), THEN lin_satD] have "φ'' ∈ set b"
using lexpands_fm.intros(7)[THEN lexpands.intros(1)] by fastforce+
with Neg Neg' less show ?thesis by simp
qed
qed
qed
subsection ‹Soundness of the Calculus›
subsubsection ‹Soundness of Closedness›
lemmas wf_trancl_hmem_rel = wf_trancl[OF wf_hmem_rel]
lemma trancl_hmem_rel_not_refl: "(x, x) ∉ hmem_rel⇧+"
using wf_trancl_hmem_rel by simp
lemma mem_trancl_elts_rel_if_member_seq:
assumes "member_seq s cs t"
assumes "cs ≠ []"
assumes "∀a ∈ set cs. I⇩s⇩a M a"
shows "(I⇩s⇩t M s, I⇩s⇩t M t) ∈ hmem_rel⇧+"
using assms
proof(induction rule: member_seq.induct)
case (2 s s' u cs t)
show ?case
proof(cases cs)
case Nil
with 2 show ?thesis
unfolding hmem_rel_def by auto
next
case (Cons c cs')
with 2 have "(I⇩s⇩t M u, I⇩s⇩t M t) ∈ hmem_rel⇧+"
by simp
moreover from 2 have "I⇩s⇩a M (s ∈⇩s u)"
by simp
ultimately show ?thesis
unfolding hmem_rel_def by (simp add: trancl_into_trancl2)
qed
qed simp_all
lemma bclosed_sound:
assumes "bclosed b"
shows "∃φ ∈ set b. ¬ interp I⇩s⇩a M φ"
using assms
proof -
have False if "∀φ ∈ set b. interp I⇩s⇩a M φ"
using assms that
proof(induction rule: bclosed.induct)
case (memberCycle cs b)
then have "∀a ∈ set cs. I⇩s⇩a M a"
unfolding Atoms_def by fastforce
from memberCycle obtain s where "member_seq s cs s"
using member_cycle.elims(2) by blast
with memberCycle ‹∀a ∈ set cs. I⇩s⇩a M a› have "(I⇩s⇩t M s, I⇩s⇩t M s) ∈ hmem_rel⇧+"
using mem_trancl_elts_rel_if_member_seq member_cycle.simps(2) by blast
with trancl_hmem_rel_not_refl show ?case
by blast
qed (use interp.simps(4) in ‹fastforce+›)
then show ?thesis
by blast
qed
lemma types_term_lt_if_member_seq:
includes Set_member_no_ascii_notation
fixes cs :: "'a pset_atom list"
assumes "∀a ∈ set cs. v ⊢ a"
assumes "member_seq s cs t" "cs ≠ []"
shows "∃ls lt. v ⊢ s : ls ∧ v ⊢ t : lt ∧ ls < lt"
using assms
proof(induction s cs t rule: member_seq.induct)
case (2 s s' u cs t)
then show ?case
proof(cases cs)
case (Cons c cs')
with 2 obtain lu lt where "v ⊢ u : lu" "v ⊢ t : lt" "lu < lt"
by auto
moreover from 2 obtain ls where "v ⊢ s : ls" "ls < lu"
using ‹v ⊢ u : lu› by (auto simp: types_pset_atom.simps dest: types_term_unique)
ultimately show ?thesis
by fastforce
qed (fastforce simp: types_pset_atom.simps)
qed auto
lemma no_member_cycle_if_types_last:
fixes b :: "'a branch"
assumes "wf_branch b"
assumes "∃v. v ⊢ last b"
shows "¬ (member_cycle cs ∧ set cs ⊆ Atoms (set b))"
proof
presume "member_cycle cs" "set cs ⊆ Atoms (set b)"
then obtain s where "member_seq s cs s" "cs ≠ []"
using member_cycle.elims(2) by blast
moreover from assms obtain v where "∀φ ∈ set b. v ⊢ φ"
using types_urelems by blast
with ‹set cs ⊆ Atoms (set b)› have "∀a ∈ set cs. v ⊢ a"
unfolding Atoms_def by (auto dest!: types_fmD(6))
ultimately show False
using types_term_lt_if_member_seq types_term_unique by blast
qed simp_all
subsubsection ‹Soundness of the Expansion Rules›
lemma lexpands_sound:
assumes "lexpands b' b"
assumes "φ ∈ set b'"
assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
shows "interp I⇩s⇩a M φ"
using assms
proof(induction rule: lexpands.induct)
case (1 b' b)
then show ?case
by (induction rule: lexpands_fm.induct)
(metis empty_iff empty_set interp.simps(2,3,4) set_ConsD)+
next
case (2 b' b)
then show ?case
proof(induction rule: lexpands_un.induct)
case (4 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case
by force
next
case (5 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case
by force
qed force+
next
case (3 b' b)
then show ?case
proof(induction rule: lexpands_int.induct)
case (4 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case
by force
next
case (5 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case
by force
qed force+
next
case (4 b' b)
then show ?case
proof(induction rule: lexpands_diff.induct)
case (4 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case by force
next
case (5 s t1 t2 branch)
with this(1)[THEN this(4)] show ?case by force
qed force+
next
case (5 b' b)
then show ?case
by (induction rule: lexpands_single.induct) force+
next
case (6 b' b)
then show ?case
proof(induction rule: lexpands_eq_induct')
case (subst t1 t2 t1' t2' p l b)
with this(1,2)[THEN this(6)] show ?case
by (cases l; cases p) auto
next
case (neq s t s' b)
with this(1,2)[THEN this(4)] show ?case by force
qed
qed
lemma bexpands_nowit_sound:
assumes "bexpands_nowit bs' b"
assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
shows "∃b' ∈ bs'. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ"
using assms
by (induction rule: bexpands_nowit.induct) force+
lemma I⇩s⇩t_upd_eq_if_not_mem_vars_term:
assumes "x ∉ vars t"
shows "I⇩s⇩t (M(x := y)) t = I⇩s⇩t M t"
using assms by (induction t) auto
lemma I⇩s⇩a_upd_eq_if_not_mem_vars_atom:
assumes "x ∉ vars a"
shows "I⇩s⇩a (M(x := y)) a = I⇩s⇩a M a"
using assms
by (cases a) (auto simp: I⇩s⇩t_upd_eq_if_not_mem_vars_term)
lemma interp_upd_eq_if_not_mem_vars_fm:
assumes "x ∉ vars φ"
shows "interp I⇩s⇩a (M(x := y)) φ = interp I⇩s⇩a M φ"
using assms
by (induction φ) (auto simp: I⇩s⇩a_upd_eq_if_not_mem_vars_atom)
lemma bexpands_wit_sound:
assumes "bexpands_wit s t x bs' b"
assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
shows "∃M. ∃b' ∈ bs'. ∀ψ ∈ set (b' @ b). interp I⇩s⇩a M ψ"
using assms
proof (induction rule: bexpands_wit.induct)
let ?bs'="{[AT (Var x ∈⇩s s), AF (Var x ∈⇩s t)],
[AT (Var x ∈⇩s t), AF (Var x ∈⇩s s)]}"
case (1 b)
with this(1)[THEN this(9)] have "I⇩s⇩t M s ≠ I⇩s⇩t M t"
by auto
then obtain y where y:
"y ❙∈ I⇩s⇩t M s ∧ y ❙∉ I⇩s⇩t M t ∨
y ❙∈ I⇩s⇩t M t ∧ y ❙∉ I⇩s⇩t M s"
by auto
have "x ∉ vars s" "x ∉ vars t"
using 1 by (auto simp: vars_fm_vars_branchI)
then have "I⇩s⇩t (M(x := y)) s = I⇩s⇩t M s" "I⇩s⇩t (M(x := y)) t = I⇩s⇩t M t"
using I⇩s⇩t_upd_eq_if_not_mem_vars_term by metis+
then have "∃b' ∈ ?bs'. ∀ψ ∈ set b'. interp I⇩s⇩a (M(x := y)) ψ"
using 1 y by auto
moreover have "∀ψ ∈ set b. interp I⇩s⇩a (M(x := y)) ψ"
using "1"(9) ‹x ∉ vars b› interp_upd_eq_if_not_mem_vars_fm
by (metis vars_fm_vars_branchI)
ultimately show ?case
by auto (metis fun_upd_same)+
qed
lemma bexpands_sound:
assumes "bexpands bs' b"
assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
shows "∃M. ∃b' ∈ bs'. ∀ψ ∈ set (b' @ b). interp I⇩s⇩a M ψ"
using assms
proof(induction rule: bexpands.induct)
case (1 bs' b)
with bexpands_nowit_sound[OF this(1)] have "∃b' ∈ bs'. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ"
by blast
with 1 show ?case
by auto
next
case (2 t1 t2 x bs b)
then show ?case using bexpands_wit_sound by metis
qed
subsection ‹Upper Bounding the Cardinality of a Branch›
lemma Ex_bexpands_wits_if_in_wits:
assumes "wf_branch b"
assumes "x ∈ wits b"
obtains t1 t2 bs b2 b1 where
"expandss b (b2 @ b1)" "bexpands_wit t1 t2 x bs b1" "b2 ∈ bs" "expandss b1 [last b]"
"x ∉ wits b1" "wits (b2 @ b1) = insert x (wits b1)"
proof -
from assms obtain φ where "expandss b [φ]"
unfolding wf_branch_def by blast
then have "last b = φ"
by simp
from ‹expandss b [φ]› ‹x ∈ wits b› that show ?thesis
unfolding ‹last b = φ›
proof(induction b "[φ]" rule: expandss.induct)
case 1
then show ?case by simp
next
case (2 b2 b1)
with expandss_mono have "b1 ≠ []"
by fastforce
with lexpands_wits_eq[OF ‹lexpands b2 b1› this] 2 show ?case
by (metis (no_types, lifting) expandss.intros(2))
next
case (3 bs _ b2)
then show ?case
proof(induction rule: bexpands.induct)
case (1 bs b1)
with expandss_mono have "b1 ≠ []"
by fastforce
with bexpands_nowit_wits_eq[OF ‹bexpands_nowit bs b1› ‹b2 ∈ bs› this] 1 show ?case
by (metis bexpands.intros(1) expandss.intros(3))
next
case (2 t1 t2 y bs b1)
show ?case
proof(cases "x ∈ wits b1")
case True
from 2 have "expandss (b2 @ b1) b1"
using expandss.intros(3)[OF _ "2.prems"(1)] bexpands.intros(2)[OF "2.hyps"]
by (metis expandss.intros(1))
with True 2 show ?thesis
using expandss_trans by blast
next
case False
from 2 have "b1 ≠ []"
using expandss_mono by fastforce
with bexpands_witD[OF "2"(1)] "2"(2-) have "wits (b2 @ b1) = insert y (wits b1)"
unfolding wits_def
by (metis "2.hyps" bexpands_wit_wits_eq wits_def)
moreover from ‹y ∉ vars_branch b1› have "y ∉ wits b1"
unfolding wits_def by simp
moreover from calculation have "y = x"
using False 2 by simp
ultimately show ?thesis
using 2 by (metis expandss.intros(1))
qed
qed
qed
qed
lemma card_wits_ub_if_wf_branch:
assumes "wf_branch b"
shows "card (wits b) ≤ (card (subterms (last b)))⇧2"
proof -
from assms obtain φ where "expandss b [φ]"
unfolding wf_branch_def by blast
with wf_branch_not_Nil[OF assms] have [simp]: "last b = φ"
using expandss_last_eq by force
have False if card_gt: "card (wits b) > (card (subterms φ))⇧2"
proof -
define ts where "ts ≡ (λx. SOME t1_t2. ∃bs b2 b1.
expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit (fst t1_t2) (snd t1_t2) x bs b1 ∧ expandss b1 [φ])"
from ‹expandss b [φ]› ‹last b = φ›
have *: "∃t1_t2 bs b2 b1.
expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit (fst t1_t2) (snd t1_t2) x bs b1 ∧ expandss b1 [φ]"
if "x ∈ wits b" for x
using that Ex_bexpands_wits_if_in_wits[OF ‹wf_branch b› that] by (metis fst_conv snd_conv)
have ts_wd:
"∃bs b2 b1. expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit t1 t2 x bs b1 ∧ expandss b1 [φ]"
if "ts x = (t1, t2)" "x ∈ wits b" for t1 t2 x
using exE_some[OF * that(1)[THEN eq_reflection, symmetric, unfolded ts_def], OF that(2)]
by simp
with ‹last b = φ› ‹expandss b [φ]› have in_subterms_fm:
"t1 ∈ subterms φ" "t2 ∈ subterms φ"
if "ts x = (t1, t2)" "x ∈ wits b" for t1 t2 x
using that bexpands_witD
by (metis expandss_last_eq list.discI)+
have "¬ inj_on ts (wits b)"
proof -
from in_subterms_fm have "ts ` wits b ⊆ subterms φ × subterms φ"
by (intro subrelI) (metis imageE mem_Sigma_iff)
then have "card (ts ` wits b) ≤ card (subterms φ × subterms φ)"
by (intro card_mono) (simp_all add: finite_subterms_fm)
moreover have "card (subterms φ × subterms φ) = (card (subterms φ))⇧2"
unfolding card_cartesian_product by algebra
ultimately show "¬ inj_on ts (wits b)"
using card_gt by (metis card_image linorder_not_less)
qed
from ‹¬ inj_on ts (wits b)› obtain x t1 t2 xb1 xbs2 xb2 y yb1 ybs2 yb2 where x_y:
"x ≠ y" "x ∈ wits b" "y ∈ wits b"
"expandss xb1 [φ]" "bexpands_wit t1 t2 x xbs2 xb1" "xb2 ∈ xbs2" "expandss b (xb2 @ xb1)"
"expandss yb1 [φ]" "bexpands_wit t1 t2 y ybs2 yb1" "yb2 ∈ ybs2" "expandss b (yb2 @ yb1)"
unfolding inj_on_def by (metis ts_wd prod.exhaust)
have "xb2 ≠ yb2"
using x_y(5)[THEN bexpands_witD(1)] x_y(9)[THEN bexpands_witD(1)] x_y(1,6,10)
by auto
moreover from x_y have "suffix (xb2 @ xb1) (yb2 @ yb1) ∨ suffix (yb2 @ yb1) (xb2 @ xb1)"
using expandss_suffix suffix_same_cases by blast
then have "suffix (xb2 @ xb1) yb1 ∨ suffix (yb2 @ yb1) xb1"
using x_y(5)[THEN bexpands_witD(1)] x_y(9)[THEN bexpands_witD(1)] x_y(1,6,10)
by (auto simp: suffix_Cons)
ultimately show False
using bexpands_witD(1,5,6)[OF x_y(5)] bexpands_witD(1,5,6)[OF x_y(9)] x_y(6,10)
by (auto dest!: set_mono_suffix)
qed
then show ?thesis
using linorder_not_le ‹last b = φ› by blast
qed
lemma card_subterms_branch_ub_if_wf_branch:
assumes "wf_branch b"
shows "card (subterms b) ≤ card (subterms (last b)) + card (wits b)"
unfolding subterms_branch_eq_if_wf_branch[OF assms, unfolded wits_subterms_def]
by (simp add: assms card_Un_disjoint card_image_le finite_wits finite_subterms_fm
wits_subterms_last_disjnt)
lemma card_literals_branch_if_wf_branch:
assumes "wf_branch b"
shows "card {a ∈ set b. is_literal a}
≤ 2 * (2 * (card (subterms (last b)) + card (wits b))⇧2)"
proof -
have "card {a ∈ set b. is_literal a}
≤ card (pset_atoms_branch b) + card (pset_atoms_branch b)" (is "card ?A ≤ _")
proof -
have "?A = {AT a |a. AT a ∈ set b}
∪ {AF a |a. AF a ∈ set b}" (is "_ = ?ATs ∪ ?AFs")
by auto (metis is_literal.elims(2))
moreover have
"?ATs ⊆ AT ` pset_atoms_branch b" "?AFs ⊆ AF ` pset_atoms_branch b"
by force+
moreover from calculation have "finite ?ATs" "finite ?AFs"
by (simp_all add: finite_surj[OF finite_pset_atoms_branch])
moreover have "?ATs ∩ ?AFs = {}"
by auto
ultimately show ?thesis
by (simp add: add_mono card_Un_disjoint finite_pset_atoms_branch surj_card_le)
qed
then have "card ?A ≤ 2 * card (pset_atoms_branch b)"
by simp
moreover
have "atoms φ ⊆
case_prod Elem ` (subterms φ × subterms φ)
∪ case_prod Equal ` (subterms φ × subterms φ)" for φ :: "'a pset_fm"
proof(induction φ)
case (Atom x)
then show ?case by (cases x) auto
qed auto
then have "pset_atoms_branch b ⊆
case_prod Elem ` (subterms b × subterms b)
∪ case_prod Equal ` (subterms b × subterms b)" (is "_ ⊆ ?Els ∪ ?Eqs")
unfolding subterms_branch_def
by force
have "card (pset_atoms_branch b)
≤ (card (subterms b))⇧2 + (card (subterms b))⇧2"
proof -
from finite_subterms_branch have "finite (subterms b × subterms b)"
using finite_cartesian_product by auto
then have "finite ?Els" "finite ?Eqs"
by blast+
moreover have "inj_on (case_prod Elem) A" "inj_on (case_prod Equal) A"
for A :: "('a pset_term × 'a pset_term) set"
unfolding inj_on_def by auto
ultimately have "card ?Els = (card (subterms b))⇧2" "card ?Eqs = (card (subterms b))⇧2"
using card_image[where ?A="subterms b × subterms b"] card_cartesian_product
unfolding power2_eq_square by metis+
with card_mono[OF _ ‹pset_atoms_branch b ⊆ ?Els ∪ ?Eqs›] show ?thesis
using ‹finite ?Els› ‹finite ?Eqs›
by (metis card_Un_le finite_UnI sup.boundedE sup_absorb2)
qed
then have "card (pset_atoms_branch b) ≤ 2 * (card (subterms b))⇧2"
by simp
ultimately show ?thesis
using card_subterms_branch_ub_if_wf_branch[OF assms]
by (meson dual_order.trans mult_le_mono2 power2_nat_le_eq_le)
qed
lemma lexpands_not_literal_mem_subfms_last:
defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
assumes "lexpands b' b" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-)
by (induction b' b rule: lexpands_induct) (fastforce simp: P_def dest: subfmsD)+
lemma bexpands_not_literal_mem_subfms_last:
defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
assumes "bexpands bs b" "b' ∈ bs" "b ≠ []"
assumes "P b"
shows "P (b' @ b)"
using assms(2-)
proof(induction bs b rule: bexpands.induct)
case (1 bs' b)
then show ?case
apply(induction rule: bexpands_nowit.induct)
apply(fastforce simp: P_def dest: subfmsD)+
done
next
case (2 t1 t2 x bs' b)
then show ?case
apply(induction rule: bexpands_wit.induct)
apply(fastforce simp: P_def dest: subfmsD)+
done
qed
lemma expandss_not_literal_mem_subfms_last:
defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
assumes "expandss b' b" "b ≠ []"
assumes "P b"
shows "P b'"
using assms(2-)
proof(induction b' b rule: expandss.induct)
case (2 b3 b2 b1)
then have "b2 ≠ []"
using expandss_suffix suffix_bot.extremum_uniqueI by blast
with 2 show ?case
using lexpands_not_literal_mem_subfms_last unfolding P_def by blast
next
case (3 bs b2 b3 b1)
then have "b2 ≠ []"
using expandss_suffix suffix_bot.extremum_uniqueI by blast
with 3 show ?case
using bexpands_not_literal_mem_subfms_last unfolding P_def by blast
qed simp
lemma card_not_literal_branch_if_wf_branch:
assumes "wf_branch b"
shows "card {φ ∈ set b. ¬ is_literal φ} ≤ 2 * card (subfms (last b))"
proof -
from assms obtain φ where "expandss b [φ]"
unfolding wf_branch_def by blast
then have [simp]: "last b = φ"
by simp
have "{ψ ∈ set b. ¬ is_literal ψ} ⊆ subfms φ ∪ Neg ` subfms φ"
using expandss_not_literal_mem_subfms_last[OF ‹expandss b [φ]›]
by auto
from card_mono[OF _ this] have
"card {ψ ∈ set b. ¬ is_literal ψ} ≤ card (subfms φ ∪ Neg ` subfms φ)"
using finite_subfms finite_imageI by fast
also have "… ≤ card (subfms φ) + card (Neg ` subfms φ)"
using card_Un_le by blast
also have "… ≤ 2 * card (subfms φ)"
unfolding mult_2 by (simp add: card_image_le finite_subfms)
finally show ?thesis
by simp
qed
lemma card_wf_branch_ub:
assumes "wf_branch b"
shows "card (set b)
≤ 2 * card (subfms (last b)) + 16 * (card (subterms (last b)))^4"
proof -
let ?csts = "card (subterms (last b))"
have "set b = {ψ ∈ set b. ¬ is_literal ψ} ∪ {ψ ∈ set b. is_literal ψ}"
by auto
then have "card (set b)
= card ({ψ ∈ set b. ¬ is_literal ψ}) + card ({ψ ∈ set b. is_literal ψ})"
using card_Un_disjoint finite_Un
by (metis (no_types, lifting) List.finite_set disjoint_iff mem_Collect_eq)
also have "… ≤ 2 * card (subfms (last b)) + 4 * (?csts + card (wits b))⇧2"
using assms card_literals_branch_if_wf_branch card_not_literal_branch_if_wf_branch
by fastforce
also have "… ≤ 2 * card (subfms (last b)) + 4 * (?csts + ?csts⇧2)⇧2"
using assms card_wits_ub_if_wf_branch by auto
also have "… ≤ 2 * card (subfms (last b)) + 16 * ?csts^4"
proof -
have "1 ≤ ?csts"
using finite_subterms_fm[THEN card_0_eq]
by (auto intro: Suc_leI)
then have "(?csts + ?csts⇧2)⇧2 = ?csts⇧2 + 2 * ?csts^3 + ?csts^4"
by algebra
also have "… ≤ ?csts⇧2 + 2 * ?csts^4 + ?csts^4"
using power_increasing[OF _ ‹1 ≤ ?csts›] by simp
also have "… ≤ ?csts^4 + 2 * ?csts^4 + ?csts^4"
using power_increasing[OF _ ‹1 ≤ ?csts›] by simp
also have "… ≤ 4 * ?csts^4"
by simp
finally show ?thesis
by simp
qed
finally show ?thesis .
qed
subsection ‹The Decision Procedure›
locale mlss_proc =
fixes lexpand :: "'a branch ⇒ 'a branch"
assumes lexpands_lexpand:
"¬ lin_sat b ⟹ lexpands (lexpand b) b ∧ set b ⊂ set (lexpand b @ b)"
fixes bexpand :: "'a branch ⇒ 'a branch set"
assumes bexpands_bexpand:
"¬ sat b ⟹ lin_sat b ⟹ bexpands (bexpand b) b"
begin
function (domintros) mlss_proc_branch :: "'a branch ⇒ bool" where
"¬ lin_sat b
⟹ mlss_proc_branch b = mlss_proc_branch (lexpand b @ b)"
| "⟦ lin_sat b; bclosed b ⟧ ⟹ mlss_proc_branch b = True"
| "⟦ ¬ sat b; bopen b; lin_sat b ⟧
⟹ mlss_proc_branch b = (∀b' ∈ bexpand b. mlss_proc_branch (b' @ b))"
| "⟦ lin_sat b; sat b ⟧ ⟹ mlss_proc_branch b = bclosed b"
by auto
lemma mlss_proc_branch_dom_if_wf_branch:
assumes "wf_branch b"
shows "mlss_proc_branch_dom b"
proof -
define card_ub :: "'a branch ⇒ nat" where
"card_ub ≡ λb. 2 * card (subfms (last b)) + 16 * (card (subterms (last b)))^4"
from assms show ?thesis
proof(induction "card_ub b - card (set b)"
arbitrary: b rule: less_induct)
case less
have less': "mlss_proc_branch_dom b'" if "set b ⊂ set b'" "expandss b' b" for b'
proof -
note expandss_last_eq[OF ‹expandss b' b› wf_branch_not_Nil[OF ‹wf_branch b›]]
then have "card_ub b' = card_ub b"
unfolding card_ub_def by simp
moreover from that ‹wf_branch b› have "wf_branch b'"
by (meson expandss_trans wf_branch_def)
ultimately have "mlss_proc_branch_dom b'" if "card (set b') > card (set b)"
using less(1)[OF _ ‹wf_branch b'›] card_wf_branch_ub that
by (metis (no_types, lifting) card_ub_def diff_less_mono2 order_less_le_trans)
with that show ?thesis
by (simp add: psubset_card_mono)
qed
then show ?case
proof(cases "sat b")
case False
then consider
b' where "¬ lin_sat b" "lexpands b' b" "set b ⊂ set (b' @ b)" |
bs' where "lin_sat b" "¬ sat b" "bexpands bs' b" "bs' ≠ {}"
"∀b' ∈ bs'. set b ⊂ set (b' @ b)"
unfolding sat_def lin_sat_def
using bexpands_strict_mono bexpands_nonempty
by (metis (no_types, opaque_lifting) inf_sup_aci(5) psubsetI set_append sup_ge1)
then show ?thesis
proof(cases)
case 1
with less' show ?thesis
using mlss_proc_branch.domintros(1)
by (metis expandss.intros(1,2) lexpands_lexpand)
next
case 2
then show ?thesis
using less' bexpands_bexpand mlss_proc_branch.domintros(2,3)
by (metis bexpands_strict_mono expandss.intros(1,3))
qed
qed (use mlss_proc_branch.domintros(4) sat_def in metis)
qed
qed
definition mlss_proc :: "'a pset_fm ⇒ bool" where
"mlss_proc φ ≡ mlss_proc_branch [φ]"
lemma mlss_proc_branch_complete:
fixes b :: "'a branch"
assumes "wf_branch b" "∃v. v ⊢ last b"
assumes "¬ mlss_proc_branch b"
assumes "infinite (UNIV :: 'a set)"
shows "∃M. interp I⇩s⇩a M (last b)"
proof -
from mlss_proc_branch_dom_if_wf_branch[OF assms(1)] assms(1,2,3)
show ?thesis
proof(induction rule: mlss_proc_branch.pinduct)
case (1 b)
let ?b' = "lexpand b"
from 1 lexpands_lexpand have "wf_branch (?b' @ b)"
using wf_branch_lexpands by blast
moreover from 1 lexpands_lexpand have "¬ mlss_proc_branch (?b' @ b)"
by (simp add: mlss_proc_branch.psimps)
ultimately obtain M where "interp I⇩s⇩a M (last (?b' @ b))"
using 1 by auto
with 1 show ?case
using wf_branch_not_Nil by auto
next
case (2 b)
then show ?case by (simp add: mlss_proc_branch.psimps)
next
case (3 b)
let ?bs' = "bexpand b"
from 3 bexpands_bexpand obtain b' where b': "b' ∈ ?bs'" "¬ mlss_proc_branch (b' @ b)"
using mlss_proc_branch.psimps(3) by metis
with 3 bexpands_bexpand have "wf_branch (b' @ b)"
using wf_branch_expandss[OF ‹wf_branch b› expandss.intros(3)]
using expandss.intros(1) by blast
with 3 b' obtain M where "interp I⇩s⇩a M (last (b' @ b))"
by auto
with 3 show ?case
by auto
next
case (4 b)
then have "bopen b"
by (simp add: mlss_proc_branch.psimps)
interpret open_branch b
using ‹wf_branch b› ‹∃v. v ⊢ last b› ‹bopen b› ‹infinite UNIV›
by unfold_locales assumption+
from coherence[OF ‹sat b› last_in_set] show ?case
using wf_branch wf_branch_not_Nil by blast
qed
qed
lemma mlss_proc_branch_sound:
assumes "wf_branch b"
assumes "∀ψ ∈ set b. interp I⇩s⇩a M ψ"
shows "¬ mlss_proc_branch b"
proof
assume "mlss_proc_branch b"
with mlss_proc_branch_dom_if_wf_branch[OF ‹wf_branch b›]
have "∃b'. expandss b' b ∧ (∃M. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ) ∧ bclosed b'"
using assms
proof(induction arbitrary: M rule: mlss_proc_branch.pinduct)
case (1 b)
let ?b' = "lexpand b"
from 1 lexpands_lexpand ‹wf_branch b› have "wf_branch (?b' @ b)"
using wf_branch_lexpands by metis
with 1 lexpands_sound lexpands_lexpand obtain b'' where
"expandss b'' (?b' @ b)" "∃M. ∀ψ ∈ set b''. interp I⇩s⇩a M ψ" "bclosed b''"
by (fastforce simp: mlss_proc_branch.psimps)
with 1 lexpands_lexpand show ?case
using expandss_trans expandss.intros(1,2) by meson
next
case (3 b)
let ?bs' = "bexpand b"
from 3 ‹wf_branch b› bexpands_bexpand have wf_branch_b':
"wf_branch (b' @ b)" if "b' ∈ ?bs'" for b'
using that expandss.intros(3) wf_branch_def by metis
from bexpands_sound bexpands_bexpand 3 obtain M' b' where
"b' ∈ ?bs'" "∀ψ ∈ set (b' @ b). interp I⇩s⇩a M' ψ"
by metis
with "3.IH" ‹mlss_proc_branch b› wf_branch_b' obtain b'' where
"b' ∈ ?bs'" "expandss b'' (b' @ b)"
"∃M. ∀ψ ∈ set b''. interp I⇩s⇩a M ψ" "bclosed b''"
using mlss_proc_branch.psimps(3)[OF "3.hyps"(2-4,1)] by blast
with 3 bexpands_bexpand show ?case
using expandss_trans expandss.intros(1,3) by metis
qed (use expandss.intros(1) mlss_proc_branch.psimps(4) in ‹blast+›)
with bclosed_sound show False by blast
qed
theorem mlss_proc_complete:
fixes φ :: "'a pset_fm"
assumes "¬ mlss_proc φ"
assumes "∃v. v ⊢ φ"
assumes "infinite (UNIV :: 'a set)"
shows "∃M. interp I⇩s⇩a M φ"
using assms mlss_proc_branch_complete[of "[φ]"]
unfolding mlss_proc_def by simp
theorem mlss_proc_sound:
assumes "interp I⇩s⇩a M φ"
shows "¬ mlss_proc φ"
using assms mlss_proc_branch_sound[of "[φ]"]
unfolding mlss_proc_def by simp
end
end