Theory Lifting_to_Non_Ground_Calculi
section ‹Lifting to Non-ground Calculi›
text ‹The section 3.1 to 3.3 of the report are covered by the current section.
Various forms of lifting are proven correct. These allow to obtain the dynamic
refutational completeness of a non-ground calculus from the static refutational
completeness of its ground counterpart.›
theory Lifting_to_Non_Ground_Calculi
imports
Intersection_Calculus
Calculus_Variations
Well_Quasi_Orders.Minimal_Elements
begin
subsection ‹Standard Lifting›
locale standard_lifting = inference_system Inf_F +
ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G
for
Inf_F :: ‹'f inference set› and
Bot_G :: ‹'g set› and
Inf_G :: ‹'g inference set› and
entails_G :: ‹'g set ⇒ 'g set ⇒ bool› (infix ‹⊨G› 50) and
Red_I_G :: ‹'g set ⇒ 'g inference set› and
Red_F_G :: ‹'g set ⇒ 'g set›
+ fixes
Bot_F :: ‹'f set› and
𝒢_F :: ‹'f ⇒ 'g set› and
𝒢_I :: ‹'f inference ⇒ 'g inference set option›
assumes
Bot_F_not_empty: "Bot_F ≠ {}" and
Bot_map_not_empty: ‹B ∈ Bot_F ⟹ 𝒢_F B ≠ {}› and
Bot_map: ‹B ∈ Bot_F ⟹ 𝒢_F B ⊆ Bot_G› and
Bot_cond: ‹𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F› and
inf_map: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))›
begin
abbreviation 𝒢_Fset :: ‹'f set ⇒ 'g set› where
‹𝒢_Fset N ≡ ⋃ (𝒢_F ` N)›
lemma 𝒢_subset: ‹N1 ⊆ N2 ⟹ 𝒢_Fset N1 ⊆ 𝒢_Fset N2› by auto
abbreviation entails_𝒢 :: ‹'f set ⇒ 'f set ⇒ bool› (infix ‹⊨𝒢› 50) where
‹N1 ⊨𝒢 N2 ≡ 𝒢_Fset N1 ⊨G 𝒢_Fset N2›
lemma subs_Bot_G_entails:
assumes
not_empty: ‹sB ≠ {}› and
in_bot: ‹sB ⊆ Bot_G›
shows ‹sB ⊨G N›
proof -
have ‹∃B. B ∈ sB› using not_empty by auto
then obtain B where B_in: ‹B ∈ sB› by auto
then have r_trans: ‹{B} ⊨G N› using ground.bot_entails_all in_bot by auto
have l_trans: ‹sB ⊨G {B}› using B_in ground.subset_entailed by auto
then show ?thesis using r_trans ground.entails_trans[of sB "{B}"] by auto
qed
sublocale consequence_relation Bot_F entails_𝒢
proof
show "Bot_F ≠ {}" using Bot_F_not_empty .
next
show ‹B∈Bot_F ⟹ {B} ⊨𝒢 N› for B N
proof -
assume ‹B ∈ Bot_F›
then show ‹{B} ⊨𝒢 N›
using Bot_map ground.bot_entails_all[of _ "𝒢_Fset N"] subs_Bot_G_entails Bot_map_not_empty
by auto
qed
next
fix N1 N2 :: ‹'f set›
assume
‹N2 ⊆ N1›
then show ‹N1 ⊨𝒢 N2› using 𝒢_subset ground.subset_entailed by auto
next
fix N1 N2
assume
N1_entails_C: ‹∀C ∈ N2. N1 ⊨𝒢 {C}›
show ‹N1 ⊨𝒢 N2› using ground.all_formulas_entailed N1_entails_C
by (smt UN_E UN_I ground.entail_set_all_formulas singletonI)
next
fix N1 N2 N3
assume
‹N1 ⊨𝒢 N2› and ‹N2 ⊨𝒢 N3›
then show ‹N1 ⊨𝒢 N3› using ground.entails_trans by blast
qed
definition Red_I_𝒢 :: "'f set ⇒ 'f inference set" where
‹Red_I_𝒢 N = {ι ∈ Inf_F. (𝒢_I ι ≠ None ∧ the (𝒢_I ι) ⊆ Red_I_G (𝒢_Fset N))
∨ (𝒢_I ι = None ∧ 𝒢_F (concl_of ι) ⊆ 𝒢_Fset N ∪ Red_F_G (𝒢_Fset N))}›
definition Red_F_𝒢 :: "'f set ⇒ 'f set" where
‹Red_F_𝒢 N = {C. ∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N)}›
end
subsection ‹Strong Standard Lifting›
locale strong_standard_lifting = inference_system Inf_F +
ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G
for
Inf_F :: ‹'f inference set› and
Bot_G :: ‹'g set› and
Inf_G :: ‹'g inference set› and
entails_G :: ‹'g set ⇒ 'g set ⇒ bool› (infix ‹⊨G› 50) and
Red_I_G :: ‹'g set ⇒ 'g inference set› and
Red_F_G :: ‹'g set ⇒ 'g set›
+ fixes
Bot_F :: ‹'f set› and
𝒢_F :: ‹'f ⇒ 'g set› and
𝒢_I :: ‹'f inference ⇒ 'g inference set option›
assumes
Bot_F_not_empty: "Bot_F ≠ {}" and
Bot_map_not_empty: ‹B ∈ Bot_F ⟹ 𝒢_F B ≠ {}› and
Bot_map: ‹B ∈ Bot_F ⟹ 𝒢_F B ⊆ Bot_G› and
Bot_cond: ‹𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F› and
strong_inf_map: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ concl_of ` (the (𝒢_I ι)) ⊆ (𝒢_F (concl_of ι))› and
inf_map_in_Inf: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Inf_G›
begin
sublocale standard_lifting Inf_F Bot_G Inf_G "(⊨G)" Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
proof
show "Bot_F ≠ {}" using Bot_F_not_empty .
next
fix B
assume b_in: "B ∈ Bot_F"
show "𝒢_F B ≠ {}" using Bot_map_not_empty[OF b_in] .
next
fix B
assume b_in: "B ∈ Bot_F"
show "𝒢_F B ⊆ Bot_G" using Bot_map[OF b_in] .
next
show "⋀C. 𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F" using Bot_cond .
next
fix ι
assume i_in: "ι ∈ Inf_F" and
some_g: "𝒢_I ι ≠ None"
show "the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))"
proof
fix ιG
assume ig_in1: "ιG ∈ the (𝒢_I ι)"
then have ig_in2: "ιG ∈ Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast
show "ιG ∈ Red_I_G (𝒢_F (concl_of ι))"
using strong_inf_map[OF i_in some_g] ground.Red_I_of_Inf_to_N[OF ig_in2]
ig_in1 by blast
qed
qed
end
subsection ‹Lifting with a Family of Tiebreaker Orderings›
locale tiebreaker_lifting =
empty_ord?: standard_lifting Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
for
Bot_F :: ‹'f set› and
Inf_F :: ‹'f inference set› and
Bot_G :: ‹'g set› and
entails_G :: ‹'g set ⇒ 'g set ⇒ bool› (infix ‹⊨G› 50) and
Inf_G :: ‹'g inference set› and
Red_I_G :: ‹'g set ⇒ 'g inference set› and
Red_F_G :: ‹'g set ⇒ 'g set› and
𝒢_F :: "'f ⇒ 'g set" and
𝒢_I :: "'f inference ⇒ 'g inference set option"
+ fixes
Prec_F_g :: ‹'g ⇒ 'f ⇒ 'f ⇒ bool›
assumes
all_wf: "minimal_element (Prec_F_g g) UNIV"
begin
definition Red_F_𝒢 :: "'f set ⇒ 'f set" where
‹Red_F_𝒢 N = {C. ∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)}›
lemma Prec_trans:
assumes
‹Prec_F_g D A B› and
‹Prec_F_g D B C›
shows
‹Prec_F_g D A C›
using minimal_element.po assms unfolding po_on_def transp_on_def by (smt UNIV_I all_wf)
lemma prop_nested_in_set: "D ∈ P C ⟹ C ∈ {C. ∀D ∈ P C. A D ∨ B C D} ⟹ A D ∨ B C D"
by blast
lemma Red_F_𝒢_equiv_def:
‹Red_F_𝒢 N = {C. ∀Di ∈ 𝒢_F C. Di ∈ Red_F_G (𝒢_Fset N) ∨
(∃E ∈ (N - Red_F_𝒢 N). Prec_F_g Di E C ∧ Di ∈ 𝒢_F E)}›
proof (rule; clarsimp)
fix C D
assume
C_in: ‹C ∈ Red_F_𝒢 N› and
D_in: ‹D ∈ 𝒢_F C› and
not_sec_case: ‹∀E ∈ N - Red_F_𝒢 N. Prec_F_g D E C ⟶ D ∉ 𝒢_F E›
have C_in_unfolded: "C ∈ {C. ∀Di ∈ 𝒢_F C. Di ∈ Red_F_G (𝒢_Fset N) ∨
(∃E∈N. Prec_F_g Di E C ∧ Di ∈ 𝒢_F E)}"
using C_in unfolding Red_F_𝒢_def .
have neg_not_sec_case: ‹¬ (∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
using not_sec_case by clarsimp
have unfol_C_D: ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
using prop_nested_in_set[of D 𝒢_F C "λx. x ∈ Red_F_G (⋃ (𝒢_F ` N))"
"λx y. ∃E ∈ N. Prec_F_g y E x ∧ y ∈ 𝒢_F E", OF D_in C_in_unfolded] by blast
show ‹D ∈ Red_F_G (𝒢_Fset N)›
proof (rule ccontr)
assume contrad: ‹D ∉ Red_F_G (𝒢_Fset N)›
have non_empty: ‹∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E› using contrad unfol_C_D by auto
define B where ‹B = {E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F E}›
then have B_non_empty: ‹B ≠ {}› using non_empty by auto
interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
obtain F :: 'f where F: ‹F = min_elt B› by auto
then have D_in_F: ‹D ∈ 𝒢_F F› unfolding B_def using non_empty
by (smt Sup_UNIV Sup_upper UNIV_I contra_subsetD empty_iff empty_subsetI mem_Collect_eq
min_elt_mem unfol_C_D)
have F_prec: ‹Prec_F_g D F C› using F min_elt_mem[of B, OF _ B_non_empty] unfolding B_def by auto
have F_not_in: ‹F ∉ Red_F_𝒢 N›
proof
assume F_in: ‹F ∈ Red_F_𝒢 N›
have unfol_F_D: ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃G∈N. Prec_F_g D G F ∧ D ∈ 𝒢_F G)›
using F_in D_in_F unfolding Red_F_𝒢_def by auto
then have ‹∃G∈N. Prec_F_g D G F ∧ D ∈ 𝒢_F G› using contrad D_in unfolding Red_F_𝒢_def by auto
then obtain G where G_in: ‹G ∈ N› and G_prec: ‹Prec_F_g D G F› and G_map: ‹D ∈ 𝒢_F G› by auto
have ‹Prec_F_g D G C› using G_prec F_prec Prec_trans by blast
then have ‹G ∈ B› unfolding B_def using G_in G_map by auto
then show ‹False› using F G_prec min_elt_minimal[of B G, OF _ B_non_empty] by auto
qed
have ‹F ∈ N› using F by (metis B_def B_non_empty mem_Collect_eq min_elt_mem top_greatest)
then have ‹F ∈ N - Red_F_𝒢 N› using F_not_in by auto
then show ‹False›
using D_in_F neg_not_sec_case F_prec by blast
qed
next
fix C
assume only_if: ‹∀D∈𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
show ‹C ∈ Red_F_𝒢 N› unfolding Red_F_𝒢_def using only_if by auto
qed
lemma not_red_map_in_map_not_red: ‹𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊆ 𝒢_Fset (N - Red_F_𝒢 N)›
proof
fix D
assume
D_hyp: ‹D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N)›
interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
have D_in: ‹D ∈ 𝒢_Fset N› using D_hyp by blast
have D_not_in: ‹D ∉ Red_F_G (𝒢_Fset N)› using D_hyp by blast
have exist_C: ‹∃C. C ∈ N ∧ D ∈ 𝒢_F C› using D_in by auto
define B where ‹B = {C ∈ N. D ∈ 𝒢_F C}›
obtain C where C: ‹C = min_elt B› by auto
have C_in_N: ‹C ∈ N›
using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
have D_in_C: ‹D ∈ 𝒢_F C›
using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
have C_not_in: ‹C ∉ Red_F_𝒢 N›
proof
assume C_in: ‹C ∈ Red_F_𝒢 N›
have ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
using C_in D_in_C unfolding Red_F_𝒢_def by auto
then show ‹False›
proof
assume ‹D ∈ Red_F_G (𝒢_Fset N)›
then show ‹False› using D_not_in by simp
next
assume ‹∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E›
then show ‹False›
using C by (metis (no_types, lifting) B_def UNIV_I empty_iff mem_Collect_eq
min_elt_minimal top_greatest)
qed
qed
show ‹D ∈ 𝒢_Fset (N - Red_F_𝒢 N)› using D_in_C C_not_in C_in_N by blast
qed
lemma Red_F_Bot_F: ‹B ∈ Bot_F ⟹ N ⊨𝒢 {B} ⟹ N - Red_F_𝒢 N ⊨𝒢 {B}›
proof -
fix B N
assume
B_in: ‹B ∈ Bot_F› and
N_entails: ‹N ⊨𝒢 {B}›
then have to_bot: ‹𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊨G 𝒢_F B›
using ground.Red_F_Bot Bot_map
by (smt cSup_singleton ground.entail_set_all_formulas image_insert image_is_empty subsetCE)
have from_f: ‹𝒢_Fset (N - Red_F_𝒢 N) ⊨G 𝒢_Fset N - Red_F_G (𝒢_Fset N)›
using ground.subset_entailed[OF not_red_map_in_map_not_red] by blast
then have ‹𝒢_Fset (N - Red_F_𝒢 N) ⊨G 𝒢_F B› using to_bot ground.entails_trans by blast
then show ‹N - Red_F_𝒢 N ⊨𝒢 {B}› using Bot_map by simp
qed
lemma Red_F_of_subset_F: ‹N ⊆ N' ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 N'›
using ground.Red_F_of_subset unfolding Red_F_𝒢_def by clarsimp (meson 𝒢_subset subsetD)
lemma Red_I_of_subset_F: ‹N ⊆ N' ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 N'›
using Collect_mono 𝒢_subset subset_iff ground.Red_I_of_subset unfolding Red_I_𝒢_def
by (smt ground.Red_F_of_subset Un_iff)
lemma Red_F_of_Red_F_subset_F: ‹N' ⊆ Red_F_𝒢 N ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 (N - N')›
proof
fix N N' C
assume
N'_in_Red_F_N: ‹N' ⊆ Red_F_𝒢 N› and
C_in_red_F_N: ‹C ∈ Red_F_𝒢 N›
have lem8: ‹∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ (N - Red_F_𝒢 N). Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
using Red_F_𝒢_equiv_def C_in_red_F_N by blast
show ‹C ∈ Red_F_𝒢 (N - N')› unfolding Red_F_𝒢_def
proof (rule,rule)
fix D
assume ‹D ∈ 𝒢_F C›
then have ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ (N - Red_F_𝒢 N). Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
using lem8 by auto
then show ‹D ∈ Red_F_G (𝒢_Fset (N - N')) ∨ (∃E∈N - N'. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
proof
assume ‹D ∈ Red_F_G (𝒢_Fset N)›
then have ‹D ∈ Red_F_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))›
using ground.Red_F_of_Red_F_subset[of "Red_F_G (𝒢_Fset N)" "𝒢_Fset N"] by auto
then have ‹D ∈ Red_F_G (𝒢_Fset (N - Red_F_𝒢 N))›
using ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
then have ‹D ∈ Red_F_G (𝒢_Fset (N - N'))›
using N'_in_Red_F_N 𝒢_subset[of "N - Red_F_𝒢 N" "N - N'"]
by (smt DiffE DiffI ground.Red_F_of_subset subsetCE subsetI)
then show ?thesis by blast
next
assume ‹∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E›
then obtain E where
E_in: ‹E∈N - Red_F_𝒢 N› and
E_prec_C: ‹Prec_F_g D E C› and
D_in: ‹D ∈ 𝒢_F E›
by auto
have ‹E ∈ N - N'› using E_in N'_in_Red_F_N by blast
then show ?thesis using E_prec_C D_in by blast
qed
qed
qed
lemma Red_I_of_Red_F_subset_F: ‹N' ⊆ Red_F_𝒢 N ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 (N - N') ›
proof
fix N N' ι
assume
N'_in_Red_F_N: ‹N' ⊆ Red_F_𝒢 N› and
i_in_Red_I_N: ‹ι ∈ Red_I_𝒢 N›
have i_in: ‹ι ∈ Inf_F› using i_in_Red_I_N unfolding Red_I_𝒢_def by blast
{
assume not_none: "𝒢_I ι ≠ None"
have ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset N)›
using not_none i_in_Red_I_N unfolding Red_I_𝒢_def by auto
then have ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))›
using not_none ground.Red_I_of_Red_F_subset by blast
then have ip_in_Red_I_G: ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset (N - Red_F_𝒢 N))›
using not_none ground.Red_I_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
then have not_none_in: ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset (N - N'))›
using not_none N'_in_Red_F_N
by (meson Diff_mono ground.Red_I_of_subset 𝒢_subset subset_iff subset_refl)
then have "the (𝒢_I ι) ⊆ Red_I_G (𝒢_Fset (N - N'))" by blast
}
moreover {
assume none: "𝒢_I ι = None"
have ground_concl_subs: "𝒢_F (concl_of ι) ⊆ (𝒢_Fset N ∪ Red_F_G (𝒢_Fset N))"
using none i_in_Red_I_N unfolding Red_I_𝒢_def by blast
then have d_in_imp12: "D ∈ 𝒢_F (concl_of ι) ⟹ D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N) ∨ D ∈ Red_F_G (𝒢_Fset N)"
by blast
have d_in_imp1: "D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N) ⟹ D ∈ 𝒢_Fset (N - N')"
using not_red_map_in_map_not_red N'_in_Red_F_N by blast
have d_in_imp_d_in: "D ∈ Red_F_G (𝒢_Fset N) ⟹ D ∈ Red_F_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))"
using ground.Red_F_of_Red_F_subset[of "Red_F_G (𝒢_Fset N)" "𝒢_Fset N"] by blast
have g_subs1: "𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊆ 𝒢_Fset (N - Red_F_𝒢 N)"
using not_red_map_in_map_not_red unfolding Red_F_𝒢_def by auto
have g_subs2: "𝒢_Fset (N - Red_F_𝒢 N) ⊆ 𝒢_Fset (N - N')"
using N'_in_Red_F_N by blast
have d_in_imp2: "D ∈ Red_F_G (𝒢_Fset N) ⟹ D ∈ Red_F_G (𝒢_Fset (N - N'))"
using ground.Red_F_of_subset ground.Red_F_of_subset[OF g_subs1]
ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast
have "𝒢_F (concl_of ι) ⊆ (𝒢_Fset (N - N') ∪ Red_F_G (𝒢_Fset (N - N')))"
using d_in_imp12 d_in_imp1 d_in_imp2
by (smt ground.Red_F_of_Red_F_subset ground.Red_F_of_subset UnCI UnE Un_Diff_cancel2
ground_concl_subs g_subs1 g_subs2 subset_iff)
}
ultimately show ‹ι ∈ Red_I_𝒢 (N - N')› using i_in unfolding Red_I_𝒢_def by auto
qed
lemma Red_I_of_Inf_to_N_F:
assumes
i_in: ‹ι ∈ Inf_F› and
concl_i_in: ‹concl_of ι ∈ N›
shows
‹ι ∈ Red_I_𝒢 N ›
proof -
have ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))› using inf_map by simp
moreover have ‹Red_I_G (𝒢_F (concl_of ι)) ⊆ Red_I_G (𝒢_Fset N)›
using concl_i_in ground.Red_I_of_subset by blast
moreover have "ι ∈ Inf_F ⟹ 𝒢_I ι = None ⟹ concl_of ι ∈ N ⟹ 𝒢_F (concl_of ι) ⊆ 𝒢_Fset N"
by blast
ultimately show ?thesis using i_in concl_i_in unfolding Red_I_𝒢_def by auto
qed
sublocale calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢
proof
fix B N N' ι
show ‹Red_I_𝒢 N ⊆ Inf_F› unfolding Red_I_𝒢_def by blast
show ‹B ∈ Bot_F ⟹ N ⊨𝒢 {B} ⟹ N - Red_F_𝒢 N ⊨𝒢 {B}› using Red_F_Bot_F by simp
show ‹N ⊆ N' ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 N'› using Red_F_of_subset_F by simp
show ‹N ⊆ N' ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 N'› using Red_I_of_subset_F by simp
show ‹N' ⊆ Red_F_𝒢 N ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 (N - N')› using Red_F_of_Red_F_subset_F by simp
show ‹N' ⊆ Red_F_𝒢 N ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 (N - N')› using Red_I_of_Red_F_subset_F by simp
show ‹ι ∈ Inf_F ⟹ concl_of ι ∈ N ⟹ ι ∈ Red_I_𝒢 N› using Red_I_of_Inf_to_N_F by simp
qed
end
lemma wf_empty_rel: "minimal_element (λ_ _. False) UNIV"
by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on)
lemma standard_empty_tiebreaker_equiv: "standard_lifting Inf_F Bot_G Inf_G entails_G Red_I_G
Red_F_G Bot_F 𝒢_F 𝒢_I = tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G
Red_F_G 𝒢_F 𝒢_I (λg C C'. False)"
proof -
have "tiebreaker_lifting_axioms (λg C C'. False)"
unfolding tiebreaker_lifting_axioms_def using wf_empty_rel by simp
then show ?thesis
unfolding standard_lifting_def tiebreaker_lifting_def by blast
qed
context standard_lifting
begin
interpretation empt_ord: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G
Red_F_G 𝒢_F 𝒢_I "λg C C'. False"
using standard_empty_tiebreaker_equiv using standard_lifting_axioms by blast
lemma red_f_equiv: "empt_ord.Red_F_𝒢 = Red_F_𝒢"
unfolding Red_F_𝒢_def empt_ord.Red_F_𝒢_def by simp
sublocale calc?: calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢
using empt_ord.calculus_axioms red_f_equiv by fastforce
lemma grounded_inf_in_ground_inf: "ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Inf_G"
using inf_map ground.Red_I_to_Inf by blast
abbreviation ground_Inf_overapproximated :: "'f set ⇒ bool" where
"ground_Inf_overapproximated N ≡ ground.Inf_from (𝒢_Fset N)
⊆ {ι. ∃ι'∈ Inf_from N. 𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')} ∪ Red_I_G (𝒢_Fset N)"
lemma sat_inf_imp_ground_red:
assumes
"saturated N" and
"ι' ∈ Inf_from N" and
"𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')"
shows "ι ∈ Red_I_G (𝒢_Fset N)"
using assms Red_I_𝒢_def unfolding saturated_def by auto
lemma sat_imp_ground_sat:
"saturated N ⟹ ground_Inf_overapproximated N ⟹ ground.saturated (𝒢_Fset N)"
unfolding ground.saturated_def using sat_inf_imp_ground_red by auto
theorem stat_ref_comp_to_non_ground:
assumes
stat_ref_G: "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G" and
sat_n_imp: "⋀N. saturated N ⟹ ground_Inf_overapproximated N"
shows
"statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢"
proof
fix B N
assume
b_in: "B ∈ Bot_F" and
sat_n: "saturated N" and
n_entails_bot: "N ⊨𝒢 {B}"
have ground_n_entails: "𝒢_Fset N ⊨G 𝒢_F B"
using n_entails_bot by simp
then obtain BG where bg_in1: "BG ∈ 𝒢_F B"
using Bot_map_not_empty[OF b_in] by blast
then have bg_in: "BG ∈ Bot_G"
using Bot_map[OF b_in] by blast
have ground_n_entails_bot: "𝒢_Fset N ⊨G {BG}"
using ground_n_entails bg_in1 ground.entail_set_all_formulas by blast
have "ground.Inf_from (𝒢_Fset N) ⊆
{ι. ∃ι'∈ Inf_from N. 𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')} ∪ Red_I_G (𝒢_Fset N)"
using sat_n_imp[OF sat_n] .
have "ground.saturated (𝒢_Fset N)"
using sat_imp_ground_sat[OF sat_n sat_n_imp[OF sat_n]] .
then have "∃BG'∈Bot_G. BG' ∈ (𝒢_Fset N)"
using stat_ref_G ground.calculus_axioms bg_in ground_n_entails_bot
unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
by blast
then show "∃B'∈ Bot_F. B' ∈ N"
using bg_in Bot_cond Bot_map_not_empty Bot_cond
by blast
qed
end
context tiebreaker_lifting
begin
lemma saturated_empty_order_equiv_saturated:
"saturated N = calc.saturated N"
by (rule refl)
lemma static_empty_order_equiv_static:
"statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢 =
statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 empty_ord.Red_F_𝒢"
unfolding statically_complete_calculus_def
by (rule iffI) (standard,(standard)[],simp)+
theorem static_to_dynamic:
"statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 empty_ord.Red_F_𝒢 =
dynamically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢"
using dyn_equiv_stat static_empty_order_equiv_static
by blast
end
subsection ‹Lifting with a Family of Redundancy Criteria›
locale lifting_intersection = inference_system Inf_F +
ground: inference_system_family Q Inf_G_q +
ground: consequence_relation_family Bot_G Q entails_q
for
Inf_F :: "'f inference set" and
Bot_G :: "'g set" and
Q :: "'q set" and
Inf_G_q :: ‹'q ⇒ 'g inference set› and
entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
Red_F_q :: "'q ⇒ 'g set ⇒ 'g set"
+ fixes
Bot_F :: "'f set" and
𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option" and
Prec_F_g :: "'g ⇒ 'f ⇒ 'f ⇒ bool"
assumes
standard_lifting_family:
"∀q ∈ Q. tiebreaker_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q)
(Red_F_q q) (𝒢_F_q q) (𝒢_I_q q) Prec_F_g"
begin
abbreviation 𝒢_Fset_q :: "'q ⇒ 'f set ⇒ 'g set" where
"𝒢_Fset_q q N ≡ ⋃ (𝒢_F_q q ` N)"
definition Red_I_𝒢_q :: "'q ⇒ 'f set ⇒ 'f inference set" where
"Red_I_𝒢_q q N = {ι ∈ Inf_F. (𝒢_I_q q ι ≠ None ∧ the (𝒢_I_q q ι) ⊆ Red_I_q q (𝒢_Fset_q q N))
∨ (𝒢_I_q q ι = None ∧ 𝒢_F_q q (concl_of ι) ⊆ (𝒢_Fset_q q N ∪ Red_F_q q (𝒢_Fset_q q N)))}"
definition Red_F_𝒢_empty_q :: "'q ⇒ 'f set ⇒ 'f set" where
"Red_F_𝒢_empty_q q N = {C. ∀D ∈ 𝒢_F_q q C. D ∈ Red_F_q q (𝒢_Fset_q q N)}"
definition Red_F_𝒢_q :: "'q ⇒ 'f set ⇒ 'f set" where
"Red_F_𝒢_q q N =
{C. ∀D ∈ 𝒢_F_q q C. D ∈ Red_F_q q (𝒢_Fset_q q N) ∨ (∃E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F_q q E)}"
abbreviation entails_𝒢_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ bool" where
"entails_𝒢_q q N1 N2 ≡ entails_q q (𝒢_Fset_q q N1) (𝒢_Fset_q q N2)"
lemma red_crit_lifting_family:
assumes q_in: "q ∈ Q"
shows "calculus Bot_F Inf_F (entails_𝒢_q q) (Red_I_𝒢_q q) (Red_F_𝒢_q q)"
proof -
interpret wf_lift:
tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
"Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" Prec_F_g
using standard_lifting_family q_in by metis
have "Red_I_𝒢_q q = wf_lift.Red_I_𝒢"
unfolding Red_I_𝒢_q_def wf_lift.Red_I_𝒢_def by blast
moreover have "Red_F_𝒢_q q = wf_lift.Red_F_𝒢"
unfolding Red_F_𝒢_q_def wf_lift.Red_F_𝒢_def by blast
ultimately show ?thesis
using wf_lift.calculus_axioms by simp
qed
lemma red_crit_lifting_family_empty_ord:
assumes q_in: "q ∈ Q"
shows "calculus Bot_F Inf_F (entails_𝒢_q q) (Red_I_𝒢_q q) (Red_F_𝒢_empty_q q)"
proof -
interpret wf_lift:
tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
"Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" Prec_F_g
using standard_lifting_family q_in by metis
have "Red_I_𝒢_q q = wf_lift.Red_I_𝒢"
unfolding Red_I_𝒢_q_def wf_lift.Red_I_𝒢_def by blast
moreover have "Red_F_𝒢_empty_q q = wf_lift.empty_ord.Red_F_𝒢"
unfolding Red_F_𝒢_empty_q_def wf_lift.empty_ord.Red_F_𝒢_def by blast
ultimately show ?thesis
using wf_lift.calc.calculus_axioms by simp
qed
sublocale consequence_relation_family Bot_F Q entails_𝒢_q
proof (unfold_locales; (intro ballI)?)
show "Q ≠ {}"
by (rule ground.Q_nonempty)
next
fix qi
assume qi_in: "qi ∈ Q"
interpret lift: tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q qi" "Inf_G_q qi"
"Red_I_q qi" "Red_F_q qi" "𝒢_F_q qi" "𝒢_I_q qi" Prec_F_g
using qi_in by (metis standard_lifting_family)
show "consequence_relation Bot_F (entails_𝒢_q qi)"
by unfold_locales
qed
sublocale intersection_calculus Bot_F Inf_F Q entails_𝒢_q Red_I_𝒢_q Red_F_𝒢_q
by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family)
abbreviation entails_𝒢 :: "'f set ⇒ 'f set ⇒ bool" (infix ‹⊨∩𝒢› 50) where
"(⊨∩𝒢) ≡ entails"
abbreviation Red_I_𝒢 :: "'f set ⇒ 'f inference set" where
"Red_I_𝒢 ≡ Red_I"
abbreviation Red_F_𝒢 :: "'f set ⇒ 'f set" where
"Red_F_𝒢 ≡ Red_F"
lemmas entails_𝒢_def = entails_def
lemmas Red_I_𝒢_def = Red_I_def
lemmas Red_F_𝒢_def = Red_F_def
sublocale empty_ord: intersection_calculus Bot_F Inf_F Q entails_𝒢_q Red_I_𝒢_q Red_F_𝒢_empty_q
by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family_empty_ord)
abbreviation Red_F_𝒢_empty :: "'f set ⇒ 'f set" where
"Red_F_𝒢_empty ≡ empty_ord.Red_F"
lemmas Red_F_𝒢_empty_def = empty_ord.Red_F_def
lemma sat_inf_imp_ground_red_fam_inter:
assumes
sat_n: "saturated N" and
i'_in: "ι' ∈ Inf_from N" and
q_in: "q ∈ Q" and
grounding: "𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')"
shows "ι ∈ Red_I_q q (𝒢_Fset_q q N)"
proof -
have "ι' ∈ Red_I_𝒢_q q N"
using sat_n i'_in q_in all_red_crit calculus.saturated_def sat_int_to_sat_q
by blast
then have "the (𝒢_I_q q ι') ⊆ Red_I_q q (𝒢_Fset_q q N)"
by (simp add: Red_I_𝒢_q_def grounding)
then show ?thesis
using grounding by blast
qed
abbreviation ground_Inf_overapproximated :: "'q ⇒ 'f set ⇒ bool" where
"ground_Inf_overapproximated q N ≡
ground.Inf_from_q q (𝒢_Fset_q q N)
⊆ {ι. ∃ι'∈ Inf_from N. 𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')} ∪ Red_I_q q (𝒢_Fset_q q N)"
abbreviation ground_saturated :: "'q ⇒ 'f set ⇒ bool" where
"ground_saturated q N ≡ ground.Inf_from_q q (𝒢_Fset_q q N) ⊆ Red_I_q q (𝒢_Fset_q q N)"
lemma sat_imp_ground_sat_fam_inter:
"saturated N ⟹ q ∈ Q ⟹ ground_Inf_overapproximated q N ⟹ ground_saturated q N"
using sat_inf_imp_ground_red_fam_inter by auto
theorem stat_ref_comp_to_non_ground_fam_inter:
assumes
stat_ref_G:
"∀q ∈ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q)
(Red_F_q q)" and
sat_n_imp: "⋀N. saturated N ⟹ ∃q ∈ Q. ground_Inf_overapproximated q N"
shows
"statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢_empty"
using empty_ord.calculus_axioms unfolding statically_complete_calculus_def
statically_complete_calculus_axioms_def
proof (standard, clarify)
fix B N
assume
b_in: "B ∈ Bot_F" and
sat_n: "saturated N" and
entails_bot: "N ⊨∩𝒢 {B}"
then obtain q where
q_in: "q ∈ Q" and
inf_subs: "ground.Inf_from_q q (𝒢_Fset_q q N) ⊆
{ι. ∃ι'∈ Inf_from N. 𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')}
∪ Red_I_q q (𝒢_Fset_q q N)"
using sat_n_imp[of N] by blast
interpret q_calc: calculus Bot_F Inf_F "entails_𝒢_q q" "Red_I_𝒢_q q" "Red_F_𝒢_q q"
using all_red_crit[rule_format, OF q_in] .
have n_q_sat: "q_calc.saturated N"
using q_in sat_int_to_sat_q sat_n by simp
interpret lifted_q_calc:
tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
"Red_F_q q" "𝒢_F_q q" "𝒢_I_q q"
using q_in by (simp add: standard_lifting_family)
have n_lift_sat: "lifted_q_calc.calc.saturated N"
using n_q_sat unfolding Red_I_𝒢_q_def lifted_q_calc.Red_I_𝒢_def
lifted_q_calc.saturated_def q_calc.saturated_def by auto
have ground_sat_n: "lifted_q_calc.ground.saturated (𝒢_Fset_q q N)"
by (rule lifted_q_calc.sat_imp_ground_sat[OF n_lift_sat])
(use n_lift_sat inf_subs ground.Inf_from_q_def in auto)
have ground_n_entails_bot: "entails_𝒢_q q N {B}"
using q_in entails_bot unfolding entails_𝒢_def by simp
interpret statically_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_I_q q"
"Red_F_q q"
using stat_ref_G[rule_format, OF q_in] .
obtain BG where bg_in: "BG ∈ 𝒢_F_q q B"
using lifted_q_calc.Bot_map_not_empty[OF b_in] by blast
then have "BG ∈ Bot_G" using lifted_q_calc.Bot_map[OF b_in] by blast
then have "∃BG'∈Bot_G. BG' ∈ 𝒢_Fset_q q N"
using ground_sat_n ground_n_entails_bot statically_complete[of BG, OF _ ground_sat_n]
bg_in lifted_q_calc.ground.entail_set_all_formulas[of "𝒢_Fset_q q N" "𝒢_Fset_q q {B}"]
by simp
then show "∃B'∈ Bot_F. B' ∈ N" using lifted_q_calc.Bot_cond by blast
qed
lemma sat_eq_sat_empty_order: "saturated N = empty_ord.saturated N"
by (rule refl)
lemma static_empty_ord_inter_equiv_static_inter:
"statically_complete_calculus Bot_F Inf_F entails Red_I Red_F =
statically_complete_calculus Bot_F Inf_F entails Red_I Red_F_𝒢_empty"
unfolding statically_complete_calculus_def
by (simp add: empty_ord.calculus_axioms calculus_axioms)
theorem stat_eq_dyn_ref_comp_fam_inter: "statically_complete_calculus Bot_F Inf_F
entails Red_I Red_F_𝒢_empty =
dynamically_complete_calculus Bot_F Inf_F entails Red_I Red_F"
using dyn_equiv_stat static_empty_ord_inter_equiv_static_inter
by blast
end
end