Theory AGM_Contraction
theory AGM_Contraction
imports AGM_Logic AGM_Remainder
begin
section ‹Contractions›
text‹The first operator of belief change of the AGM framework is contraction. This operator consist to remove
a sentence @{term ‹φ›} from a belief set @{term ‹K›} in such a way that @{term ‹K›} no longer imply @{term ‹φ›}.
In the following we will first axiomatize such operators at different levels of logics (Tarskian, supraclassical and compact)
and then we will give constructions satisfying these axioms. The following graph summarizes all equivalences we established:
\includegraphics[width=\textwidth]{"graph_locales.pdf"}
We will use the extension feature of locales in Isabelle/HOL to incrementally define the contraction
operator as shown by blue arrows in the previous figure. Then, using the interpretation feature of locales, we will prove the equivalence between
descriptive and constructive approaches at each level depending on the adopted logics (black arrows).
›
subsection‹AGM contraction postulates›
text‹
The operator of contraction is denoted by the symbol @{text ‹÷›} and respects the six following conditions :
▪ @{text ‹contract_closure›} : a belief set @{term ‹K›} contracted by @{term ‹φ›} should be logically closed
▪ @{text ‹contract_inclusion›} : a contracted set @{term ‹K›} should be a subset of the original one
▪ @{text ‹contract_vacuity›} : if @{term ‹φ›} is not included in a set @{term ‹K›} then the contraction of @{term ‹K›} by @{term ‹φ›} involves no change at all
▪ @{text ‹contract_success›} : if a set @{term ‹K›} is contracted by @{term ‹φ›} then @{term ‹K›} does not imply @{term ‹φ›}
▪ @{text ‹contract_recovery›}: all propositions removed in a set @{term ‹K›} by contraction of @{term ‹φ›} will be recovered by expansion of @{term ‹φ›}
▪ @{text ‹contract_extensionality›} : Extensionality guarantees that the logic of contraction is extensional in the sense of allowing logically
quivalent sentences to be freely substituted for each other›
locale AGM_Contraction = Tarskian_logic +
fixes contraction::‹'a set ⇒ 'a ⇒ 'a set› (infix ‹÷› 55)
assumes contract_closure: ‹K = Cn(A) ⟹ K ÷ φ = Cn(K ÷ φ)›
and contract_inclusion: ‹K = Cn(A) ⟹ K ÷ φ ⊆ K›
and contract_vacuity: ‹K = Cn(A) ⟹ φ ∉ K ⟹ K ÷ φ = K›
and contract_success: ‹K = Cn(A) ⟹ φ ∉ Cn({}) ⟹ φ ∉ K ÷ φ›
and contract_recovery: ‹K = Cn(A) ⟹ K ⊆ ((K ÷ φ) ⊕ φ)›
and contract_extensionality: ‹K = Cn(A) ⟹ Cn({φ}) = Cn({ψ}) ⟹ K ÷ φ = K ÷ ψ›
text‹
A full contraction is defined by two more postulates to rule the conjunction. We base on a supraclassical logic.
▪ @{text ‹contract_conj_overlap›} : An element in both @{text ‹K ÷ φ›} and @{text ‹K ÷ ψ›} is also an element of @{text ‹K ÷ (φ ∧ ψ)›}
▪ @{text ‹contract_conj_inclusion›} : If @{term ‹φ›} not in @{text ‹K ÷ (φ ∧ ψ)›} then all elements removed by this contraction are also removed from @{text ‹K ÷ φ›}›
locale AGM_FullContraction = AGM_Contraction + Supraclassical_logic +
assumes contract_conj_overlap: ‹K = Cn(A) ⟹ (K ÷ φ) ∩ (K ÷ ψ) ⊆ (K ÷ (φ .∧. ψ))›
and contract_conj_inclusion: ‹K = Cn(A) ⟹ φ ∉ (K ÷ (φ .∧. ψ)) ⟹ ((K ÷ (φ .∧. ψ) ⊆ (K ÷ φ)))›
begin
text‹@{text ‹contract_conj_overlap_variant›} does not need ‹ψ› to occur in the left side! ›
corollary contract_conj_overlap_variant: ‹K = Cn(A) ⟹ (K ÷ φ) ∩ Cn({φ}) ⊆ (K ÷ (φ .∧. ψ))›
proof -
assume a:‹K = Cn(A)›
{ assume b:‹K ⊢ φ› and c:‹K ⊢ ψ›
hence d:‹K ÷ (φ .∧. ψ) = K ÷ (φ .∧. ((.¬ φ) .∨. ψ))›
apply(rule_tac contract_extensionality[OF a])
using conj_overlap[of _ φ ψ] by (simp add: Cn_same)
have e:‹K ∩ Cn {φ} ⊆ K ÷ (.¬ φ .∨. ψ)›
proof(safe)
fix χ
assume f:‹χ ∈ K› and g:‹χ ∈ Cn {φ}›
have ‹K ÷ (.¬ φ .∨. ψ) ⊢ (.¬ φ .∨. ψ) .⟶. χ›
by (metis a contract_recovery expansion_def f impI_PL infer_def subset_eq)
hence ‹K ÷ (.¬ φ .∨. ψ) ⊢ .¬ φ .⟶. χ›
by (meson disjI1_PL imp_trans inclusion_L infer_def insert_subset validD_L valid_imp_PL)
with g show ‹χ ∈ K ÷ (.¬ φ .∨. ψ)›
by (metis a contract_closure disjE_PL ex_mid_PL infer_def validD_L valid_imp_PL)
qed
have ?thesis
unfolding d using e contract_conj_overlap[OF a, of φ ‹(.¬ φ .∨. ψ)›] a contract_inclusion by force
}
then show ?thesis
apply (cases ‹¬ K ⊢ φ ∨ ¬ K ⊢ ψ›)
by (metis IntE a assumption_L conjE1_PL conjE2_PL contract_inclusion contract_vacuity subsetD subsetI) blast
qed
text‹@{text ‹contract_conj_inclusion_variant›}: Everything retained in @{text ‹K ÷ (φ ∧ ψ)›} is retained in @{text ‹K ÷ ψ›}›
corollary contract_conj_inclusion_variant : ‹K = Cn(A) ⟹ (K ÷ (φ .∧. ψ) ⊆ (K ÷ φ)) ∨ (K ÷ (φ .∧. ψ) ⊆ (K ÷ ψ))›
proof -
assume a:‹K = Cn(A)›
{ assume d:‹φ ∈ (K ÷ (φ .∧. ψ)) ∧ ψ ∈ (K ÷ (φ .∧. ψ))›
hence ‹φ .∧. ψ ∈ (K ÷ (φ .∧. ψ))›
using Supraclassical_logic.conjI_PL Supraclassical_logic_axioms a contract_closure by fastforce
with d have ?thesis
by (metis (no_types, lifting) Supraclassical_logic.valid_conj_PL Supraclassical_logic_axioms
Tarskian_logic.valid_expansion Tarskian_logic_axioms a contract_closure contract_inclusion
contract_recovery contract_success dual_order.trans expansion_def)
}
then show ?thesis
by (metis a conj_com_Cn contract_conj_inclusion contract_extensionality)
qed
end
subsection ‹Partial meet contraction definition›
text‹A partial meet contraction of @{term ‹K›} by @{term ‹φ›} is the intersection of some sets that not imply @{term ‹φ›}.
We define these sets as the "remainders" @{text ‹(K .⊥. φ›}.
The function of selection @{term ‹γ›} select the best set of the remainders that do not imply @{term ‹φ›}.
This function respect these postulates :
▪ @{text ‹is_selection›} : if there exist some set that do not imply @{term ‹φ›} then the function selection @{term ‹γ›} is a subset of these sets
▪ @{text ‹tautology_selection›} : if there is no set that do not imply @{term ‹φ›} then the result of the selection function is @{term ‹K›}
▪ @{text nonempty_selection} : An empty selection function do not exist
▪ @{text extensional_selection} : Two proposition with the same closure have the same selection function›
locale PartialMeetContraction = Tarskian_logic +
fixes selection::‹'a set ⇒ 'a ⇒ 'a set set› (‹γ›)
assumes is_selection: ‹K = Cn(A) ⟹ (K .⊥. φ) ≠ {} ⟹ γ K φ ⊆ (K .⊥. φ)›
assumes tautology_selection: ‹K = Cn(A) ⟹ (K .⊥. φ) = {} ⟹ γ K φ = {K}›
assumes nonempty_selection: ‹K = Cn(A) ⟹ γ K φ ≠ {}›
assumes extensional_selection: ‹K = Cn(A) ⟹ Cn({φ}) = Cn({ψ}) ⟹ γ K φ = γ K ψ›
begin
text ‹A partial meet is the intersection of set of selected element.›
definition (in Tarskian_logic) meet_contraction::‹'a set ⇒ ('a set ⇒ 'a ⇒ 'a set set) ⇒ 'a ⇒ 'a set› (‹_ ÷⇘_⇙ _› [60,50,60]55)
where mc: ‹(A ÷⇘γ⇙ φ) ≡ ⋂(γ A φ)›
text ‹Following this definition 4 postulates of AGM can be proved on a partial meet contraction:
▪ @{text ‹contract_inclusion›}
▪ @{text ‹ contract_vacuity›}
▪ @{text ‹ contract_closure›}
▪ @{text ‹ contract_extensionality›}›
text ‹@{text ‹pmc_inclusion› } :a partial meet contraction is a subset of the contracted set›
lemma pmc_inclusion: ‹K = Cn(A) ⟹ K ÷⇘γ⇙ φ ⊆ K›
apply (cases ‹(K .⊥. φ) = {}›, simp_all add: mc tautology_selection)
by (meson Inf_less_eq in_mono is_selection nonempty_selection rem_inclusion)
text‹@{text ‹pmc_vacuity›} : if @{term ‹φ›} is not included in a set @{term ‹K›} then the partial meet contraction of @{term ‹K›} by @{term ‹φ›} involves not change at all›
lemma pmc_vacuity: ‹K = Cn(A) ⟹ ¬ K ⊢ φ ⟹ K ÷⇘γ⇙ φ = K›
unfolding mc nonconsequence_remainder
by (metis Inf_superset_mono Un_absorb1 cInf_singleton insert_not_empty is_selection mc nonconsequence_remainder pmc_inclusion sup_commute)
text‹@{text ‹pmc_closure›} : a partial meet contraction is logically closed›
lemma pmc_closure: ‹K = Cn(A) ⟹ (K ÷⇘γ⇙ φ) = Cn(K ÷⇘γ⇙ φ)›
proof (rule subset_antisym, simp_all add:inclusion_L mc transitivity_L, goal_cases)
case 1
have ‹⋂(γ (Cn A) φ) = ⋂{Cn(B)|B. B ∈ γ (Cn A) φ}›
by auto (metis idempotency_L insert_absorb insert_iff insert_subset is_selection rem_closure tautology_selection)+
from Cn_Inter[OF this] show ?case by blast
qed
text ‹@{text ‹pmc_extensionality›} : Extensionality guarantees that the logic of contraction is extensional in the sense of allowing logically equivalent sentences to be freely substituted for each other›
lemma pmc_extensionality: ‹K = Cn(A) ⟹ Cn({φ}) = Cn({ψ}) ⟹ K ÷⇘γ⇙ φ = K ÷⇘γ⇙ ψ›
by (metis extensional_selection mc)
text ‹@{text ‹pmc_tautology›} : if @{term ‹φ›} is a tautology then the partial meet contraction of @{term ‹K›} by @{term ‹φ›} is @{term ‹K›}›
lemma pmc_tautology: ‹K = Cn(A) ⟹ ⊩ φ ⟹ K ÷⇘γ⇙ φ = K›
by (simp add: mc taut2emptyrem tautology_selection)
text‹@{text ‹completion›} is a an operator that can build an equivalent selection from an existing one›
definition (in Tarskian_logic) completion::‹('a set ⇒ 'a ⇒ 'a set set) ⇒ 'a set ⇒ 'a ⇒ 'a set set› (‹*›)
where ‹* γ A φ ≡ if (A .⊥. φ) = {} then {A} else {B. B ∈ A .⊥. φ ∧ ⋂ (γ A φ) ⊆ B}›
lemma selection_completion: "K = Cn(A) ⟹ γ K φ ⊆ * γ K φ"
using completion_def is_selection tautology_selection by fastforce
lemma (in Tarskian_logic) completion_completion: "K = Cn(A) ⟹ * (* γ) K φ = * γ K φ"
by (auto simp add:completion_def)
lemma pmc_completion: ‹K = Cn(A) ⟹ K ÷⇘*γ⇙ φ = K ÷⇘γ⇙ φ›
apply(auto simp add: mc completion_def tautology_selection)
by (metis Inter_lower equals0D in_mono is_selection)
end
text‹A transitively relational meet contraction is a partial meet contraction using a binary relation between the elements of the selection function›
text‹A relation is :
▪ transitive (@{text ‹trans_rel›})
▪ non empty (there is always an element preferred to the others (@{text ‹nonempty_rel›}))›
text‹A selection function @{term ‹γ⇩T⇩R›} is transitively relational @{text ‹rel_sel›} with the following condition :
▪ If the the remainders @{text ‹K .⊥. φ›} is empty then the selection function return @{term ‹K›}
▪ Else the selection function return a non empty transitive relation on the remainders›
locale TransitivelyRelationalMeetContraction = Tarskian_logic +
fixes relation::‹'a set ⇒ 'a set ⇒ 'a set ⇒ bool› (‹_ ≼⇘_⇙ _› [60,50,60]55)
assumes trans_rel: ‹K = Cn(A) ⟹ B ≼⇘K⇙ C ⟹ C ≼⇘K⇙ D ⟹ B ≼⇘K⇙ D›
assumes nonempty_rel: ‹K = Cn(A) ⟹ (K .⊥. φ) ≠ {} ⟹ ∃B∈(K .⊥. φ). (∀C∈(K .⊥. φ). C ≼⇘K⇙ B)›
fixes rel_sel::‹'a set ⇒ 'a ⇒ 'a set set› (‹γ⇩T⇩R›)
defines rel_sel: ‹γ⇩T⇩R K φ ≡ if (K .⊥. φ) = {} then {K}
else {B. B∈(K .⊥. φ) ∧ (∀C∈(K .⊥. φ). C ≼⇘K⇙ B)}›
begin
text‹A transitively relational selection function respect the partial meet contraction postulates.›
sublocale PartialMeetContraction where selection = γ⇩T⇩R
apply(unfold_locales)
apply(simp_all add: rel_sel)
using nonempty_rel apply blast
using remainder_extensionality by blast
end
text‹A full meet contraction is a limiting case of the partial meet contraction where if the remainders are not empty then
the selection function return all the remainders (as defined by @{text ‹full_sel›}›
locale FullMeetContraction = Tarskian_logic +
fixes full_sel::‹'a set ⇒ 'a ⇒ 'a set set› (‹γ⇩F⇩C›)
defines full_sel: ‹γ⇩F⇩C K φ ≡ if K .⊥. φ = {} then {K} else K .⊥. φ›
begin
text‹A full selection and a relation ? is a transitively relational meet contraction postulates.›
sublocale TransitivelyRelationalMeetContraction where relation = ‹λ K A B. True› and rel_sel=γ⇩F⇩C
by (unfold_locales, auto simp add:full_sel, rule eq_reflection, simp)
end
subsection‹Equivalence of partial meet contraction and AGM contraction›
locale PMC_SC = PartialMeetContraction + Supraclassical_logic + Compact_logic
begin
text ‹In a context of a supraclassical and a compact logic the two remaining postulates of AGM contraction :
▪ @{text ‹contract_recovery›}
▪ @{text ‹contract_success›}
can be proved on a partial meet contraction.›
text‹@{text ‹pmc_recovery›} : all proposition removed by a partial meet contraction of @{term ‹φ›} will be recovered by the expansion of @{term ‹φ›}›
lemma pmc_recovery: ‹K = Cn(A) ⟹ K ⊆ ((K ÷⇘γ⇙ φ) ⊕ φ)›
apply(cases ‹(K .⊥. φ) = {}›, simp_all (no_asm) add:mc expansion_def)
using inclusion_L tautology_selection apply fastforce
proof -
assume a:‹K = Cn(A)› and b:‹K .⊥. φ ≠ {}›
{ fix ψ
assume d:‹K ⊢ ψ›
have ‹φ .⟶. ψ ∈ ⋂(γ K φ)›
using is_selection[OF a b]
by auto (metis a d infer_def rem_closure remainder_recovery subsetD)
}
with a b show ‹K ⊆ Cn (insert φ (⋂ (γ K φ)))›
by (metis (no_types, lifting) Un_commute assumption_L imp_PL infer_def insert_is_Un subsetI)
qed
text ‹@{text ‹pmc_success›} : a partial meet contraction of @{term ‹K›} by @{term ‹φ›} not imply @{term ‹φ›}›
lemma pmc_success: ‹K = Cn(A) ⟹ φ ∉ Cn({}) ⟹ φ ∉ K ÷⇘γ⇙ φ›
proof
assume a:‹K = Cn(A)› and b:‹φ ∉ Cn({})› and c:‹φ ∈ K ÷⇘γ⇙ φ›
from c show False unfolding mc
proof(cases ‹K .⊥. φ = {K}›)
case True
then show ?thesis
by (meson assumption_L c nonconsequence_remainder pmc_inclusion[OF a] subsetD)
next
case False
hence ‹∀B∈K .⊥. φ. φ ∉ B› using assumption_L rem by auto
moreover have ‹K .⊥. φ ≠ {}› using b emptyrem2taut validD_L by blast
ultimately show ?thesis
using b c mc nonempty_selection[OF a] validD_L emptyrem2taut is_selection[OF a]
by (metis Inter_iff bot.extremum_uniqueI subset_iff)
qed
qed
text‹As a partial meet contraction has been proven to respect all postulates of AGM contraction
the equivalence between the both are straightforward›
sublocale AGM_Contraction where contraction = ‹λA φ. A ÷⇘γ⇙ φ›
using pmc_closure pmc_inclusion pmc_vacuity
pmc_success pmc_recovery pmc_extensionality
expansion_def idempotency_L infer_def
by (unfold_locales) metis+
end
locale AGMC_SC = AGM_Contraction + Supraclassical_logic + Compact_logic
begin
text ‹obs 2.5 page 514›
definition AGM_selection::‹'a set ⇒ 'a ⇒ 'a set set› (‹γ⇩A⇩G⇩M›)
where AGM_sel: ‹γ⇩A⇩G⇩M A φ ≡ if A .⊥. φ = {} then {A} else {B. B ∈ A .⊥. φ ∧ A ÷ φ ⊆ B}›
text‹The selection function @{term ‹γ⇩A⇩G⇩M›} respect the partial meet contraction postulates›
sublocale PartialMeetContraction where selection = γ⇩A⇩G⇩M
proof(unfold_locales, unfold AGM_sel, simp_all, goal_cases)
case (1 K A φ)
then show ?case using upper_remainder[of ‹K ÷ φ› K φ] contract_success[OF 1(1)]
by (metis contract_closure contract_inclusion infer_def taut2emptyrem valid_def)
next
case (2 K A φ ψ)
then show ?case
by (metis (mono_tags, lifting) contract_extensionality Collect_cong remainder_extensionality)
qed
text ‹@{text ‹contraction_is_pmc›} : an AGM contraction is equivalent to a partial met contraction using the selection function ‹γ⇩A⇩G⇩M››
lemma contraction_is_pmc: ‹K = Cn(A) ⟹ K ÷ φ = K ÷⇘γ⇩A⇩G⇩M⇙ φ›
proof
assume a:‹K = Cn(A)›
show ‹K ÷ φ ⊆ K ÷⇘γ⇩A⇩G⇩M⇙ φ›
using contract_inclusion[OF a] by (auto simp add:mc AGM_sel)
next
assume a:‹K = Cn(A)›
show ‹K ÷⇘γ⇩A⇩G⇩M⇙ φ ⊆ K ÷ φ›
proof (cases ‹⊩ φ›)
case True
hence ‹K .⊥. φ = {}›
using nonconsequence_remainder taut2emptyrem by auto
then show ?thesis
apply(simp_all add:mc AGM_sel)
by (metis a emptyrem2taut contract_closure contract_recovery valid_expansion)
next
case validFalse:False
then show ?thesis
proof (cases ‹K ⊢ φ›)
case True
hence b:‹K .⊥. φ ≠ {}›
using emptyrem2taut validFalse by blast
have d:‹ψ ∈ K ⟹ φ .⟶. ψ ∈ K ÷ φ› for ψ
using Supraclassical_logic.impI_PL Supraclassical_logic_axioms a contract_closure contract_recovery expansion_def by fastforce
{ fix ψ
assume e:‹ψ ∈ K › and f:‹ψ ∉ K ÷ φ›
have ‹(ψ .⟶. φ) .⟶. φ ∉ K ÷ φ›
using imp_recovery2[of ‹K ÷ φ› φ ψ] a contract_closure d e f by auto
hence g:‹¬ (K ÷ φ) ∪ {ψ .⟶. φ} ⊢ φ›
using a contract_closure impI_PL by fastforce
then obtain B where h:‹(K ÷ φ) ∪ {ψ .⟶. φ} ⊆ B› and i:‹B ∈ K .⊥. φ›
using upper_remainder[of ‹(K ÷ φ) ∪ {ψ .⟶. φ}› K φ] a True contract_inclusion idempotency_L impI2 by auto
hence j:‹ψ ∉ Cn(B)›
by (metis (no_types, lifting) CollectD mp_PL Un_insert_right a infer_def insert_subset rem rem_closure)
have ‹ψ ∉ K ÷⇘γ⇩A⇩G⇩M⇙ φ›
apply(simp add:mc AGM_sel b, rule_tac x=B in exI)
by (meson Tarskian_logic.assumption_L Tarskian_logic_axioms h i j le_sup_iff)
}
then show ?thesis
using a pmc_inclusion by fastforce
next
case False
hence ‹K .⊥. φ = {K}›
using nonconsequence_remainder taut2emptyrem by auto
then show ?thesis
using False a contract_vacuity idempotency_L pmc_vacuity by auto
qed
qed
qed
lemma contraction_with_completion: ‹K = Cn(A) ⟹ K ÷ φ = K ÷⇘* γ⇩A⇩G⇩M⇙ φ›
by (simp add: contraction_is_pmc pmc_completion)
end
locale TRMC_SC = TransitivelyRelationalMeetContraction + PMC_SC where selection = γ⇩T⇩R
begin
text ‹A transitively relational selection function respect conjuctive overlap.›
lemma rel_sel_conj_overlap: ‹K = Cn(A) ⟹ γ⇩T⇩R K (φ .∧. ψ) ⊆ γ⇩T⇩R K φ ∪ γ⇩T⇩R K ψ›
proof(intro subsetI)
fix B
assume a:‹K = Cn(A)› and b:‹B ∈ γ⇩T⇩R K (φ .∧. ψ)›
show ‹B ∈ γ⇩T⇩R K φ ∪ γ⇩T⇩R K ψ› (is ?A)
proof(cases ‹⊩ φ ∨ ⊩ ψ ∨ ¬ K ⊢ φ ∨ ¬ K ⊢ ψ›, elim disjE)
assume ‹⊩ φ›
hence c:‹Cn({φ .∧. ψ}) = Cn({ψ})›
using conj_equiv valid_Cn_equiv valid_def by blast
from b show ?A
by (metis Un_iff a c extensional_selection)
next
assume ‹⊩ ψ›
hence c:‹Cn({φ .∧. ψ}) = Cn({φ})›
by (simp add: Cn_conj_bis Cn_same validD_L)
from b show ?A
by (metis Un_iff a c extensional_selection)
next
assume ‹¬ K ⊢ φ›
then show ?A
by (metis UnI1 a b conjE1_PL is_selection nonconsequence_remainder nonempty_selection tautology_selection subset_singletonD)
next
assume ‹¬ K ⊢ ψ›
then show ?A
by (metis UnI2 a b conjE2_PL is_selection nonconsequence_remainder nonempty_selection tautology_selection subset_singletonD)
next
assume d:‹¬ (⊩ φ ∨ ⊩ ψ ∨ ¬ K ⊢ φ ∨ ¬ K ⊢ ψ)›
hence h:‹K .⊥. φ ≠ {}› and i:‹K .⊥. ψ ≠ {}› and j:‹K .⊥. (φ .∧. ψ) ≠ {}› and k:"K ⊢ φ .∧. ψ"
using d emptyrem2taut valid_conj_PL apply auto
by (meson Supraclassical_logic.conjI_PL Supraclassical_logic_axioms d)
show ?A
using remainder_conj[OF a k] b h i j rel_sel by auto
qed
qed
text‹A transitively relational meet contraction respect conjuctive overlap.›
lemma trmc_conj_overlap: ‹K = Cn(A) ⟹ (K ÷⇘γ⇩T⇩R⇙ φ) ∩ (K ÷⇘γ⇩T⇩R⇙ ψ) ⊆ (K ÷⇘γ⇩T⇩R⇙ (φ .∧. ψ))›
unfolding mc using rel_sel_conj_overlap by blast
text‹A transitively relational selection function respect conjuctive inclusion›
lemma rel_sel_conj_inclusion: ‹K = Cn(A) ⟹ γ⇩T⇩R K (φ .∧. ψ) ∩ (K .⊥. φ) ≠ {} ⟹ γ⇩T⇩R K φ ⊆ γ⇩T⇩R K (φ .∧. ψ)›
proof(intro subsetI)
fix B
assume a:‹K = Cn(A)› and b:‹γ⇩T⇩R K (φ .∧. ψ) ∩ (K .⊥. φ) ≠ {}› and c:‹B ∈ γ⇩T⇩R K φ›
show ‹B ∈ γ⇩T⇩R K (φ .∧. ψ)› (is ?A)
proof(cases ‹⊩ φ ∨ ⊩ ψ ∨ ¬ K ⊢ φ ∨ ¬ K ⊢ ψ›, auto)
assume ‹⊩ φ›
then show ?A
using b taut2emptyrem by auto
next
assume ‹⊩ ψ›
hence ‹Cn({φ .∧. ψ}) = Cn({φ})›
by (simp add: Cn_conj_bis Cn_same validD_L)
then show ?A
using a c extensional_selection by blast
next
assume d:‹φ ∉ Cn K›
with d show ?A
by (metis Int_emptyI Tarskian_logic.nonconsequence_remainder Tarskian_logic_axioms a b c idempotency_L
inf_bot_right is_selection nonempty_selection singletonD subset_singletonD)
next
assume d:‹ψ ∉ Cn K›
hence e:‹(φ .∧. ψ) ∉ Cn K›
by (meson Supraclassical_logic.conjE2_PL Supraclassical_logic_axioms)
hence f:‹γ⇩T⇩R K (φ .∧. ψ) = {K}›
by (metis Tarskian_logic.nonconsequence_remainder Tarskian_logic_axioms a insert_not_empty is_selection
nonempty_selection subset_singletonD)
with b have g:‹(K .⊥. φ) = {K}›
unfolding nonconsequence_remainder[symmetric] using rem by auto
with d f show ?A
using a c is_selection by fastforce
next
assume d:‹¬ ⊩ φ› and e:‹¬ ⊩ ψ› and f:‹φ ∈ Cn K› and g:‹ψ ∈ Cn K›
hence h:‹K .⊥. φ ≠ {}› and i:‹K .⊥. ψ ≠ {}› and j:‹K .⊥. (φ .∧. ψ) ≠ {}› and k:"K ⊢ φ .∧. ψ"
using e d emptyrem2taut valid_conj_PL apply auto
by (meson Supraclassical_logic.conjI_PL Supraclassical_logic_axioms f g)
have o:‹B ∈ K .⊥. φ ⟹ B ∈ K .⊥. (φ .∧. ψ)› for B
using a k remainder_conj by auto
from b obtain B' where l:‹B' ∈ K .⊥. (φ .∧. ψ)› and m:‹∀C∈K .⊥. (φ .∧. ψ). C ≼⇘K⇙ B'› and n:‹φ ∉ B'›
apply (auto simp add:mc rel_sel j)
using assumption_L rem by force
have p:‹B' ∈ K .⊥. φ›
apply(simp add: rem)
by (metis (no_types, lifting) Supraclassical_logic.conjE1_PL Supraclassical_logic_axioms
Tarskian_logic.rem Tarskian_logic_axioms a l mem_Collect_eq n rem_closure)
from c show ?A
apply (simp add:rel_sel o j h)
using m p trans_rel a by blast
qed
qed
text‹A transitively relational meet contraction respect conjuctive inclusion›
lemma trmc_conj_inclusion: ‹K = Cn(A) ⟹ φ ∉ (K ÷⇘γ⇩T⇩R⇙ (φ .∧. ψ)) ⟹ ((K ÷⇘γ⇩T⇩R⇙ (φ .∧. ψ) ⊆ (K ÷⇘γ⇩T⇩R⇙ φ)))›
proof -
assume a:‹K = Cn(A)› and b:‹φ ∉ (K ÷⇘γ⇩T⇩R⇙ (φ .∧. ψ))›
then obtain B where c:‹B ∈ γ⇩T⇩R K (φ .∧. ψ)› and d:‹¬ B ⊢ φ› apply(simp add:mc)
by (metis b emptyrem2taut is_selection pmc_tautology rem_closure subset_iff validD_L valid_conj_PL)
hence ‹B ∈ (K .⊥. φ)›
using remainder_recovery_bis[OF a _ d, of ‹φ .∧. ψ›]
by (metis (no_types, opaque_lifting) a conj_PL emptyrem2taut insert_not_empty is_selection
nonconsequence_remainder subsetD taut2emptyrem)
with c have e:‹γ⇩T⇩R K (φ .∧. ψ) ∩ (K .⊥. φ) ≠ {}› by blast
then show ‹((K ÷⇘γ⇩T⇩R⇙ (φ .∧. ψ) ⊆ (K ÷⇘γ⇩T⇩R⇙ φ)))›
unfolding mc using rel_sel_conj_inclusion[OF a e] by blast
qed
text‹As a transitively relational meet contraction has been proven to respect all postulates of AGM full contraction
the equivalence between the both are straightforward›
sublocale AGM_FullContraction where contraction = ‹λA φ. A ÷⇘γ⇩T⇩R⇙ φ›
using trmc_conj_inclusion trmc_conj_overlap
by (unfold_locales, simp_all)
end
locale AGMFC_SC = AGM_FullContraction + AGMC_SC
begin
text‹An AGM relation is defined as ?›
definition AGM_relation::‹'a set ⇒ 'a set ⇒ 'a set ⇒ bool›
where AGM_rel: ‹AGM_relation C K B ≡ (C = K ∧ B = K) ∨ ( (∃φ. K ⊢ φ ∧ C ∈ K .⊥. φ)
∧ (∃φ. K ⊢ φ ∧ B ∈ K .⊥. φ ∧ K ÷ φ ⊆ B)
∧ (∀φ. (K ⊢ φ ∧ C ∈ K .⊥. φ ∧ B ∈ K .⊥. φ ∧ K ÷ φ ⊆ C) ⟶ K ÷ φ ⊆ B))›
text‹An AGM relational selection is defined as a function that return @{term ‹K›} if the remainders of @{text ‹K .⊥. φ›} is empty and
the best element of the remainders according to an AGM relation›
definition AGM_relational_selection::‹'a set ⇒ 'a ⇒ 'a set set› (‹γ⇩A⇩G⇩M⇩T⇩R›)
where AGM_rel_sel: ‹γ⇩A⇩G⇩M⇩T⇩R K φ ≡ if (K .⊥. φ) = {}
then {K}
else {B. B∈(K .⊥. φ) ∧ (∀C∈(K .⊥. φ). AGM_relation C K B)}›
lemma AGM_rel_sel_completion: ‹K = Cn(A) ⟹ γ⇩A⇩G⇩M⇩T⇩R K φ = * γ⇩A⇩G⇩M K φ›
apply (unfold AGM_rel_sel, simp add:completion_def split: if_splits)
proof(auto simp add:AGM_sel)
fix S B C
assume a:‹S ∈ Cn(A) .⊥. φ› and b:‹B ∈ Cn(A) .⊥. φ› and c:‹⋂ {B ∈ Cn(A) .⊥. φ. Cn(A) ÷ φ ⊆ B} ⊆ B›
and d:‹C ∈ Cn(A) .⊥. φ›
hence e:‹φ ∉ Cn(A) ÷ φ›
using Tarskian_logic.taut2emptyrem Tarskian_logic_axioms contract_success by fastforce
show ‹AGM_relation C (Cn(A)) B›
proof(cases ‹φ ∈ Cn(A)›)
case True
{ fix ψ
assume ‹Cn A ÷ ψ ⊆ C›
hence ‹Cn A ÷ (φ .∧. ψ) ⊆ Cn A ÷ φ›
using contract_conj_inclusion_variant[of ‹Cn(A)› A φ ψ]
by (metis (mono_tags, lifting) assumption_L contract_conj_inclusion d mem_Collect_eq rem subset_iff)
} note f = this
{ fix ψ φ'
assume g:‹ψ ∈ Cn A ÷ φ'› and h:‹B ∈ Cn A .⊥. φ'› and j:‹Cn A ÷ φ' ⊆ C› and i:‹ψ ∉ B›
hence ‹φ' .∨. ψ ∈ Cn A ÷ φ'›
using Supraclassical_logic.disjI2_PL Supraclassical_logic_axioms contract_closure by fastforce
hence k:‹φ' .∨. ψ ∈ Cn A ÷ φ›
using contract_conj_overlap_variant[of ‹Cn(A)› A φ' φ] f[OF j]
by (metis IntI Supraclassical_logic.disjI1_PL Supraclassical_logic_axioms conj_com_Cn
contract_extensionality inclusion_L singletonI subsetD)
hence l:‹Cn A ÷ φ ⊆ B› using c by auto
from k l have m:‹φ' .∨. ψ ∈ B› and n:‹B =Cn(B)›
using b rem_closure by blast+
have ‹B ∪ {ψ} ⊢ φ'› using g h i
by (simp add:rem) (metis contract_inclusion insertI1 insert_subsetI psubsetI subsetD subset_insertI)
with n m have ‹B ⊢ φ'›
by (metis Cn_equiv assumption_L disjE_PL disj_com equiv_PL imp_PL)
with h have False
using assumption_L rem by auto
} note g = this
with True show ?thesis
apply(unfold AGM_rel, rule_tac disjI2)
using d b c by (auto simp add:AGM_rel idempotency_L del:subsetI) blast+
next
case False
then show ?thesis
by (metis AGM_rel b d idempotency_L infer_def nonconsequence_remainder singletonD)
qed
next
fix S B ψ
assume a:‹S ∈ Cn(A) .⊥. φ› and b:‹B ∈ Cn(A) .⊥. φ› and c:‹∀C∈Cn A .⊥. φ. AGM_relation C (Cn A) B›
and d:‹∀C'. C' ∈ Cn A .⊥. φ ∧ Cn A ÷ φ ⊆ C' ⟶ ψ ∈ C'›
then show ‹ψ ∈ B›
unfolding AGM_rel
by (metis (no_types, lifting) AGM_sel empty_Collect_eq insert_Diff insert_not_empty
nonconsequence_remainder nonempty_selection singletonD)
qed
text‹A transitively relational selection and an AGM relation is a transitively relational meet contraction›
sublocale TransitivelyRelationalMeetContraction where relation = AGM_relation and rel_sel = ‹γ⇩A⇩G⇩M⇩T⇩R›
proof(unfold_locales, simp_all (no_asm) only:atomize_eq, goal_cases)
case a:(1 K A C B' B)
from a(2,3) show ?case
unfolding AGM_rel apply(elim disjE conjE, simp_all)
proof(intro disjI2 allI impI, elim exE conjE, goal_cases)
case (1 ψ _ _ φ)
have b:‹B ∈ K .⊥. (φ .∧. ψ)› and c:‹B' ∈ K .⊥. (φ .∧. ψ)› and d:‹C ∈ K .⊥. (φ .∧. ψ)›
using remainder_conj[OF a(1)] 1 conjI_PL by auto
hence e:‹K ÷ (φ .∧. ψ) ⊆ B›
using contract_conj_inclusion_variant[OF a(1), of φ ψ]
by (meson "1"(1) "1"(12) "1"(16) "1"(2) "1"(3) "1"(8) Supraclassical_logic.conj_PL
Supraclassical_logic_axioms dual_order.trans)
{ fix χ
assume f:‹χ ∈ K ÷ ψ›
have ‹ψ .∨. χ ∈ (K ÷ ψ) ∩ Cn {ψ}›
by (metis Int_iff Supraclassical_logic.disjI1_PL Supraclassical_logic.disjI2_PL Supraclassical_logic_axioms
f a(1) contract_closure in_mono inclusion_L singletonI)
hence g:‹ψ .∨. χ ∈ B›
using contract_conj_overlap_variant[OF a(1), of ψ]
by (metis AGM_Contraction.contract_extensionality AGM_Contraction_axioms a(1) conj_com_Cn e in_mono)
have ‹ψ .⟶. χ ∈ B›
by (metis a(1) "1"(10) "1"(15) "1"(16) assumption_L f in_mono infer_def rem_closure rem_inclusion remainder_recovery)
with g have ‹χ ∈ B›
by (metis 1(15) a(1) disjE_PL infer_def order_refl rem_closure validD_L valid_Cn_imp)
}
then show ?case by blast
qed
next
case (2 K A φ)
hence ‹* γ⇩A⇩G⇩M K φ ≠ {}›
using nonempty_selection[OF 2(1), of φ] selection_completion[OF 2(1), of φ] by blast
then show ?case
using AGM_rel_sel_completion[OF 2(1), of φ] AGM_rel_sel 2(1,2) by force
next
case (3 K φ)
then show ?case using AGM_rel_sel_completion AGM_rel_sel by simp
qed
lemmas fullcontraction_is_pmc = contraction_is_pmc
lemmas fullcontraction_is_trmc = contraction_with_completion
end
locale FMC_SC = FullMeetContraction + TRMC_SC
begin
lemma full_meet_weak1: ‹K = Cn(A) ⟹ K ⊢ φ ⟹ (K ÷⇘γ⇩F⇩C⇙ φ) = K ∩ Cn({.¬ φ})›
proof(intro subset_antisym Int_greatest)
assume a:‹K = Cn(A)› and b:‹K ⊢ φ›
then show ‹ (K ÷⇘γ⇩F⇩C⇙ φ) ⊆ K›
by (simp add: Inf_less_eq full_sel mc rem_inclusion)
next
assume a:‹K = Cn(A)› and b:‹K ⊢ φ›
show ‹(K ÷⇘γ⇩F⇩C⇙ φ) ⊆ Cn({.¬ φ})›
proof
fix ψ
assume c:‹ψ ∈ (K ÷⇘γ⇩F⇩C⇙ φ)›
{ assume ‹¬ {.¬ φ} ⊢ ψ›
hence ‹¬ {.¬ ψ} ⊢ φ›
by (metis Un_insert_right insert_is_Un not_PL notnot_PL)
hence ‹¬ {φ .∨. .¬ ψ} ⊢ φ›
by (metis assumption_L disjI2_PL singleton_iff transitivity2_L)
then obtain B where d:‹{φ .∨. .¬ ψ} ⊆ B› and e:‹B ∈ K .⊥. φ›
by (metis a b disjI1_PL empty_subsetI idempotency_L infer_def insert_subset upper_remainder)
hence f:‹¬ ψ ∈ B›
by (metis (no_types, lifting) CollectD assumption_L insert_subset disj_notE_PL rem)
hence ‹¬ ψ ∈ (K ÷⇘γ⇩F⇩C⇙ φ)›
using e mc full_sel by auto
}
then show ‹ψ ∈ Cn({.¬ φ})›
using c infer_def by blast
qed
next
assume a:‹K = Cn(A)› and b:‹K ⊢ φ›
show ‹K ∩ Cn({.¬ φ}) ⊆ (K ÷⇘γ⇩F⇩C⇙ φ)›
proof(safe)
fix ψ
assume c:‹ψ ∈ K› and d: ‹ψ ∈ Cn {.¬ φ}›
have e:‹B ⊢ .¬ φ .⟶. ψ› for B
by (simp add: d validD_L valid_imp_PL)
{ fix B
assume f:‹B ∈ K .⊥. φ›
hence ‹B ⊢ φ .⟶. ψ›
using a assumption_L c remainder_recovery by auto
then have f:‹B ⊢ ψ› using d e
using disjE_PL ex_mid_PL by blast
}
then show ‹ψ ∈ (K ÷⇘γ⇩F⇩C⇙ φ)›
apply(simp_all add:mc c full_sel)
using a rem_closure by blast
qed
qed
lemma full_meet_weak2:‹K = Cn(A) ⟹ K ⊢ φ ⟹ Cn((K ÷⇘γ⇩F⇩C⇙ φ) ∪ {.¬ φ}) = Cn({.¬ φ})›
unfolding full_meet_weak1
by (metis Cn_union idempotency_L inf.cobounded2 sup.absorb_iff2 sup_commute)
end
end