Theory Modular_Splitting_Calculus
theory Modular_Splitting_Calculus
imports
Calculi_And_Annotations
Light_Lifting_to_Non_Ground_Calculi
List_Extra
FSet_Extra
begin
section ‹Core splitting calculus›
text ‹
In this section, we formalize an abstract version of a splitting calculus.
We start by considering only two basic rules:
▪ \textsc{Base} performs an inference from our inference system;
▪ \textsc{Unsat} replaces a set of prosopositionally unsatisfiable formulas with ‹⊥›.
›
locale annotated_calculus = calculus_with_annotated_consrel bot FInf entails entails_sound FRed⇩I
FRed⇩F fml asn
for bot :: 'f and
FInf :: ‹'f inference set› and
entails :: ‹[ 'f set, 'f set ] ⇒ bool› (infix ‹⊨› 50) and
entails_sound :: ‹[ 'f set, 'f set ] ⇒ bool› (infix ‹⊨s› 50) and
FRed⇩I :: ‹'f set ⇒ 'f inference set› and
FRed⇩F :: ‹'f set ⇒ 'f set› and
fml :: ‹'v :: countable ⇒ 'f› and
asn :: ‹'f sign ⇒ 'v sign set›
+ assumes
entails_nontrivial: ‹¬ {} ⊨ {}› and
reducedness: ‹Inf_between UNIV (FRed⇩F N) ⊆ FRed⇩I N› and
complete: ‹bot ∉ FRed⇩F N› and
all_red_to_bot: ‹𝒞 ≠ bot ⟹ 𝒞 ∈ FRed⇩F {bot}›
begin
notation sound_cons.entails_neg (infix ‹⊨s⇩∼› 50)
subsection ‹The inference rules›
text ‹
Every inference rule $X$ is defined using two functions: $X\_pre$ and $X\_inf$.
$X\_inf$ is the inference rule itself, while $X\_pre$ are side-conditions for
the rule to be applicable.
›
abbreviation base_pre :: ‹('f, 'v) AF list ⇒ 'f ⇒ bool› where
‹base_pre 𝒩 D ≡ Infer (map F_of 𝒩) D ∈ FInf›
abbreviation base_inf :: ‹('f, 'v) AF list ⇒ 'f ⇒ ('f, 'v) AF inference› where
‹base_inf 𝒩 D ≡ Infer 𝒩 (Pair D (ffUnion (fset_of_list (map A_of 𝒩))))›
abbreviation unsat_pre :: ‹('f, 'v) AF list ⇒ bool› where
‹unsat_pre 𝒩 ≡ (∀ x ∈ set 𝒩. F_of x = bot) ∧ propositionally_unsatisfiable (set 𝒩)›
abbreviation unsat_inf :: ‹('f, 'v) AF list ⇒ ('f, 'v) AF inference› where
‹unsat_inf 𝒩 ≡ Infer 𝒩 (to_AF bot)›
text ‹
We consider first only the inference rules \textsc{Base} and \textsc{Unsat}. The optional
inference and simplification rules are handled separately in the locales
‹splitting_calculus_extensions› and ‹splitting_calculus_with_simps› respectively.
›
inductive_set SInf :: ‹('f, 'v) AF inference set› where
base: ‹base_pre 𝒩 D ⟹ base_inf 𝒩 D ∈ SInf›
| unsat: ‹unsat_pre 𝒩 ⟹ unsat_inf 𝒩 ∈ SInf›
text ‹
The predicates in @{term Splitting_rules} form a valid inference system.
›
interpretation SInf_inf_system: inference_system SInf .
lemma not_empty_entails_bot: ‹¬{} ⊨ {bot}›
using entails_bot_to_entails_empty entails_nontrivial
by blast
text ‹
The proof for Lemma 13 is split into two parts, for each inclusion in the set equality.
›
lemma SInf_commutes_Inf1:
‹bot ∉ 𝒩 proj⇩J J ⟹ (inference_system.Inf_from SInf 𝒩) ιproj⇩J J ⊆ Inf_from (𝒩 proj⇩J J)›
proof (intro subsetI)
fix ι⇩S
assume bot_not_in_proj: ‹bot ∉ 𝒩 proj⇩J J› and
ι⇩S_is_inf: ‹ι⇩S ∈ (inference_system.Inf_from SInf 𝒩) ιproj⇩J J›
have no_enabled_prop_clause_in_𝒩: ‹∀ 𝒞 ∈ 𝒩. enabled 𝒞 J ⟶ F_of 𝒞 ≠ bot›
using bot_not_in_proj
unfolding enabled_projection_def
by blast
obtain ι⇩F where ι⇩S_is: ‹ι⇩S = ιF_of ι⇩F› and
ι⇩F_is_inf: ‹ι⇩F ∈ inference_system.Inf_from SInf 𝒩› and
ι⇩F_is_enabled: ‹enabled_inf ι⇩F J›
using ι⇩S_is_inf enabled_projection_Inf_def
by auto
then have ι⇩F_in_S: ‹ι⇩F ∈ SInf›
by (simp add: inference_system.Inf_from_def)
moreover have prems_of_ι⇩F_subset_𝒩: ‹set (prems_of ι⇩F) ⊆ 𝒩›
using ι⇩F_is_inf
by (simp add: inference_system.Inf_from_def)
moreover have ‹ιF_of ι⇩F ∈ FInf›
unfolding ιF_of_def
using ι⇩F_in_S
proof (cases ι⇩F rule: SInf.cases)
case (base 𝒩 D)
then show ‹base_pre (prems_of ι⇩F) (F_of (concl_of ι⇩F))›
by auto
next
case (unsat 𝒩)
moreover have ‹enabled_inf ι⇩F J›
using ι⇩F_is_enabled
by fastforce
then have ‹∀ 𝒞 ∈ set 𝒩. F_of 𝒞 ≠ bot›
by (metis enabled_inf_def inference.sel(1) local.unsat(1) no_enabled_prop_clause_in_𝒩
prems_of_ι⇩F_subset_𝒩 subset_eq)
then have ‹False›
using not_empty_entails_bot unsat(2) enabled_projection_def prop_proj_in
propositional_model_def propositionally_unsatisfiable_def by auto
ultimately show ‹base_pre (prems_of ι⇩F) (F_of (concl_of ι⇩F))›
by blast
qed
moreover have ‹set (prems_of (ιF_of ι⇩F)) ⊆ 𝒩 proj⇩J J›
using ι⇩F_is_enabled prems_of_ι⇩F_subset_𝒩
by (auto simp add: enabled_inf_def enabled_projection_def ιF_of_def)
ultimately have ‹ιF_of ι⇩F ∈ Inf_from (𝒩 proj⇩J J)›
by (simp add: Inf_from_def)
then show ‹ι⇩S ∈ Inf_from (𝒩 proj⇩J J)›
by (simp add: ι⇩S_is)
qed
lemma SInf_commutes_Inf2:
‹bot ∉ 𝒩 proj⇩J J ⟹ Inf_from (𝒩 proj⇩J J) ⊆ (inference_system.Inf_from SInf 𝒩) ιproj⇩J J›
proof (intro subsetI)
fix ι⇩F
assume bot_not_in_proj: ‹bot ∉ 𝒩 proj⇩J J› and
ι⇩F_in_inf: ‹ι⇩F ∈ Inf_from (𝒩 proj⇩J J)›
have ι⇩F_is_Inf: ‹ι⇩F ∈ FInf›
using Inf_if_Inf_from ι⇩F_in_inf
by blast
have ‹set (prems_of ι⇩F) ⊆ 𝒩 proj⇩J J›
using Inf_from_def ι⇩F_in_inf
by blast
then have ‹∀ 𝒞 ∈ set (prems_of ι⇩F). ∃ A. Pair 𝒞 A ∈ 𝒩 ∧ enabled (Pair 𝒞 A) J›
by (smt (verit, ccfv_SIG) AF.collapse enabled_projection_def mem_Collect_eq subsetD)
then have ‹list_all (λ 𝒞. ∃ A. Pair 𝒞 A ∈ 𝒩 ∧ enabled (Pair 𝒞 A) J) (prems_of ι⇩F)›
using Ball_set
by blast
then obtain As where
length_As_is_length_prems_ι⇩F: ‹length (prems_of ι⇩F) = length As› and
As_def: ‹∀ (C, A) ∈ set (zip (prems_of ι⇩F) As). Pair C A ∈ 𝒩 ∧ enabled (Pair C A) J›
by (smt (verit, del_insts) Ball_set_list_all list_all2_iff list_all_exists_is_exists_list_all2)
define ι⇩S where
‹ι⇩S ≡ Infer [ Pair 𝒞 A. (𝒞, A) ← zip (prems_of ι⇩F) As ]
(Pair (concl_of ι⇩F) (ffUnion (fset_of_list As)))›
have ι⇩F_is_Inf2: ‹Infer (map F_of [ Pair 𝒞 A. (𝒞, A) ← zip (prems_of ι⇩F) As ]) (concl_of ι⇩F) ∈ FInf›
using length_As_is_length_prems_ι⇩F
by (auto simp add: ι⇩F_is_Inf)
then have ι⇩S_is_SInf: ‹ι⇩S ∈ SInf›
using SInf.base[OF ι⇩F_is_Inf2] length_As_is_length_prems_ι⇩F
unfolding ι⇩S_def
by auto
moreover have ‹set (prems_of ι⇩S) ⊆ 𝒩›
unfolding ι⇩S_def
using As_def
by auto
then have ‹ι⇩S ∈ inference_system.Inf_from SInf 𝒩›
using inference_system.Inf_from_def ι⇩S_is_SInf
by blast
moreover have ‹ιF_of ι⇩S = ι⇩F›
unfolding ι⇩S_def ιF_of_def
by (simp add: length_As_is_length_prems_ι⇩F)
moreover have ‹enabled_inf ι⇩S J›
unfolding enabled_inf_def ι⇩S_def
using As_def
by auto
ultimately have ‹∃ ι'. ι⇩F = ιF_of ι' ∧ ι' ∈ inference_system.Inf_from SInf 𝒩 ∧ enabled_inf ι' J›
by blast
then show ‹ι⇩F ∈ (inference_system.Inf_from SInf 𝒩) ιproj⇩J J›
unfolding enabled_projection_Inf_def
by simp
qed
text ‹
We use @{thm SInf_commutes_Inf1} and @{thm SInf_commutes_Inf2} to put the Lemma 13
together into a single proof.
›
lemma SInf_commutes_Inf:
‹bot ∉ 𝒩 proj⇩J J ⟹ (inference_system.Inf_from SInf 𝒩) ιproj⇩J J = Inf_from (𝒩 proj⇩J J)›
using SInf_commutes_Inf1 SInf_commutes_Inf2
by blast
theorem SInf_sound_wrt_entails_sound: ‹ι⇩S ∈ SInf ⟹ set (prems_of ι⇩S) ⊨s⇩A⇩F {concl_of ι⇩S}›
proof -
assume ‹ι⇩S ∈ SInf›
then show ‹set (prems_of ι⇩S) ⊨s⇩A⇩F {concl_of ι⇩S}›
proof (cases ι⇩S rule: SInf.cases)
case (base 𝒩 D)
assume ‹base_pre 𝒩 D›
then have inf_is_sound: ‹set (map F_of 𝒩) ⊨s {D}›
using sound
by fastforce
then show ?thesis
unfolding AF_entails_sound_def sound_cons.entails_neg_def
proof (intro allI impI)
fix J
assume ‹enabled_set {concl_of ι⇩S} J›
then have Pair_D_A_of_𝒩_is_enabled: ‹enabled_set {concl_of ι⇩S} J›
using base
by simp
then have ‹F_of ` {concl_of ι⇩S} = {D}›
using base
by simp
moreover have ‹fset (ffUnion (fset_of_list (map A_of 𝒩))) ⊆ total_strip J›
using Pair_D_A_of_𝒩_is_enabled
unfolding enabled_set_def enabled_def
by (simp add: local.base(1))
then have ‹fBall (fset_of_list (map A_of 𝒩)) (λ As. fset As ⊆ total_strip J)›
using fset_ffUnion_subset_iff_all_fsets_subset
by fast
then have ‹∀ As ∈ set (map A_of 𝒩). fset As ⊆ total_strip J›
by (meson fset_of_list_elem)
then have ‹∀ 𝒞 ∈ set 𝒩. enabled 𝒞 J›
unfolding enabled_def
by simp
then have ‹set 𝒩 proj⇩J J = F_of ` set 𝒩›
unfolding enabled_projection_def
by auto
moreover have ‹{C. Pos C ∈ fml_ext ` total_strip J ∪ Pos ` F_of ` set 𝒩} ⊨s {D}›
using inf_is_sound
by (smt (verit, ccfv_threshold) UnCI imageI list.set_map mem_Collect_eq
sound_cons.entails_subsets subsetI)
moreover have ‹{C. Neg C ∈ Pos ` F_of ` {concl_of ι⇩S}} = {}›
by fast
ultimately show ‹{C. Pos C ∈ fml_ext ` total_strip J ∪ Pos ` (set (prems_of ι⇩S) proj⇩J J)} ∪
{C. Neg C ∈ Pos ` F_of ` {concl_of ι⇩S}} ⊨s
{C. Pos C ∈ Pos ` F_of ` {concl_of ι⇩S}} ∪
{C. Neg C ∈ fml_ext ` total_strip J ∪ Pos ` (set (prems_of ι⇩S) proj⇩J J)}›
using base
by (smt (verit, del_insts) UnCI imageI inference.sel(1) inference.sel(2) mem_Collect_eq
sound_cons.entails_subsets subsetI)
qed
next
case (unsat 𝒩)
assume pre_cond: ‹unsat_pre 𝒩›
then have heads_of_𝒩_are_bot: ‹∀ x ∈ set 𝒩. F_of x = bot› and
𝒩_is_prop_unsat: ‹propositionally_unsatisfiable (set 𝒩)›
by blast+
then have ‹proj⇩⊥ (set 𝒩) = set 𝒩›
using heads_of_𝒩_are_bot propositional_projection_def
by blast
then have ‹∀ J. bot ∈ (set 𝒩) proj⇩J J›
using 𝒩_is_prop_unsat propositional_model_def propositionally_unsatisfiable_def
by force
then show ?thesis
unfolding AF_entails_sound_def sound_cons.entails_neg_def
using unsat
by auto
(smt (verit) Un_insert_right insertI1 insert_absorb sound_cons.bot_entails_empty
sound_cons.entails_subsets subsetI sup_bot_right)
qed
qed
text ‹The lifted calculus provides a consequence relation and a sound inference system.›
interpretation AF_sound_cons_rel: consequence_relation ‹to_AF bot› ‹(⊨s⇩A⇩F)›
by (rule AF_ext_sound_cons_rel)
interpretation SInf_sound_inf_system: sound_inference_system SInf ‹to_AF bot› ‹(⊨s⇩A⇩F)›
by (standard, auto simp add: SInf_sound_wrt_entails_sound)
subsection ‹The redundancy criterion›
definition SRed⇩F :: ‹('f, 'v) AF set ⇒ ('f, 'v) AF set› where
‹SRed⇩F 𝒩 = { AF.Pair C A | C A. ∀ 𝒥. total_strip 𝒥 ⊇ fset A ⟶ C ∈ FRed⇩F (𝒩 proj⇩J 𝒥) }
∪ { AF.Pair C A | C A. ∃ 𝒞 ∈ 𝒩. F_of 𝒞 = C ∧ A_of 𝒞 |⊂| A }›
definition SRed⇩I :: ‹('f, 'v) AF set ⇒ ('f, 'v) AF inference set› where
‹SRed⇩I 𝒩 = { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (𝒩 proj⇩J 𝒥)) }
∪ { unsat_inf ℳ | ℳ. unsat_pre ℳ ∧ to_AF bot ∈ 𝒩 }›
lemma sredI_𝒩_proj_J_subset_redI_proj_J: ‹to_AF bot ∉ 𝒩 ⟹ (SRed⇩I 𝒩) ιproj⇩J J ⊆ FRed⇩I (𝒩 proj⇩J J)›
proof -
assume ‹to_AF bot ∉ 𝒩›
then have SRed⇩I_𝒩_is:
‹SRed⇩I 𝒩 = { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. {base_inf ℳ 𝒞} ιproj⇩J 𝒥 ⊆ FRed⇩I (𝒩 proj⇩J 𝒥)) }›
using SRed⇩I_def
by auto
then show ‹(SRed⇩I 𝒩) ιproj⇩J J ⊆ FRed⇩I (𝒩 proj⇩J J)›
proof (cases ‹(SRed⇩I 𝒩) ιproj⇩J J = {}›)
case True
then show ?thesis
by fast
next
case False
then obtain ι⇩S where ‹ι⇩S ∈ SRed⇩I 𝒩›
using enabled_projection_Inf_def
by fastforce
then have ‹{ι⇩S} ιproj⇩J J ⊆ FRed⇩I (𝒩 proj⇩J J)›
using SRed⇩I_𝒩_is
by auto
then show ?thesis
using SRed⇩I_𝒩_is enabled_projection_Inf_def
by force
qed
qed
lemma bot_not_in_sredF_𝒩: ‹to_AF bot ∉ SRed⇩F 𝒩›
proof -
have ‹to_AF bot ∉ { AF.Pair C A | C A. ∀ 𝒥. total_strip 𝒥 ⊇ fset A ⟶ C ∈ FRed⇩F (𝒩 proj⇩J 𝒥) }›
by (simp add: complete to_AF_def)
moreover have ‹to_AF bot ∉ { AF.Pair C A | C A. ∃ 𝒞 ∈ 𝒩. F_of 𝒞 = C ∧ A_of 𝒞 |⊂| A }›
by (simp add: to_AF_def)
moreover have ‹to_AF bot ∉ { AF.Pair C A | C A. ∀ J. ¬ fset A ⊆ total_strip J }›
by (simp add: to_AF_def)
ultimately show ?thesis
using SRed⇩F_def
by auto
qed
text ‹
We need to set things up for the proof of lemma 18.
We first restrict @{const SRed⇩I} to \textsc{Base} inferences (under the name ‹ARed⇩I›) and show
that it is a redundancy criterion.
And then we consider the case of \textsc{Unsat} inferences separately.
›
definition ARed⇩F :: ‹('f, 'v) AF set ⇒ ('f, 'v) AF set› where
‹ARed⇩F 𝒩 ≡ SRed⇩F 𝒩›
definition ARed⇩I :: ‹('f, 'v) AF set ⇒ ('f, 'v) AF inference set› where
‹ARed⇩I 𝒩 ≡ { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (𝒩 proj⇩J 𝒥)) }›
definition AInf :: ‹('f, 'v) AF inference set› where
‹AInf ≡ { base_inf 𝒩 D | 𝒩 D. base_pre 𝒩 D }›
definition 𝒢⇩F :: ‹'v total_interpretation ⇒ ('f, 'v) AF ⇒ 'f set› where
‹𝒢⇩F 𝒥 𝒞 ≡ {𝒞} proj⇩J 𝒥›
definition 𝒢⇩I :: ‹'v total_interpretation ⇒ ('f, 'v) AF inference ⇒ 'f inference set› where
‹𝒢⇩I 𝒥 ι ≡ {ι} ιproj⇩J 𝒥›
text ‹We define a wellfounded ordering on A-formulas to strengthen @{const ARed⇩I}.
Basically, ‹A ← 𝒞 ⊐ A ← 𝒞'› if ‹𝒞 ⊂ 𝒞'›.›
definition tiebreaker_order :: ‹('f, 'v :: countable) AF rel› where
‹tiebreaker_order ≡ { (𝒞, 𝒞'). F_of 𝒞 = F_of 𝒞' ∧ A_of 𝒞 |⊂| A_of 𝒞' }›
abbreviation sqsupset_is_tiebreaker_order (infix ‹⊐› 50) where
‹𝒞 ⊐ 𝒞' ≡ (𝒞, 𝒞') ∈ tiebreaker_order›
lemma tiebreaker_order_is_strict_partial_order: ‹po_on (⊐) UNIV›
unfolding po_on_def irreflp_on_def transp_on_def tiebreaker_order_def
by auto
lemma wfp_on_fsubset: ‹wfp_on (|⊂|) UNIV›
using wf_fsubset
by auto
lemma wfp_on_tiebreaker_order: ‹wfp_on (⊐) (UNIV :: ('f, 'v) AF set)›
unfolding wfp_on_def
proof (intro notI)
assume ‹∃ f. ∀ i. f i ∈ UNIV ∧ f (Suc i) ⊐ f i›
then obtain f where f_is: ‹∀ i. f i ∈ UNIV ∧ f (Suc i) ⊐ f i›
by auto
define f' where ‹f' = (λ i. A_of (f i))›
have ‹∀ i. f' i ∈ UNIV ∧ f' (Suc i) |⊂| f' i›
using f_is
unfolding f'_def tiebreaker_order_def
by auto
then show ‹False›
using wfp_on_fsubset
unfolding wfp_on_def
by blast
qed
text ‹We can lift inferences from ‹FRed⇩I› to ‹ARed⇩I›.›
interpretation lift_from_FRed_to_ARed: light_tiebreaker_lifting ‹{to_AF bot}› AInf ‹{bot}› ‹(⊨∩)›
FInf FRed⇩I FRed⇩F ‹𝒢⇩F 𝒥› ‹Some ∘ 𝒢⇩I 𝒥› ‹λ_. (⊐)›
proof (standard)
fix N
show ‹FRed⇩I N ⊆ FInf›
using Red_I_to_Inf
by presburger
next
fix B N
assume ‹B ∈ {bot}› and
‹N ⊨∩ {B}›
then show ‹N - FRed⇩F N ⊨∩ {B}›
using Red_F_Bot consequence_relation.entails_conjunctive_def consequence_relation_axioms
by fastforce
next
fix N N' :: ‹'f set›
assume ‹N ⊆ N'›
then show ‹FRed⇩F N ⊆ FRed⇩F N'›
using Red_F_of_subset
by presburger
next
fix N N' :: ‹'f set›
assume ‹N ⊆ N'›
then show ‹FRed⇩I N ⊆ FRed⇩I N'›
using Red_I_of_subset
by presburger
next
fix N N'
assume ‹N' ⊆ FRed⇩F N›
then show ‹FRed⇩F N ⊆ FRed⇩F (N - N')›
using Red_F_of_Red_F_subset
by presburger
next
fix N N'
assume ‹N' ⊆ FRed⇩F N›
then show ‹FRed⇩I N ⊆ FRed⇩I (N - N')›
using Red_I_of_Red_F_subset
by presburger
next
fix ι N
assume ‹ι ∈ FInf› and
‹concl_of ι ∈ N›
then show ‹ι ∈ FRed⇩I N›
using Red_I_of_Inf_to_N
by blast
next
show ‹{to_AF bot} ≠ {}›
by fast
next
fix B :: ‹('f, 'v) AF›
assume ‹B ∈ {to_AF bot}›
then show ‹𝒢⇩F 𝒥 B ≠ {}›
by (simp add: 𝒢⇩F_def enabled_def enabled_projection_def to_AF_def)
next
fix B :: ‹('f, 'v) AF›
assume ‹B ∈ {to_AF bot}›
then show ‹𝒢⇩F 𝒥 B ⊆ {bot}›
using 𝒢⇩F_def enabled_projection_def
by (auto simp add: F_of_to_AF)
next
fix ι⇩A
assume ι⇩A_is_ainf: ‹ι⇩A ∈ AInf› and
‹(Some ∘ 𝒢⇩I 𝒥) ι⇩A ≠ None›
have ‹𝒢⇩I 𝒥 ι⇩A ⊆ FRed⇩I (𝒢⇩F 𝒥 (concl_of ι⇩A))›
proof (intro subsetI)
fix x
assume x_in_𝒢⇩I_of_ι⇩A: ‹x ∈ 𝒢⇩I 𝒥 ι⇩A›
then obtain 𝒩 D where ι⇩A_is: ‹ι⇩A = base_inf 𝒩 D› and
infer_𝒩_D_is_inf: ‹base_pre 𝒩 D›
using AInf_def ι⇩A_is_ainf
by auto
moreover have ι⇩A_is_enabled: ‹enabled_inf ι⇩A 𝒥› and
x_is: ‹x = ιF_of ι⇩A›
using 𝒢⇩I_def enabled_projection_Inf_def x_in_𝒢⇩I_of_ι⇩A
by auto
then have ‹prems_of ι⇩A = 𝒩›
using ι⇩A_is
by auto
then have ‹fBall (fset_of_list (map A_of 𝒩)) (λ As. fset As ⊆ total_strip 𝒥)›
using ι⇩A_is ι⇩A_is_enabled
unfolding enabled_inf_def enabled_def
by (simp add: fBall_fset_of_list_iff_Ball_set)
then have ‹fset (ffUnion (A_of |`| fset_of_list 𝒩)) ⊆ total_strip 𝒥›
by (simp add: fset_ffUnion_subset_iff_all_fsets_subset)
then have ‹enabled (AF.Pair D (ffUnion (A_of |`| fset_of_list 𝒩))) 𝒥›
unfolding enabled_def
by auto
then have ‹{AF.Pair D (ffUnion (fset_of_list (map A_of 𝒩)))} proj⇩J 𝒥 = {D}›
unfolding enabled_projection_def F_of_def
using ι⇩A_is_enabled ι⇩A_is
by auto
then have ‹x ∈ FRed⇩I (𝒢⇩F 𝒥 (Pair D (ffUnion (fset_of_list (map A_of 𝒩)))))›
using x_in_𝒢⇩I_of_ι⇩A ι⇩A_is_enabled x_is infer_𝒩_D_is_inf ι⇩A_is
unfolding 𝒢⇩I_def 𝒢⇩F_def ιF_of_def
by (simp add: Red_I_of_Inf_to_N)
then show ‹x ∈ FRed⇩I (𝒢⇩F 𝒥 (concl_of ι⇩A))›
by (simp add: ι⇩A_is)
qed
then show ‹the ((Some ∘ 𝒢⇩I 𝒥) ι⇩A) ⊆ FRed⇩I (𝒢⇩F 𝒥 (concl_of ι⇩A))›
by simp
next
fix g
show ‹po_on (⊐) UNIV›
using tiebreaker_order_is_strict_partial_order
by blast
next
fix g
show ‹wfp_on (⊐) UNIV›
using wfp_on_tiebreaker_order
by blast
qed
lemma ARed⇩I_is_FRed⇩I: ‹ARed⇩I 𝒩 = (⋂ J. lift_from_FRed_to_ARed.Red_I_𝒢 J 𝒩)›
proof (intro subset_antisym subsetI)
fix ι
assume ‹ι ∈ ARed⇩I 𝒩›
then obtain ℳ 𝒞 where ι_is: ‹ι = base_inf ℳ 𝒞› and
Infer_ℳ_𝒞_in_Inf: ‹base_pre ℳ 𝒞› and
ι_in_FRed⇩I: ‹∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (𝒩 proj⇩J 𝒥)›
using ARed⇩I_def
by fastforce
then have ι_is_AInf: ‹ι ∈ AInf›
using AInf_def
by blast
then have ‹∀ J. {ι} ιproj⇩J J ⊆ FRed⇩I (⋃ (𝒢⇩F J ` 𝒩))›
unfolding 𝒢⇩F_def
using ι_in_FRed⇩I ι_is Union_of_enabled_projection_is_enabled_projection
by auto
then have ‹∀ J. ι ∈ lift_from_FRed_to_ARed.Red_I_𝒢 J 𝒩›
using ι_is_AInf
unfolding lift_from_FRed_to_ARed.Red_I_𝒢_def 𝒢⇩I_def
by auto
then show ‹ι ∈ (⋂ J. lift_from_FRed_to_ARed.Red_I_𝒢 J 𝒩)›
by blast
next
fix ι
assume ι_in_FRed⇩I_𝒢: ‹ι ∈ (⋂ J. lift_from_FRed_to_ARed.Red_I_𝒢 J 𝒩)›
then have ι_is_AInf: ‹ι ∈ AInf› and
all_J_𝒢⇩I_subset_FRed⇩I: ‹∀ J. 𝒢⇩I J ι ⊆ FRed⇩I (⋃ (𝒢⇩F J ` 𝒩))›
unfolding lift_from_FRed_to_ARed.Red_I_𝒢_def
by auto
then obtain ℳ 𝒞 where ι_is: ‹ι = base_inf ℳ 𝒞› and
Infer_ℳ_𝒞_is_Inf: ‹base_pre ℳ 𝒞›
using AInf_def
by auto
then obtain ι⇩F where ι⇩F_is: ‹ι⇩F = ιF_of ι›
by auto
then have ‹∃ ℳ 𝒞. ι = base_inf ℳ 𝒞 ∧ base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (𝒩 proj⇩J 𝒥))›
using ι_is Infer_ℳ_𝒞_is_Inf all_J_𝒢⇩I_subset_FRed⇩I
unfolding 𝒢⇩I_def 𝒢⇩F_def
using Union_of_enabled_projection_is_enabled_projection
by fastforce
then show ‹ι ∈ ARed⇩I 𝒩›
unfolding ARed⇩I_def
by auto
qed
lemma ARed⇩F_is_FRed⇩F: ‹ARed⇩F 𝒩 = (⋂ J. lift_from_FRed_to_ARed.Red_F_𝒢 J 𝒩)›
proof (intro subset_antisym subsetI)
fix 𝒞
assume 𝒞_in_ARed⇩F: ‹𝒞 ∈ ARed⇩F 𝒩›
then obtain C A where 𝒞_is: ‹𝒞 = AF.Pair C A›
unfolding ARed⇩F_def SRed⇩F_def
by blast
consider (a) ‹∀ 𝒥. fset A ⊆ total_strip 𝒥 ⟶ C ∈ FRed⇩F (𝒩 proj⇩J 𝒥)› |
(b) ‹∃ 𝒞 ∈ 𝒩. F_of 𝒞 = C ∧ A_of 𝒞 |⊂| A›
using 𝒞_in_ARed⇩F 𝒞_is
unfolding ARed⇩F_def SRed⇩F_def
by blast
then show ‹𝒞 ∈ (⋂ J. lift_from_FRed_to_ARed.Red_F_𝒢 J 𝒩)›
unfolding lift_from_FRed_to_ARed.Red_F_𝒢_def
proof (cases)
case a
then have ‹∀ J. ∀ D ∈ 𝒢⇩F J 𝒞. D ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩))›
unfolding Red⇩F_strict_def 𝒢⇩F_def
using Union_of_enabled_projection_is_enabled_projection 𝒞_is enabled_projection_def
𝒞_is complete enabled_projection_def
using enabled_def
by force
then have ‹𝒞 ∈ (⋂ J. { C. ∀ D ∈ 𝒢⇩F J C. D ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) })›
by blast
then show ‹𝒞 ∈ (⋂ J. { C. ∀ D ∈ 𝒢⇩F J C. D ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) ∨
(∃ E ∈ 𝒩. E ⊐ C ∧ D ∈ 𝒢⇩F J E) })›
by blast
next
case b
then have ‹∀ J. ∀ D ∈ 𝒢⇩F J 𝒞. ∃ E ∈ 𝒩. E ⊐ 𝒞 ∧ D ∈ 𝒢⇩F J E›
unfolding 𝒢⇩F_def tiebreaker_order_def enabled_projection_def
using subformula_of_enabled_formula_is_enabled
by (smt (verit, ccfv_SIG) AF.sel(1) AF.sel(2) 𝒞_is case_prodI mem_Collect_eq
singletonD singletonI)
then have ‹𝒞 ∈ (⋂ J. { C. ∀ D ∈ 𝒢⇩F J C. ∃ E ∈ 𝒩. E ⊐ C ∧ D ∈ 𝒢⇩F J E })›
by blast
then show ‹𝒞 ∈ (⋂ J. { C. ∀ D ∈ 𝒢⇩F J C. D ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) ∨
(∃ E ∈ 𝒩. E ⊐ C ∧ D ∈ 𝒢⇩F J E) })›
by blast
qed
next
fix 𝒞
assume 𝒞_in_FRed⇩F_𝒢: ‹𝒞 ∈ (⋂ J. lift_from_FRed_to_ARed.Red_F_𝒢 J 𝒩)›
then have 𝒞_in_FRed⇩F_𝒢_unfolded:
‹∀ J. ∀ D ∈ 𝒢⇩F J 𝒞. D ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) ∨ (∃ E ∈ 𝒩. E ⊐ 𝒞 ∧ D ∈ 𝒢⇩F J E)›
unfolding lift_from_FRed_to_ARed.Red_F_𝒢_def
by blast
then have 𝒞_in_FRed⇩F_𝒢_if_enabled:
‹∀ J. enabled 𝒞 J ⟶ F_of 𝒞 ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) ∨ (∃ E ∈ 𝒩. E ⊐ 𝒞 ∧ F_of 𝒞 ∈ 𝒢⇩F J E)›
unfolding 𝒢⇩F_def enabled_projection_def
by auto
obtain C A where 𝒞_is: ‹𝒞 = AF.Pair C A›
by (meson AF.exhaust_sel)
then have
‹∀ J. fset A ⊆ total_strip J ⟶
C ∈ FRed⇩F (⋃ (𝒢⇩F J ` 𝒩)) ∨ (∃ E ∈ 𝒩. E ⊐ 𝒞 ∧ C ∈ 𝒢⇩F J E)›
using 𝒞_in_FRed⇩F_𝒢_if_enabled
unfolding enabled_def
by simp
then show ‹𝒞 ∈ ARed⇩F 𝒩›
using 𝒞_is 𝒞_in_FRed⇩F_𝒢_if_enabled
unfolding ARed⇩F_def SRed⇩F_def 𝒢⇩F_def enabled_def tiebreaker_order_def
using Union_of_enabled_projection_is_enabled_projection
by auto
qed
lemma entails_is_entails_𝒢: ‹ℳ ⊨⇩A⇩F {𝒞} ⟷ (∀ 𝒥. lift_from_FRed_to_ARed.entails_𝒢 𝒥 ℳ {𝒞})›
proof (intro iffI allI)
fix 𝒥
assume ‹ℳ ⊨⇩A⇩F {𝒞}›
then show ‹lift_from_FRed_to_ARed.entails_𝒢 𝒥 ℳ {𝒞}›
unfolding 𝒢⇩F_def AF_entails_def enabled_projection_def enabled_set_def entails_conjunctive_def
by (simp add: Union_of_singleton_is_setcompr)
next
assume entails_𝒢_ℳ_𝒞: ‹∀ 𝒥. lift_from_FRed_to_ARed.entails_𝒢 𝒥 ℳ {𝒞}›
show ‹ℳ ⊨⇩A⇩F {𝒞}›
unfolding 𝒢⇩F_def AF_entails_def enabled_set_def
proof (intro allI impI)
fix J
assume ‹∀ 𝒞 ∈ {𝒞}. enabled 𝒞 J›
then show ‹ℳ proj⇩J J ⊨ F_of ` {𝒞}›
using entails_𝒢_ℳ_𝒞
unfolding 𝒢⇩F_def enabled_projection_def entails_conjunctive_def
by (simp add: Union_of_singleton_is_setcompr)
qed
qed
lemma SRed⇩I_in_SInf: ‹SRed⇩I N ⊆ SInf›
using SRed⇩I_def SInf.simps
by force
lemma SRed⇩F_entails_bot: ‹N ⊨⇩A⇩F {to_AF bot} ⟹ N - SRed⇩F N ⊨⇩A⇩F {to_AF bot}›
proof -
fix N
have And_to_Union:
‹⋀ J. N - lift_from_FRed_to_ARed.Red_F_𝒢 J N ⊆ (⋃ J. N - lift_from_FRed_to_ARed.Red_F_𝒢 J N)›
by blast
assume N_entails_bot: ‹N ⊨⇩A⇩F {to_AF bot}›
have ‹lift_from_FRed_to_ARed.entails_𝒢 J N {to_AF bot} ⟹
lift_from_FRed_to_ARed.entails_𝒢 J (N - lift_from_FRed_to_ARed.Red_F_𝒢 J N) {to_AF bot}›
for J
using lift_from_FRed_to_ARed.Red_F_Bot_F
by blast
then have ‹N ⊨⇩A⇩F {to_AF bot} ⟹ N - ARed⇩F N ⊨⇩A⇩F {to_AF bot}›
proof -
assume ‹N ⊨⇩A⇩F {to_AF bot}› and
‹⋀ J. lift_from_FRed_to_ARed.entails_𝒢 J N {to_AF bot} ⟹
lift_from_FRed_to_ARed.entails_𝒢 J (N - lift_from_FRed_to_ARed.Red_F_𝒢 J N) {to_AF bot}›
then have FRed⇩F_𝒢_entails_𝒢_bot:
‹lift_from_FRed_to_ARed.entails_𝒢 J (N - lift_from_FRed_to_ARed.Red_F_𝒢 J N) {to_AF bot}›
for J
using entails_is_entails_𝒢
by blast
then have
‹lift_from_FRed_to_ARed.entails_𝒢 J (⋃ J. N - lift_from_FRed_to_ARed.Red_F_𝒢 J N) {to_AF bot}›
for J
using And_to_Union
by (meson lift_from_FRed_to_ARed.entails_trans lift_from_FRed_to_ARed.subset_entailed)
then show ‹N - ARed⇩F N ⊨⇩A⇩F {to_AF bot}›
using ARed⇩F_is_FRed⇩F entails_is_entails_𝒢
by fastforce
qed
then show ‹N - SRed⇩F N ⊨⇩A⇩F {to_AF bot}›
using ARed⇩F_def N_entails_bot
by force
qed
lemma SRed⇩F_of_subset_F: ‹N ⊆ N' ⟹ SRed⇩F N ⊆ SRed⇩F N'›
proof -
fix N N' :: ‹('f, 'v) AF set›
assume ‹N ⊆ N'›
then show ‹SRed⇩F N ⊆ SRed⇩F N'›
unfolding SRed⇩F_def enabled_projection_def
by auto
(smt (verit, best) Collect_mono Red_F_of_subset subset_iff)
qed
lemma SRed⇩I_of_subset_F: ‹N ⊆ N' ⟹ SRed⇩I N ⊆ SRed⇩I N'›
proof -
fix N N' :: ‹('f, 'v) AF set›
assume ‹N ⊆ N'›
then show ‹SRed⇩I N ⊆ SRed⇩I N'›
unfolding SRed⇩I_def enabled_projection_Inf_def enabled_projection_def enabled_inf_def ιF_of_def
by (auto, (smt (verit, best) Red_I_of_subset mem_Collect_eq subset_iff)+)
qed
lemma SRed⇩F_of_SRed⇩F_subset_F: ‹N' ⊆ SRed⇩F N ⟹ SRed⇩F N ⊆ SRed⇩F (N - N')›
proof -
fix N N'
assume N'_subset_SRed⇩F_N: ‹N' ⊆ SRed⇩F N›
have ‹N' ⊆ ARed⇩F N ⟹ ARed⇩F N ⊆ ARed⇩F (N - N')›
using lift_from_FRed_to_ARed.Red_F_of_Red_F_subset_F
proof -
assume N'_subset_ARed⇩F_N: ‹N' ⊆ ARed⇩F N› and
‹(⋀ N' 𝒥 N. N' ⊆ lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N ⟹
lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N ⊆ lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 (N - N'))›
then have ‹⋀ N' N. N' ⊆ (⋂ 𝒥. lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N) ⟹
(⋂ 𝒥. lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N) ⊆
(⋂ 𝒥. lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 (N - N'))›
by (meson INF_mono' UNIV_I le_INF_iff)
then show ‹ARed⇩F N ⊆ ARed⇩F (N - N')›
using ARed⇩F_is_FRed⇩F N'_subset_ARed⇩F_N
by presburger
qed
then show ‹SRed⇩F N ⊆ SRed⇩F (N - N')›
by (simp add: ARed⇩F_def N'_subset_SRed⇩F_N)
qed
lemma SRed⇩I_of_SRed⇩F_subset_F: ‹N' ⊆ SRed⇩F N ⟹ SRed⇩I N ⊆ SRed⇩I (N - N')›
proof -
fix N N'
assume N'_subset_SRed⇩F_N: ‹N' ⊆ SRed⇩F N›
have works_for_ARed⇩I: ‹N' ⊆ ARed⇩F N ⟹ ARed⇩I N ⊆ ARed⇩I (N - N')›
using lift_from_FRed_to_ARed.Red_I_of_Red_F_subset_F
proof -
assume N'_subset_ARed⇩F_N: ‹N' ⊆ ARed⇩F N› and
‹(⋀ N' 𝒥 N. N' ⊆ lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N ⟹
lift_from_FRed_to_ARed.Red_I_𝒢 𝒥 N ⊆ lift_from_FRed_to_ARed.Red_I_𝒢 𝒥 (N - N'))›
then have ‹⋀ N' N. N' ⊆ (⋂ 𝒥. lift_from_FRed_to_ARed.Red_F_𝒢 𝒥 N) ⟹
(⋂ 𝒥. lift_from_FRed_to_ARed.Red_I_𝒢 𝒥 N) ⊆
(⋂ 𝒥. lift_from_FRed_to_ARed.Red_I_𝒢 𝒥 (N - N'))›
by (metis (no_types, lifting) INF_mono' UNIV_I le_INF_iff)
then show ‹ARed⇩I N ⊆ ARed⇩I (N - N')›
using ARed⇩I_is_FRed⇩I ARed⇩F_is_FRed⇩F N'_subset_ARed⇩F_N
by presburger
qed
moreover have ‹unsat_pre 𝒩 ⟹ unsat_inf 𝒩 ∈ SRed⇩I (N - N')›
if ι_is_redundant: ‹unsat_inf 𝒩 ∈ SRed⇩I N›
for 𝒩
using bot_not_in_sredF_𝒩 N'_subset_SRed⇩F_N ι_is_redundant
unfolding SRed⇩I_def SRed⇩F_def
by (smt (verit, del_insts) ARed⇩F_def ARed⇩I_def Diff_iff N'_subset_SRed⇩F_N Un_iff
bot_not_in_sredF_𝒩 works_for_ARed⇩I mem_Collect_eq subsetD)
ultimately show ‹SRed⇩I N ⊆ SRed⇩I (N - N')›
using N'_subset_SRed⇩F_N bot_not_in_sredF_𝒩
unfolding SRed⇩F_def ARed⇩F_def SRed⇩I_def ARed⇩I_def
by (smt (verit, del_insts) Collect_cong Diff_iff N'_subset_SRed⇩F_N Un_iff
bot_not_in_sredF_𝒩 subset_iff)
qed
lemma SRed⇩I_of_SInf_to_N_F: ‹ι⇩S ∈ SInf ⟹ concl_of ι⇩S ∈ N ⟹ ι⇩S ∈ SRed⇩I N›
proof -
fix ι⇩S N
assume ‹ι⇩S ∈ SInf› and
concl_ι⇩S_in_N: ‹concl_of ι⇩S ∈ N›
then show ‹ι⇩S ∈ SRed⇩I N›
unfolding SRed⇩I_def
proof (cases ι⇩S rule: SInf.cases)
case (base 𝒩 D)
obtain ℳ 𝒞 where ι⇩S_is: ‹ι⇩S = base_inf ℳ 𝒞› and
Infer_ℳ_𝒞_is_Inf: ‹base_pre ℳ 𝒞›
using base
by blast
have ‹∀ J. { base_inf ℳ 𝒞 } ιproj⇩J J ⊆ FRed⇩I (N proj⇩J J)›
unfolding enabled_projection_Inf_def enabled_projection_def ιF_of_def enabled_inf_def
proof (intro allI subsetI)
fix J
have ‹∀𝒞∈set ℳ. enabled 𝒞 J ⟹ Infer (map F_of ℳ) 𝒞 ∈ FRed⇩I {F_of 𝒞 |𝒞. 𝒞 ∈ N ∧ enabled 𝒞 J}›
proof -
assume all_enabled_in_ℳ: ‹∀ 𝒞 ∈ set ℳ. enabled 𝒞 J›
then have A_of_ℳ_to_𝒞_in_N: ‹AF.Pair 𝒞 (ffUnion (fset_of_list (map A_of ℳ))) ∈ N›
using ι⇩S_is concl_ι⇩S_in_N
by auto
moreover have ‹fBall (fset_of_list ℳ) (λ x. fset (A_of x) ⊆ total_strip J)›
using all_enabled_in_ℳ
unfolding enabled_def
by (simp add: fset_of_list_elem)
then have ‹fBall (A_of |`| fset_of_list ℳ) (λ x. fset x ⊆ total_strip J)›
by auto
then have ‹enabled (AF.Pair 𝒞 (ffUnion (A_of |`| fset_of_list ℳ))) J›
using A_of_ℳ_to_𝒞_in_N
unfolding enabled_def
using fset_ffUnion_subset_iff_all_fsets_subset
by (metis AF.sel(2))
ultimately show ‹Infer (map F_of ℳ) 𝒞 ∈ FRed⇩I {F_of 𝒞 | 𝒞. 𝒞 ∈ N ∧ enabled 𝒞 J}›
by (metis (mono_tags, lifting) AF.sel(1) Infer_ℳ_𝒞_is_Inf Red_I_of_Inf_to_N
fset_of_list_map inference.sel(2) mem_Collect_eq)
qed
then show ‹x ∈ {Infer (map F_of (prems_of ι)) (F_of (concl_of ι)) |ι.
ι ∈ {base_inf ℳ 𝒞} ∧ (∀𝒞∈set (prems_of ι). enabled 𝒞 J)} ⟹
x ∈ FRed⇩I {F_of 𝒞 |𝒞. 𝒞 ∈ N ∧ enabled 𝒞 J}› for x
by simp
qed
then have ‹ι⇩S ∈ { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (N proj⇩J 𝒥))}›
using ι⇩S_is Infer_ℳ_𝒞_is_Inf
by auto
then show ‹ι⇩S ∈ { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (N proj⇩J 𝒥)) } ∪
{ unsat_inf ℳ | ℳ. unsat_pre ℳ ∧ to_AF bot ∈ N }›
by fast
next
case (unsat 𝒩)
then have ‹ι⇩S ∈ { unsat_inf ℳ | ℳ. unsat_pre ℳ ∧ to_AF bot ∈ N}›
using concl_ι⇩S_in_N
by fastforce
then show ‹ι⇩S ∈ { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (N proj⇩J 𝒥)) } ∪
{ unsat_inf ℳ | ℳ. unsat_pre ℳ ∧ to_AF bot ∈ N }›
by fast
qed
qed
end
subsection ‹Standard completeness›
context annotated_calculus
begin
lemmas SRed_rules = SRed⇩F_entails_bot SRed⇩F_of_subset_F SRed⇩I_of_subset_F SRed⇩F_of_SRed⇩F_subset_F
SRed⇩I_of_SRed⇩F_subset_F SRed⇩I_of_SInf_to_N_F SRed⇩I_in_SInf
sublocale S_calculus: calculus ‹to_AF bot› SInf AF_entails SRed⇩I SRed⇩F
by (standard; simp add: SRed_rules)
lemma S_saturated_to_F_saturated: ‹S_calculus.saturated 𝒩 ⟹ saturated (𝒩 proj⇩J 𝒥)›
proof -
assume 𝒩_is_S_saturated: ‹S_calculus.saturated 𝒩›
then show ‹saturated (𝒩 proj⇩J 𝒥)›
unfolding saturated_def S_calculus.saturated_def
proof (intro subsetI)
fix ι⇩F
assume ‹ι⇩F ∈ Inf_from (𝒩 proj⇩J 𝒥)›
then have ι⇩F_is_Inf: ‹ι⇩F ∈ FInf› and
prems_of_ι⇩F_in_𝒩_proj_𝒥: ‹set (prems_of ι⇩F) ⊆ 𝒩 proj⇩J 𝒥›
unfolding Inf_from_def
by auto
moreover have ‹∀ C ∈ set (prems_of ι⇩F). ∃ 𝒞 ∈ 𝒩. F_of 𝒞 = C ∧ enabled 𝒞 𝒥›
using prems_of_ι⇩F_in_𝒩_proj_𝒥
unfolding enabled_projection_def
by blast
then have ‹list_all (λ C. ∃ 𝒞 ∈ 𝒩. F_of 𝒞 = C ∧ enabled 𝒞 𝒥) (prems_of ι⇩F)›
using Ball_set
by blast
then have ‹∃ 𝒞s. length 𝒞s = length (prems_of ι⇩F) ∧
list_all2 (λ C 𝒞. 𝒞 ∈ 𝒩 ∧ F_of 𝒞 = C ∧ enabled 𝒞 𝒥) (prems_of ι⇩F) 𝒞s›
using list_all_ex_to_ex_list_all2
by (smt (verit, best) Ball_set)
then have ‹∃ As. length As = length (prems_of ι⇩F) ∧
list_all2 (λ C A. AF.Pair C A ∈ 𝒩 ∧ enabled (AF.Pair C A) 𝒥) (prems_of ι⇩F) As›
by (smt (verit, del_insts) AF.exhaust AF.sel(1) list.pred_mono_strong
list_all_ex_to_ex_list_all2)
then have ‹∃ As. length As = length (prems_of ι⇩F) ∧
list_all (λ 𝒞. 𝒞 ∈ 𝒩 ∧ enabled 𝒞 𝒥) (map2 AF.Pair (prems_of ι⇩F) As)›
using list_all2_to_map[where f = ‹λ C A. AF.Pair C A›]
by (smt (verit) list_all2_mono)
then obtain As :: ‹'v sign fset list›
where ‹∀ 𝒞 ∈ set (map2 AF.Pair (prems_of ι⇩F) As). 𝒞 ∈ 𝒩 ∧ enabled 𝒞 𝒥› and
length_As_eq_length_prems: ‹length As = length (prems_of ι⇩F)›
by (metis (no_types, lifting) Ball_set_list_all)
then have set_prems_As_subset_𝒩: ‹set (map2 AF.Pair (prems_of ι⇩F) As) ⊆ 𝒩› and
all_enabled: ‹∀ 𝒞 ∈ set (map2 AF.Pair (prems_of ι⇩F) As). enabled 𝒞 𝒥›
by auto
let ?prems = ‹map2 AF.Pair (prems_of ι⇩F) As›
have ‹set ?prems ⊆ 𝒩›
using set_prems_As_subset_𝒩 .
moreover have ‹length ?prems = length (prems_of ι⇩F)›
using length_As_eq_length_prems
by simp
then have F_of_dummy_prems_is_prems_of_ι⇩F: ‹map F_of ?prems = prems_of ι⇩F›
by (simp add: length_As_eq_length_prems)
moreover have ‹∀ 𝒞 ∈ set (map A_of (map2 AF.Pair (prems_of ι⇩F) As)). fset 𝒞 ⊆ total_strip 𝒥›
using
all_enabled ball_set_f_to_ball_set_map[where P = ‹λ x. fset x ⊆ total_strip 𝒥› and f = A_of]
unfolding enabled_def
by blast
then have ‹∀ 𝒞 ∈ set As. fset 𝒞 ⊆ total_strip 𝒥›
using map_A_of_map2_Pair length_As_eq_length_prems
by metis
then have ‹fset (ffUnion (fset_of_list As)) ⊆ total_strip 𝒥›
using all_enabled
unfolding enabled_def[of _ 𝒥]
by (simp add: fBall_fset_of_list_iff_Ball_set fset_ffUnion_subset_iff_all_fsets_subset)
then have base_inf_enabled: ‹enabled_inf (base_inf ?prems (concl_of ι⇩F)) 𝒥›
using all_enabled enabled_inf_def
by auto
moreover have pre_holds: ‹base_pre ?prems (concl_of ι⇩F)›
using ι⇩F_is_Inf F_of_dummy_prems_is_prems_of_ι⇩F
by force
moreover have ιF_of_base_inf_is_ι⇩F: ‹ιF_of (base_inf ?prems (concl_of ι⇩F)) = ι⇩F›
using F_of_dummy_prems_is_prems_of_ι⇩F ιF_of_def
by force
ultimately have ι⇩F_in_Inf_𝒩_proj_𝒥: ‹ι⇩F ∈ (S_calculus.Inf_from 𝒩) ιproj⇩J 𝒥›
using SInf.base[OF pre_holds]
unfolding enabled_projection_Inf_def S_calculus.Inf_from_def
by (metis (mono_tags, lifting) inference.sel(1) mem_Collect_eq)
then have ‹∃ ℳ D. base_inf ℳ D ∈ S_calculus.Inf_from 𝒩 ∧
ιF_of (base_inf ℳ D) = ι⇩F ∧ enabled_inf (base_inf ℳ D) 𝒥›
using ιF_of_base_inf_is_ι⇩F
unfolding enabled_projection_Inf_def
by (metis (mono_tags, lifting) CollectI S_calculus.Inf_from_def SInf.base
base_inf_enabled inference.sel(1) pre_holds set_prems_As_subset_𝒩)
then obtain ℳ D where base_inf_in_Inf_𝒩: ‹base_inf ℳ D ∈ S_calculus.Inf_from 𝒩› and
ιF_of_base_inf_is_ι⇩F: ‹ιF_of (base_inf ℳ D) = ι⇩F› and
base_inf_enabled: ‹enabled_inf (base_inf ℳ D) 𝒥›
by blast
then have ‹base_inf ℳ D ∈ SRed⇩I 𝒩›
using 𝒩_is_S_saturated
unfolding S_calculus.saturated_def
by blast
moreover have ‹base_pre ℳ D›
using ιF_of_base_inf_is_ι⇩F ι⇩F_is_Inf
by (simp add: ιF_of_def)
ultimately show ‹ι⇩F ∈ FRed⇩I (𝒩 proj⇩J 𝒥)›
using ι⇩F_in_Inf_𝒩_proj_𝒥 ιF_of_base_inf_is_ι⇩F base_inf_enabled
unfolding SRed⇩I_def enabled_projection_Inf_def ιF_of_def enabled_def enabled_projection_def
by auto
(metis (mono_tags, lifting) AF.sel(2) F_of_to_AF Red_I_of_Inf_to_N bot_fset.rep_eq
empty_subsetI inference.sel(2) mem_Collect_eq to_AF_def)
qed
qed
notation AF_cons_rel.entails_conjunctive (infix ‹⊨∩⇩A⇩F› 50)
theorem S_calculus_statically_complete:
assumes F_statically_complete: ‹statically_complete_calculus bot FInf (⊨) FRed⇩I FRed⇩F›
shows ‹statically_complete_calculus (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
using F_statically_complete
unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
proof (intro conjI allI impI; elim conjE)
show ‹calculus (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
using S_calculus.calculus_axioms
by force
next
fix N
assume ‹calculus bot FInf (⊨) FRed⇩I FRed⇩F› and
if_F_saturated_and_N_entails_bot_then_bot_in_N:
‹∀ N. saturated N ⟶ N ⊨ {bot} ⟶ bot ∈ N› and
N_is_S_saturated: ‹S_calculus.saturated N› and
N_entails_bot: ‹N ⊨⇩A⇩F {to_AF bot}›
then have N_proj_𝒥_entails_bot: ‹∀ 𝒥. N proj⇩J 𝒥 ⊨ {bot}›
unfolding AF_entails_def
using F_of_to_AF[of bot]
by (smt (verit) enabled_to_AF_set image_empty image_insert)
then have N_proj_𝒥_F_saturated: ‹∀ 𝒥. saturated (N proj⇩J 𝒥)›
using N_is_S_saturated
using S_saturated_to_F_saturated
by blast
then have ‹∀ 𝒥. bot ∈ N proj⇩J 𝒥›
using N_proj_𝒥_entails_bot if_F_saturated_and_N_entails_bot_then_bot_in_N
by presburger
then have prop_proj_N_is_prop_unsat: ‹propositionally_unsatisfiable (proj⇩⊥ N)›
unfolding enabled_projection_def propositional_model_def propositional_projection_def
propositionally_unsatisfiable_def
by fast
then have ‹proj⇩⊥ N ≠ {}›
unfolding propositionally_unsatisfiable_def propositional_model_def
using enabled_projection_def prop_proj_in
by auto
then have ‹∃ ℳ. set ℳ ⊆ proj⇩⊥ N ∧ finite (set ℳ) ∧ propositionally_unsatisfiable (set ℳ)›
by (metis finite_list prop_proj_N_is_prop_unsat prop_unsat_compactness)
then obtain ℳ where ℳ_subset_prop_proj_N: ‹set ℳ ⊆ proj⇩⊥ N› and
ℳ_subset_N: ‹set ℳ ⊆ N› and
‹finite (set ℳ)› and
ℳ_prop_unsat: ‹propositionally_unsatisfiable (set ℳ)› and
ℳ_not_empty: ‹ℳ ≠ []›
by (smt (verit, del_insts) AF_cons_rel.entails_bot_to_entails_empty
AF_cons_rel.entails_empty_reflexive_dangerous compactness_AF_proj equiv_prop_entails
finite_list image_empty prop_proj_N_is_prop_unsat prop_proj_in propositional_model2_def
propositionally_unsatisfiable_def set_empty2 subset_empty subset_trans to_AF_proj_J)
then have ‹unsat_inf ℳ ∈ S_calculus.Inf_from N› and
Infer_ℳ_bot_in_SInf: ‹unsat_inf ℳ ∈ SInf›
using SInf.unsat S_calculus.Inf_from_def propositional_projection_def
by fastforce+
then have ‹unsat_inf ℳ ∈ SRed⇩I N›
using N_is_S_saturated S_calculus.saturated_def
by blast
then show ‹to_AF bot ∈ N›
unfolding SRed⇩I_def
proof (elim UnE)
assume ‹unsat_inf ℳ ∈ { base_inf ℳ 𝒞 | ℳ 𝒞. base_pre ℳ 𝒞 ∧
(∀ 𝒥. { base_inf ℳ 𝒞 } ιproj⇩J 𝒥 ⊆ FRed⇩I (N proj⇩J 𝒥)) }›
then have ‹unsat_inf ℳ = base_inf ℳ bot›
by (smt (verit, best) AF.exhaust_sel AF.sel(2) F_of_to_AF inference.inject mem_Collect_eq)
then have ‹to_AF bot = AF.Pair bot (ffUnion (A_of |`| fset_of_list ℳ))›
by simp
then have ‹ffUnion (A_of |`| fset_of_list ℳ) = {||}›
by (metis AF.sel(2) A_of_to_AF)
then consider (ℳ_empty) ‹A_of |`| fset_of_list ℳ = {||}› |
(no_assertions_in_ℳ) ‹fBall (A_of |`| fset_of_list ℳ) (λ x. x = {||})›
using Union_empty_if_set_empty_or_all_empty
by auto
then show ?thesis
proof (cases)
case ℳ_empty
then have ‹fset_of_list ℳ = {||}›
by blast
then have ‹ℳ = []›
by (metis bot_fset.rep_eq fset_of_list.rep_eq set_empty2)
then show ?thesis
using ℳ_not_empty
by contradiction
next
case no_assertions_in_ℳ
then have ‹fBall (fset_of_list ℳ) (λ x. A_of x = {||})›
using fBall_fimage_is_fBall
by simp
then have ‹∀ x ∈ set ℳ. A_of x = {||}›
using fBall_fset_of_list_iff_Ball_set
by fast
then have ‹to_AF bot ∈ set ℳ›
using ℳ_subset_prop_proj_N ℳ_not_empty
unfolding propositional_projection_def to_AF_def
by (metis (mono_tags, lifting) AF.exhaust_sel CollectD ex_in_conv set_empty subset_code(1))
then show ?thesis
using ℳ_subset_N
by blast
qed
next
assume ‹unsat_inf ℳ ∈ { unsat_inf ℳ | ℳ. unsat_pre ℳ ∧ to_AF bot ∈ N }›
then show ?thesis
by fastforce
qed
qed
lemma entails_conj_is_entails_disj_if_right_singleton: ‹ℳ ⊨∩⇩A⇩F {𝒞} ⟷ ℳ ⊨⇩A⇩F {𝒞}›
unfolding AF_cons_rel.entails_conjunctive_def
by blast
lemma S_with_conj_is_calculus: ‹Calculus.calculus {to_AF bot} SInf (⊨∩⇩A⇩F) SRed⇩I SRed⇩F›
proof (standard)
fix N
show ‹SRed⇩I N ⊆ SInf›
by (simp only: SRed_rules)
next
fix N B
show ‹B ∈ {to_AF bot} ⟹ N ⊨∩⇩A⇩F {B} ⟹ N - SRed⇩F N ⊨∩⇩A⇩F {B}›
by (simp add: AF_cons_rel.entails_conjunctive_def SRed⇩F_entails_bot)
next
fix N N'
show ‹N ⊆ N' ⟹ SRed⇩F N ⊆ SRed⇩F N'›
by (simp only: SRed_rules)
next
fix N N'
show ‹N ⊆ N' ⟹ SRed⇩I N ⊆ SRed⇩I N'›
by (simp only: SRed_rules)
next
fix N N'
show ‹N' ⊆ SRed⇩F N ⟹ SRed⇩F N ⊆ SRed⇩F (N - N')›
by (simp only: SRed_rules)
next
fix N N'
show ‹N' ⊆ SRed⇩F N ⟹ SRed⇩I N ⊆ SRed⇩I (N - N')›
by (simp only: SRed_rules)
next
fix ι N
show ‹ι ∈ SInf ⟹ concl_of ι ∈ N ⟹ ι ∈ SRed⇩I N›
by (simp only: SRed_rules)
qed
lemma saturated_equiv: ‹S_calculus.saturated N ⟷ Calculus.calculus.saturated SInf SRed⇩I N›
by (meson Calculus.calculus.saturated_def S_calculus.saturated_def S_with_conj_is_calculus)
lemma derivation_equiv:
‹is_derivation S_calculus.derive Ns ⟷ chain (Calculus.calculus.derive SRed⇩F) (to_llist Ns)›
proof -
have ‹S_calculus.derive M N ⟷ Calculus.calculus.derive SRed⇩F M N› for M N
unfolding S_calculus.derive_def
proof (intro iffI)
show ‹M - N ⊆ SRed⇩F N ⟹ Calculus.calculus.derive SRed⇩F M N›
using S_with_conj_is_calculus calculus.derive.intros
by blast
next
assume ‹Calculus.calculus.derive SRed⇩F M N›
then have ‹M - N ⊆ SRed⇩F N›
by (meson S_with_conj_is_calculus calculus.derive.cases)
then show ‹M - N ⊆ SRed⇩F N› .
qed
moreover have ‹(∀ i. R (llnth M i) (llnth M (Suc i))) ⟷ chain R (to_llist M)› for R M
proof (intro iffI)
assume all_of_M_in_rel: ‹∀ i. R (llnth M i) (llnth M (Suc i))›
then show ‹chain R (to_llist M)›
proof -
have ‹¬ lnull (to_llist M)›
by (metis enat.simps(3) llength_eq_0 llength_of_to_llist_is_infinite zero_enat_def)
moreover have ‹∀ j. enat (j + 1) < ∞ ⟶ R (llnth M j) (llnth M (Suc j))›
using all_of_M_in_rel
by blast
then have ‹∀ j. enat (j + 1) < ∞ ⟶ R (lnth (to_llist M) j) (lnth (to_llist M) (Suc j))›
by (simp add: llnth.rep_eq)
ultimately show ‹chain R (to_llist M)›
by (metis Suc_eq_plus1 all_of_M_in_rel llnth.rep_eq lnth_rel_chain)
qed
next
assume chain_R_M: ‹chain R (to_llist M)›
then show ‹∀ i. R (llnth M i) (llnth M (Suc i))›
proof (intro allI)
fix i
have ‹enat i < ∞›
using enat_ord_code(4)
by presburger
then have ‹R (lnth (to_llist M) i) (lnth (to_llist M) (Suc i))›
by (simp add: chain_R_M chain_lnth_rel llength_of_to_llist_is_infinite)
then show ‹R (llnth M i) (llnth M (Suc i))›
by (simp add: llnth.rep_eq)
qed
qed
ultimately have
‹(∀ i. S_calculus.derive (llnth Ns i) (llnth Ns (Suc i))) ⟷
chain (Calculus.calculus.derive SRed⇩F) (to_llist Ns)›
by metis
then show ?thesis
by (simp add: is_derivation_def)
qed
lemma fair_equiv: ‹S_calculus.fair Ns ⟷ Calculus.calculus.fair SInf SRed⇩I (to_llist Ns)›
proof -
have ‹S_calculus.Inf_from (Liminf_llist (to_llist Ns)) ⊆ Sup_llist (lmap SRed⇩I (to_llist Ns)) ⟷
S_calculus.Inf_from (Liminf_infinite_llist Ns) ⊆ Sup_infinite_llist (llmap SRed⇩I Ns)›
by transfer meson
then show ?thesis
using S_calculus.weakly_fair_def S_with_conj_is_calculus calculus.fair_def
by blast
qed
text ‹
The following proof works as follows.
We assume that ‹(Inf, (Red⇩I, Red⇩F))› is statically complete.
From that and theorem @{thm S_calculus_statically_complete}, we obtain that
‹(SInf, (SRed⇩I, SRed⇩F))› is statically complete.
This means that for all ‹𝒩 ⊆ UNIV›, if ‹𝒩› is saturated w.r.t. ‹(SInf, SRed⇩I)›
and ‹𝒩 ⊨∪⇩A⇩F {⊥}› then ‹⊥ ∈ 𝒩›.
Since ‹⊨∪⇩A⇩F ≡ ⊨∩⇩A⇩F› when the right hand side is a singleton set, we have that
for all ‹𝒩 ⊆ UNIV›, if ‹𝒩› is saturated w.r.t. ‹(SInf, SRed⇩I)› and ‹𝒩 ⊨∩⇩A⇩F {⊥}› then ‹⊥ ∈ 𝒩›.
Because ‹⊨∩⇩A⇩F› is a consequence relation for the Saturation Framework, we can derive
that ‹(SInf, (SRed⇩I, SRed⇩F))› is dynamically complete (using the conjunctive entailment).
We then proceed as above but in the opposite way to show that ‹(SInf, (SRed⇩I, SRed⇩F))›
is dynamically complete using the disjunctive entailment ‹⊨∪⇩A⇩F›.
›
corollary S_calculus_dynamically_complete:
assumes F_statically_complete: ‹statically_complete_calculus bot FInf (⊨) FRed⇩I FRed⇩F›
shows ‹dynamically_complete_calculus (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
proof -
have ‹statically_complete_calculus (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
using S_calculus_statically_complete F_statically_complete
by blast
then have ‹statically_complete_calculus_axioms (to_AF bot) SInf (⊨∩⇩A⇩F) SRed⇩I›
using entails_conj_is_entails_disj_if_right_singleton[where ?𝒞 = ‹to_AF bot›]
unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
by blast
then have ‹Calculus.statically_complete_calculus_axioms {to_AF bot} SInf (⊨∩⇩A⇩F) SRed⇩I›
unfolding statically_complete_calculus_axioms_def
Calculus.statically_complete_calculus_axioms_def
using saturated_equiv
by blast
then have ‹Calculus.statically_complete_calculus {to_AF bot} SInf (⊨∩⇩A⇩F) SRed⇩I SRed⇩F›
using Calculus.statically_complete_calculus.intro S_with_conj_is_calculus
by blast
then have ‹Calculus.dynamically_complete_calculus {to_AF bot} SInf (⊨∩⇩A⇩F) SRed⇩I SRed⇩F›
using S_with_conj_is_calculus calculus.dyn_equiv_stat
by blast
then have ‹Calculus.dynamically_complete_calculus_axioms {to_AF bot} SInf (⊨∩⇩A⇩F) SRed⇩I SRed⇩F›
using Calculus.dynamically_complete_calculus_def
by blast
then have ‹dynamically_complete_calculus_axioms (to_AF bot) SInf (⊨∩⇩A⇩F) SRed⇩I SRed⇩F›
unfolding dynamically_complete_calculus_axioms_def
Calculus.dynamically_complete_calculus_axioms_def
by (metis derivation_equiv fair_equiv llhd.rep_eq llnth.rep_eq singletonD singletonI)
then have ‹dynamically_complete_calculus_axioms (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
unfolding dynamically_complete_calculus_axioms_def
using entails_conj_is_entails_disj_if_right_singleton
by presburger
then show ‹dynamically_complete_calculus (to_AF bot) SInf (⊨⇩A⇩F) SRed⇩I SRed⇩F›
by (simp add: dynamically_complete_calculus_def
S_calculus.calculus_axioms)
qed
subsection ‹Strong completeness›
theorem S_calculus_strong_statically_complete:
assumes F_statically_complete: ‹statically_complete_calculus bot FInf (⊨) FRed⇩I FRed⇩F› and
𝒩_locally_saturated: ‹locally_saturated 𝒩› and
𝒩_entails_bot: ‹𝒩 ⊨⇩A⇩F {to_AF bot}›
shows ‹to_AF bot ∈ 𝒩›
using 𝒩_locally_saturated
unfolding locally_saturated_def
proof (elim disjE)
show ‹to_AF bot ∈ 𝒩 ⟹ to_AF bot ∈ 𝒩›
by blast
next
assume ‹∃ J. J ⊨⇩p 𝒩 ∧ saturated (𝒩 proj⇩J J)›
then obtain J where J_prop_model_of_𝒩: ‹J ⊨⇩p 𝒩› and
𝒩_proj_J_saturated: ‹saturated (𝒩 proj⇩J J)›
by blast
then have ‹𝒩 proj⇩J J ⊨ {bot}›
using 𝒩_entails_bot AF_entails_def enabled_to_AF_set
by (metis (no_types, lifting) f_of_to_AF image_insert image_is_empty)
then have ‹bot ∈ 𝒩 proj⇩J J›
using 𝒩_proj_J_saturated F_statically_complete
by (simp add: statically_complete_calculus.statically_complete)
then show ‹to_AF bot ∈ 𝒩›
using J_prop_model_of_𝒩
using enabled_projection_def propositional_model_def propositional_projection_def
by force
qed
lemma SRed_of_lim_inf:
‹SRed⇩F (lim_inf 𝒩i) proj⇩J J ⊆ FRed⇩F (lim_inf 𝒩i proj⇩J J) ∪ (lim_inf 𝒩i proj⇩J J)›
proof (intro subsetI)
fix f
assume ‹f ∈ SRed⇩F (lim_inf 𝒩i) proj⇩J J›
then show ‹f ∈ FRed⇩F (lim_inf 𝒩i proj⇩J J) ∪ (lim_inf 𝒩i proj⇩J J)›
unfolding SRed⇩F_def enabled_projection_def enabled_def
using less_eq_fset.rep_eq
by (auto, fastforce)
qed
lemma bot_at_i_implies_bot_at_liminf:
‹is_derivation S_calculus.derive 𝒩i ⟹ to_AF bot ∈ llnth 𝒩i i ⟹ to_AF bot ∈ lim_inf 𝒩i›
proof -
assume 𝒩i_is_derivation: ‹is_derivation S_calculus.derive 𝒩i› and
bot_at_i: ‹to_AF bot ∈ llnth 𝒩i i›
then have ‹∀ i. llnth 𝒩i i - llnth 𝒩i (Suc i) ⊆ SRed⇩F (llnth 𝒩i (Suc i))›
unfolding is_derivation_def S_calculus.derive_def
by blast
then show ?thesis
using bot_at_i
proof (transfer fixing: bot i FRed⇩F)
fix 𝒩i'
assume llength_is_infinity: ‹llength 𝒩i' = ∞› and
bot_at_i: ‹to_AF bot ∈ lnth 𝒩i' i› and
all_at_i_minus_next_i_are_redundant:
‹∀ i. lnth 𝒩i' i - lnth 𝒩i' (Suc i) ⊆ SRed⇩F (lnth 𝒩i' (Suc i))›
then have ‹to_AF bot ∈ lnth 𝒩i' (Suc i)›
using bot_not_in_sredF_𝒩
by auto
then have ‹∀ j ≥ i. to_AF bot ∈ lnth 𝒩i' j›
proof (intro allI impI)
fix j
assume ‹i ≤ j›
then show ‹to_AF bot ∈ lnth 𝒩i' j›
proof (induct j rule: full_nat_induct)
case less: (1 n)
show ?case
proof (cases ‹i = n›)
case True
then show ?thesis
using bot_at_i
by force
next
case False
then have i_less_than_n: ‹i < n›
using le_eq_less_or_eq less.prems
by presburger
then have n_positive: ‹n > 0›
by force
then have ‹to_AF bot ∈ lnth 𝒩i' (n - 1)›
using i_less_than_n less.hyps
by fastforce
then show ?thesis
using all_at_i_minus_next_i_are_redundant[rule_format, of ‹n - 1›]
bot_not_in_sredF_𝒩 n_positive
by auto
qed
qed
qed
then have ‹∃ i. ∀ j ≥ i. to_AF bot ∈ lnth 𝒩i' j›
by blast
then show ‹to_AF bot ∈ Liminf_llist 𝒩i'›
using llength_is_infinity
unfolding Liminf_llist_def
by auto
qed
qed
lemma Red_I_of_inf_FRed⇩F_subset_Red_I_of_inf:
‹FRed⇩I ((lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J)) = FRed⇩I (lim_inf 𝒩i proj⇩J J)›
proof (intro subset_antisym)
have ‹FRed⇩F (lim_inf 𝒩i proj⇩J J) ⊆ FRed⇩F ((lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J))›
by (simp add: Red_F_of_subset)
then show ‹FRed⇩I ((lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J)) ⊆ FRed⇩I (lim_inf 𝒩i proj⇩J J)›
by (smt (verit, del_insts) DiffE Red_I_of_Red_F_subset Red_I_of_subset Un_iff subset_iff)
next
show ‹FRed⇩I (lim_inf 𝒩i proj⇩J J) ⊆ FRed⇩I ((lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J))›
by (simp add: Red_I_of_subset)
qed
lemma locally_fair_derivation_is_saturated_at_liminf:
‹is_derivation S_calculus.derive 𝒩i ⟹ locally_fair 𝒩i ⟹ locally_saturated (lim_inf 𝒩i)›
proof -
assume 𝒩i_is_derivation: ‹is_derivation S_calculus.derive 𝒩i› and
‹locally_fair 𝒩i›
then show ‹locally_saturated (lim_inf 𝒩i)›
unfolding locally_fair_def
proof (elim disjE)
assume ‹∃ i. to_AF bot ∈ llnth 𝒩i i›
then obtain i where ‹to_AF bot ∈ llnth 𝒩i i›
by blast
then have ‹to_AF bot ∈ lim_inf 𝒩i›
using bot_at_i_implies_bot_at_liminf[OF 𝒩i_is_derivation]
by blast
then show ?thesis
unfolding locally_saturated_def
by blast
next
assume ‹∃ J. J ⊨⇩p limit 𝒩i ∧ Inf_from (limit 𝒩i proj⇩J J) ⊆ (⋃ i. FRed⇩I (llnth 𝒩i i proj⇩J J))›
then obtain J where J_prop_model_of_limit: ‹J ⊨⇩p limit 𝒩i› and
all_inf_of_limit_are_redundant:
‹Inf_from (limit 𝒩i proj⇩J J) ⊆ (⋃ i. FRed⇩I (llnth 𝒩i i proj⇩J J))›
by blast
then have ‹∀ i. llnth 𝒩i i ⊆ lim_inf 𝒩i ∪ SRed⇩F (lim_inf 𝒩i)›
using Calculus.calculus.i_in_Liminf_or_Red_F[OF S_with_conj_is_calculus, of ‹to_llist 𝒩i›]
derivation_equiv[of ‹𝒩i›]
by (simp add: Liminf_infinite_llist.rep_eq 𝒩i_is_derivation llength_of_to_llist_is_infinite
llnth.rep_eq sup_commute)
then have ‹∀ i. llnth 𝒩i i proj⇩J J ⊆ (lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J)›
by (smt (verit, best) SRed_of_lim_inf UN_iff UnE UnI1 Un_commute
Union_of_enabled_projection_is_enabled_projection subset_iff)
then have FRed⇩I_in_Red_I_of_FRed⇩F:
‹(⋃ i. FRed⇩I (llnth 𝒩i i proj⇩J J)) ⊆
(⋃ i. FRed⇩I ((lim_inf 𝒩i proj⇩J J) ∪ FRed⇩F (lim_inf 𝒩i proj⇩J J)))›
by (meson Red_I_of_subset SUP_mono UNIV_I)
then have ‹(⋃ i. FRed⇩I (llnth 𝒩i i proj⇩J J)) ⊆ (⋃ i. FRed⇩I (lim_inf 𝒩i proj⇩J J))›
using Red_I_of_inf_FRed⇩F_subset_Red_I_of_inf
by auto
then show ?thesis
unfolding locally_saturated_def
using J_prop_model_of_limit all_inf_of_limit_are_redundant saturated_def
by force
qed
qed
lemma llhd_is_llnth_0: ‹llhd S = llnth S 0›
by (transfer, metis infinity_ne_i0 llength_lnull lnth_0_conv_lhd)
theorem S_calculus_strong_dynamically_complete:
assumes F_statically_complete: ‹statically_complete_calculus bot FInf (⊨) FRed⇩I FRed⇩F› and
𝒩i_is_derivation: ‹is_derivation S_calculus.derive 𝒩i› and
𝒩i_is_locally_fair: ‹locally_fair 𝒩i› and
𝒩i0_entails_bot: ‹llhd 𝒩i ⊨⇩A⇩F {to_AF bot}›
shows ‹∃ i. to_AF bot ∈ llnth 𝒩i i›
proof -
have ‹llhd 𝒩i ⊆ (⋃ i. llnth 𝒩i i)›
by (simp add: SUP_upper llhd_is_llnth_0)
then have ‹(⋃ i. llnth 𝒩i i) ⊨⇩A⇩F {to_AF bot}›
using 𝒩i0_entails_bot
by (meson AF_cons_rel.entails_trans AF_cons_rel.subset_entailed
entails_conj_is_entails_disj_if_right_singleton)
then have ‹(⋃ i. llnth 𝒩i i) - SRed⇩F (⋃ i. llnth 𝒩i i) ⊨⇩A⇩F {to_AF bot}›
using SRed⇩F_entails_bot
by blast
moreover have ‹chain (Calculus.calculus.derive SRed⇩F) (to_llist 𝒩i)›
using derivation_equiv[of ‹𝒩i›] 𝒩i_is_derivation
by blast
then have ‹Sup_llist (to_llist 𝒩i) - Liminf_llist (to_llist 𝒩i) ⊆ SRed⇩F (Sup_llist (to_llist 𝒩i))›
using Calculus.calculus.Red_in_Sup[OF S_with_conj_is_calculus]
by blast
then have ‹(⋃ i. llnth 𝒩i i) - SRed⇩F (⋃ i. llnth 𝒩i i) ⊆ lim_inf 𝒩i›
by (transfer fixing: FRed⇩F, unfold Sup_llist_def Liminf_llist_def, auto)
ultimately have 𝒩i_inf_entails_bot: ‹lim_inf 𝒩i ⊨⇩A⇩F {to_AF bot}›
by (meson AF_cons_rel.entails_subsets subset_iff)
then have 𝒩i_inf_locally_saturated: ‹locally_saturated (lim_inf 𝒩i)›
using 𝒩i_is_derivation 𝒩i_is_locally_fair
using locally_fair_derivation_is_saturated_at_liminf
by blast
then have ‹to_AF bot ∈ lim_inf 𝒩i›
using F_statically_complete S_calculus_strong_statically_complete 𝒩i_inf_entails_bot
by blast
then show ‹∃ i. to_AF bot ∈ llnth 𝒩i i›
by (transfer fixing: bot)
(meson Liminf_llist_imp_exists_index)
qed
end
section ‹Extensions: Inferences and simplifications›
subsection ‹Simplifications›