Theory Disjunctive_Consequence_Relations
theory Disjunctive_Consequence_Relations
imports Saturation_Framework.Calculus
Propositional_Proof_Systems.Compactness
"HOL-Library.Library"
"HOL-Library.Product_Lexorder"
Lazy_List_Limsup
FSet_Extra
begin
section ‹Disjunctive Consequence Relations›
no_notation Sema.formula_semantics (infix "⊨" 51)
locale consequence_relation =
fixes
bot :: "'f" and
entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50)
assumes
bot_entails_empty: "{bot} ⊨ {}" and
entails_reflexive: "{C} ⊨ {C}" and
entails_subsets: "M' ⊆ M ⟹ N' ⊆ N ⟹ M' ⊨ N' ⟹ M ⊨ N" and
entails_cut: "M ⊨ N ∪ {C} ⟹ M' ∪ {C} ⊨ N' ⟹ M ∪ M'⊨ N ∪ N'" and
entails_compactness: "M ⊨ N ⟹ ∃ M' N'. (M' ⊆ M ∧ N' ⊆ N ∧ finite M' ∧ finite N' ∧ M' ⊨ N')"
begin
definition order_double_subsets :: "('f set * 'f set) ⇒ ('f set * 'f set) ⇒ bool"
(infix "≼⇩s" 50) where
‹(≼⇩s) ≡ λC1 C2. fst C1 ⊆ fst C2 ∧ snd C1 ⊆ snd C2›
definition order_double_subsets_strict :: "('f set * 'f set) ⇒ ('f set * 'f set) ⇒ bool"
(infix "≺⇩s" 50) where
‹(≺⇩s) ≡ λC1 C2. C1 ≼⇩s C2 ∧ C1 ≠ C2›
lemma trivial_induction_order : ‹C1 ⊆ B ∧ C2 ⊆ B' ⟶ (C1,C2) ≼⇩s (B,B')›
unfolding order_double_subsets_def
by simp
lemma zorn_relation_trans : ‹∀C1 C2 C3. (C1 ≼⇩s C2) ⟶ (C2 ≼⇩s C3) ⟶ (C1 ≼⇩s C3)›
proof -
have ‹∀C1 C2 C3. fst C1 ⊆ fst C2 ⟶ fst C2 ⊆ fst C3 ⟶ fst C1 ⊆ fst C3›
by blast
then have ‹∀C1 C2 C3. snd C1 ⊆ snd C2 ⟶ snd C2 ⊆ snd C3 ⟶ snd C1 ⊆ snd C3›
by blast
then show ?thesis
unfolding order_double_subsets_def
by auto
qed
lemma zorn_strict_relation_trans :
‹∀(C1::'f set × 'f set) C2 C3. (C1 ≺⇩s C2) ⟶ (C2 ≺⇩s C3) ⟶ (C1 ≺⇩s C3)›
by (metis order_double_subsets_def order_double_subsets_strict_def prod.expand subset_antisym
zorn_relation_trans)
lemma zorn_relation_antisym : ‹∀C1 C2. (C1 ≼⇩s C2) ⟶ (C2 ≼⇩s C1) ⟶ (C1 = C2)›
proof -
have ‹∀C1 C2. (fst C1 ⊆ fst C2) ⟶ (fst C2 ⊆ fst C1) ⟶ (fst C1 = fst C2)›
by force
then have ‹∀C1 C2. (snd C1 ⊆ snd C2) ⟶ (snd C2 ⊆ snd C1) ⟶ (snd C1 = snd C2)›
by force
then show ?thesis
unfolding order_double_subsets_def
using dual_order.eq_iff
by auto
qed
lemma entails_supsets : "(∀M' N'. (M' ⊇ M ∧ N' ⊇ N ∧ M' ∪ N' = UNIV) ⟶ M' ⊨ N') ⟹ M ⊨ N"
proof (rule ccontr)
assume
not_M_entails_N : ‹¬M ⊨ N› and
hyp_entails_sup : ‹(∀M' N'. (M' ⊇ M ∧ N' ⊇ N ∧ M' ∪ N' = UNIV) ⟶ M' ⊨ N')›
have contrapos_hyp_entails_sup: ‹∃M' N'. (M' ⊇ M ∧ N' ⊇ N ∧ M' ∪ N' = UNIV) ∧ ¬M' ⊨ N'›
proof -
define A :: "('f set * 'f set) set" where ‹A = {(M',N'). M ⊆ M' ∧ N ⊆ N' ∧ ¬M' ⊨ N'}›
define zorn_relation :: "(('f set * 'f set) × ('f set * 'f set)) set" where
‹zorn_relation = {(C1,C2) ∈ A × A. C1≼⇩sC2}›
define max_chain :: "('f set * 'f set) set ⇒ 'f set * 'f set" where
‹max_chain = (λC. if C = {} then (M,N)
else (⋃{C1. ∃C2. (C1,C2) ∈ C},⋃{C2. ∃C1. (C1,C2) ∈ C}))›
have relation_in_A : ‹⋀C. C ∈ Chains zorn_relation ⟹ ∀ C1 ∈ C. C1 ∈ A›
using in_ChainsD zorn_relation_def
by (metis (no_types, lifting) mem_Collect_eq mem_Sigma_iff old.prod.case)
have M_N_in_A : ‹(M,N) ∈ A›
using not_M_entails_N A_def by simp
then have not_empty_A : ‹A≠{}›
by force
have trivial_replacement_order [simp] : ‹∀C1 C2. (C1,C2) ∈ zorn_relation ⟶ (C1 ≼⇩s C2)›
unfolding zorn_relation_def by force
moreover have zorn_relation_refl : ‹∀C∈A. C ≼⇩s C›
proof -
have ‹∀C∈A. fst C ⊆ fst C ∧ snd C ⊆ snd C›
by blast
then show ?thesis
unfolding order_double_subsets_def
by simp
qed
moreover have refl_on_zorn_relation : "refl_on A zorn_relation"
using zorn_relation_refl
by (smt (verit, ccfv_SIG) case_prod_conv mem_Collect_eq mem_Sigma_iff refl_onI
subrelI zorn_relation_def)
moreover have zorn_relation_field_is_A : "Field zorn_relation = A"
proof -
have ‹∀ C0 ∈ A. (M,N) ≼⇩s C0›
unfolding order_double_subsets_def
using A_def by simp
then have ‹∀ C0 ∈ A. ((M,N),C0) ∈ zorn_relation›
unfolding zorn_relation_def
using M_N_in_A by simp
then have "A ⊆ Range zorn_relation"
unfolding Range_def by fast
moreover have ‹∀C0. C0 ∈ (Range zorn_relation) ⟶ C0 ∈ A›
unfolding Range_iff using refl_on_zorn_relation zorn_relation_def by blast
moreover have ‹∀C0. C0 ∈ (Domain zorn_relation) ⟶ C0 ∈ A›
using zorn_relation_def by blast
ultimately show ?thesis
by (metis Field_def Un_absorb1 subrelI subset_antisym)
qed
ultimately have zorn_hypothesis_po: "Partial_order zorn_relation"
proof -
have antisym_zorn_relation : "antisym zorn_relation"
proof -
have ‹∀C1 C2. (C1,C2) ∈ zorn_relation ∧ (C2,C1) ∈ zorn_relation ⟶ (C1 ≼⇩s C2) ∧ (C2 ≼⇩s C1)›
by force
then show ?thesis using zorn_relation_antisym
by (meson antisymI)
qed
moreover have "trans zorn_relation"
proof -
have ‹∀C1 C2 C3. (C1,C2) ∈ zorn_relation
⟶ (C2,C3) ∈ zorn_relation ⟶ (C1 ≼⇩s C2) ⟶ (C2 ≼⇩s C3)›
unfolding zorn_relation_def by blast
then have ‹∀C1∈A. ∀C2∈A. (C1 ≼⇩s C2) ⟶ (C1,C2) ∈ zorn_relation›
unfolding zorn_relation_def by blast
then show ?thesis using zorn_relation_trans
by (metis (no_types, opaque_lifting) FieldI1 FieldI2 transI
trivial_replacement_order zorn_relation_field_is_A zorn_relation_trans)
qed
ultimately have "preorder_on A zorn_relation"
unfolding preorder_on_def refl_on_zorn_relation
using refl_on_zorn_relation
using zorn_relation_def by blast
then have "partial_order_on A zorn_relation"
unfolding partial_order_on_def
using antisym_zorn_relation by simp
moreover have zorn_relation_field : "Field zorn_relation = A"
proof -
have ‹∀ C0 ∈ A. (M,N) ≼⇩s C0›
unfolding order_double_subsets_def
using A_def by simp
then have ‹∀ C0 ∈ A. ((M,N),C0) ∈ zorn_relation›
unfolding zorn_relation_def
using M_N_in_A by simp
then have "A ⊆ Range zorn_relation"
unfolding Range_def by fast
moreover have ‹∀C0. C0 ∈ (Range zorn_relation) ⟶ C0 ∈ A›
unfolding Range_iff using refl_on_zorn_relation zorn_relation_def by blast
moreover have ‹∀C0. C0 ∈ (Domain zorn_relation) ⟶ C0 ∈ A›
using zorn_relation_def by blast
ultimately show ?thesis
by (metis Field_def Un_absorb1 subrelI subset_antisym)
qed
show ?thesis using zorn_relation_field calculation by simp
qed
have max_chain_is_a_max : ‹⋀C. C ∈ Chains zorn_relation ⟹ ∀C1∈C. (C1 ≼⇩s max_chain C)›
proof -
fix C
assume C_is_a_chain : ‹C ∈ Chains zorn_relation›
consider (a) "C = {}" | (b) "C ≠ {}"
by auto
then show ‹∀ C1 ∈ C. C1 ≼⇩s max_chain C›
proof cases
case a
show ?thesis by (simp add: a)
next
case b
have ‹C ⊆ A›
using C_is_a_chain relation_in_A by blast
then have ‹∀ C1 ∈ C. ∃ (C2,C3) ∈ C. C1 = (C2,C3)›
by blast
moreover have ‹∀ (C1,C2) ∈ C. C1 ⊆ ⋃{C3. ∃ C4. (C3,C4) ∈ C}›
by blast
moreover have ‹∀ (C1,C2) ∈ C. C2 ⊆ ⋃{C4. ∃ C3. (C3,C4) ∈ C}›
by blast
moreover have ‹∀ (C1,C2) ∈ C.
((C1 ⊆ ⋃{C3. ∃ C4. (C3,C4) ∈ C} ∧ C2 ⊆ ⋃{C4. ∃ C3. (C3,C4) ∈ C}) ⟶
(C1,C2) ≼⇩s (⋃{C3. ∃ C4. (C3,C4) ∈ C}, ⋃{C4. ∃ C3. (C3,C4) ∈ C}))›
unfolding order_double_subsets_def
using trivial_induction_order
by simp
ultimately have ‹∀ (C1,C2) ∈ C.
(C1,C2) ≼⇩s (⋃{C3. ∃ C4. (C3,C4) ∈ C},⋃{C4. ∃ C3. (C3,C4) ∈ C})›
by fastforce
then have ‹∀ (C1,C2) ∈ C. (C1,C2) ≼⇩s max_chain C›
unfolding max_chain_def
by simp
then show ‹∀ C1 ∈ C. C1 ≼⇩s max_chain C›
by fast
qed
qed
have M_N_less_than_max_chain : ‹⋀C. C ∈ Chains zorn_relation ⟹ (M,N) ≼⇩s max_chain C›
proof -
fix C
assume C_chain : ‹C ∈ Chains zorn_relation›
consider (a) "C = {}" | (b) "C ≠ {}"
by blast
then show ‹(M,N) ≼⇩s max_chain C›
proof cases
case a
assume "C = {}"
then have ‹max_chain C = (M,N)›
unfolding max_chain_def
by simp
then show ‹(M,N) ≼⇩s max_chain C›
using M_N_in_A zorn_relation_refl
by simp
next
case b
assume C_not_empty : "C ≠ {}"
have M_minor_first : ‹∀ C1 ∈ C. M ⊆ fst C1›
using A_def C_chain relation_in_A by fastforce
have N_minor_second : ‹∀ C1 ∈ C. N ⊆ snd C1›
using A_def C_chain relation_in_A by fastforce
moreover have ‹(∀ C1 ∈ C. (fst C1 ⊆ fst (max_chain C)) ∧ snd C1 ⊆ snd (max_chain C))›
using order_double_subsets_def C_chain max_chain_is_a_max
by presburger
moreover have ‹(∃C1 ∈ C. (M ⊆ fst C1 ∧ N ⊆ snd C1)
⟶ fst C1 ⊆ fst (max_chain C) ∧ snd C1 ⊆ snd (max_chain C))
⟶ M ⊆ fst (max_chain C) ∧ N ⊆ snd (max_chain C)›
using M_minor_first N_minor_second
by blast
ultimately have ‹M ⊆ fst (max_chain C) ∧ N ⊆ snd (max_chain C)›
by (meson order_double_subsets_def C_chain C_not_empty ex_in_conv max_chain_is_a_max)
then show ‹(M,N) ≼⇩s max_chain C›
unfolding order_double_subsets_def
by simp
qed
qed
moreover have left_U_not_entails_right_U:
‹⋀C. C ∈ Chains zorn_relation ⟹ ¬ fst (max_chain C)⊨ snd (max_chain C)›
proof -
fix C
assume C_chain :‹C ∈ Chains zorn_relation›
consider (a) "C = {}" | (b) "C ≠ {}"
by fast
then show ‹¬ fst (max_chain C)⊨ snd (max_chain C)›
proof cases
case a
then show ?thesis using not_M_entails_N
unfolding max_chain_def
by simp
next
case b
assume C_not_empty :‹C ≠ {}›
show ?thesis
proof (rule ccontr)
assume ‹¬¬fst (max_chain C) ⊨ snd (max_chain C)›
then have abs_fst_entails_snd : ‹fst (max_chain C) ⊨ snd (max_chain C)›
by auto
then obtain M' N' where
abs_max_chain_compactness : ‹M' ⊆ fst (max_chain C)
∧ N' ⊆ snd (max_chain C)
∧ finite M'
∧ finite N'
∧ M' ⊨ N'›
using entails_compactness by fastforce
then have not_empty_M'_or_N' : ‹(M' ≠ {}) ∨ (N' ≠ {})›
by (meson empty_subsetI entails_subsets not_M_entails_N)
then have finite_M'_subset : ‹(finite M') ∧ M' ⊆ ⋃{C1. ∃C2. (C1,C2) ∈ C}›
using C_not_empty abs_max_chain_compactness max_chain_def
by simp
then have M'_in_great_union : ‹M' ⊆ ⋃{C1. ∃C2. (C1,C2) ∈ C ∧ C1 ∩ M' ≠ {}}›
by blast
then have M'_in_finite_union :
‹∃P ⊆ {C1. ∃C2. (C1,C2) ∈ C ∧ C1 ∩ M' ≠ {}}. finite P ∧ M' ⊆ ⋃P›
by (meson finite_M'_subset finite_subset_Union)
moreover have finite_N'_subset : ‹(finite N') ∧ N' ⊆ ⋃{C2. ∃C1. (C1,C2) ∈ C}›
using C_not_empty abs_max_chain_compactness
using max_chain_def
by simp
then have N'_in_great_union : ‹N' ⊆ ⋃{C2. ∃C1. (C1,C2) ∈ C ∧ C2 ∩ N' ≠ {}}›
by blast
then have N'_in_finite_union :
‹∃Q ⊆ {C2. ∃C1. (C1,C2) ∈ C ∧ C2 ∩ N' ≠ {}}. finite Q ∧ N' ⊆ ⋃Q›
by (meson finite_N'_subset finite_subset_Union)
ultimately obtain P Q where
P_subset : ‹P ⊆ {C1. ∃C2. (C1,C2) ∈ C ∧ C1 ∩ M' ≠ {}}› and
finite_P: ‹finite P› and
P_supset : ‹M' ⊆ ⋃P› and
Q_subset : ‹Q ⊆ {C2. ∃C1. (C1,C2) ∈ C ∧ C2 ∩ N' ≠ {}}›
and finite_Q : ‹finite Q› and Q_supset : ‹N' ⊆ ⋃Q›
by auto
have not_empty_P_or_Q : ‹P ≠ {} ∨ Q ≠ {}›
using not_empty_M'_or_N' P_supset Q_supset by blast
have P_linked_C : ‹∀C1∈P. ∃C2. (C1,C2)∈C›
using P_subset by auto
then have Q_linked_C : ‹∀C2∈Q. ∃C1. (C1,C2)∈C›
using Q_subset by auto
then have ‹∃𝒫 ⊆ C. 𝒫 = {(C1,C2). (C1,C2) ∈ C ∧ C1 ∈ P}›
by fastforce
then obtain 𝒫 where
𝒫_def: ‹𝒫 = {(C1,C2). (C1,C2) ∈ C ∧ C1 ∈ P}›
by auto
then have 𝒫_in_C : ‹𝒫 ⊆ C›
by auto
have P_linked_𝒫 : ‹∀C1∈P. ∃C2. (C1,C2)∈𝒫›
using P_linked_C 𝒫_def
by simp
define f where
‹f = (λC1. if (∃C2. (C1,C2)∈𝒫) then (SOME C2. (C1,C2) ∈ 𝒫) else {})›
have ‹∀(C1,C2)∈𝒫. C1∈P›
using 𝒫_def by blast
have f_stability_in_𝒫 : ‹⋀ C1 C2. (C1,C2)∈𝒫 ⟹ (C1, f C1)∈𝒫›
proof -
fix C1 C2
show ‹(C1,C2)∈𝒫 ⟹ (C1, f C1)∈𝒫›
proof -
assume C1_C2_in_𝒫 : ‹(C1,C2)∈𝒫›
then have ‹∃C3. (C1,C3)∈𝒫›
by blast
then have ‹(C1, f C1) = (C1, SOME C3. (C1,C3) ∈ 𝒫)›
unfolding f_def by simp
then have ‹(C1, f C1)∈𝒫›
by (metis C1_C2_in_𝒫 someI_ex)
then show ‹(C1,C2)∈𝒫 ⟹ (C1, f C1)∈𝒫› by blast
qed
qed
define 𝒫' where
‹𝒫' = {(C1, f C1)|C1. ∃C2. (C1,C2)∈𝒫}›
then have injectivity_𝒫' : ‹∀C1 C2 C2'.(((C1, C2) ∈ 𝒫' ∧ (C1, C2') ∈ 𝒫') ⟶ C2 = C2')›
by auto
have 𝒫'_in_𝒫 : ‹𝒫' ⊆ 𝒫›
unfolding 𝒫'_def
using f_stability_in_𝒫
by blast
then have 𝒫'_in_C : ‹𝒫' ⊆ C›
using 𝒫_in_C
by blast
have 𝒫'_less_than_P : ‹∀C0 ∈ 𝒫'. fst C0∈P›
unfolding 𝒫'_def 𝒫_def by fastforce
have P_less_than_𝒫 : ‹∀C1 ∈ P. ∃C2. (C1,C2)∈𝒫›
unfolding 𝒫_def
using P_linked_C by simp
then have P_less_than_𝒫_reformulated : ‹∀C1 ∈ P. ∃C0∈𝒫'. (fst C0) = C1›
unfolding 𝒫'_def
by simp
then have union_P_in_union_fst_𝒫' : ‹⋃P ⊆ ⋃{C1. ∃C0 ∈ 𝒫'. (fst C0) = C1}›
using Union_mono subsetI
by fastforce
have injectivity_𝒫'_reformulated :
‹∀C0 C0'. ((C0 ∈ 𝒫' ∧ C0' ∈ 𝒫' ∧ C0' ≠ C0) ⟶ (fst C0) ≠ (fst C0'))›
unfolding 𝒫'_def
by force
define bij_𝒫':: "('f set × 'f set) ⇒ 'f set" where
‹bij_𝒫' ≡ fst›
have injectivity_bij_𝒫' : ‹∀C0∈𝒫'. ∀C0'∈𝒫'. bij_𝒫' C0 = bij_𝒫' C0' ⟶ C0 = C0'›
unfolding bij_𝒫'_def
using injectivity_𝒫'_reformulated by blast
then have bij_𝒫'_injectivity : ‹inj_on bij_𝒫' 𝒫'›
unfolding inj_on_def
by simp
moreover have surjectivity_bij_𝒫'_first_inc : ‹bij_𝒫' ` 𝒫' ⊆ P›
unfolding bij_𝒫'_def
using 𝒫'_less_than_P image_subset_iff by auto
moreover have surjectivity_bij_𝒬'_second_inc : ‹P ⊆ bij_𝒫' ` 𝒫'›
unfolding bij_𝒫'_def
using P_less_than_𝒫_reformulated by auto
ultimately have surjectivity_bij_𝒫' : ‹bij_𝒫' ` 𝒫' = P›
by blast
then have bij : ‹bij_betw bij_𝒫' 𝒫' P›
unfolding bij_betw_def
using bij_𝒫'_injectivity by simp
then have finite_𝒫' : ‹finite 𝒫'›
using bij_𝒫'_injectivity finite_P inj_on_finite surjectivity_bij_𝒫'_first_inc by auto
moreover have ‹∃𝒬 ⊆ C. 𝒬 = {(C1,C2). (C1,C2) ∈ C ∧ C2 ∈ Q}›
by fastforce
then obtain 𝒬 where
𝒬_def: ‹𝒬 = {(C1,C2). (C1,C2) ∈ C ∧ C2 ∈ Q}›
by auto
then have 𝒬_in_C : ‹𝒬 ⊆ C›
by auto
define g where
‹g = (λC2. if (∃C1. (C1,C2)∈𝒬) then (SOME C1. (C1,C2) ∈ 𝒬) else {})›
have ‹∀(C1,C2)∈𝒬. C2∈Q›
using 𝒬_def by blast
have g_stability_in_𝒬 : ‹⋀ C1 C2. (C1,C2)∈𝒬 ⟹ (g C2, C2)∈𝒬›
proof -
fix C1 C2
show ‹(C1,C2)∈𝒬 ⟹ (g C2, C2)∈𝒬›
proof -
assume C1_C2_in_𝒬 : ‹(C1,C2)∈𝒬›
then have ‹∃C3. (C3,C2)∈𝒬›
by blast
then have ‹(g C2, C2) = ((SOME C1. (C1,C2) ∈ 𝒬), C2)›
unfolding g_def by simp
then have ‹(g C2, C2)∈𝒬›
by (metis C1_C2_in_𝒬 someI_ex)
then show ‹(C1,C2)∈𝒬 ⟹ (g C2, C2)∈𝒬› by blast
qed
qed
define 𝒬' where
‹𝒬' = {(g C2, C2)|C2. ∃C1. (C1,C2)∈𝒬}›
then have injectivity_𝒬' : ‹∀C1 C2 C1'.(((C1, C2) ∈ 𝒬' ∧ (C1', C2) ∈ 𝒬') ⟶ C1 = C1')›
by auto
have 𝒬'_in_𝒬 : ‹𝒬' ⊆ 𝒬›
unfolding 𝒬'_def
using g_stability_in_𝒬
by blast
then have 𝒬'_in_C : ‹𝒬' ⊆ C›
using 𝒬_in_C
by blast
have 𝒬'_less_than_Q : ‹∀C0 ∈ 𝒬'. snd C0∈Q›
unfolding 𝒬'_def 𝒬_def by fastforce
have Q_less_than_𝒬 : ‹∀C2 ∈ Q. ∃C1. (C1,C2)∈𝒬›
unfolding 𝒬_def
using Q_linked_C by simp
then have Q_less_than_𝒬_reformulated :‹∀C2 ∈ Q. ∃C0∈𝒬'. (snd C0) = C2›
unfolding 𝒬'_def
by simp
then have union_Q_in_union_fst_𝒬' : ‹⋃Q ⊆ ⋃{C2. ∃C0 ∈ 𝒬'. (snd C0) = C2}›
using Union_mono subsetI
by fastforce
have injectivity_𝒬'_reformulated :
‹∀C0 C0'. ((C0 ∈ 𝒬' ∧ C0' ∈ 𝒬' ∧ C0' ≠ C0) ⟶ (snd C0) ≠ (snd C0'))›
unfolding 𝒬'_def
by force
define bij_𝒬':: "('f set × 'f set) ⇒ 'f set" where
‹bij_𝒬' ≡ snd›
have injectivity_bij_𝒬' : ‹∀C0∈𝒬'. ∀C0'∈𝒬'. bij_𝒬' C0 = bij_𝒬' C0' ⟶ C0 = C0'›
unfolding bij_𝒬'_def
using injectivity_𝒬'_reformulated by blast
then have bij_𝒬'_injectivity : ‹inj_on bij_𝒬' 𝒬'›
unfolding inj_on_def
by simp
moreover have surjectivity_bij_𝒬'_first_inc : ‹bij_𝒬' ` 𝒬' ⊆ Q›
unfolding bij_𝒬'_def
using 𝒬'_less_than_Q image_subset_iff by auto
moreover have surjectivity_bij_𝒬'_second_inc : ‹Q ⊆ bij_𝒬' ` 𝒬'›
unfolding bij_𝒬'_def
using Q_less_than_𝒬_reformulated by auto
ultimately have surjectivity_bij_𝒬' : ‹bij_𝒬' ` 𝒬' = Q›
by blast
then have bij : ‹bij_betw bij_𝒬' 𝒬' Q›
unfolding bij_betw_def
using bij_𝒬'_injectivity by simp
then have finite_𝒬' : ‹finite 𝒬'›
using bij_𝒬'_injectivity finite_Q inj_on_finite surjectivity_bij_𝒬'_first_inc by auto
have not_empty_𝒫_or_𝒬 : ‹𝒫 ≠ {} ∨ 𝒬 ≠ {}›
using 𝒫'_in_𝒫 𝒬'_in_𝒬 surjectivity_bij_𝒫' surjectivity_bij_𝒬' not_empty_P_or_Q
by fastforce
then have not_empty_𝒫'_or_𝒬' : ‹𝒫' ≠ {} ∨ 𝒬' ≠ {}›
using not_empty_P_or_Q surjectivity_bij_𝒫' surjectivity_bij_𝒬' by blast
define ℛ' where ‹ℛ' = 𝒫'∪𝒬'›
have ‹∀ (C1,C2) ∈ ℛ'. C1∈P ∨ C2∈Q›
unfolding ℛ'_def 𝒫'_def 𝒬'_def 𝒫_def 𝒬_def
by fastforce
have finite_ℛ' : ‹finite ℛ'›
unfolding ℛ'_def
using finite_𝒫' finite_𝒬' by simp
moreover have ℛ'_in_C : ‹ℛ' ⊆ C›
unfolding ℛ'_def
using 𝒫'_in_C 𝒬'_in_C
by blast
moreover have not_empty_ℛ' : ‹ℛ' ≠ {}›
using ℛ'_def not_empty_𝒫'_or_𝒬' by blast
have max_ℛ' : ‹∃(M0,N0)∈ℛ'. (∀(M,N)∈ℛ'. (M,N) ≼⇩s (M0,N0))›
proof (rule ccontr)
assume ‹¬(∃(M0,N0)∈ℛ'. (∀(M,N)∈ℛ'. (M,N) ≼⇩s (M0,N0)))›
then have abs_max_ℛ' : ‹∀(M0,N0)∈ℛ'. (∃(M,N)∈ℛ'. ¬((M,N) ≼⇩s (M0,N0)))›
by auto
have ‹∀(M0,N0)∈C. ∀(M,N)∈C.
¬((M,N),(M0,N0))∈zorn_relation ⟶ ((M0,N0),(M,N))∈zorn_relation›
unfolding zorn_relation_def
using C_chain
by (smt (verit, best) Chains_def case_prodI2 mem_Collect_eq zorn_relation_def)
then have ‹∀(M0,N0)∈C. ∀(M,N)∈C. ¬(M,N) ≼⇩s (M0,N0) ⟶ (M0,N0) ≼⇩s (M,N)›
unfolding zorn_relation_def
using trivial_replacement_order
by blast
then have ‹∀(M0,N0)∈ℛ'. ∀(M,N)∈ℛ'. ¬(M,N) ≼⇩s (M0,N0) ⟶ (M0,N0) ≼⇩s (M,N)›
using ℛ'_in_C
by auto
then have ‹∀(M0,N0)∈ℛ'. ∀(M,N)∈ℛ'. ¬(M,N) ≼⇩s (M0,N0) ⟶ (M0,N0) ≺⇩s (M,N)›
unfolding order_double_subsets_strict_def
by blast
then have abs_max_ℛ'_reformulated : ‹∀(M0,N0)∈ℛ'. (∃(M,N)∈ℛ'. (M0,N0) ≺⇩s (M,N))›
using abs_max_ℛ'
by blast
define find_dif :: "('f set × 'f set) ⇒ ('f set × 'f set)" where
‹find_dif = (λ(M0,N0). if (∃(M,N)∈ℛ'. (M0,N0) ≺⇩s (M,N))
then (SOME (M,N). (M,N)∈ℛ' ∧ (M0,N0) ≺⇩s (M,N))
else ({},{}))›
obtain M0 N0 where M0_N0_def : ‹(M0,N0)∈ ℛ'›
using not_empty_ℛ' by auto
define bij_nat :: "nat ⇒ ('f set × 'f set)" where
‹bij_nat ≡ λk. (find_dif^^k) (M0, N0)›
have bij_nat_in_ℛ' : ‹bij_nat k ∈ ℛ'› for k
proof (induction k)
case 0
then show ?case
unfolding bij_nat_def
using M0_N0_def
by simp
next
case (Suc k)
assume ‹bij_nat k ∈ ℛ'›
have new_major_k : ‹∃(M,N)∈ℛ'. bij_nat k ≺⇩s (M,N)›
using abs_max_ℛ'_reformulated Suc
by simp
then have ‹find_dif (bij_nat k) = (SOME (M,N). (M,N)∈ℛ' ∧ bij_nat k ≺⇩s (M,N))›
unfolding find_dif_def
by auto
then have ‹bij_nat (Suc k) = (SOME (M,N). (M,N)∈ℛ' ∧ bij_nat k ≺⇩s (M,N))›
unfolding bij_nat_def
by simp
then show ?case
by (metis (mono_tags, lifting) new_major_k case_prod_conv some_eq_imp surj_pair)
qed
then have new_major_general : ‹∃(M,N)∈ℛ'. (bij_nat k) ≺⇩s (M,N)› for k
using abs_max_ℛ'_reformulated
by simp
then have ‹find_dif (bij_nat k) = (SOME (M,N). (M,N)∈ℛ' ∧ bij_nat k ≺⇩s (M,N))› for k
unfolding find_dif_def
by auto
then have ‹bij_nat k ≺⇩s find_dif (bij_nat k)› for k
by (metis (mono_tags, lifting) case_prod_conv new_major_general some_eq_imp surj_pair)
then have bij_nat_croiss: ‹(bij_nat (k::nat)) ≺⇩s (bij_nat (Suc k))› for k
using bij_nat_def by simp
have bij_nat_general_croiss : ‹i < j ⟹ bij_nat i ≺⇩s bij_nat j› for i j
proof -
assume hyp_croiss : ‹i < j›
have ‹bij_nat i ≺⇩s bij_nat (i+1+(k::nat))› for k
proof (induction k)
case 0
then show ?case using bij_nat_croiss by simp
next
case (Suc k)
have ‹bij_nat (i+1+k) ≺⇩s bij_nat (i+1+(Suc k))›
using bij_nat_croiss by simp
then show ?case using zorn_strict_relation_trans Suc by blast
qed
then have ‹bij_nat i ≺⇩s bij_nat j›
by (metis Suc_eq_plus1_left hyp_croiss add.assoc add.commute less_natE)
then show ?thesis by simp
qed
have ‹bij_nat i = bij_nat j ∧ ¬i=j ⟹ False› for i j
proof -
assume bij_nat_i_equals_bij_nat_j : ‹bij_nat i = bij_nat j ∧ ¬i=j›
then have ‹i < j ∨ j < i›
by auto
then have ‹bij_nat i ≺⇩s bij_nat j ∨ bij_nat j ≺⇩s bij_nat i›
using bij_nat_general_croiss
by blast
then have ‹bij_nat i ≠ bij_nat j›
unfolding order_double_subsets_strict_def
by force
then show ?thesis
using bij_nat_i_equals_bij_nat_j by simp
qed
then have bij_nat_inj : ‹bij_nat i = bij_nat j ⟶ i = j› for i j
unfolding bij_nat_def
by auto
then have bij_nat_inj_gen : ‹∀ i j. bij_nat i = bij_nat j ⟶ i = j›
by auto
then have ‹inj_on bij_nat (UNIV :: nat set)›
unfolding inj_on_def
by simp
then have bij_nat_is_a_bij :
‹bij_betw bij_nat (UNIV :: nat set) (bij_nat `(UNIV :: nat set))›
unfolding bij_betw_def
by simp
then have ‹finite (UNIV :: nat set) ⟷ finite (bij_nat `(UNIV:: nat set))›
using bij_betw_finite by auto
moreover have ‹¬(finite (UNIV :: nat set))›
by simp
ultimately have ‹¬finite (bij_nat `(UNIV:: nat set))›
by blast
moreover have ‹bij_nat `(UNIV:: nat set) ⊆ ℛ'›
unfolding bij_nat_def
using ℛ'_in_C bij_nat_in_ℛ' image_subset_iff bij_nat_def
by blast
ultimately have ‹¬(finite ℛ')›
using finite_subset by blast
then show "False" using finite_ℛ' by blast
qed
then obtain M_max N_max where
M_N_max_def : ‹(M_max,N_max)∈ℛ' ∧ (∀(M,N)∈ℛ'. (M,N) ≼⇩s (M_max,N_max))›
by auto
then have ‹∀C1∈P. ∃(M0,N0)∈ℛ'. M0 = C1 ›
using ℛ'_def P_less_than_𝒫_reformulated by fastforce
then have ‹⋃P ⊆ ⋃{C1. ∃C0 ∈ ℛ'. (fst C0) = C1}›
unfolding ℛ'_def
by fastforce
moreover have ‹∀C1. (∃C0 ∈ ℛ'. (fst C0) = C1 ∧ C0 ≼⇩s (M_max,N_max)) ⟶ C1 ⊆ M_max›
unfolding M_N_max_def order_double_subsets_def
by auto
then have ‹∀C1 ∈ {C1. ∃C0 ∈ ℛ'. (fst C0) = C1}. C1 ⊆ M_max ›
using M_N_max_def by auto
then have ‹⋃{C1. ∃C0 ∈ ℛ'. (fst C0) = C1} ⊆ M_max›
by auto
ultimately have union_P_in_M_max : ‹⋃P ⊆ M_max›
by blast
moreover have ‹∀C2∈Q. ∃(M0,N0)∈ℛ'. N0 = C2 ›
using ℛ'_def Q_less_than_𝒬_reformulated by fastforce
then have ‹⋃Q ⊆ ⋃{C2. ∃C0 ∈ ℛ'. (snd C0) = C2}›
unfolding ℛ'_def
by fastforce
moreover have ‹∀C2. (∃C0 ∈ ℛ'. (snd C0) = C2 ∧ C0 ≼⇩s (M_max,N_max)) ⟶ C2 ⊆ N_max›
unfolding M_N_max_def order_double_subsets_def
by auto
then have ‹∀C2 ∈ {C2. ∃C0 ∈ ℛ'. (snd C0) = C2}. C2 ⊆ N_max ›
using M_N_max_def by auto
then have ‹⋃{C2. ∃C0 ∈ ℛ'. (snd C0) = C2} ⊆ N_max›
by auto
ultimately have union_Q_in_N_max : ‹⋃Q ⊆ N_max›
by blast
have ‹M' ⊆ M_max ∧ N' ⊆ N_max›
using P_supset Q_supset union_P_in_M_max union_Q_in_N_max by auto
then have ‹M_max ⊨ N_max›
using abs_max_chain_compactness entails_subsets
by force
moreover have ‹(M_max,N_max) ∈ ℛ'›
using M_N_max_def
by simp
then have ‹(M_max,N_max) ∈ C›
using ℛ'_in_C by auto
then have ‹(M_max,N_max) ∈ A›
using C_chain relation_in_A by auto
then have ‹¬M_max ⊨ N_max›
unfolding A_def
by auto
ultimately show "False"
by simp
qed
qed
qed
moreover have ‹⋀C. C ∈ Chains zorn_relation ⟹ M ⊆ fst (max_chain C)›
using M_N_less_than_max_chain order_double_subsets_def fst_eqD
by metis
moreover have ‹⋀C. C ∈ Chains zorn_relation ⟹ N ⊆ snd (max_chain C)›
using M_N_less_than_max_chain order_double_subsets_def snd_eqD
by metis
ultimately have max_chain_in_A : ‹⋀C. C ∈ Chains zorn_relation ⟹ max_chain C ∈ A›
unfolding A_def using M_N_less_than_max_chain case_prod_beta
by force
then have ‹⋀C. C ∈ Chains zorn_relation ⟹
(max_chain C) ∈ A ∧ (∀C0∈C. (C0, max_chain C) ∈ zorn_relation)›
unfolding zorn_relation_def
using zorn_relation_field_is_A max_chain_is_a_max relation_in_A zorn_relation_def
by fastforce
then have zorn_hypothesis_u :
‹⋀C. C ∈ Chains zorn_relation ⟹ ∃u∈Field zorn_relation. ∀a∈C. (a, u) ∈ zorn_relation›
using zorn_relation_field_is_A max_chain_is_a_max by auto
then have ‹∃Cmax∈Field zorn_relation. ∀C∈Field zorn_relation.
(Cmax, C) ∈ zorn_relation ⟶ C = Cmax›
using Zorns_po_lemma zorn_hypothesis_u zorn_hypothesis_po by blast
then have zorn_result : ‹∃Cmax∈A. ∀C∈A. (Cmax, C) ∈ zorn_relation ⟶ C = Cmax›
using zorn_relation_field_is_A by blast
then obtain Cmax where
Cmax_in_A : ‹Cmax∈A› and
Cmax_is_max : ‹∀C∈A. (Cmax, C) ∈ zorn_relation ⟶ C = Cmax›
by blast
have Cmax_not_entails : ‹¬ fst Cmax ⊨ snd Cmax›
unfolding A_def
using Cmax_in_A
using A_def by force
have M_less_fst_Cmax : ‹M ⊆ fst Cmax›
using A_def Cmax_in_A by force
moreover have N_less_snd_Cmax : ‹N ⊆ snd Cmax›
using A_def Cmax_in_A by force
have ‹fst Cmax ∪ snd Cmax = UNIV›
proof (rule ccontr)
assume ‹¬fst Cmax ∪ snd Cmax = UNIV›
then have ‹∃C0. C0 ∉ fst Cmax ∪ snd Cmax›
by auto
then obtain C0 where C0_def : ‹C0 ∉ fst Cmax ∪ snd Cmax›
by auto
have fst_max_entailment_extended : ‹(fst Cmax) ∪ {C0} ⊨ snd Cmax›
proof (rule ccontr)
assume ‹¬(fst Cmax) ∪ {C0} ⊨ snd Cmax›
then have fst_extended_Cmax_in_A : ‹((fst Cmax ∪ {C0}), snd Cmax) ∈ A›
unfolding A_def
using M_less_fst_Cmax N_less_snd_Cmax by blast
then have ‹(Cmax,((fst Cmax) ∪ {C0},snd Cmax)) ∈ zorn_relation›
unfolding zorn_relation_def order_double_subsets_def
using Cmax_in_A by auto
then have ‹Cmax = ((fst Cmax) ∪ {C0},snd Cmax)›
using Cmax_is_max fst_extended_Cmax_in_A by fastforce
then have ‹C0 ∈ (fst Cmax)›
by (metis UnI2 fst_eqD singleton_iff)
then show "False" using C0_def by auto
qed
moreover have snd_max_entailment_extended : ‹fst Cmax ⊨ snd Cmax ∪ {C0}›
proof (rule ccontr)
assume ‹¬fst Cmax ⊨ snd Cmax ∪ {C0}›
then have snd_extended_Cmax_in_A : ‹(fst Cmax,snd Cmax ∪ {C0}) ∈ A›
unfolding A_def
using M_less_fst_Cmax N_less_snd_Cmax by blast
then have ‹(Cmax,(fst Cmax,snd Cmax ∪ {C0})) ∈ zorn_relation›
unfolding zorn_relation_def order_double_subsets_def
using Cmax_in_A by auto
then have ‹Cmax = (fst Cmax,snd Cmax ∪ {C0})›
using Cmax_is_max snd_extended_Cmax_in_A by fastforce
then have ‹C0 ∈ (snd Cmax)›
by (metis UnI2 singleton_iff sndI)
then show "False" using C0_def by auto
qed
ultimately have ‹fst Cmax ⊨ snd Cmax›
using entails_cut by force
then have ‹Cmax ∉ A›
unfolding A_def
by fastforce
then show "False"
using Cmax_in_A by simp
qed
then show ?thesis using M_less_fst_Cmax N_less_snd_Cmax Cmax_not_entails by auto
qed
then show "False" using hyp_entails_sup by auto
qed
lemma entails_each: "M ⊨ P ⟹ ∀C∈M. N ⊨ Q ∪ {C} ⟹ ∀D∈P. N ∪ {D} ⊨ Q ⟹ N ⊨ Q"
proof -
fix M P N Q
assume m_entails_p: ‹M ⊨ P›
and n_to_q_m: ‹∀C∈M. N ⊨ Q ∪ {C}›
and n_p_to_q: ‹∀D∈P. N ∪ {D} ⊨ Q›
have ‹N ⊆ M' ⟹ Q ⊆ N' ⟹ M' ∪ N' = UNIV ⟹ M' ⊨ N'› for M' N'
proof -
fix M' N'
assume n_sub_mp: ‹M' ⊇ N› and
q_sub_np: ‹N' ⊇ Q› and
union_univ: ‹M' ∪ N' = UNIV›
consider (a) "¬ (M' ∩ P = {})" | (b) "¬ (N' ∩ M = {})" | (c) "P ⊆ N' ∧ M ⊆ M'"
using union_univ by auto
then show ‹M' ⊨ N'›
proof cases
case a
assume ‹M' ∩ P ≠ {}›
then obtain D where d_in: ‹D ∈ M' ∩ P› by auto
then have ‹N ∪ {D} ⊆ M'› using n_sub_mp by auto
moreover have ‹N ∪ {D} ⊨ Q› using n_p_to_q d_in by blast
ultimately show ?thesis
using entails_subsets[OF _ q_sub_np] by blast
next
case b
assume ‹N' ∩ M ≠ {}›
then obtain C where c_in: ‹C ∈ M ∩ N'› by auto
then have ‹Q ∪ {C} ⊆ N'› using q_sub_np by auto
moreover have ‹N ⊨ Q ∪ {C}› using n_to_q_m c_in by blast
ultimately show ?thesis
using entails_subsets[OF n_sub_mp] by blast
next
case c
then show ?thesis
using entails_subsets[OF _ _ m_entails_p] by simp
qed
qed
then show ‹N ⊨ Q›
using entails_supsets by simp
qed
lemma entails_bot_to_entails_empty: ‹{} ⊨ {bot} ⟹ {} ⊨ {}›
using entails_reflexive[of bot] entails_each[of "{}" "{bot}" "{}" "{}"] bot_entails_empty
by auto
abbreviation equi_entails :: "'f set ⇒ 'f set ⇒ bool" where
"equi_entails M N ≡ (M ⊨ N ∧ N ⊨ M)"
lemma entails_cond_reflexive: ‹N ≠ {} ⟹ N ⊨ N›
using entails_reflexive entails_subsets by (meson bot.extremum from_nat_into insert_subset)
lemma entails_empty_reflexive_dangerous: ‹{} ⊨ {} ⟹ M ⊨ N›
using entails_subsets[of "{}" M "{}" N] by simp
definition entails_conjunctive :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨∩" 50) where
"M ⊨∩ N ≡ ∀C∈N. M ⊨ {C}"
sublocale Calculus.consequence_relation "{bot}" "(⊨∩)"
proof
show "{bot} ≠ {}" by simp
next
fix B N
assume b_in: "B ∈ {bot}"
then have b_is: "B = bot" by simp
show "{B} ⊨∩ N"
unfolding entails_conjunctive_def
using entails_subsets[of "{B}" "{B}" "{}"] b_is bot_entails_empty by blast
next
fix M N
assume m_subs: "(M :: 'f set) ⊆ N"
show ‹N ⊨∩ M› unfolding entails_conjunctive_def
proof
fix C
assume "C ∈ M"
then have c_subs: ‹{C} ⊆ N› using m_subs by fast
show ‹N ⊨ {C}› using entails_subsets[OF c_subs _ entails_reflexive[of C]] by simp
qed
next
fix M N
assume ‹∀C∈M. N ⊨∩ {C}›
then show ‹N ⊨∩ M›
unfolding entails_conjunctive_def by blast
next
fix M N P
assume
trans1: ‹M ⊨∩ N› and
trans2: ‹N ⊨∩ P›
show ‹M ⊨∩ P› unfolding entails_conjunctive_def
proof
fix C
assume ‹C ∈ P›
then have n_to_c: ‹N ⊨ {C}› using trans2 unfolding entails_conjunctive_def by simp
have "M ∪ {C} ⊨ {C}"
using entails_subsets[OF _ _ entails_reflexive[of C], of "M ∪ {C}" "{C}"] by fast
then have m_c_to_c: ‹∀D∈{C}. M ∪ {D} ⊨ {C}› by blast
have m_to_c_n: "∀D∈N. M ⊨ {C} ∪ {D}"
using trans1 entails_subsets[of M M] unfolding entails_conjunctive_def by blast
show ‹M ⊨ {C}›
using entails_each[OF n_to_c m_to_c_n m_c_to_c] unfolding entails_conjunctive_def .
qed
qed
end
section ‹Extension to Negated Formulas›