Theory Labeled_Lifting_to_Non_Ground_Calculi
section ‹Labeled Lifting to Non-Ground Calculi›
text ‹This section formalizes the extension of the lifting results to labeled
calculi. This corresponds to section 3.4 of the report.›
theory Labeled_Lifting_to_Non_Ground_Calculi
imports Lifting_to_Non_Ground_Calculi
begin
lemma po_on_empty_rel[simp]: "po_on (λ_ _. False) UNIV"
unfolding po_on_def irreflp_on_def transp_on_def by auto
subsection ‹Labeled Lifting with a Family of Tiebreaker Orderings›
locale labeled_tiebreaker_lifting = no_labels: tiebreaker_lifting Bot_F Inf_F
Bot_G entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F
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" and
Prec_F :: "'g ⇒ 'f ⇒ 'f ⇒ bool" (infix ‹⊏› 50)
+ fixes
Inf_FL :: ‹('f × 'l) inference set›
assumes
Inf_F_to_Inf_FL: ‹ι⇩F ∈ Inf_F ⟹ length (Ll :: 'l list) = length (prems_of ι⇩F) ⟹
∃L0. Infer (zip (prems_of ι⇩F) Ll) (concl_of ι⇩F, L0) ∈ Inf_FL› and
Inf_FL_to_Inf_F: ‹ι⇩F⇩L ∈ Inf_FL ⟹ Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F›
begin
definition to_F :: ‹('f × 'l) inference ⇒ 'f inference› where
‹to_F ι⇩F⇩L = Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L))›
abbreviation Bot_FL :: ‹('f × 'l) set› where
‹Bot_FL ≡ Bot_F × UNIV›
abbreviation 𝒢_F_L :: ‹('f × 'l) ⇒ 'g set› where
‹𝒢_F_L CL ≡ 𝒢_F (fst CL)›
abbreviation 𝒢_I_L :: ‹('f × 'l) inference ⇒ 'g inference set option› where
‹𝒢_I_L ι⇩F⇩L ≡ 𝒢_I (to_F ι⇩F⇩L)›
sublocale standard_lifting Inf_FL Bot_G Inf_G "(⊨G)" Red_I_G Red_F_G Bot_FL 𝒢_F_L 𝒢_I_L
proof
show "Bot_FL ≠ {}"
using no_labels.Bot_F_not_empty by simp
next
show "B ∈ Bot_FL ⟹ 𝒢_F_L B ≠ {}" for B
using no_labels.Bot_map_not_empty by auto
next
show "B ∈ Bot_FL ⟹ 𝒢_F_L B ⊆ Bot_G" for B
using no_labels.Bot_map by force
next
fix CL
show "𝒢_F_L CL ∩ Bot_G ≠ {} ⟶ CL ∈ Bot_FL"
using no_labels.Bot_cond by (metis SigmaE UNIV_I UNIV_Times_UNIV mem_Sigma_iff prod.sel(1))
next
fix ι
assume
i_in: ‹ι ∈ Inf_FL› and
ground_not_none: ‹𝒢_I_L ι ≠ None›
then show "the (𝒢_I_L ι) ⊆ Red_I_G (𝒢_F_L (concl_of ι))"
unfolding to_F_def using no_labels.inf_map Inf_FL_to_Inf_F by fastforce
qed
notation entails_𝒢 (infix ‹⊨𝒢L› 50)
lemma labeled_entailment_lifting: "NL1 ⊨𝒢L NL2 ⟷ fst ` NL1 ⊨𝒢 fst ` NL2"
by simp
lemma red_inf_impl: "ι ∈ Red_I_𝒢 NL ⟹ to_F ι ∈ no_labels.Red_I_𝒢 (fst ` NL)"
unfolding Red_I_𝒢_def no_labels.Red_I_𝒢_def using Inf_FL_to_Inf_F by (auto simp: to_F_def)
lemma labeled_saturation_lifting: "saturated NL ⟹ no_labels.saturated (fst ` NL)"
unfolding saturated_def no_labels.saturated_def Inf_from_def no_labels.Inf_from_def
proof clarify
fix ι
assume
subs_Red_I: "{ι ∈ Inf_FL. set (prems_of ι) ⊆ NL} ⊆ Red_I_𝒢 NL" and
i_in: "ι ∈ Inf_F" and
i_prems: "set (prems_of ι) ⊆ fst ` NL"
define Lli where "Lli i = (SOME x. ((prems_of ι)!i,x) ∈ NL)" for i
have [simp]:"((prems_of ι)!i,Lli i) ∈ NL" if "i < length (prems_of ι)" for i
using that i_prems unfolding Lli_def by (metis nth_mem someI_ex DomainE Domain_fst subset_eq)
define Ll where "Ll = map Lli [0..<length (prems_of ι)]"
have Ll_length: "length Ll = length (prems_of ι)" unfolding Ll_def by auto
have subs_NL: "set (zip (prems_of ι) Ll) ⊆ NL" unfolding Ll_def by (auto simp:in_set_zip)
obtain L0 where L0: "Infer (zip (prems_of ι) Ll) (concl_of ι, L0) ∈ Inf_FL"
using Inf_F_to_Inf_FL[OF i_in Ll_length] ..
define ι_FL where "ι_FL = Infer (zip (prems_of ι) Ll) (concl_of ι, L0)"
then have "set (prems_of ι_FL) ⊆ NL" using subs_NL by simp
then have "ι_FL ∈ {ι ∈ Inf_FL. set (prems_of ι) ⊆ NL}" unfolding ι_FL_def using L0 by blast
then have "ι_FL ∈ Red_I_𝒢 NL" using subs_Red_I by fast
moreover have "ι = to_F ι_FL" unfolding to_F_def ι_FL_def using Ll_length by (cases ι) auto
ultimately show "ι ∈ no_labels.Red_I_𝒢 (fst ` NL)" by (auto intro: red_inf_impl)
qed
lemma stat_ref_comp_to_labeled_sta_ref_comp:
assumes static:
"statically_complete_calculus Bot_F Inf_F (⊨𝒢) no_labels.Red_I_𝒢 no_labels.Red_F_𝒢"
shows "statically_complete_calculus Bot_FL Inf_FL (⊨𝒢L) Red_I_𝒢 Red_F_𝒢"
proof
fix Bl :: ‹'f × 'l› and Nl :: ‹('f × 'l) set›
assume
Bl_in: ‹Bl ∈ Bot_FL› and
Nl_sat: ‹saturated Nl› and
Nl_entails_Bl: ‹Nl ⊨𝒢L {Bl}›
define B where "B = fst Bl"
have B_in: "B ∈ Bot_F" using Bl_in B_def SigmaE by force
define N where "N = fst ` Nl"
have N_sat: "no_labels.saturated N"
using N_def Nl_sat labeled_saturation_lifting by blast
have N_entails_B: "N ⊨𝒢 {B}"
using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force
have "∃B' ∈ Bot_F. B' ∈ N" using B_in N_sat N_entails_B
using static[unfolded statically_complete_calculus_def
statically_complete_calculus_axioms_def] by blast
then obtain B' where in_Bot: "B' ∈ Bot_F" and in_N: "B' ∈ N" by force
then have "B' ∈ fst ` Bot_FL" by fastforce
obtain Bl' where in_Nl: "Bl' ∈ Nl" and fst_Bl': "fst Bl' = B'"
using in_N unfolding N_def by blast
have "Bl' ∈ Bot_FL" using fst_Bl' in_Bot vimage_fst by fastforce
then show ‹∃Bl'∈Bot_FL. Bl' ∈ Nl› using in_Nl by blast
qed
end
subsection ‹Labeled Lifting with a Family of Redundancy Criteria›
locale labeled_lifting_intersection = no_labels: lifting_intersection Inf_F
Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q Bot_F 𝒢_F_q 𝒢_I_q "λg Cl Cl'. False"
for
Bot_F :: "'f set" and
Inf_F :: "'f inference set" and
Bot_G :: "'g set" and
Q :: "'q set" and
entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
Inf_G_q :: "'q ⇒ 'g inference set" and
Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
Red_F_q :: "'q ⇒ 'g set ⇒ 'g set" and
𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option"
+ fixes
Inf_FL :: ‹('f × 'l) inference set›
assumes
Inf_F_to_Inf_FL:
‹ι⇩F ∈ Inf_F ⟹ length (Ll :: 'l list) = length (prems_of ι⇩F) ⟹
∃L0. Infer (zip (prems_of ι⇩F) Ll) (concl_of ι⇩F, L0) ∈ Inf_FL› and
Inf_FL_to_Inf_F: ‹ι⇩F⇩L ∈ Inf_FL ⟹ Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F›
begin
definition to_F :: ‹('f × 'l) inference ⇒ 'f inference› where
‹to_F ι⇩F⇩L = Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L))›
abbreviation Bot_FL :: ‹('f × 'l) set› where
‹Bot_FL ≡ Bot_F × UNIV›
abbreviation 𝒢_F_L_q :: ‹'q ⇒ ('f × 'l) ⇒ 'g set› where
‹𝒢_F_L_q q CL ≡ 𝒢_F_q q (fst CL)›
abbreviation 𝒢_I_L_q :: ‹'q ⇒ ('f × 'l) inference ⇒ 'g inference set option› where
‹𝒢_I_L_q q ι⇩F⇩L ≡ 𝒢_I_q q (to_F ι⇩F⇩L)›
abbreviation 𝒢_Fset_L_q :: "'q ⇒ ('f × 'l) set ⇒ 'g set" where
"𝒢_Fset_L_q q N ≡ ⋃ (𝒢_F_L_q q ` N)"
definition Red_I_𝒢_L_q :: "'q ⇒ ('f × 'l) set ⇒ ('f × 'l) inference set" where
"Red_I_𝒢_L_q q N =
{ι ∈ Inf_FL. (𝒢_I_L_q q ι ≠ None ∧ the (𝒢_I_L_q q ι) ⊆ Red_I_q q (𝒢_Fset_L_q q N))
∨ (𝒢_I_L_q q ι = None ∧ 𝒢_F_L_q q (concl_of ι) ⊆ 𝒢_Fset_L_q q N ∪ Red_F_q q (𝒢_Fset_L_q q N))}"
abbreviation Red_I_𝒢_L :: "('f × 'l) set ⇒ ('f × 'l) inference set" where
"Red_I_𝒢_L N ≡ (⋂q ∈ Q. Red_I_𝒢_L_q q N)"
abbreviation entails_𝒢_L_q :: "'q ⇒ ('f × 'l) set ⇒ ('f × 'l) set ⇒ bool" where
"entails_𝒢_L_q q N1 N2 ≡ entails_q q (𝒢_Fset_L_q q N1) (𝒢_Fset_L_q q N2)"
lemma lifting_q:
assumes "q ∈ Q"
shows "labeled_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) (λg Cl Cl'. False) Inf_FL"
using assms no_labels.standard_lifting_family Inf_F_to_Inf_FL Inf_FL_to_Inf_F
by (simp add: labeled_tiebreaker_lifting_axioms_def labeled_tiebreaker_lifting_def)
lemma lifted_q:
assumes q_in: "q ∈ Q"
shows "standard_lifting Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q)
Bot_FL (𝒢_F_L_q q) (𝒢_I_L_q q)"
proof -
interpret q_lifting: labeled_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" "λg Cl Cl'. False" Inf_FL
using lifting_q[OF q_in] .
have "𝒢_I_L_q q = q_lifting.𝒢_I_L"
unfolding to_F_def q_lifting.to_F_def by simp
then show ?thesis
using q_lifting.standard_lifting_axioms by simp
qed
lemma ord_fam_lifted_q:
assumes q_in: "q ∈ Q"
shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q)
(Red_F_q q) (𝒢_F_L_q q) (𝒢_I_L_q q) (λg Cl Cl'. False)"
proof -
interpret standard_q_lifting: standard_lifting Inf_FL Bot_G "Inf_G_q q" "entails_q q"
"Red_I_q q" "Red_F_q q" Bot_FL "𝒢_F_L_q q" "𝒢_I_L_q q"
using lifted_q[OF q_in] .
have "minimal_element (λCl Cl'. False) UNIV"
by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on)
then show ?thesis
using standard_q_lifting.standard_lifting_axioms
by (simp add: tiebreaker_lifting_axioms_def tiebreaker_lifting_def)
qed
definition Red_F_𝒢_empty_L_q :: "'q ⇒ ('f × 'l) set ⇒ ('f × 'l) set" where
"Red_F_𝒢_empty_L_q q N = {C. ∀D ∈ 𝒢_F_L_q q C. D ∈ Red_F_q q (𝒢_Fset_L_q q N) ∨
(∃E ∈ N. False ∧ D ∈ 𝒢_F_L_q q E)}"
abbreviation Red_F_𝒢_empty_L :: "('f × 'l) set ⇒ ('f × 'l) set" where
"Red_F_𝒢_empty_L N ≡ (⋂q ∈ Q. Red_F_𝒢_empty_L_q q N)"
lemma all_lifted_red_crit:
assumes q_in: "q ∈ Q"
shows "calculus Bot_FL Inf_FL (entails_𝒢_L_q q) (Red_I_𝒢_L_q q) (Red_F_𝒢_empty_L_q q)"
proof -
interpret ord_q_lifting: tiebreaker_lifting Bot_FL Inf_FL Bot_G "entails_q q"
"Inf_G_q q" "Red_I_q q" "Red_F_q q" "𝒢_F_L_q q" "𝒢_I_L_q q" "λg Cl Cl'. False"
using ord_fam_lifted_q[OF q_in] .
have "Red_I_𝒢_L_q q = ord_q_lifting.Red_I_𝒢"
unfolding Red_I_𝒢_L_q_def ord_q_lifting.Red_I_𝒢_def by simp
moreover have "Red_F_𝒢_empty_L_q q = ord_q_lifting.Red_F_𝒢"
unfolding Red_F_𝒢_empty_L_q_def ord_q_lifting.Red_F_𝒢_def by simp
ultimately show ?thesis
using ord_q_lifting.calculus_axioms by argo
qed
lemma all_lifted_cons_rel:
assumes q_in: "q ∈ Q"
shows "consequence_relation Bot_FL (entails_𝒢_L_q q)"
using all_lifted_red_crit calculus_def q_in by blast
sublocale consequence_relation_family Bot_FL Q entails_𝒢_L_q
using all_lifted_cons_rel by (simp add: consequence_relation_family.intro no_labels.Q_nonempty)
sublocale intersection_calculus Bot_FL Inf_FL Q entails_𝒢_L_q Red_I_𝒢_L_q Red_F_𝒢_empty_L_q
using intersection_calculus.intro[OF consequence_relation_family_axioms]
by (simp add: all_lifted_red_crit intersection_calculus_axioms_def no_labels.Q_nonempty)
lemma in_Inf_FL_imp_to_F_in_Inf_F: "ι ∈ Inf_FL ⟹ to_F ι ∈ Inf_F"
by (simp add: Inf_FL_to_Inf_F to_F_def)
lemma in_Inf_from_imp_to_F_in_Inf_from: "ι ∈ Inf_from N ⟹ to_F ι ∈ no_labels.Inf_from (fst ` N)"
unfolding Inf_from_def no_labels.Inf_from_def to_F_def by (auto intro: Inf_FL_to_Inf_F)
notation no_labels.entails_𝒢 (infix ‹⊨∩𝒢› 50)
abbreviation entails_𝒢_L :: "('f × 'l) set ⇒ ('f × 'l) set ⇒ bool" (infix ‹⊨∩𝒢L› 50) where
"(⊨∩𝒢L) ≡ entails"
lemmas entails_𝒢_L_def = entails_def
lemma labeled_entailment_lifting: "NL1 ⊨∩𝒢L NL2 ⟷ fst ` NL1 ⊨∩𝒢 fst ` NL2"
unfolding no_labels.entails_𝒢_def entails_𝒢_L_def by force
lemma red_inf_impl: "ι ∈ Red_I NL ⟹ to_F ι ∈ no_labels.Red_I_𝒢 (fst ` NL)"
unfolding no_labels.Red_I_𝒢_def Red_I_def
proof clarify
fix X Xa q
assume
q_in: "q ∈ Q" and
i_in_inter: "ι ∈ (⋂q ∈ Q. Red_I_𝒢_L_q q NL)"
have i_in_q: "ι ∈ Red_I_𝒢_L_q q NL" using q_in i_in_inter image_eqI by blast
then have i_in: "ι ∈ Inf_FL" unfolding Red_I_𝒢_L_q_def by blast
have to_F_in: "to_F ι ∈ Inf_F" unfolding to_F_def using Inf_FL_to_Inf_F[OF i_in] .
have rephrase1: "(⋃CL∈NL. 𝒢_F_q q (fst CL)) = (⋃ (𝒢_F_q q ` fst ` NL))" by blast
have rephrase2: "fst (concl_of ι) = concl_of (to_F ι)"
unfolding concl_of_def to_F_def by simp
have subs_red: "(𝒢_I_L_q q ι ≠ None ∧ the (𝒢_I_L_q q ι) ⊆ Red_I_q q (𝒢_Fset_L_q q NL))
∨ (𝒢_I_L_q q ι = None ∧ 𝒢_F_L_q q (concl_of ι) ⊆ 𝒢_Fset_L_q q NL ∪ Red_F_q q (𝒢_Fset_L_q q NL))"
using i_in_q unfolding Red_I_𝒢_L_q_def by blast
then have to_F_subs_red: "(𝒢_I_q q (to_F ι) ≠ None ∧
the (𝒢_I_q q (to_F ι)) ⊆ Red_I_q q (no_labels.𝒢_Fset_q q (fst ` NL)))
∨ (𝒢_I_q q (to_F ι) = None ∧
𝒢_F_q q (concl_of (to_F ι))
⊆ no_labels.𝒢_Fset_q q (fst ` NL) ∪ Red_F_q q (no_labels.𝒢_Fset_q q (fst ` NL)))"
using rephrase1 rephrase2 by metis
then show "to_F ι ∈ no_labels.Red_I_𝒢_q q (fst ` NL)"
using to_F_in unfolding no_labels.Red_I_𝒢_q_def by simp
qed
lemma labeled_family_saturation_lifting: "saturated NL ⟹ no_labels.saturated (fst ` NL)"
unfolding saturated_def no_labels.saturated_def Inf_from_def no_labels.Inf_from_def
proof clarify
fix ιF
assume
labeled_sat: "{ι ∈ Inf_FL. set (prems_of ι) ⊆ NL} ⊆ Red_I NL" and
iF_in: "ιF ∈ Inf_F" and
iF_prems: "set (prems_of ιF) ⊆ fst ` NL"
define Lli where "Lli i = (SOME x. ((prems_of ιF)!i,x) ∈ NL)" for i
have [simp]:"((prems_of ιF)!i,Lli i) ∈ NL" if "i < length (prems_of ιF)" for i
using that iF_prems nth_mem someI_ex unfolding Lli_def by (metis DomainE Domain_fst subset_eq)
define Ll where "Ll = map Lli [0..<length (prems_of ιF)]"
have Ll_length: "length Ll = length (prems_of ιF)" unfolding Ll_def by auto
have subs_NL: "set (zip (prems_of ιF) Ll) ⊆ NL" unfolding Ll_def by (auto simp:in_set_zip)
obtain L0 where L0: "Infer (zip (prems_of ιF) Ll) (concl_of ιF, L0) ∈ Inf_FL"
using Inf_F_to_Inf_FL[OF iF_in Ll_length] ..
define ιFL where "ιFL = Infer (zip (prems_of ιF) Ll) (concl_of ιF, L0)"
then have "set (prems_of ιFL) ⊆ NL" using subs_NL by simp
then have "ιFL ∈ {ι ∈ Inf_FL. set (prems_of ι) ⊆ NL}" unfolding ιFL_def using L0 by blast
then have "ιFL ∈ Red_I NL" using labeled_sat by fast
moreover have "ιF = to_F ιFL" unfolding to_F_def ιFL_def using Ll_length by (cases ιF) auto
ultimately show "ιF ∈ no_labels.Red_I_𝒢 (fst ` NL)"
by (auto intro: red_inf_impl)
qed
theorem labeled_static_ref:
assumes calc: "statically_complete_calculus Bot_F Inf_F (⊨∩𝒢) no_labels.Red_I_𝒢
no_labels.Red_F_𝒢_empty"
shows "statically_complete_calculus Bot_FL Inf_FL (⊨∩𝒢L) Red_I Red_F"
proof
fix Bl :: ‹'f × 'l› and Nl :: ‹('f × 'l) set›
assume
Bl_in: ‹Bl ∈ Bot_FL› and
Nl_sat: ‹saturated Nl› and
Nl_entails_Bl: ‹Nl ⊨∩𝒢L {Bl}›
define B where "B = fst Bl"
have B_in: "B ∈ Bot_F" using Bl_in B_def SigmaE by force
define N where "N = fst ` Nl"
have N_sat: "no_labels.saturated N"
using N_def Nl_sat labeled_family_saturation_lifting by blast
have N_entails_B: "N ⊨∩𝒢 {B}"
using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force
have "∃B' ∈ Bot_F. B' ∈ N" using B_in N_sat N_entails_B
calc[unfolded statically_complete_calculus_def
statically_complete_calculus_axioms_def]
by blast
then obtain B' where in_Bot: "B' ∈ Bot_F" and in_N: "B' ∈ N" by force
then have "B' ∈ fst ` Bot_FL" by fastforce
obtain Bl' where in_Nl: "Bl' ∈ Nl" and fst_Bl': "fst Bl' = B'"
using in_N unfolding N_def by blast
have "Bl' ∈ Bot_FL" using fst_Bl' in_Bot vimage_fst by fastforce
then show ‹∃Bl'∈Bot_FL. Bl' ∈ Nl› using in_Nl by blast
qed
end
end