Theory Probability_Inequality_Completeness
chapter ‹ Introduction ›
theory Probability_Inequality_Completeness
imports
"Suppes_Theorem.Probability_Logic"
begin
unbundle no funcset_syntax
text ‹ We introduce a novel logical calculus and prove completeness for
probability inequalities. This is a vast generalization of ∗‹Suppes' Theorem›
which lays the foundation for this theory.›
text ‹ We provide two new logical judgements: ∗‹measure deduction› ‹($⊢)› and
∗‹counting deduction› ‹(#⊢)›. Both judgements capture a notion of ∗‹measure›
or quantity. In both cases premises must be partially or completely ∗‹consumed›
in sense to prove multiple conclusions. That is to say, a portion of the
premises must be used to prove each conclusion which cannot be reused. Counting
deduction counts the number of times a particular conclusion can be proved
(as the name implies), while measure deduction includes multiple, different
conclusions which must be proven via the premises. ›
text ‹ We also introduce an abstract notion of MaxSAT, which is the
maximal number of clauses in a list of clauses that can be simultaneously
satisfied. ›
text ‹ We show the following are equivalent:
▪ ‹❙∼ Γ $⊢ ❙∼ Φ›
▪ ‹(❙∼ Γ @ Φ) #⊢ (length Φ) ⊥›
▪ ‹MaxSAT (❙∼ Γ @ Φ) ≤ length Γ›
▪ ‹∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) ≤ (∑γ←Γ. δ γ)›
▪ ‹∀ 𝒫 ∈ probabilities. (∑φ←Φ. 𝒫 φ) ≤ (∑γ←Γ. 𝒫 γ)›
›
text ‹ In the special case of MaxSAT, we show the following are
equivalent:
▪ ‹MaxSAT (❙∼ Γ @ Φ) + c ≤ length Γ›
▪ ‹∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) + c ≤ (∑γ←Γ. δ γ)›
▪ ‹∀ 𝒫 ∈ probabilities. (∑φ←Φ. 𝒫 φ) + c ≤ (∑γ←Γ. 𝒫 γ)›
›
chapter ‹ Measure Deduction and Counting Deduction ›
section ‹ Definition of Measure Deduction ›
text ‹ To start, we introduce a common combinator for modifying functions
that take two arguments. ›
definition uncurry :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'b ⇒ 'c"
where uncurry_def [simp]: "uncurry f = (λ (x, y). f x y)"
text ‹ Our new logical calculus is a recursively defined relation ‹($⊢)›
using ∗‹list deduction› \<^term>‹(:⊢)›. ›
text ‹ We call our new logical relation ∗‹measure deduction›: ›
primrec (in classical_logic)
measure_deduction :: "'a list ⇒ 'a list ⇒ bool" (infix ‹$⊢› 60)
where
"Γ $⊢ [] = True"
| "Γ $⊢ (φ # Φ) =
(∃ Ψ. mset (map snd Ψ) ⊆# mset Γ
∧ map (uncurry (⊔)) Ψ :⊢ φ
∧ map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ) $⊢ Φ)"
text ‹ Let us briefly analyze what the above definition is saying. ›
text ‹ From the above we must find a special list-of-pairs ‹Ψ›,
which we refer to as a ∗‹witness›, in order to establish
\<^term>‹Γ $⊢ (φ # Φ)›. ›
text ‹ We may motivate measure deduction as follows. In the simplest case
we know ‹𝒫 φ ≤ 𝒫 ψ + Σ› if and only if
‹𝒫 ( χ ⊔ φ ) + 𝒫 ( ∼ χ ⊔ φ ) ≤ 𝒫 ψ + Σ›, or equivalently
‹𝒫 ( χ ⊔ φ ) + 𝒫 ( χ → φ ) ≤ 𝒫 ψ + Σ›. So it suffices to prove
‹𝒫 ( χ ⊔ φ ) ≤ 𝒫 ψ› and ‹𝒫 ( χ → φ ) ≤ Σ ›. Here ‹[(χ,φ)]›
is like the ∗‹witness› in our recursive definition, which reflects the
‹∃ Ψ. …› formula is our definition. The fact that measure deduction
reflects proving theorems in the theory of inequalities of probability
logic is the elementary intuition behind the soundness theorem we will
ultimately prove in \S\ref{subsubsec:measure-deduction-soundness}. ›
text ‹ A key difference from the simple motivation above is that, as in the
case of Suppes' Theorem where we prove ‹ ❙∼ Γ :⊢ ∼ φ › if and only if
‹𝒫 φ ≤ (∑ γ ← Γ . 𝒫 γ)› for all ‹𝒫›, soundness in this context means
‹ ❙∼ Γ $⊢ ❙∼ Φ › implies ‹∀ 𝒫. (∑γ←Γ. 𝒫 γ) ≥ (∑φ←Φ. 𝒫 φ) ›. ›
text ‹ Another way of thinking about measure deduction is to think of ‹Γ›
and ‹Σ› as bags of balls of soft clay and \<^term>‹Γ $⊢ Σ› meaning that
we have shown ‹Γ› is ∗‹heavier than› ‹Σ› (ignoring, for the moment,
that \<^term>‹($⊢)› is not totally ordered). We have a scale \<^term>‹(:⊢)›
that lets us weigh several things on the left and one thing on the
right at a time. We go through each clay ball ‹σ› in ‹Σ› one at a
time without replacement, putting ‹σ› on the right of the scale. Then,
we take a bunch of clay balls from ‹Γ›, cut them up as necessary (that
is the ‹ψ ⊔ γ› trick using the witness ‹Ψ›), and show they are heavier
using our scale. We take the parts ‹ψ → γ› that we didn't use and put
them back in our bag ‹Γ›. We will be able to reuse them later. If we
can do this trick for every element ‹σ› in ‹Σ› successively using
combinations of split leftovers in ‹Γ›, then we can show ‹Γ› is
heavier than ‹Σ› (i.e., \<^term>‹Γ $⊢ Σ›). ›
section ‹ Definition of the Stronger Theory Relation ›
text ‹ We next turn to looking at a subrelation of \<^term>‹($⊢)›, which
we call the ∗‹stronger theory› relation ‹(≼)›. Here we construe a
∗‹theory› as a list of propositions. We say theory ‹Γ› is
∗‹stronger than› ‹Σ› where, for each element ‹σ› in ‹Σ›, we can take
an element ‹γ› of ‹Γ› ∗‹without replacement› such that ‹⊢ γ → σ›. ›
text ‹ To motivate this notion, let's reuse the metaphor that ‹Γ› and ‹Σ›
are bags of balls of clay, and we need to show ‹Γ› is heavier without
simply weighing the two bags. A sufficient (but incomplete) approach
is to take each ball of clay ‹σ› in ‹Σ› and find another ball of clay
‹γ› in ‹Γ› (without replacement) that is heavier. This simple approach
avoids the complexity of iteratively cutting up balls of clay. ›
definition (in implication_logic)
stronger_theory_relation :: "'a list ⇒ 'a list ⇒ bool" (infix ‹≼› 100)
where
"Σ ≼ Γ =
(∃ Φ. map snd Φ = Σ
∧ mset (map fst Φ) ⊆# mset Γ
∧ (∀ (γ,σ) ∈ set Φ. ⊢ γ → σ))"
abbreviation (in implication_logic)
stronger_theory_relation_op :: "'a list ⇒ 'a list ⇒ bool" (infix ‹≽› 100)
where
"Γ ≽ Σ ≡ Σ ≼ Γ"
section ‹ The Stronger Theory Relation is a Preorder ›
text ‹ Next, we show that \<^term>‹(≼)› is a preorder by establishing reflexivity
and transitivity. ›
text ‹ We first prove the following lemma with respect to multisets and
stronger theories. ›
lemma (in implication_logic) msub_stronger_theory_intro:
assumes "mset Σ ⊆# mset Γ"
shows "Σ ≼ Γ"
proof -
let ?ΔΣ = "map (λ x. (x,x)) Σ"
have "map snd ?ΔΣ = Σ"
by (induct Σ, simp, simp)
moreover have "map fst ?ΔΣ = Σ"
by (induct Σ, simp, simp)
hence "mset (map fst ?ΔΣ) ⊆# mset Γ"
using assms by simp
moreover have "∀ (γ,σ) ∈ set ?ΔΣ. ⊢ γ → σ"
by (induct Σ, simp, simp,
metis list_implication.simps(1) list_implication_axiom_k)
ultimately show ?thesis using stronger_theory_relation_def by (simp, blast)
qed
text ‹ The ∗‹reflexive› property immediately follows: ›
lemma (in implication_logic) stronger_theory_reflexive [simp]: "Γ ≼ Γ"
using msub_stronger_theory_intro by auto
lemma (in implication_logic) weakest_theory [simp]: "[] ≼ Γ"
using msub_stronger_theory_intro by auto
lemma (in implication_logic) stronger_theory_empty_list_intro [simp]:
assumes "Γ ≼ []"
shows "Γ = []"
using assms stronger_theory_relation_def by simp
text ‹ Next, we turn to proving transitivity. We first prove two permutation
theorems. ›
lemma (in implication_logic) stronger_theory_right_permutation:
assumes "Γ ⇌ Δ"
and "Σ ≼ Γ"
shows "Σ ≼ Δ"
proof -
from assms(1) have "mset Γ = mset Δ"
by simp
thus ?thesis
using assms(2) stronger_theory_relation_def
by fastforce
qed
lemma (in implication_logic) stronger_theory_left_permutation:
assumes "Σ ⇌ Δ"
and "Σ ≼ Γ"
shows "Δ ≼ Γ"
proof -
have "∀ Σ Γ. Σ ⇌ Δ ⟶ Σ ≼ Γ ⟶ Δ ≼ Γ"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Σ Γ
assume "Σ ⇌ (δ # Δ)" "Σ ≼ Γ"
from this obtain Φ where Φ:
"map snd Φ = Σ"
"mset (map fst Φ) ⊆# mset Γ"
"∀ (γ,δ) ∈ set Φ. ⊢ γ → δ"
using stronger_theory_relation_def by fastforce
with ‹Σ ⇌ (δ # Δ)› have "δ ∈# mset (map snd Φ)"
by fastforce
from this obtain γ where γ: "(γ, δ) ∈# mset Φ"
by (induct Φ, fastforce+)
let ?Φ⇩0 = "remove1 (γ, δ) Φ"
let ?Σ⇩0 = "map snd ?Φ⇩0"
from γ Φ(2) have "mset (map fst ?Φ⇩0) ⊆# mset (remove1 γ Γ)"
by (metis ex_mset
list_subtract_monotonic
list_subtract_mset_homomorphism
mset_remove1
remove1_pairs_list_projections_fst)
moreover have "mset ?Φ⇩0 ⊆# mset Φ" by simp
with Φ(3) have "∀ (γ,δ) ∈ set ?Φ⇩0. ⊢ γ → δ" by fastforce
ultimately have "?Σ⇩0 ≼ remove1 γ Γ"
unfolding stronger_theory_relation_def by blast
moreover have "Δ ⇌ (remove1 δ Σ)" using ‹Σ ⇌ (δ # Δ)›
by (metis perm_remove_perm perm_sym remove_hd)
moreover from γ Φ(1) have "mset ?Σ⇩0 = mset (remove1 δ Σ)"
using remove1_pairs_list_projections_snd
by fastforce
hence "?Σ⇩0 ⇌ remove1 δ Σ"
by blast
ultimately have "Δ ≼ remove1 γ Γ" using Cons
by presburger
from this obtain Ψ⇩0 where Ψ⇩0:
"map snd Ψ⇩0 = Δ"
"mset (map fst Ψ⇩0) ⊆# mset (remove1 γ Γ)"
"∀ (γ,δ) ∈ set Ψ⇩0. ⊢ γ → δ"
using stronger_theory_relation_def by fastforce
let ?Ψ = "(γ, δ) # Ψ⇩0"
have "map snd ?Ψ = (δ # Δ)"
by (simp add: Ψ⇩0(1))
moreover have "mset (map fst ?Ψ) ⊆# mset (γ # (remove1 γ Γ))"
using Ψ⇩0(2) by auto
moreover from γ Φ(3) Ψ⇩0(3) have "∀ (γ,σ) ∈ set ?Ψ. ⊢ γ → σ" by auto
ultimately have "(δ # Δ) ≼ (γ # (remove1 γ Γ))"
unfolding stronger_theory_relation_def by metis
moreover from γ Φ(2) have "γ ∈# mset Γ"
using mset_subset_eqD by fastforce
hence "(γ # (remove1 γ Γ)) ⇌ Γ"
by auto
ultimately have "(δ # Δ) ≼ Γ"
using stronger_theory_right_permutation by blast
}
then show ?case by blast
qed
with assms show ?thesis by blast
qed
lemma (in implication_logic) stronger_theory_transitive:
assumes "Σ ≼ Δ" and "Δ ≼ Γ"
shows "Σ ≼ Γ"
proof -
have "∀ Δ Γ. Σ ≼ Δ ⟶ Δ ≼ Γ ⟶ Σ ≼ Γ"
proof (induct Σ)
case Nil
then show ?case using stronger_theory_relation_def by simp
next
case (Cons σ Σ)
{
fix Δ Γ
assume "(σ # Σ) ≼ Δ" "Δ ≼ Γ"
from this obtain Φ where Φ:
"map snd Φ = σ # Σ"
"mset (map fst Φ) ⊆# mset Δ"
"∀ (δ,σ) ∈ set Φ. ⊢ δ → σ"
using stronger_theory_relation_def by (simp, metis)
let ?δ = "fst (hd Φ)"
from Φ(1) have "Φ ≠ []" by (induct Φ, simp+)
hence "?δ ∈# mset (map fst Φ)" by (induct Φ, simp+)
with Φ(2) have "?δ ∈# mset Δ" by (meson mset_subset_eqD)
hence "mset (map fst (remove1 (hd Φ) Φ)) ⊆# mset (remove1 ?δ Δ)"
using ‹Φ ≠ []› Φ(2)
by (simp,
metis
diff_single_eq_union
hd_in_set
image_mset_add_mset
insert_subset_eq_iff
set_mset_mset)
moreover have "remove1 (hd Φ) Φ = tl Φ"
using ‹Φ ≠ []›
by (induct Φ, simp+)
moreover from Φ(1) have "map snd (tl Φ) = Σ"
by (simp add: map_tl)
moreover from Φ(3) have "∀ (δ,σ) ∈ set (tl Φ). ⊢ δ → σ"
by (simp add: ‹Φ ≠ []› list.set_sel(2))
ultimately have "Σ ≼ remove1 ?δ Δ"
using stronger_theory_relation_def by auto
from ‹?δ ∈# mset Δ› have "?δ # (remove1 ?δ Δ) ⇌ Δ"
by fastforce
with ‹Δ ≼ Γ› have "(?δ # (remove1 ?δ Δ)) ≼ Γ"
using stronger_theory_left_permutation perm_sym by blast
from this obtain Ψ where Ψ:
"map snd Ψ = (?δ # (remove1 ?δ Δ))"
"mset (map fst Ψ) ⊆# mset Γ"
"∀ (γ,δ) ∈ set Ψ. ⊢ γ → δ"
using stronger_theory_relation_def by (simp, metis)
let ?γ = "fst (hd Ψ)"
from Ψ(1) have "Ψ ≠ []" by (induct Ψ, simp+)
hence "?γ ∈# mset (map fst Ψ)" by (induct Ψ, simp+)
with Ψ(2) have "?γ ∈# mset Γ" by (meson mset_subset_eqD)
hence "mset (map fst (remove1 (hd Ψ) Ψ)) ⊆# mset (remove1 ?γ Γ)"
using ‹Ψ ≠ []› Ψ(2)
by (simp,
metis
diff_single_eq_union
hd_in_set
image_mset_add_mset
insert_subset_eq_iff
set_mset_mset)
moreover from ‹Ψ ≠ []› have "remove1 (hd Ψ) Ψ = tl Ψ"
by (induct Ψ, simp+)
moreover from Ψ(1) have "map snd (tl Ψ) = (remove1 ?δ Δ)"
by (simp add: map_tl)
moreover from Ψ(3) have "∀ (γ,δ) ∈ set (tl Ψ). ⊢ γ → δ"
by (simp add: ‹Ψ ≠ []› list.set_sel(2))
ultimately have "remove1 ?δ Δ ≼ remove1 ?γ Γ"
using stronger_theory_relation_def by auto
with ‹Σ ≼ remove1 ?δ Δ› Cons.hyps have "Σ ≼ remove1 ?γ Γ"
by blast
from this obtain Ω⇩0 where Ω⇩0:
"map snd Ω⇩0 = Σ"
"mset (map fst Ω⇩0) ⊆# mset (remove1 ?γ Γ)"
"∀ (γ,σ) ∈ set Ω⇩0. ⊢ γ → σ"
using stronger_theory_relation_def by (simp, metis)
let ?Ω = "(?γ, σ) # Ω⇩0"
from Ω⇩0(1) have "map snd ?Ω = σ # Σ" by simp
moreover from Ω⇩0(2) have "mset (map fst ?Ω) ⊆# mset (?γ # (remove1 ?γ Γ))"
by simp
moreover from Φ(1) Ψ(1) have "σ = snd (hd Φ)" "?δ = snd (hd Ψ)" by fastforce+
with Φ(3) Ψ(3) ‹Φ ≠ []› ‹Ψ ≠ []› hd_in_set have "⊢ ?δ → σ" "⊢ ?γ → ?δ"
by fastforce+
hence "⊢ ?γ → σ" using modus_ponens hypothetical_syllogism by blast
with Ω⇩0(3) have "∀ (γ,σ) ∈ set ?Ω. ⊢ γ → σ"
by auto
ultimately have "(σ # Σ) ≼ (?γ # (remove1 ?γ Γ))"
unfolding stronger_theory_relation_def
by metis
moreover from ‹?γ ∈# mset Γ› have "(?γ # (remove1 ?γ Γ)) ⇌ Γ"
by force
ultimately have "(σ # Σ) ≼ Γ"
using stronger_theory_right_permutation
by blast
}
then show ?case by blast
qed
thus ?thesis using assms by blast
qed
section ‹ The Stronger Theory Relation is a Subrelation of of Measure Deduction ›
text ‹ Next, we show that ‹ Γ ≽ Σ › implies ‹Γ $⊢ Σ›. Before doing so we
establish several helpful properties regarding the stronger theory
relation \<^term>‹(≽)›. ›
lemma (in implication_logic) stronger_theory_witness:
assumes "σ ∈ set Σ"
shows "Σ ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ))"
proof (rule iffI)
assume "Σ ≼ Γ"
from this obtain Φ where Φ:
"map snd Φ = Σ"
"mset (map fst Φ) ⊆# mset Γ"
"∀ (γ,σ) ∈ set Φ. ⊢ γ → σ"
unfolding stronger_theory_relation_def by blast
from assms Φ(1) obtain γ where γ: "(γ, σ) ∈# mset Φ"
by (induct Φ, fastforce+)
hence "γ ∈# mset (map fst Φ)" by force
hence "γ ∈# mset Γ" using Φ(2)
by (meson mset_subset_eqD)
moreover
let ?Φ⇩0 = "remove1 (γ, σ) Φ"
let ?Σ⇩0 = "map snd ?Φ⇩0"
from γ Φ(2) have "mset (map fst ?Φ⇩0) ⊆# mset (remove1 γ Γ)"
by (metis
ex_mset
list_subtract_monotonic
list_subtract_mset_homomorphism
remove1_pairs_list_projections_fst
mset_remove1)
moreover have "mset ?Φ⇩0 ⊆# mset Φ" by simp
with Φ(3) have "∀ (γ,σ) ∈ set ?Φ⇩0. ⊢ γ → σ" by fastforce
ultimately have "?Σ⇩0 ≼ remove1 γ Γ"
unfolding stronger_theory_relation_def by blast
moreover from γ Φ(1) have "mset ?Σ⇩0 = mset (remove1 σ Σ)"
using remove1_pairs_list_projections_snd
by fastforce
hence "?Σ⇩0 ⇌ remove1 σ Σ"
by linarith
ultimately have "remove1 σ Σ ≼ remove1 γ Γ"
using stronger_theory_left_permutation
by blast
moreover from γ Φ(3) have "⊢ γ → σ" by (simp, fast)
moreover from γ Φ(2) have "γ ∈# mset Γ"
using mset_subset_eqD by fastforce
ultimately show "∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ)" by auto
next
assume "∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ)"
from this obtain Φ γ where γ: "γ ∈ set Γ" "⊢ γ → σ"
and Φ: "map snd Φ = (remove1 σ Σ)"
"mset (map fst Φ) ⊆# mset (remove1 γ Γ)"
"∀ (γ,σ) ∈ set Φ. ⊢ γ → σ"
unfolding stronger_theory_relation_def by blast
let ?Φ = "(γ, σ) # Φ"
from Φ(1) have "map snd ?Φ = σ # (remove1 σ Σ)" by simp
moreover from Φ(2) γ(1) have "mset (map fst ?Φ) ⊆# mset Γ"
by (simp add: insert_subset_eq_iff)
moreover from Φ(3) γ(2) have "∀ (γ,σ) ∈ set ?Φ. ⊢ γ → σ"
by auto
ultimately have "(σ # (remove1 σ Σ)) ≼ Γ"
unfolding stronger_theory_relation_def by metis
moreover from assms have "σ # (remove1 σ Σ) ⇌ Σ"
by force
ultimately show "Σ ≼ Γ"
using stronger_theory_left_permutation by blast
qed
lemma (in implication_logic) stronger_theory_cons_witness:
"(σ # Σ) ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ Σ ≼ (remove1 γ Γ))"
proof -
have "σ ∈# mset (σ # Σ)" by simp
hence "(σ # Σ) ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ (σ # Σ)) ≼ (remove1 γ Γ))"
by (meson list.set_intros(1) stronger_theory_witness)
thus ?thesis by simp
qed
lemma (in implication_logic) stronger_theory_left_cons:
assumes "(σ # Σ) ≼ Γ"
shows "Σ ≼ Γ"
proof -
from assms obtain Φ where Φ:
"map snd Φ = σ # Σ"
"mset (map fst Φ) ⊆# mset Γ"
"∀ (δ,σ) ∈ set Φ. ⊢ δ → σ"
using stronger_theory_relation_def by (simp, metis)
let ?Φ' = "remove1 (hd Φ) Φ"
from Φ(1) have "map snd ?Φ' = Σ" by (induct Φ, simp+)
moreover from Φ(2) have "mset (map fst ?Φ') ⊆# mset Γ"
by (metis diff_subset_eq_self
list_subtract.simps(1)
list_subtract.simps(2)
list_subtract_mset_homomorphism
map_monotonic
subset_mset.dual_order.trans)
moreover from Φ(3) have "∀ (δ,σ) ∈ set ?Φ'. ⊢ δ → σ" by fastforce
ultimately show ?thesis unfolding stronger_theory_relation_def by blast
qed
lemma (in implication_logic) stronger_theory_right_cons:
assumes "Σ ≼ Γ"
shows "Σ ≼ (γ # Γ)"
proof -
from assms obtain Φ where Φ:
"map snd Φ = Σ"
"mset (map fst Φ) ⊆# mset Γ"
"∀(γ, σ)∈set Φ. ⊢ γ → σ"
unfolding stronger_theory_relation_def
by auto
hence "mset (map fst Φ) ⊆# mset (γ # Γ)"
by (metis Diff_eq_empty_iff_mset
list_subtract.simps(2)
list_subtract_mset_homomorphism
mset_zero_iff remove1.simps(1))
with Φ(1) Φ(3) show ?thesis
unfolding stronger_theory_relation_def
by auto
qed
lemma (in implication_logic) stronger_theory_left_right_cons:
assumes "⊢ γ → σ"
and "Σ ≼ Γ"
shows "(σ # Σ) ≼ (γ # Γ)"
proof -
from assms(2) obtain Φ where Φ:
"map snd Φ = Σ"
"mset (map fst Φ) ⊆# mset Γ"
"∀(γ, σ)∈set Φ. ⊢ γ → σ"
unfolding stronger_theory_relation_def
by auto
let ?Φ = "(γ, σ) # Φ"
from assms(1) Φ have
"map snd ?Φ = σ # Σ"
"mset (map fst ?Φ) ⊆# mset (γ # Γ)"
"∀(γ, σ)∈set ?Φ. ⊢ γ → σ"
by fastforce+
thus ?thesis
unfolding stronger_theory_relation_def
by metis
qed
lemma (in implication_logic) stronger_theory_relation_alt_def:
"Σ ≼ Γ = (∃Φ. mset (map snd Φ) = mset Σ ∧
mset (map fst Φ) ⊆# mset Γ ∧
(∀(γ, σ)∈set Φ. ⊢ γ → σ))"
proof (induct Γ arbitrary: Σ)
case Nil
then show ?case
using stronger_theory_empty_list_intro
stronger_theory_reflexive
by (simp, blast)
next
case (Cons γ Γ)
have "Σ ≼ (γ # Γ) = (∃Φ. mset (map snd Φ) = mset Σ ∧
mset (map fst Φ) ⊆# mset (γ # Γ) ∧
(∀(γ, σ) ∈ set Φ. ⊢ γ → σ))"
proof (rule iffI)
assume "Σ ≼ (γ # Γ)"
thus "∃Φ. mset (map snd Φ) = mset Σ ∧
mset (map fst Φ) ⊆# mset (γ # Γ) ∧
(∀(γ, σ)∈set Φ. ⊢ γ → σ)"
unfolding stronger_theory_relation_def
by metis
next
assume "∃Φ. mset (map snd Φ) = mset Σ ∧
mset (map fst Φ) ⊆# mset (γ # Γ) ∧
(∀(γ, σ)∈set Φ. ⊢ γ → σ)"
from this obtain Φ where Φ:
"mset (map snd Φ) = mset Σ"
"mset (map fst Φ) ⊆# mset (γ # Γ)"
"∀(γ, σ)∈set Φ. ⊢ γ → σ"
by metis
show "Σ ≼ (γ # Γ)"
proof (cases "∃ σ. (γ, σ) ∈ set Φ")
assume "∃ σ. (γ, σ) ∈ set Φ"
from this obtain σ where σ: "(γ, σ) ∈ set Φ" by auto
let ?Φ = "remove1 (γ, σ) Φ"
from σ have "mset (map snd ?Φ) = mset (remove1 σ Σ)"
using Φ(1) remove1_pairs_list_projections_snd by force+
moreover
from σ have "mset (map fst ?Φ) = mset (remove1 γ (map fst Φ))"
using Φ(1) remove1_pairs_list_projections_fst by force+
with Φ(2) have "mset (map fst ?Φ) ⊆# mset Γ"
by (simp add: subset_eq_diff_conv)
moreover from Φ(3) have "∀(γ, σ)∈set ?Φ. ⊢ γ → σ"
by fastforce
ultimately have "remove1 σ Σ ≼ Γ" using Cons by blast
from this obtain Ψ where Ψ:
"map snd Ψ = remove1 σ Σ"
"mset (map fst Ψ) ⊆# mset Γ"
"∀(γ, σ)∈set Ψ. ⊢ γ → σ"
unfolding stronger_theory_relation_def
by blast
let ?Ψ = "(γ, σ) # Ψ"
from Ψ have "map snd ?Ψ = σ # (remove1 σ Σ)"
"mset (map fst ?Ψ) ⊆# mset (γ # Γ)"
by simp+
moreover from Φ(3) σ have "⊢ γ → σ" by auto
with Ψ(3) have "∀(γ, σ)∈set ?Ψ. ⊢ γ → σ" by auto
ultimately have "(σ # (remove1 σ Σ)) ≼ (γ # Γ)"
unfolding stronger_theory_relation_def
by metis
moreover
have "σ ∈ set Σ"
by (metis Φ(1) σ set_mset_mset set_zip_rightD zip_map_fst_snd)
hence "Σ ⇌ σ # (remove1 σ Σ)"
by auto
hence "Σ ≼ (σ # (remove1 σ Σ))"
using stronger_theory_reflexive
stronger_theory_right_permutation
by blast
ultimately show ?thesis
using stronger_theory_transitive
by blast
next
assume "∄σ. (γ, σ) ∈ set Φ"
hence "γ ∉ set (map fst Φ)" by fastforce
with Φ(2) have "mset (map fst Φ) ⊆# mset Γ"
by (metis diff_single_trivial
in_multiset_in_set
insert_DiffM2
mset_remove1
remove_hd
subset_eq_diff_conv)
hence "Σ ≼ Γ"
using Cons Φ(1) Φ(3)
by blast
thus ?thesis
using stronger_theory_right_cons
by auto
qed
qed
thus ?case by auto
qed
lemma (in implication_logic) stronger_theory_deduction_monotonic:
assumes "Σ ≼ Γ"
and "Σ :⊢ φ"
shows "Γ :⊢ φ"
using assms
proof (induct Σ arbitrary: φ)
case Nil
then show ?case
by (simp add: list_deduction_weaken)
next
case (Cons σ Σ)
assume "(σ # Σ) ≼ Γ" "(σ # Σ) :⊢ φ"
hence "Σ :⊢ σ → φ" "Σ ≼ Γ"
using
list_deduction_theorem
stronger_theory_left_cons
by (blast, metis)
with Cons have "Γ :⊢ σ → φ" by blast
moreover
have "σ ∈ set (σ # Σ)" by auto
with ‹(σ # Σ) ≼ Γ› obtain γ where γ: "γ ∈ set Γ" "⊢ γ → σ"
using stronger_theory_witness by blast
hence "Γ :⊢ σ"
using
list_deduction_modus_ponens
list_deduction_reflection
list_deduction_weaken
by blast
ultimately have "Γ :⊢ φ"
using list_deduction_modus_ponens by blast
then show ?case by blast
qed
lemma (in classical_logic) measure_msub_left_monotonic:
assumes "mset Σ ⊆# mset Γ"
and "Σ $⊢ Φ"
shows "Γ $⊢ Φ"
using assms
proof (induct Φ arbitrary: Σ Γ)
case Nil
then show ?case by simp
next
case (Cons φ Φ)
from this obtain Ψ where Ψ:
"mset (map snd Ψ) ⊆# mset Σ"
"map (uncurry (⊔)) Ψ :⊢ φ"
"map (uncurry (→)) Ψ @ Σ ⊖ (map snd Ψ) $⊢ Φ"
using measure_deduction.simps(2) by blast
let ?Ψ = "map snd Ψ"
let ?Ψ' = "map (uncurry (→)) Ψ"
let ?Σ' = "?Ψ' @ (Σ ⊖ ?Ψ)"
let ?Γ' = "?Ψ' @ (Γ ⊖ ?Ψ)"
from Ψ have "mset ?Ψ ⊆# mset Γ"
using ‹mset Σ ⊆# mset Γ› subset_mset.trans by blast
moreover have "mset (Σ ⊖ ?Ψ) ⊆# mset (Γ ⊖ ?Ψ)"
by (metis ‹mset Σ ⊆# mset Γ› list_subtract_monotonic)
hence "mset ?Σ' ⊆# mset ?Γ'"
by simp
with Cons.hyps Ψ(3) have "?Γ' $⊢ Φ" by blast
ultimately have "Γ $⊢ (φ # Φ)"
using Ψ(2) by fastforce
then show ?case
by simp
qed
lemma (in classical_logic) witness_weaker_theory:
assumes "mset (map snd Σ) ⊆# mset Γ"
shows "map (uncurry (⊔)) Σ ≼ Γ"
proof -
have "∀ Γ. mset (map snd Σ) ⊆# mset Γ ⟶ map (uncurry (⊔)) Σ ≼ Γ"
proof (induct Σ)
case Nil
then show ?case by simp
next
case (Cons σ Σ)
{
fix Γ
assume "mset (map snd (σ # Σ)) ⊆# mset Γ"
hence "mset (map snd Σ) ⊆# mset (remove1 (snd σ) Γ)"
by (simp add: insert_subset_eq_iff)
with Cons have "map (uncurry (⊔)) Σ ≼ remove1 (snd σ) Γ" by blast
moreover have "uncurry (⊔) = (λ σ. fst σ ⊔ snd σ)" by fastforce
hence "uncurry (⊔) σ = fst σ ⊔ snd σ" by simp
moreover have "⊢ snd σ → (fst σ ⊔ snd σ)"
unfolding disjunction_def
by (simp add: axiom_k)
ultimately have "map (uncurry (⊔)) (σ # Σ) ≼ (snd σ # (remove1 (snd σ) Γ))"
by (simp add: stronger_theory_left_right_cons)
moreover have "mset (snd σ # (remove1 (snd σ) Γ)) = mset Γ"
using ‹mset (map snd (σ # Σ)) ⊆# mset Γ›
by (simp, meson insert_DiffM mset_subset_eq_insertD)
ultimately have "map (uncurry (⊔)) (σ # Σ) ≼ Γ"
unfolding stronger_theory_relation_alt_def
by simp
}
then show ?case by blast
qed
with assms show ?thesis by simp
qed
lemma (in implication_logic) stronger_theory_combine:
assumes "Φ ≼ Δ"
and "Ψ ≼ Γ"
shows "(Φ @ Ψ) ≼ (Δ @ Γ)"
proof -
have "∀ Φ. Φ ≼ Δ ⟶ (Φ @ Ψ) ≼ (Δ @ Γ)"
proof (induct Δ)
case Nil
then show ?case
using assms(2) stronger_theory_empty_list_intro by fastforce
next
case (Cons δ Δ)
{
fix Φ
assume "Φ ≼ (δ # Δ)"
from this obtain Σ where Σ:
"map snd Σ = Φ"
"mset (map fst Σ) ⊆# mset (δ # Δ)"
"∀ (δ,φ) ∈ set Σ. ⊢ δ → φ"
unfolding stronger_theory_relation_def
by blast
have "(Φ @ Ψ) ≼ ((δ # Δ) @ Γ)"
proof (cases "∃ φ . (δ, φ) ∈ set Σ")
assume "∃ φ . (δ, φ) ∈ set Σ"
from this obtain φ where φ: "(δ, φ) ∈ set Σ" by auto
let ?Σ = "remove1 (δ, φ) Σ"
from φ Σ(1) have "mset (map snd ?Σ) = mset (remove1 φ Φ)"
using remove1_pairs_list_projections_snd by fastforce
moreover from φ have "mset (map fst ?Σ) = mset (remove1 δ (map fst Σ))"
using remove1_pairs_list_projections_fst by fastforce
hence "mset (map fst ?Σ) ⊆# mset Δ"
using Σ(2) mset.simps(1) subset_eq_diff_conv by force
moreover from Σ(3) have "∀ (δ,φ) ∈ set ?Σ. ⊢ δ → φ" by auto
ultimately have "remove1 φ Φ ≼ Δ"
unfolding stronger_theory_relation_alt_def by blast
hence "(remove1 φ Φ @ Ψ) ≼ (Δ @ Γ)" using Cons by auto
from this obtain Ω where Ω:
"map snd Ω = (remove1 φ Φ) @ Ψ"
"mset (map fst Ω) ⊆# mset (Δ @ Γ)"
"∀ (α,β) ∈ set Ω. ⊢ α → β"
unfolding stronger_theory_relation_def
by blast
let ?Ω = "(δ, φ) # Ω"
have "map snd ?Ω = φ # remove1 φ Φ @ Ψ"
using Ω(1) by simp
moreover have "mset (map fst ?Ω) ⊆# mset ((δ # Δ) @ Γ)"
using Ω(2) by simp
moreover have "⊢ δ → φ"
using Σ(3) φ by blast
hence "∀ (α,β) ∈ set ?Ω. ⊢ α → β" using Ω(3) by auto
ultimately have "(φ # remove1 φ Φ @ Ψ) ≼ ((δ # Δ) @ Γ)"
by (metis stronger_theory_relation_def)
moreover have "φ ∈ set Φ"
using Σ(1) φ by force
hence "(φ # remove1 φ Φ) ⇌ Φ"
by force
hence "(φ # remove1 φ Φ @ Ψ) ⇌ Φ @ Ψ"
by (metis append_Cons perm_append2)
ultimately show ?thesis
using stronger_theory_left_permutation by blast
next
assume "∄φ. (δ, φ) ∈ set Σ"
hence "δ ∉ set (map fst Σ)"
"mset Δ + add_mset δ (mset []) = mset (δ # Δ)"
by auto
hence "mset (map fst Σ) ⊆# mset Δ"
by (metis (no_types) ‹mset (map fst Σ) ⊆# mset (δ # Δ)›
diff_single_trivial
mset.simps(1)
set_mset_mset
subset_eq_diff_conv)
with Σ(1) Σ(3) have "Φ ≼ Δ"
unfolding stronger_theory_relation_def
by blast
hence "(Φ @ Ψ) ≼ (Δ @ Γ)" using Cons by auto
then show ?thesis
by (simp add: stronger_theory_right_cons)
qed
}
then show ?case by blast
qed
thus ?thesis using assms by blast
qed
text ‹ We now turn to proving that \<^term>‹(≽)› is a subrelation of \<^term>‹(:⊢)›. ›
lemma (in classical_logic) stronger_theory_to_measure_deduction:
assumes "Γ ≽ Σ"
shows "Γ $⊢ Σ"
proof -
have "∀ Γ. Σ ≼ Γ ⟶ Γ $⊢ Σ"
proof (induct Σ)
case Nil
then show ?case by fastforce
next
case (Cons σ Σ)
{
fix Γ
assume "(σ # Σ) ≼ Γ"
from this obtain γ where γ: "γ ∈ set Γ" "⊢ γ → σ" "Σ ≼ (remove1 γ Γ)"
using stronger_theory_cons_witness by blast
let ?Φ = "[(γ,γ)]"
from γ Cons have "(remove1 γ Γ) $⊢ Σ" by blast
moreover have "mset (remove1 γ Γ) ⊆# mset (map (uncurry (→)) ?Φ @ Γ ⊖ (map snd ?Φ))"
by simp
ultimately have "map (uncurry (→)) ?Φ @ Γ ⊖ (map snd ?Φ) $⊢ Σ"
using measure_msub_left_monotonic by blast
moreover have "map (uncurry (⊔)) ?Φ :⊢ σ"
by (simp, metis γ(2)
Peirces_law
disjunction_def
list_deduction_def
list_deduction_modus_ponens
list_deduction_weaken
list_implication.simps(1)
list_implication.simps(2))
moreover from γ(1) have "mset (map snd ?Φ) ⊆# mset Γ" by simp
ultimately have "Γ $⊢ (σ # Σ)"
using measure_deduction.simps(2) by blast
}
then show ?case by blast
qed
thus ?thesis using assms by blast
qed
section ‹ Measure Deduction is a Preorder ›
text ‹ We next show that measure deduction is a preorder. ›
text ‹ Reflexivity follows immediately because \<^term>‹(≼)› is a subrelation
and is itself reflexive. ›
theorem (in classical_logic) measure_reflexive: "Γ $⊢ Γ"
by (simp add: stronger_theory_to_measure_deduction)
text ‹ Transitivity is complicated. It requires constructing many witnesses
and involves a lot of metatheorems. Below we provide various witness
constructions that allow us to establish \<^term>‹Γ $⊢ Λ ⟹ Λ $⊢ Δ ⟹ Γ $⊢ Δ›. ›
primrec (in implication_logic)
first_component :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔄›)
where
"𝔄 Ψ [] = []"
| "𝔄 Ψ (δ # Δ) =
(case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
None ⇒ 𝔄 Ψ Δ
| Some ψ ⇒ ψ # (𝔄 (remove1 ψ Ψ) Δ))"
primrec (in implication_logic)
second_component :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔅›)
where
"𝔅 Ψ [] = []"
| "𝔅 Ψ (δ # Δ) =
(case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
None ⇒ 𝔅 Ψ Δ
| Some ψ ⇒ δ # (𝔅 (remove1 ψ Ψ) Δ))"
lemma (in implication_logic) first_component_second_component_mset_connection:
"mset (map (uncurry (→)) (𝔄 Ψ Δ)) = mset (map snd (𝔅 Ψ Δ))"
proof -
have "∀ Ψ. mset (map (uncurry (→)) (𝔄 Ψ Δ)) = mset (map snd (𝔅 Ψ Δ))"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "mset (map (uncurry (→)) (𝔄 Ψ (δ # Δ))) =
mset (map snd (𝔅 Ψ (δ # Δ)))"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
then show ?thesis using Cons by simp
next
case False
from this obtain ψ where
"find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
"uncurry (→) ψ = snd δ"
using find_Some_predicate
by fastforce
then show ?thesis using Cons by simp
qed
}
then show ?case by blast
qed
thus ?thesis by blast
qed
lemma (in implication_logic) second_component_right_empty [simp]:
"𝔅 [] Δ = []"
by (induct Δ, simp+)
lemma (in implication_logic) first_component_msub:
"mset (𝔄 Ψ Δ) ⊆# mset Ψ"
proof -
have "∀ Ψ. mset (𝔄 Ψ Δ) ⊆# mset Ψ"
proof(induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "mset (𝔄 Ψ (δ # Δ)) ⊆# mset Ψ"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
then show ?thesis using Cons by simp
next
case False
from this obtain ψ where
ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
"ψ ∈ set Ψ"
using find_Some_set_membership
by fastforce
have "mset (𝔄 (remove1 ψ Ψ) Δ) ⊆# mset (remove1 ψ Ψ)"
using Cons by metis
thus ?thesis using ψ by (simp add: insert_subset_eq_iff)
qed
}
then show ?case by blast
qed
thus ?thesis by blast
qed
lemma (in implication_logic) second_component_msub:
"mset (𝔅 Ψ Δ) ⊆# mset Δ"
proof -
have "∀Ψ. mset (𝔅 Ψ Δ) ⊆# mset Δ"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "mset (𝔅 Ψ (δ # Δ)) ⊆# mset (δ # Δ)"
using Cons
by (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None",
simp,
metis add_mset_remove_trivial
diff_subset_eq_self
subset_mset.order_trans,
auto)
}
thus ?case by blast
qed
thus ?thesis by blast
qed
lemma (in implication_logic) second_component_snd_projection_msub:
"mset (map snd (𝔅 Ψ Δ)) ⊆# mset (map (uncurry (→)) Ψ)"
proof -
have "∀Ψ. mset (map snd (𝔅 Ψ Δ)) ⊆# mset (map (uncurry (→)) Ψ)"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "mset (map snd (𝔅 Ψ (δ # Δ))) ⊆# mset (map (uncurry (→)) Ψ)"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
then show ?thesis
using Cons by simp
next
case False
from this obtain ψ where ψ:
"find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = Some ψ"
by auto
hence "𝔅 Ψ (δ # Δ) = δ # (𝔅 (remove1 ψ Ψ) Δ)"
using ψ by fastforce
with Cons have "mset (map snd (𝔅 Ψ (δ # Δ))) ⊆#
mset ((snd δ) # map (uncurry (→)) (remove1 ψ Ψ))"
by (simp, metis mset_map mset_remove1)
moreover from ψ have "snd δ = (uncurry (→)) ψ"
using find_Some_predicate by fastforce
ultimately have
"mset (map snd (𝔅 Ψ (δ # Δ))) ⊆#
mset (map (uncurry (→)) (ψ # (remove1 ψ Ψ)))"
by simp
thus ?thesis
by (metis
first_component_msub
first_component_second_component_mset_connection
map_monotonic)
qed
}
thus ?case by blast
qed
thus ?thesis by blast
qed
lemma (in implication_logic) second_component_diff_msub:
assumes "mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
shows "mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ (map snd Ψ))"
proof -
have "∀ Ψ Γ. mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ)) ⟶
mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ (map snd Ψ))"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ Γ
assume ♢: "mset (map snd (δ # Δ)) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)"
have "mset (map snd ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ))) ⊆# mset (Γ ⊖ map snd Ψ)"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
hence A: "snd δ ∉ set (map (uncurry (→)) Ψ)"
proof (induct Ψ)
case Nil
then show ?case by simp
next
case (Cons ψ Ψ)
then show ?case
by (cases "uncurry (→) ψ = snd δ", simp+)
qed
moreover have
"mset (map snd Δ)
⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) - {#snd δ#}"
using ♢ insert_subset_eq_iff by fastforce
ultimately have
"mset (map snd Δ)
⊆# mset (map (uncurry (→)) Ψ @ (remove1 (snd δ) Γ)
⊖ map snd Ψ)"
by (metis (no_types)
mset_remove1
union_code
list_subtract.simps(2)
list_subtract_remove1_cons_perm
remove1_append)
hence B: "mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (remove1 (snd δ) Γ ⊖ (map snd Ψ))"
using Cons by blast
have C: "snd δ ∈# mset (snd δ # map snd Δ @
(map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) ⊖ (snd δ # map snd Δ))"
by (meson in_multiset_in_set list.set_intros(1))
have "mset (map snd (δ # Δ))
+ (mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)
- mset (map snd (δ # Δ)))
= mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)"
using ♢ subset_mset.add_diff_inverse by blast
then have "snd δ ∈# mset (map (uncurry (→)) Ψ) + (mset Γ - mset (map snd Ψ))"
using C by simp
with A have "snd δ ∈ set Γ"
by (metis (no_types) diff_subset_eq_self
in_multiset_in_set
subset_mset.add_diff_inverse
union_iff)
have D: "𝔅 Ψ Δ = 𝔅 Ψ (δ # Δ)"
using ‹find (λψ. uncurry (→) ψ = snd δ) Ψ = None›
by simp
obtain diff :: "'a list ⇒ 'a list ⇒ 'a list" where
"∀x0 x1. (∃v2. x1 @ v2 ⇌ x0) = (x1 @ diff x0 x1 ⇌ x0)"
by moura
then have E:
"mset (map snd (𝔅 Ψ (δ # Δ))
@ diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))
= mset (map (uncurry (→)) Ψ)"
by (meson second_component_snd_projection_msub mset_le_perm_append)
have F: "∀a m ma. (add_mset (a::'a) m ⊆# ma) = (a ∈# ma ∧ m ⊆# ma - {#a#})"
using insert_subset_eq_iff by blast
then have "snd δ ∈# mset (map snd (𝔅 Ψ (δ # Δ))
@ diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))
+ mset (Γ ⊖ map snd Ψ)"
using E ♢ by force
then have "snd δ ∈# mset (Γ ⊖ map snd Ψ)"
using A E by (metis (no_types) in_multiset_in_set union_iff)
then have G: "add_mset (snd δ) (mset (map snd (Δ ⊖ 𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ map snd Ψ)"
using B F by force
have H: "∀ps psa f. ¬ mset (ps::('a × 'a) list) ⊆# mset psa ∨
mset ((map f psa::'a list) ⊖ map f ps) = mset (map f (psa ⊖ ps))"
using map_list_subtract_mset_equivalence by blast
have "snd δ ∉# mset (map snd (𝔅 Ψ (δ # Δ)))
+ mset (diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))"
using A E by auto
then have "add_mset (snd δ) (mset (map snd (Δ ⊖ 𝔅 Ψ Δ)))
= mset (map snd (δ # Δ) ⊖ map snd (𝔅 Ψ (δ # Δ)))"
using D H second_component_msub by auto
then show ?thesis
using G H by (metis (no_types) second_component_msub)
next
case False
from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
by auto
let ?Ψ' = "remove1 ψ Ψ"
let ?Γ' = "remove1 (snd ψ) Γ"
have "snd δ = uncurry (→) ψ"
"ψ ∈ set Ψ"
"mset ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ)) =
mset (Δ ⊖ 𝔅 ?Ψ' Δ)"
using ψ find_Some_predicate find_Some_set_membership
by fastforce+
moreover
have "mset (Γ ⊖ map snd Ψ) = mset (?Γ' ⊖ map snd ?Ψ')"
by (simp, metis ‹ψ ∈ set Ψ› image_mset_add_mset in_multiset_in_set insert_DiffM)
moreover
obtain search :: "('a × 'a) list ⇒ ('a × 'a ⇒ bool) ⇒ 'a × 'a" where
"∀xs P. (∃x. x ∈ set xs ∧ P x) = (search xs P ∈ set xs ∧ P (search xs P))"
by moura
then have "∀p ps. (find p ps ≠ None ∨ (∀pa. pa ∉ set ps ∨ ¬ p pa))
∧ (find p ps = None ∨ search ps p ∈ set ps ∧ p (search ps p))"
by (metis (full_types) find_None_iff)
then have "(find (λp. uncurry (→) p = snd δ) Ψ ≠ None
∨ (∀p. p ∉ set Ψ ∨ uncurry (→) p ≠ snd δ))
∧ (find (λp. uncurry (→) p = snd δ) Ψ = None
∨ search Ψ (λp. uncurry (→) p = snd δ) ∈ set Ψ
∧ uncurry (→) (search Ψ (λp. uncurry (→) p = snd δ)) = snd δ)"
by blast
hence "snd δ ∈ set (map (uncurry (→)) Ψ)"
by (metis (no_types) False image_eqI image_set)
moreover
have A: "add_mset (uncurry (→) ψ) (image_mset snd (mset Δ))
= image_mset snd (add_mset δ (mset Δ))"
by (simp add: ‹snd δ = uncurry (→) ψ›)
have B: "{#snd δ#} ⊆# image_mset (uncurry (→)) (mset Ψ)"
using ‹snd δ ∈ set (map (uncurry (→)) Ψ)› by force
have "image_mset (uncurry (→)) (mset Ψ) - {#snd δ#}
= image_mset (uncurry (→)) (mset (remove1 ψ Ψ))"
by (simp add: ‹ψ ∈ set Ψ› ‹snd δ = uncurry (→) ψ› image_mset_Diff)
then have "mset (map snd (Δ ⊖ 𝔅 (remove1 ψ Ψ) Δ))
⊆# mset (remove1 (snd ψ) Γ ⊖ map snd (remove1 ψ Ψ))"
by (metis (no_types)
A B ♢ Cons.hyps
calculation(1)
calculation(4)
insert_subset_eq_iff
mset.simps(2)
mset_map
subset_mset.diff_add_assoc2
union_code)
ultimately show ?thesis by fastforce
qed
}
then show ?case by blast
qed
thus ?thesis using assms by auto
qed
primrec (in classical_logic)
merge_witness :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔍›)
where
"𝔍 Ψ [] = Ψ"
| "𝔍 Ψ (δ # Δ) =
(case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
None ⇒ δ # 𝔍 Ψ Δ
| Some ψ ⇒ (fst δ ⊓ fst ψ, snd ψ) # (𝔍 (remove1 ψ Ψ) Δ))"
lemma (in classical_logic) merge_witness_right_empty [simp]:
"𝔍 [] Δ = Δ"
by (induct Δ, simp+)
lemma (in classical_logic) second_component_merge_witness_snd_projection:
"mset (map snd Ψ @ map snd (Δ ⊖ (𝔅 Ψ Δ))) = mset (map snd (𝔍 Ψ Δ))"
proof -
have "∀ Ψ. mset (map snd Ψ @ map snd (Δ ⊖ (𝔅 Ψ Δ))) = mset (map snd (𝔍 Ψ Δ))"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "mset (map snd Ψ @ map snd ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ))) =
mset (map snd (𝔍 Ψ (δ # Δ)))"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
then show ?thesis
using Cons
by (simp,
metis (no_types, lifting)
ab_semigroup_add_class.add_ac(1)
add_mset_add_single
image_mset_single
image_mset_union
second_component_msub
subset_mset.add_diff_assoc2)
next
case False
from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
by auto
moreover have "ψ ∈ set Ψ"
by (meson ψ find_Some_set_membership)
moreover
let ?Ψ' = "remove1 ψ Ψ"
from Cons have
"mset (map snd ?Ψ' @ map snd (Δ ⊖ 𝔅 ?Ψ' Δ)) =
mset (map snd (𝔍 ?Ψ' Δ))"
by blast
ultimately show ?thesis
by (simp,
metis (no_types, lifting)
add_mset_remove_trivial_eq
image_mset_add_mset
in_multiset_in_set
union_mset_add_mset_left)
qed
}
then show ?case by blast
qed
thus ?thesis by blast
qed
lemma (in classical_logic) second_component_merge_witness_stronger_theory:
"(map (uncurry (→)) Δ @ map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ Δ)) ≼
map (uncurry (→)) (𝔍 Ψ Δ)"
proof -
have "∀ Ψ. (map (uncurry (→)) Δ @
map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ Δ)) ≼
map (uncurry (→)) (𝔍 Ψ Δ)"
proof (induct Δ)
case Nil
then show ?case
by simp
next
case (Cons δ Δ)
{
fix Ψ
have "⊢ (uncurry (→)) δ → (uncurry (→)) δ"
using axiom_k modus_ponens implication_absorption by blast
have
"(map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) ≼
map (uncurry (→)) (𝔍 Ψ (δ # Δ))"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
thus ?thesis
using Cons
‹⊢ (uncurry (→)) δ → (uncurry (→)) δ›
by (simp, metis stronger_theory_left_right_cons)
next
case False
from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
by auto
from ψ have "snd δ = uncurry (→) ψ"
using find_Some_predicate by fastforce
from ψ ‹snd δ = uncurry (→) ψ› have
"mset (map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) =
mset (map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) (remove1 ψ Ψ) ⊖
map snd (𝔅 (remove1 ψ Ψ) Δ))"
by (simp add: find_Some_set_membership image_mset_Diff)
hence
"(map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) ≼
(map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) (remove1 ψ Ψ) ⊖ map snd (𝔅 (remove1 ψ Ψ) Δ))"
by (simp add: msub_stronger_theory_intro)
with Cons ‹⊢ (uncurry (→)) δ → (uncurry (→)) δ› have
"(map (uncurry (→)) (δ # Δ) @
map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ)))
≼ ((uncurry (→)) δ # map (uncurry (→)) (𝔍 (remove1 ψ Ψ) Δ))"
using stronger_theory_left_right_cons
stronger_theory_transitive
by fastforce
moreover
let ?α = "fst δ"
let ?β = "fst ψ"
let ?γ = "snd ψ"
have "uncurry (→) = (λ δ. fst δ → snd δ)" by fastforce
with ψ have "(uncurry (→)) δ = ?α → ?β → ?γ"
using find_Some_predicate by fastforce
hence "⊢ ((?α ⊓ ?β) → ?γ) → (uncurry (→)) δ"
using biconditional_def curry_uncurry by auto
with ψ have
"((uncurry (→)) δ # map (uncurry (→)) (𝔍 (remove1 ψ Ψ) Δ)) ≼
map (uncurry (→)) (𝔍 Ψ (δ # Δ))"
using stronger_theory_left_right_cons by auto
ultimately show ?thesis
using stronger_theory_transitive
by blast
qed
}
then show ?case by simp
qed
thus ?thesis by simp
qed
lemma (in classical_logic) merge_witness_msub_intro:
assumes "mset (map snd Ψ) ⊆# mset Γ"
and "mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
shows "mset (map snd (𝔍 Ψ Δ)) ⊆# mset Γ"
proof -
have "∀Ψ Γ. mset (map snd Ψ) ⊆# mset Γ ⟶
mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ)) ⟶
mset (map snd (𝔍 Ψ Δ)) ⊆# mset Γ"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ :: "('a × 'a) list"
fix Γ :: "'a list"
assume ♢: "mset (map snd Ψ) ⊆# mset Γ"
"mset (map snd (δ # Δ)) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
have "mset (map snd (𝔍 Ψ (δ # Δ))) ⊆# mset Γ"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
hence "snd δ ∉ set (map (uncurry (→)) Ψ)"
proof (induct Ψ)
case Nil
then show ?case by simp
next
case (Cons ψ Ψ)
hence "uncurry (→) ψ ≠ snd δ" by fastforce
with Cons show ?case by fastforce
qed
with ♢(2) have "snd δ ∈# mset (Γ ⊖ map snd Ψ)"
using mset_subset_eq_insertD by fastforce
with ♢(1) have "mset (map snd Ψ) ⊆# mset (remove1 (snd δ) Γ)"
by (metis list_subtract_mset_homomorphism
mset_remove1
single_subset_iff
subset_mset.add_diff_assoc
subset_mset.add_diff_inverse
subset_mset.le_iff_add)
moreover
have "add_mset (snd δ) (mset (Γ ⊖ map snd Ψ) - {#snd δ#}) = mset (Γ ⊖ map snd Ψ)"
by (meson ‹snd δ ∈# mset (Γ ⊖ map snd Ψ)› insert_DiffM)
then have "image_mset snd (mset Δ) - (mset Γ - add_mset (snd δ) (image_mset snd (mset Ψ)))
⊆# {#x → y. (x, y) ∈# mset Ψ#}"
using ♢(2) by (simp, metis add_mset_diff_bothsides
list_subtract_mset_homomorphism
mset_map subset_eq_diff_conv)
hence "mset (map snd Δ)
⊆# mset (map (uncurry (→)) Ψ @ (remove1 (snd δ) Γ) ⊖ (map snd Ψ))"
using subset_eq_diff_conv by (simp, blast)
ultimately have "mset (map snd (𝔍 Ψ Δ)) ⊆# mset (remove1 (snd δ) Γ)"
using Cons by blast
hence "mset (map snd (δ # (𝔍 Ψ Δ))) ⊆# mset Γ"
by (simp, metis ‹snd δ ∈# mset (Γ ⊖ map snd Ψ)›
cancel_ab_semigroup_add_class.diff_right_commute
diff_single_trivial
insert_subset_eq_iff
list_subtract_mset_homomorphism
multi_drop_mem_not_eq)
with ‹find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None›
show ?thesis
by simp
next
case False
from this obtain ψ where ψ:
"find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
by fastforce
let ?χ = "fst ψ"
let ?γ = "snd ψ"
have "uncurry (→) = (λ ψ. fst ψ → snd ψ)"
by fastforce
moreover
from this have "uncurry (→) ψ = ?χ → ?γ" by fastforce
with ψ have A: "(?χ, ?γ) ∈ set Ψ"
and B: "snd δ = ?χ → ?γ"
using find_Some_predicate
by (simp add: find_Some_set_membership, fastforce)
let ?Ψ' = "remove1 (?χ, ?γ) Ψ"
from B ♢(2) have
"mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) - {# ?χ → ?γ #}"
by (simp add: insert_subset_eq_iff)
moreover
have "mset (map (uncurry (→)) Ψ)
= add_mset (case (fst ψ, snd ψ) of (x, xa) ⇒ x → xa)
(image_mset (uncurry (→)) (mset (remove1 (fst ψ, snd ψ) Ψ)))"
by (metis (no_types)
A
image_mset_add_mset
in_multiset_in_set
insert_DiffM
mset_map
mset_remove1
uncurry_def)
ultimately have
"mset (map snd Δ) ⊆# mset (map (uncurry (→)) ?Ψ' @ Γ ⊖ map snd Ψ)"
using
add_diff_cancel_left'
add_diff_cancel_right
diff_diff_add_mset
diff_subset_eq_self
mset_append
subset_eq_diff_conv
subset_mset.diff_add
by auto
moreover from A B ♢
have "mset (Γ ⊖ map snd Ψ) = mset((remove1 ?γ Γ) ⊖ (remove1 ?γ (map snd Ψ)))"
using
image_eqI
prod.sel(2)
set_map
by force
with A have
"mset (Γ ⊖ map snd Ψ) = mset((remove1 ?γ Γ) ⊖ (map snd ?Ψ'))"
by (metis
remove1_pairs_list_projections_snd
in_multiset_in_set
list_subtract_mset_homomorphism
mset_remove1)
ultimately have
"mset (map snd Δ) ⊆# mset (map (uncurry (→)) ?Ψ'
@ (remove1 ?γ Γ)
⊖ map snd ?Ψ')"
by simp
hence "mset (map snd (𝔍 ?Ψ' Δ)) ⊆# mset (remove1 ?γ Γ)"
using Cons ♢(1) A
by (metis (no_types, lifting)
image_mset_add_mset
in_multiset_in_set
insert_DiffM
insert_subset_eq_iff
mset_map mset_remove1
prod.collapse)
with ♢(1) A have "mset (map snd (𝔍 ?Ψ' Δ)) + {# ?γ #} ⊆# mset Γ"
by (metis add_mset_add_single
image_eqI
insert_subset_eq_iff
mset_remove1
mset_subset_eqD
set_map
set_mset_mset
snd_conv)
hence "mset (map snd ((fst δ ⊓ ?χ, ?γ) # (𝔍 ?Ψ' Δ))) ⊆# mset Γ"
by simp
moreover from ψ have
"𝔍 Ψ (δ # Δ) = (fst δ ⊓ ?χ, ?γ) # (𝔍 ?Ψ' Δ)"
by simp
ultimately show ?thesis by simp
qed
}
thus ?case by blast
qed
with assms show ?thesis by blast
qed
lemma (in classical_logic) right_merge_witness_stronger_theory:
"map (uncurry (⊔)) Δ ≼ map (uncurry (⊔)) (𝔍 Ψ Δ)"
proof -
have "∀ Ψ. map (uncurry (⊔)) Δ ≼ map (uncurry (⊔)) (𝔍 Ψ Δ)"
proof (induct Δ)
case Nil
then show ?case by simp
next
case (Cons δ Δ)
{
fix Ψ
have "map (uncurry (⊔)) (δ # Δ) ≼ map (uncurry (⊔)) (𝔍 Ψ (δ # Δ))"
proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
case True
hence "𝔍 Ψ (δ # Δ) = δ # 𝔍 Ψ Δ"
by simp
moreover have "⊢ (uncurry (⊔)) δ → (uncurry (⊔)) δ"
by (metis axiom_k axiom_s modus_ponens)
ultimately show ?thesis using Cons
by (simp add: stronger_theory_left_right_cons)
next
case False
from this obtain ψ where ψ:
"find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
by fastforce
let ?χ = "fst ψ"
let ?γ = "snd ψ"
let ?μ = "fst δ"
have "uncurry (→) = (λ ψ. fst ψ → snd ψ)"
"uncurry