Theory Calculus
section ‹Calculi Based on a Redundancy Criterion›
text ‹This section introduces the most basic notions upon which the framework is
built: consequence relations and inference systems. It also defines the notion
of a family of consequence relations and of redundancy criteria. This
corresponds to sections 2.1 and 2.2 of the report.›
theory Calculus
imports
Ordered_Resolution_Prover.Lazy_List_Liminf
Ordered_Resolution_Prover.Lazy_List_Chain
begin
subsection ‹Consequence Relations›
locale consequence_relation =
fixes
Bot :: "'f set" and
entails :: "'f set ⇒ 'f set ⇒ bool" (infix ‹⊨› 50)
assumes
bot_not_empty: "Bot ≠ {}" and
bot_entails_all: "B ∈ Bot ⟹ {B} ⊨ N1" and
subset_entailed: "N2 ⊆ N1 ⟹ N1 ⊨ N2" and
all_formulas_entailed: "(∀C ∈ N2. N1 ⊨ {C}) ⟹ N1 ⊨ N2" and
entails_trans[trans]: "N1 ⊨ N2 ⟹ N2 ⊨ N3 ⟹ N1 ⊨ N3"
begin
lemma entail_set_all_formulas: "N1 ⊨ N2 ⟷ (∀C ∈ N2. N1 ⊨ {C})"
by (meson all_formulas_entailed empty_subsetI insert_subset subset_entailed entails_trans)
lemma entail_union: "N ⊨ N1 ∧ N ⊨ N2 ⟷ N ⊨ N1 ∪ N2"
using entail_set_all_formulas[of N N1] entail_set_all_formulas[of N N2]
entail_set_all_formulas[of N "N1 ∪ N2"] by blast
lemma entail_unions: "(∀i ∈ I. N ⊨ Ni i) ⟷ N ⊨ ⋃ (Ni ` I)"
using entail_set_all_formulas[of N "⋃ (Ni ` I)"] entail_set_all_formulas[of N]
Complete_Lattices.UN_ball_bex_simps(2)[of Ni I "λC. N ⊨ {C}", symmetric]
by meson
lemma entail_all_bot: "(∃B ∈ Bot. N ⊨ {B}) ⟹ ∀B' ∈ Bot. N ⊨ {B'}"
using bot_entails_all entails_trans by blast
lemma entails_trans_strong: "N1 ⊨ N2 ⟹ N1 ∪ N2 ⊨ N3 ⟹ N1 ⊨ N3"
by (meson entail_union entails_trans order_refl subset_entailed)
end
subsection ‹Families of Consequence Relations›
locale consequence_relation_family =
fixes
Bot :: "'f set" and
Q :: "'q set" and
entails_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ bool"
assumes
Q_nonempty: "Q ≠ {}" and
q_cons_rel: "∀q ∈ Q. consequence_relation Bot (entails_q q)"
begin
lemma bot_not_empty: "Bot ≠ {}"
using Q_nonempty consequence_relation.bot_not_empty consequence_relation_family.q_cons_rel
consequence_relation_family_axioms by blast
definition entails :: "'f set ⇒ 'f set ⇒ bool" (infix ‹⊨Q› 50) where
"N1 ⊨Q N2 ⟷ (∀q ∈ Q. entails_q q N1 N2)"
lemma intersect_cons_rel_family: "consequence_relation Bot entails"
unfolding consequence_relation_def entails_def
by (intro conjI bot_not_empty) (metis consequence_relation_def q_cons_rel)+
end
subsection ‹Inference Systems›