theory Prop_Normalisation
imports Prop_Logic Prop_Abstract_Transformation Nested_Multisets_Ordinals.Multiset_More
begin
text ‹Given the previous definition about abstract rewriting and theorem about them, we now have the
detailed rule making the transformation into CNF/DNF.›
section ‹Rewrite Rules›
text ‹The idea of Christoph Weidenbach's book is to remove gradually the operators: first
equivalencies, then implication, after that the unused true/false and finally the reorganizing the
or/and. We will prove each transformation seperately.›
subsection ‹Elimination of the Equivalences›
text ‹The first transformation consists in removing every equivalence symbol.›
inductive elim_equiv :: "'v propo ⇒ 'v propo ⇒ bool" where
elim_equiv[simp]: "elim_equiv (FEq φ ψ) (FAnd (FImp φ ψ) (FImp ψ φ))"
lemma elim_equiv_transformation_consistent:
"A ⊨ FEq φ ψ ⟷ A ⊨ FAnd (FImp φ ψ) (FImp ψ φ)"
by auto
lemma elim_equiv_explicit: "elim_equiv φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
by (induct rule: elim_equiv.induct, auto)
lemma elim_equiv_consistent: "preserve_models elim_equiv"
unfolding preserve_models_def by (simp add: elim_equiv_explicit)
lemma elimEquv_lifted_consistant:
"preserve_models (full (propo_rew_step elim_equiv))"
by (simp add: elim_equiv_consistent)
text ‹This function ensures that there is no equivalencies left in the formula tested by
@{term no_equiv_symb}.›
fun no_equiv_symb :: "'v propo ⇒ bool" where
"no_equiv_symb (FEq _ _) = False" |
"no_equiv_symb _ = True"
text ‹Given the definition of @{term no_equiv_symb}, it does not depend on the formula, but only on
the connective used.›
lemma no_equiv_symb_conn_characterization[simp]:
fixes c :: "'v connective" and l :: "'v propo list"
assumes wf: "wf_conn c l"
shows "no_equiv_symb (conn c l) ⟷ c ≠ CEq"
by (metis connective.distinct(13,25,35,43) wf no_equiv_symb.elims(3) no_equiv_symb.simps(1)
wf_conn.cases wf_conn_list(6))
definition no_equiv where "no_equiv = all_subformula_st no_equiv_symb"
lemma no_equiv_eq[simp]:
fixes φ ψ :: "'v propo"
shows
"¬no_equiv (FEq φ ψ)"
"no_equiv FT"
"no_equiv FF"
using no_equiv_symb.simps(1) all_subformula_st_test_symb_true_phi unfolding no_equiv_def by auto
text ‹The following lemma helps to reconstruct @{term no_equiv} expressions: this representation is
easier to use than the set definition.›
lemma all_subformula_st_decomp_explicit_no_equiv[iff]:
fixes φ ψ :: "'v propo"
shows
"no_equiv (FNot φ) ⟷ no_equiv φ"
"no_equiv (FAnd φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
"no_equiv (FOr φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
"no_equiv (FImp φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
by (auto simp: no_equiv_def)
text ‹A theorem to show the link between the rewrite relation @{term elim_equiv} and the function
@{term no_equiv_symb}. This theorem is one of the assumption we need to characterize the
transformation.›
lemma no_equiv_elim_equiv_step:
fixes φ :: "'v propo"
assumes no_equiv: "¬ no_equiv φ"
shows "∃ψ ψ'. ψ ≼ φ ∧ elim_equiv ψ ψ'"
proof -
have test_symb_false_nullary:
"∀x::'v. no_equiv_symb FF ∧ no_equiv_symb FT ∧ no_equiv_symb (FVar x)"
unfolding no_equiv_def by auto
moreover {
fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
assume a1: "elim_equiv (conn c l) ψ"
have "⋀p pa. ¬ elim_equiv (p::'v propo) pa ∨ ¬ no_equiv_symb p"
using elim_equiv.cases no_equiv_symb.simps(1) by blast
then have "elim_equiv (conn c l) ψ ⟹ ¬no_equiv_symb (conn c l) " using a1 by metis
}
moreover have H': "∀ψ. ¬elim_equiv FT ψ" "∀ψ. ¬elim_equiv FF ψ" "∀ψ x. ¬elim_equiv (FVar x) ψ"
using elim_equiv.cases by auto
moreover have "⋀φ. ¬ no_equiv_symb φ ⟹ ∃ψ. elim_equiv φ ψ"
by (case_tac φ, auto simp: elim_equiv.simps)
then have "⋀φ'. φ' ≼ φ ⟹ ¬no_equiv_symb φ' ⟹ ∃ψ. elim_equiv φ' ψ" by force
ultimately show ?thesis
using no_test_symb_step_exists no_equiv test_symb_false_nullary unfolding no_equiv_def by blast
qed
text ‹Given all the previous theorem and the characterization, once we have rewritten everything,
there is no equivalence symbol any more.›
lemma no_equiv_full_propo_rew_step_elim_equiv:
"full (propo_rew_step elim_equiv) φ ψ ⟹ no_equiv ψ"
using full_propo_rew_step_subformula no_equiv_elim_equiv_step by blast
subsection ‹Eliminate Implication›
text ‹After that, we can eliminate the implication symbols.›
inductive elim_imp :: "'v propo ⇒ 'v propo ⇒ bool" where
[simp]: "elim_imp (FImp φ ψ) (FOr (FNot φ) ψ)"
lemma elim_imp_transformation_consistent:
"A ⊨ FImp φ ψ ⟷ A ⊨ FOr (FNot φ) ψ"
by auto
lemma elim_imp_explicit: "elim_imp φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
by (induct φ ψ rule: elim_imp.induct, auto)
lemma elim_imp_consistent: "preserve_models elim_imp"
unfolding preserve_models_def by (simp add: elim_imp_explicit)
lemma elim_imp_lifted_consistant:
"preserve_models (full (propo_rew_step elim_imp))"
by (simp add: elim_imp_consistent)
fun no_imp_symb where
"no_imp_symb (FImp _ _) = False" |
"no_imp_symb _ = True"
lemma no_imp_symb_conn_characterization:
"wf_conn c l ⟹ no_imp_symb (conn c l) ⟷ c ≠ CImp"
by (induction rule: wf_conn_induct) auto
definition no_imp where "no_imp ≡ all_subformula_st no_imp_symb"
declare no_imp_def[simp]
lemma no_imp_Imp[simp]:
"¬no_imp (FImp φ ψ)"
"no_imp FT"
"no_imp FF"
unfolding no_imp_def by auto
lemma all_subformula_st_decomp_explicit_imp[simp]:
fixes φ ψ :: "'v propo"
shows
"no_imp (FNot φ) ⟷ no_imp φ"
"no_imp (FAnd φ ψ) ⟷ (no_imp φ ∧ no_imp ψ)"
"no_imp (FOr φ ψ) ⟷ (no_imp φ ∧ no_imp ψ)"
by auto
text ‹Invariant of the @{term elim_imp} transformation›
lemma elim_imp_no_equiv:
"elim_imp φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
by (induct φ ψ rule: elim_imp.induct, auto)
lemma elim_imp_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step elim_imp) φ ψ" and "no_equiv φ"
shows "no_equiv ψ"
using full_propo_rew_step_inv_stay_conn[of elim_imp no_equiv_symb φ ψ] assms elim_imp_no_equiv
no_equiv_symb_conn_characterization unfolding no_equiv_def by metis
lemma no_no_imp_elim_imp_step_exists:
fixes φ :: "'v propo"
assumes no_equiv: "¬ no_imp φ"
shows "∃ψ ψ'. ψ ≼ φ ∧ elim_imp ψ ψ'"
proof -
have test_symb_false_nullary: "∀x. no_imp_symb FF ∧ no_imp_symb FT ∧ no_imp_symb (FVar (x:: 'v))"
by auto
moreover {
fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
have H: "elim_imp (conn c l) ψ ⟹ ¬no_imp_symb (conn c l)"
by (auto elim: elim_imp.cases)
}
moreover
have H': "∀ψ. ¬elim_imp FT ψ" "∀ψ. ¬elim_imp FF ψ" "∀ψ x. ¬elim_imp (FVar x) ψ"
by (auto elim: elim_imp.cases)+
moreover
have "⋀φ. ¬ no_imp_symb φ ⟹ ∃ψ. elim_imp φ ψ"
by (case_tac φ) (force simp: elim_imp.simps)+
then have "⋀φ'. φ' ≼ φ ⟹ ¬no_imp_symb φ' ⟹ ∃ ψ. elim_imp φ' ψ" by force
ultimately show ?thesis
using no_test_symb_step_exists no_equiv test_symb_false_nullary unfolding no_imp_def by blast
qed
lemma no_imp_full_propo_rew_step_elim_imp: "full (propo_rew_step elim_imp) φ ψ ⟹ no_imp ψ"
using full_propo_rew_step_subformula no_no_imp_elim_imp_step_exists by blast
subsection "Eliminate all the True and False in the formula"
text ‹Contrary to the book, we have to give the transformation and the ``commutative''
transformation. The latter is implicit in the book.›
inductive elimTB where
ElimTB1: "elimTB (FAnd φ FT) φ" |
ElimTB1': "elimTB (FAnd FT φ) φ" |
ElimTB2: "elimTB (FAnd φ FF) FF" |
ElimTB2': "elimTB (FAnd FF φ) FF" |
ElimTB3: "elimTB (FOr φ FT) FT" |
ElimTB3': "elimTB (FOr FT φ) FT" |
ElimTB4: "elimTB (FOr φ FF) φ" |
ElimTB4': "elimTB (FOr FF φ) φ" |
ElimTB5: "elimTB (FNot FT) FF" |
ElimTB6: "elimTB (FNot FF) FT"
lemma elimTB_consistent: "preserve_models elimTB"
proof -
{
fix φ ψ:: "'b propo"
have "elimTB φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ" by (induction rule: elimTB.inducts) auto
}
then show ?thesis using preserve_models_def by auto
qed
inductive no_T_F_symb :: "'v propo ⇒ bool" where
no_T_F_symb_comp: "c ≠ CF ⟹ c ≠ CT ⟹ wf_conn c l ⟹ (∀φ ∈ set l. φ ≠ FT ∧ φ ≠ FF)
⟹ no_T_F_symb (conn c l)"
lemma wf_conn_no_T_F_symb_iff[simp]:
"wf_conn c ψs ⟹
no_T_F_symb (conn c ψs) ⟷ (c ≠ CF ∧ c ≠ CT ∧ (∀ψ∈set ψs. ψ ≠ FF ∧ ψ ≠ FT))"
unfolding no_T_F_symb.simps apply (cases c)
using wf_conn_list(1) apply fastforce
using wf_conn_list(2) apply fastforce
using wf_conn_list(3) apply fastforce
apply (metis (no_types, hide_lams) conn_inj connective.distinct(5,17))
using conn_inj apply blast+
done
lemma wf_conn_no_T_F_symb_iff_explicit[simp]:
"no_T_F_symb (FAnd φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
"no_T_F_symb (FOr φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
"no_T_F_symb (FEq φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
"no_T_F_symb (FImp φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
apply (metis conn.simps(36) conn.simps(37) conn.simps(5) propo.distinct(19)
wf_conn_helper_facts(5) wf_conn_no_T_F_symb_iff)
apply (metis conn.simps(36) conn.simps(37) conn.simps(6) propo.distinct(22)
wf_conn_helper_facts(6) wf_conn_no_T_F_symb_iff)
using wf_conn_no_T_F_symb_iff apply fastforce
by (metis conn.simps(36) conn.simps(37) conn.simps(7) propo.distinct(23) wf_conn_helper_facts(7)
wf_conn_no_T_F_symb_iff)
lemma no_T_F_symb_false[simp]:
fixes c :: "'v connective"
shows
"¬no_T_F_symb (FT :: 'v propo)"
"¬no_T_F_symb (FF :: 'v propo)"
by (metis (no_types) conn.simps(1,2) wf_conn_no_T_F_symb_iff wf_conn_nullary)+
lemma no_T_F_symb_bool[simp]:
fixes x :: "'v"
shows "no_T_F_symb (FVar x)"
using no_T_F_symb_comp wf_conn_nullary by (metis connective.distinct(3, 15) conn.simps(3)
empty_iff list.set(1))
lemma no_T_F_symb_fnot_imp:
"¬no_T_F_symb (FNot φ) ⟹ φ = FT ∨ φ = FF"
proof (rule ccontr)
assume n: "¬ no_T_F_symb (FNot φ)"
assume "¬ (φ = FT ∨ φ = FF)"
then have "∀φ' ∈ set [φ]. φ'≠FT ∧ φ'≠FF" by auto
moreover have "wf_conn CNot [φ]" by simp
ultimately have "no_T_F_symb (FNot φ)"
using no_T_F_symb.intros by (metis conn.simps(4) connective.distinct(5,17))
then show "False" using n by blast
qed
lemma no_T_F_symb_fnot[simp]:
"no_T_F_symb (FNot φ) ⟷ ¬(φ = FT ∨ φ = FF)"
using no_T_F_symb.simps no_T_F_symb_fnot_imp by (metis conn_inj_not(2) list.set_intros(1))
text ‹Actually it is not possible to remover every @{term FT} and @{term FF}: if the formula is
equal to true or false, we can not remove it.›
inductive no_T_F_symb_except_toplevel where
no_T_F_symb_except_toplevel_true[simp]: "no_T_F_symb_except_toplevel FT" |
no_T_F_symb_except_toplevel_false[simp]: "no_T_F_symb_except_toplevel FF" |
noTrue_no_T_F_symb_except_toplevel[simp]: "no_T_F_symb φ ⟹ no_T_F_symb_except_toplevel φ"
lemma no_T_F_symb_except_toplevel_bool:
fixes x :: "'v"
shows "no_T_F_symb_except_toplevel (FVar x)"
by simp
lemma no_T_F_symb_except_toplevel_not_decom:
"φ ≠ FT ⟹ φ ≠ FF ⟹ no_T_F_symb_except_toplevel (FNot φ)"
by simp
lemma no_T_F_symb_except_toplevel_bin_decom:
fixes φ ψ :: "'v propo"
assumes "φ ≠ FT" and "φ ≠ FF" and "ψ ≠ FT" and "ψ ≠ FF"
and c: "c∈ binary_connectives"
shows "no_T_F_symb_except_toplevel (conn c [φ, ψ])"
by (metis (no_types, lifting) assms c conn.simps(4) list.discI noTrue_no_T_F_symb_except_toplevel
wf_conn_no_T_F_symb_iff no_T_F_symb_fnot set_ConsD wf_conn_binary wf_conn_helper_facts(1)
wf_conn_list_decomp(1,2))
lemma no_T_F_symb_except_toplevel_if_is_a_true_false:
fixes l :: "'v propo list" and c :: "'v connective"
assumes corr: "wf_conn c l"
and "FT ∈ set l ∨ FF ∈ set l"
shows "¬no_T_F_symb_except_toplevel (conn c l)"
by (metis assms empty_iff no_T_F_symb_except_toplevel.simps wf_conn_no_T_F_symb_iff set_empty
wf_conn_list(1,2))
lemma no_T_F_symb_except_top_level_false_example[simp]:
fixes φ ψ :: "'v propo"
assumes "φ = FT ∨ ψ = FT ∨ φ = FF ∨ ψ = FF"
shows
"¬ no_T_F_symb_except_toplevel (FAnd φ ψ)"
"¬ no_T_F_symb_except_toplevel (FOr φ ψ)"
"¬ no_T_F_symb_except_toplevel (FImp φ ψ)"
"¬ no_T_F_symb_except_toplevel (FEq φ ψ)"
using assms no_T_F_symb_except_toplevel_if_is_a_true_false unfolding binary_connectives_def
by (metis (no_types) conn.simps(5-8) insert_iff list.simps(14-15) wf_conn_helper_facts(5-8))+
lemma no_T_F_symb_except_top_level_false_not[simp]:
fixes φ ψ :: "'v propo"
assumes "φ = FT ∨ φ = FF"
shows
"¬ no_T_F_symb_except_toplevel (FNot φ)"
by (simp add: assms no_T_F_symb_except_toplevel.simps)
text ‹This is the local extension of @{const no_T_F_symb_except_toplevel}.›
definition no_T_F_except_top_level where
"no_T_F_except_top_level ≡ all_subformula_st no_T_F_symb_except_toplevel"
text ‹This is another property we will use. While this version might seem to be the one we want to
prove, it is not since @{term FT} can not be reduced.›
definition no_T_F where
"no_T_F ≡ all_subformula_st no_T_F_symb"
lemma no_T_F_except_top_level_false:
fixes l :: "'v propo list" and c :: "'v connective"
assumes "wf_conn c l"
and "FT ∈ set l ∨ FF ∈ set l"
shows "¬no_T_F_except_top_level (conn c l)"
by (simp add: all_subformula_st_decomp assms no_T_F_except_top_level_def
no_T_F_symb_except_toplevel_if_is_a_true_false)
lemma no_T_F_except_top_level_false_example[simp]:
fixes φ ψ :: "'v propo"
assumes "φ = FT ∨ ψ = FT ∨ φ = FF ∨ ψ = FF"
shows
"¬no_T_F_except_top_level (FAnd φ ψ)"
"¬no_T_F_except_top_level (FOr φ ψ)"
"¬no_T_F_except_top_level (FEq φ ψ)"
"¬no_T_F_except_top_level (FImp φ ψ)"
by (metis all_subformula_st_test_symb_true_phi assms no_T_F_except_top_level_def
no_T_F_symb_except_top_level_false_example)+
lemma no_T_F_symb_except_toplevel_no_T_F_symb:
"no_T_F_symb_except_toplevel φ ⟹ φ ≠ FF ⟹ φ ≠ FT ⟹ no_T_F_symb φ"
by (induct rule: no_T_F_symb_except_toplevel.induct, auto)
text ‹The two following lemmas give the precise link between the two definitions.›
lemma no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb:
"no_T_F_except_top_level φ ⟹ φ ≠ FF ⟹ φ ≠ FT ⟹ no_T_F φ"
unfolding no_T_F_except_top_level_def no_T_F_def apply (induct φ)
using no_T_F_symb_fnot by fastforce+
lemma no_T_F_no_T_F_except_top_level:
"no_T_F φ ⟹ no_T_F_except_top_level φ"
unfolding no_T_F_except_top_level_def no_T_F_def
unfolding all_subformula_st_def by auto
lemma no_T_F_except_top_level_simp[simp]: "no_T_F_except_top_level FF" "no_T_F_except_top_level FT"
unfolding no_T_F_except_top_level_def by auto
lemma no_T_F_no_T_F_except_top_level'[simp]:
"no_T_F_except_top_level φ ⟷ (φ = FF ∨ φ = FT ∨ no_T_F φ)"
using no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb no_T_F_no_T_F_except_top_level
by auto
lemma no_T_F_bin_decomp[simp]:
assumes c: "c ∈ binary_connectives"
shows "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
proof -
have wf: "wf_conn c [φ, ψ]" using c by auto
then have "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F_symb (conn c [φ, ψ]) ∧ no_T_F φ ∧ no_T_F ψ)"
by (simp add: all_subformula_st_decomp no_T_F_def)
then show "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
using c wf all_subformula_st_decomp list.discI no_T_F_def no_T_F_symb_except_toplevel_bin_decom
no_T_F_symb_except_toplevel_no_T_F_symb no_T_F_symb_false(1,2) wf_conn_helper_facts(2,3)
wf_conn_list(1,2) by metis
qed
lemma no_T_F_bin_decomp_expanded[simp]:
assumes c: "c = CAnd ∨ c = COr ∨ c = CEq ∨ c = CImp"
shows "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
using no_T_F_bin_decomp assms unfolding binary_connectives_def by blast
lemma no_T_F_comp_expanded_explicit[simp]:
fixes φ ψ :: "'v propo"
shows
"no_T_F (FAnd φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
"no_T_F (FOr φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
"no_T_F (FEq φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
"no_T_F (FImp φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
using conn.simps(5-8) no_T_F_bin_decomp_expanded by (metis (no_types))+
lemma no_T_F_comp_not[simp]:
fixes φ ψ :: "'v propo"
shows "no_T_F (FNot φ) ⟷ no_T_F φ"
by (metis all_subformula_st_decomp_explicit(3) all_subformula_st_test_symb_true_phi no_T_F_def
no_T_F_symb_false(1,2) no_T_F_symb_fnot_imp)
lemma no_T_F_decomp:
fixes φ ψ :: "'v propo"
assumes φ: "no_T_F (FAnd φ ψ) ∨ no_T_F (FOr φ ψ) ∨ no_T_F (FEq φ ψ) ∨ no_T_F (FImp φ ψ)"
shows "no_T_F ψ" and "no_T_F φ"
using assms by auto
lemma no_T_F_decomp_not:
fixes φ :: "'v propo"
assumes φ: "no_T_F (FNot φ)"
shows "no_T_F φ"
using assms by auto
lemma no_T_F_symb_except_toplevel_step_exists:
fixes φ ψ :: "'v propo"
assumes "no_equiv φ" and "no_imp φ"
shows "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTB ψ ψ'"
proof (induct ψ rule: propo_induct_arity)
case (nullary φ' x)
then have "False" using no_T_F_symb_except_toplevel_true no_T_F_symb_except_toplevel_false by auto
then show ?case by blast
next
case (unary ψ)
then have "ψ = FF ∨ ψ = FT" using no_T_F_symb_except_toplevel_not_decom by blast
then show ?case using ElimTB5 ElimTB6 by blast
next
case (binary φ' ψ1 ψ2)
note IH1 = this(1) and IH2 = this(2) and φ' = this(3) and Fφ = this(4) and n = this(5)
{
assume "φ' = FImp ψ1 ψ2 ∨ φ' = FEq ψ1 ψ2"
then have "False" using n Fφ subformula_all_subformula_st assms
by (metis (no_types) no_equiv_eq(1) no_equiv_def no_imp_Imp(1) no_imp_def)
then have ?case by blast
}
moreover {
assume φ': "φ' = FAnd ψ1 ψ2 ∨ φ' = FOr ψ1 ψ2"
then have "ψ1 = FT ∨ ψ2 = FT ∨ ψ1 = FF ∨ ψ2 = FF"
using no_T_F_symb_except_toplevel_bin_decom conn.simps(5,6) n unfolding binary_connectives_def
by fastforce+
then have ?case using elimTB.intros φ' by blast
}
ultimately show ?case using φ' by blast
qed
lemma no_T_F_except_top_level_rew:
fixes φ :: "'v propo"
assumes noTB: "¬ no_T_F_except_top_level φ" and no_equiv: "no_equiv φ" and no_imp: "no_imp φ"
shows "∃ψ ψ'. ψ ≼ φ ∧ elimTB ψ ψ' "
proof -
have test_symb_false_nullary: "∀x. no_T_F_symb_except_toplevel (FF:: 'v propo)
∧ no_T_F_symb_except_toplevel FT ∧ no_T_F_symb_except_toplevel (FVar (x:: 'v))" by auto
moreover {
fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
have H: "elimTB (conn c l) ψ ⟹ ¬no_T_F_symb_except_toplevel (conn c l) "
by (cases "conn c l" rule: elimTB.cases, auto)
}
moreover {
fix x :: "'v"
have H': "no_T_F_except_top_level FT" " no_T_F_except_top_level FF"
"no_T_F_except_top_level (FVar x)"
by (auto simp: no_T_F_except_top_level_def test_symb_false_nullary)
}
moreover {
fix ψ
have "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTB ψ ψ'"
using no_T_F_symb_except_toplevel_step_exists no_equiv no_imp by auto
}
ultimately show ?thesis
using no_test_symb_step_exists noTB unfolding no_T_F_except_top_level_def by blast
qed
lemma elimTB_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step elimTB) φ ψ "
and "no_equiv φ" and "no_imp φ"
shows "no_equiv ψ" and "no_imp ψ"
proof -
{
fix φ ψ :: "'v propo"
have H: "elimTB φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
by (induct φ ψ rule: elimTB.induct, auto)
}
then show "no_equiv ψ"
using full_propo_rew_step_inv_stay_conn[of elimTB no_equiv_symb φ ψ]
no_equiv_symb_conn_characterization assms unfolding no_equiv_def by metis
next
{
fix φ ψ :: "'v propo"
have H: "elimTB φ ψ ⟹ no_imp φ ⟹ no_imp ψ"
by (induct φ ψ rule: elimTB.induct, auto)
}
then show "no_imp ψ"
using full_propo_rew_step_inv_stay_conn[of elimTB no_imp_symb φ ψ] assms
no_imp_symb_conn_characterization unfolding no_imp_def by metis
qed
lemma elimTB_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes "no_equiv φ" and "no_imp φ" and "full (propo_rew_step elimTB) φ ψ"
shows "no_T_F_except_top_level ψ"
using full_propo_rew_step_subformula no_T_F_except_top_level_rew assms elimTB_inv by fastforce
subsection "PushNeg"
text ‹Push the negation inside the formula, until the litteral.›
inductive pushNeg where
PushNeg1[simp]: "pushNeg (FNot (FAnd φ ψ)) (FOr (FNot φ) (FNot ψ))" |
PushNeg2[simp]: "pushNeg (FNot (FOr φ ψ)) (FAnd (FNot φ) (FNot ψ))" |
PushNeg3[simp]: "pushNeg (FNot (FNot φ)) φ"
lemma pushNeg_transformation_consistent:
"A ⊨ FNot (FAnd φ ψ) ⟷ A ⊨ (FOr (FNot φ) (FNot ψ))"
"A ⊨ FNot (FOr φ ψ) ⟷ A ⊨ (FAnd (FNot φ) (FNot ψ))"
"A ⊨ FNot (FNot φ) ⟷ A ⊨ φ"
by auto
lemma pushNeg_explicit: "pushNeg φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
by (induct φ ψ rule: pushNeg.induct, auto)
lemma pushNeg_consistent: "preserve_models pushNeg"
unfolding preserve_models_def by (simp add: pushNeg_explicit)
lemma pushNeg_lifted_consistant:
"preserve_models (full (propo_rew_step pushNeg))"
by (simp add: pushNeg_consistent)
fun simple where
"simple FT = True" |
"simple FF = True" |
"simple (FVar _) = True" |
"simple _ = False"
lemma simple_decomp:
"simple φ ⟷ (φ = FT ∨ φ = FF ∨ (∃x. φ = FVar x))"
by (cases φ) auto
lemma subformula_conn_decomp_simple:
fixes φ ψ :: "'v propo"
assumes s: "simple ψ"
shows "φ ≼ FNot ψ ⟷ (φ = FNot ψ ∨ φ = ψ)"
proof -
have "φ ≼ conn CNot [ψ] ⟷ (φ = conn CNot [ψ] ∨ (∃ ψ∈ set [ψ]. φ ≼ ψ))"
using subformula_conn_decomp wf_conn_helper_facts(1) by metis
then show "φ ≼ FNot ψ ⟷ (φ = FNot ψ ∨ φ = ψ)" using s by (auto simp: simple_decomp)
qed
lemma subformula_conn_decomp_explicit[simp]:
fixes φ :: "'v propo" and x :: "'v"
shows
"φ ≼ FNot FT ⟷ (φ = FNot FT ∨ φ = FT)"
"φ ≼ FNot FF ⟷ (φ = FNot FF ∨ φ = FF)"
"φ ≼ FNot (FVar x) ⟷ (φ = FNot (FVar x) ∨ φ = FVar x)"
by (auto simp: subformula_conn_decomp_simple)
fun simple_not_symb where
"simple_not_symb (FNot φ) = (simple φ)" |
"simple_not_symb _ = True"
definition simple_not where
"simple_not = all_subformula_st simple_not_symb"
declare simple_not_def[simp]
lemma simple_not_Not[simp]:
"¬ simple_not (FNot (FAnd φ ψ))"
"¬ simple_not (FNot (FOr φ ψ))"
by auto
lemma simple_not_step_exists:
fixes φ ψ :: "'v propo"
assumes "no_equiv φ" and "no_imp φ"
shows "ψ ≼ φ ⟹ ¬ simple_not_symb ψ ⟹ ∃ψ'. pushNeg ψ ψ'"
apply (induct ψ, auto)
apply (rename_tac ψ, case_tac ψ, auto intro: pushNeg.intros)
by (metis assms(1,2) no_imp_Imp(1) no_equiv_eq(1) no_imp_def no_equiv_def
subformula_in_subformula_not subformula_all_subformula_st)+
lemma simple_not_rew:
fixes φ :: "'v propo"
assumes noTB: "¬ simple_not φ" and no_equiv: "no_equiv φ" and no_imp: "no_imp φ"
shows "∃ψ ψ'. ψ ≼ φ ∧ pushNeg ψ ψ'"
proof -
have "∀x. simple_not_symb (FF:: 'v propo) ∧ simple_not_symb FT ∧ simple_not_symb (FVar (x:: 'v))"
by auto
moreover {
fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
have H: "pushNeg (conn c l) ψ ⟹ ¬simple_not_symb (conn c l)"
by (cases "conn c l" rule: pushNeg.cases) auto
}
moreover {
fix x :: "'v"
have H': "simple_not FT" "simple_not FF" "simple_not (FVar x)"
by simp_all
}
moreover {
fix ψ :: "'v propo"
have "ψ ≼ φ ⟹ ¬ simple_not_symb ψ ⟹ ∃ψ'. pushNeg ψ ψ'"
using simple_not_step_exists no_equiv no_imp by blast
}
ultimately show ?thesis using no_test_symb_step_exists noTB unfolding simple_not_def by blast
qed
lemma no_T_F_except_top_level_pushNeg1:
"no_T_F_except_top_level (FNot (FAnd φ ψ)) ⟹ no_T_F_except_top_level (FOr (FNot φ) (FNot ψ))"
using no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb no_T_F_comp_not no_T_F_decomp(1)
no_T_F_decomp(2) no_T_F_no_T_F_except_top_level by (metis no_T_F_comp_expanded_explicit(2)
propo.distinct(5,17))
lemma no_T_F_except_top_level_pushNeg2:
"no_T_F_except_top_level (FNot (FOr φ ψ)) ⟹ no_T_F_except_top_level (FAnd (FNot φ) (FNot ψ))"
by auto
lemma no_T_F_symb_pushNeg:
"no_T_F_symb (FOr (FNot φ') (FNot ψ'))"
"no_T_F_symb (FAnd (FNot φ') (FNot ψ'))"
"no_T_F_symb (FNot (FNot φ'))"
by auto
lemma propo_rew_step_pushNeg_no_T_F_symb:
"propo_rew_step pushNeg φ ψ ⟹ no_T_F_except_top_level φ ⟹ no_T_F_symb φ ⟹ no_T_F_symb ψ"
apply (induct rule: propo_rew_step.induct)
apply (cases rule: pushNeg.cases)
apply simp_all
apply (metis no_T_F_symb_pushNeg(1))
apply (metis no_T_F_symb_pushNeg(2))
apply (simp, metis all_subformula_st_test_symb_true_phi no_T_F_def)
proof -
fix φ φ':: "'a propo" and c:: "'a connective" and ξ ξ':: "'a propo list"
assume rel: "propo_rew_step pushNeg φ φ'"
and IH: "no_T_F φ ⟹ no_T_F_symb φ ⟹ no_T_F_symb φ'"
and wf: "wf_conn c (ξ @ φ # ξ')"
and n: "conn c (ξ @ φ # ξ') = FF ∨ conn c (ξ @ φ # ξ') = FT ∨ no_T_F (conn c (ξ @ φ # ξ'))"
and x: "c ≠ CF ∧ c ≠ CT ∧ φ ≠ FF ∧ φ ≠ FT ∧ (∀ψ ∈ set ξ ∪ set ξ'. ψ ≠ FF ∧ ψ ≠ FT)"
then have "c ≠ CF ∧ c ≠ CF ∧ wf_conn c (ξ @ φ' # ξ')"
using wf_conn_no_arity_change_helper wf_conn_no_arity_change by metis
moreover have n': "no_T_F (conn c (ξ @ φ # ξ'))" using n by (simp add: wf wf_conn_list(1,2))
moreover
{
have "no_T_F φ"
by (metis Un_iff all_subformula_st_decomp list.set_intros(1) n' wf no_T_F_def set_append)
moreover then have "no_T_F_symb φ"
by (simp add: all_subformula_st_test_symb_true_phi no_T_F_def)
ultimately have "φ' ≠ FF ∧ φ' ≠ FT"
using IH no_T_F_symb_false(1) no_T_F_symb_false(2) by blast
then have "∀ψ∈ set (ξ @ φ' # ξ'). ψ ≠ FF ∧ ψ ≠ FT" using x by auto
}
ultimately show "no_T_F_symb (conn c (ξ @ φ' # ξ'))" by (simp add: x)
qed
lemma propo_rew_step_pushNeg_no_T_F:
"propo_rew_step pushNeg φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
case global_rel
then show ?case
by (metis (no_types, lifting) no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb
no_T_F_def no_T_F_except_top_level_pushNeg1 no_T_F_except_top_level_pushNeg2
no_T_F_no_T_F_except_top_level all_subformula_st_decomp_explicit(3) pushNeg.simps
simple.simps(1,2,5,6))
next
case (propo_rew_one_step_lift φ φ' c ξ ξ')
note rel = this(1) and IH = this(2) and wf = this(3) and no_T_F = this(4)
moreover have wf': "wf_conn c (ξ @ φ' # ξ')"
using wf_conn_no_arity_change wf_conn_no_arity_change_helper wf by metis
ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))"
using all_subformula_st_test_symb_true_phi
by (fastforce simp: no_T_F_def all_subformula_st_decomp wf wf')
qed
lemma pushNeg_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step pushNeg) φ ψ"
and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ"
shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ"
proof -
{
fix φ ψ :: "'v propo"
assume rel: "propo_rew_step pushNeg φ ψ"
and no: "no_T_F_except_top_level φ"
then have " no_T_F_except_top_level ψ"
proof -
{
assume "φ = FT ∨ φ = FF"
from rel this have False
apply (induct rule: propo_rew_step.induct)
using pushNeg.cases apply blast
using wf_conn_list(1) wf_conn_list(2) by auto
then have "no_T_F_except_top_level ψ" by blast
}
moreover {
assume "φ ≠ FT ∧ φ ≠ FF"
then have "no_T_F φ"
by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
then have "no_T_F ψ"
using propo_rew_step_pushNeg_no_T_F rel by auto
then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
}
ultimately show "no_T_F_except_top_level ψ" by metis
qed
}
moreover {
fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
assume rel: "propo_rew_step pushNeg ζ ζ'"
and incl: "ζ ≼ φ"
and corr: "wf_conn c (ξ @ ζ # ξ')"
and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
and n: "no_T_F_symb_except_toplevel ζ'"
have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
proof
have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
using corr wf_conn_list(1) wf_conn_list(2) no_T_F_symb_except_toplevel_no_T_F_symb no_T_F
by blast
have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
using corr wf_conn_no_T_F_symb_iff p by blast
from rel incl have "ζ'≠FT ∧ζ'≠FF"
apply (induction ζ ζ' rule: propo_rew_step.induct)
apply (cases rule: pushNeg.cases, auto)
by (metis assms(4) no_T_F_symb_except_top_level_false_not no_T_F_except_top_level_def
all_subformula_st_test_symb_true_phi subformula_in_subformula_not
subformula_all_subformula_st append_is_Nil_conv list.distinct(1)
wf_conn_no_arity_change_helper wf_conn_list(1,2) wf_conn_no_arity_change)+
then have "∀φ ∈ set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
by (metis corr no_T_F_symb_comp wf_conn_no_arity_change wf_conn_no_arity_change_helper)
qed
}
ultimately show "no_T_F_except_top_level ψ"
using full_propo_rew_step_inv_stay_with_inc[of pushNeg no_T_F_symb_except_toplevel φ] assms
subformula_refl unfolding no_T_F_except_top_level_def full_unfold by metis
next
{
fix φ ψ :: "'v propo"
have H: "pushNeg φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
by (induct φ ψ rule: pushNeg.induct, auto)
}
then show "no_equiv ψ"
using full_propo_rew_step_inv_stay_conn[of pushNeg no_equiv_symb φ ψ]
no_equiv_symb_conn_characterization assms unfolding no_equiv_def full_unfold by metis
next
{
fix φ ψ :: "'v propo"
have H: "pushNeg φ ψ ⟹ no_imp φ ⟹ no_imp ψ"
by (induct φ ψ rule: pushNeg.induct, auto)
}
then show "no_imp ψ"
using full_propo_rew_step_inv_stay_conn[of pushNeg no_imp_symb φ ψ] assms
no_imp_symb_conn_characterization unfolding no_imp_def full_unfold by metis
qed
lemma pushNeg_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes
"no_equiv φ" and
"no_imp φ" and
"full (propo_rew_step pushNeg) φ ψ" and
"no_T_F_except_top_level φ"
shows "simple_not ψ"
using assms full_propo_rew_step_subformula pushNeg_inv(1,2) simple_not_rew by blast
subsection ‹Push Inside›
inductive push_conn_inside :: "'v connective ⇒ 'v connective ⇒ 'v propo ⇒ 'v propo ⇒ bool"
for c c':: "'v connective" where
push_conn_inside_l[simp]: "c = CAnd ∨ c = COr ⟹ c' = CAnd ∨ c' = COr
⟹ push_conn_inside c c' (conn c [conn c' [φ1, φ2], ψ])
(conn c' [conn c [φ1, ψ], conn c [φ2, ψ]])" |
push_conn_inside_r[simp]: "c = CAnd ∨ c = COr ⟹ c' = CAnd ∨ c' = COr
⟹ push_conn_inside c c' (conn c [ψ, conn c' [φ1, φ2]])
(conn c' [conn c [ψ, φ1], conn c [ψ, φ2]])"
lemma push_conn_inside_explicit: "push_conn_inside c c' φ ψ ⟹ ∀A. A⊨φ ⟷ A⊨ψ"
by (induct φ ψ rule: push_conn_inside.induct, auto)
lemma push_conn_inside_consistent: "preserve_models (push_conn_inside c c')"
unfolding preserve_models_def by (simp add: push_conn_inside_explicit)
lemma propo_rew_step_push_conn_inside[simp]:
"¬propo_rew_step (push_conn_inside c c') FT ψ" "¬propo_rew_step (push_conn_inside c c') FF ψ"
proof -
{
{
fix φ ψ
have "push_conn_inside c c' φ ψ ⟹ φ = FT ∨ φ = FF ⟹ False"
by (induct rule: push_conn_inside.induct, auto)
} note H = this
fix φ
have "propo_rew_step (push_conn_inside c c') φ ψ ⟹ φ = FT ∨ φ = FF ⟹ False"
apply (induct rule: propo_rew_step.induct, auto simp: wf_conn_list(1) wf_conn_list(2))
using H by blast+
}
then show
"¬propo_rew_step (push_conn_inside c c') FT ψ"
"¬propo_rew_step (push_conn_inside c c') FF ψ" by blast+
qed
inductive not_c_in_c'_symb:: "'v connective ⇒ 'v connective ⇒ 'v propo ⇒ bool" for c c' where
not_c_in_c'_symb_l[simp]: "wf_conn c [conn c' [φ, φ'], ψ] ⟹ wf_conn c' [φ, φ']
⟹ not_c_in_c'_symb c c' (conn c [conn c' [φ, φ'], ψ])" |
not_c_in_c'_symb_r[simp]: "wf_conn c [ψ, conn c' [φ, φ']] ⟹ wf_conn c' [φ, φ']
⟹ not_c_in_c'_symb c c' (conn c [ψ, conn c' [φ, φ']])"
abbreviation "c_in_c'_symb c c' φ ≡ ¬not_c_in_c'_symb c c' φ"
lemma c_in_c'_symb_simp:
"not_c_in_c'_symb c c' ξ ⟹ ξ = FF ∨ ξ = FT ∨ ξ = FVar x ∨ ξ = FNot FF ∨ ξ = FNot FT
∨ ξ = FNot (FVar x)⟹ False"
apply (induct rule: not_c_in_c'_symb.induct, auto simp: wf_conn.simps wf_conn_list(1-3))
using conn_inj_not(2) wf_conn_binary unfolding binary_connectives_def by fastforce+
lemma c_in_c'_symb_simp'[simp]:
"¬not_c_in_c'_symb c c' FF"
"¬not_c_in_c'_symb c c' FT"
"¬not_c_in_c'_symb c c' (FVar x)"
"¬not_c_in_c'_symb c c' (FNot FF)"
"¬not_c_in_c'_symb c c' (FNot FT)"
"¬not_c_in_c'_symb c c' (FNot (FVar x))"
using c_in_c'_symb_simp by metis+
definition c_in_c'_only where
"c_in_c'_only c c' ≡ all_subformula_st (c_in_c'_symb c c')"
lemma c_in_c'_only_simp[simp]:
"c_in_c'_only c c' FF"
"c_in_c'_only c c' FT"
"c_in_c'_only c c' (FVar x)"
"c_in_c'_only c c' (FNot FF)"
"c_in_c'_only c c' (FNot FT)"
"c_in_c'_only c c' (FNot (FVar x))"
unfolding c_in_c'_only_def by auto
lemma not_c_in_c'_symb_commute:
"not_c_in_c'_symb c c' ξ ⟹ wf_conn c [φ, ψ] ⟹ ξ = conn c [φ, ψ]
⟹ not_c_in_c'_symb c c' (conn c [ψ, φ])"
proof (induct rule: not_c_in_c'_symb.induct)
case (not_c_in_c'_symb_r φ' φ'' ψ') note H = this
then have ψ: "ψ = conn c' [φ'', ψ']" using conn_inj by auto
have "wf_conn c [conn c' [φ'', ψ'], φ]"
using H(1) wf_conn_no_arity_change length_Cons by metis
then show "not_c_in_c'_symb c c' (conn c [ψ, φ])"
unfolding ψ using not_c_in_c'_symb.intros(1) H by auto
next
case (not_c_in_c'_symb_l φ' φ'' ψ') note H = this
then have "φ = conn c' [φ', φ'']" using conn_inj by auto
moreover have "wf_conn c [ψ', conn c' [φ', φ'']]"
using H(1) wf_conn_no_arity_change length_Cons by metis
ultimately show "not_c_in_c'_symb c c' (conn c [ψ, φ])"
using not_c_in_c'_symb.intros(2) conn_inj not_c_in_c'_symb_l.hyps
not_c_in_c'_symb_l.prems(1,2) by blast
qed
lemma not_c_in_c'_symb_commute':
"wf_conn c [φ, ψ] ⟹ c_in_c'_symb c c' (conn c [φ, ψ]) ⟷ c_in_c'_symb c c' (conn c [ψ, φ])"
using not_c_in_c'_symb_commute wf_conn_no_arity_change by (metis length_Cons)
lemma not_c_in_c'_comm:
assumes wf: "wf_conn c [φ, ψ]"
shows "c_in_c'_only c c' (conn c [φ, ψ]) ⟷ c_in_c'_only c c' (conn c [ψ, φ])" (is "?A ⟷ ?B")
proof -
have "?A ⟷ (c_in_c'_symb c c' (conn c [φ, ψ])
∧ (∀ξ ∈ set [φ, ψ]. all_subformula_st (c_in_c'_symb c c') ξ))"
using all_subformula_st_decomp wf unfolding c_in_c'_only_def by fastforce
also have "… ⟷ (c_in_c'_symb c c' (conn c [ψ, φ])
∧ (∀ξ ∈ set [ψ, φ]. all_subformula_st (c_in_c'_symb c c') ξ))"
using not_c_in_c'_symb_commute' wf by auto
also
have "wf_conn c [ψ, φ]" using wf_conn_no_arity_change wf by (metis length_Cons)
then have "(c_in_c'_symb c c' (conn c [ψ, φ])
∧ (∀ξ ∈ set [ψ, φ]. all_subformula_st (c_in_c'_symb c c') ξ))
⟷ ?B"
using all_subformula_st_decomp unfolding c_in_c'_only_def by fastforce
finally show ?thesis .
qed
lemma not_c_in_c'_simp[simp]:
fixes φ1 φ2 ψ :: "'v propo" and x :: "'v"
shows
"c_in_c'_symb c c' FT"
"c_in_c'_symb c c' FF"
"c_in_c'_symb c c' (FVar x)"
"wf_conn c [conn c' [φ1, φ2], ψ] ⟹ wf_conn c' [φ1, φ2]
⟹ ¬ c_in_c'_only c c' (conn c [conn c' [φ1, φ2], ψ])"
apply (simp_all add: c_in_c'_only_def)
using all_subformula_st_test_symb_true_phi not_c_in_c'_symb_l by blast
lemma c_in_c'_symb_not[simp]:
fixes c c' :: "'v connective" and ψ :: "'v propo"
shows "c_in_c'_symb c c' (FNot ψ)"
proof -
{
fix ξ :: "'v propo"
have "not_c_in_c'_symb c c' (FNot ψ) ⟹ False"
apply (induct "FNot ψ" rule: not_c_in_c'_symb.induct)
using conn_inj_not(2) by blast+
}
then show ?thesis by auto
qed
lemma c_in_c'_symb_step_exists:
fixes φ :: "'v propo"
assumes c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
shows "ψ ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ ⟹ ∃ψ'. push_conn_inside c c' ψ ψ'"
apply (induct ψ rule: propo_induct_arity)
apply auto[2]
proof -
fix ψ1 ψ2 φ':: "'v propo"
assume IHψ1: "ψ1 ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ1 ⟹ Ex (push_conn_inside c c' ψ1)"
and IHψ2: "ψ1 ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ1 ⟹ Ex (push_conn_inside c c' ψ1)"
and φ': "φ' = FAnd ψ1 ψ2 ∨ φ' = FOr ψ1 ψ2 ∨ φ' = FImp ψ1 ψ2 ∨ φ' = FEq ψ1 ψ2"
and inφ: "φ' ≼ φ" and n0: "¬c_in_c'_symb c c' φ'"
then have n: "not_c_in_c'_symb c c' φ'" by auto
{
assume φ': "φ' = conn c [ψ1, ψ2]"
obtain a b where "ψ1 = conn c' [a, b] ∨ ψ2 = conn c' [a, b]"
using n φ' apply (induct rule: not_c_in_c'_symb.induct)
using c by force+
then have "Ex (push_conn_inside c c' φ')"
unfolding φ' apply auto
using push_conn_inside.intros(1) c c' apply blast
using push_conn_inside.intros(2) c c' by blast
}
moreover {
assume φ': "φ' ≠ conn c [ψ1, ψ2]"
have "∀φ c ca. ∃φ1 ψ1 ψ2 ψ1' ψ2' φ2'. conn (c::'v connective) [φ1, conn ca [ψ1, ψ2]] = φ
∨ conn c [conn ca [ψ1', ψ2'], φ2'] = φ ∨ c_in_c'_symb c ca φ"
by (metis not_c_in_c'_symb.cases)
then have "Ex (push_conn_inside c c' φ')"
by (metis (no_types) c c' n push_conn_inside_l push_conn_inside_r)
}
ultimately show "Ex (push_conn_inside c c' φ')" by blast
qed
lemma c_in_c'_symb_rew:
fixes φ :: "'v propo"
assumes noTB: "¬c_in_c'_only c c' φ"
and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
shows "∃ψ ψ'. ψ ≼ φ ∧ push_conn_inside c c' ψ ψ' "
proof -
have test_symb_false_nullary:
"∀x. c_in_c'_symb c c' (FF:: 'v propo) ∧ c_in_c'_symb c c' FT
∧ c_in_c'_symb c c' (FVar (x:: 'v))"
by auto
moreover {
fix x :: "'v"
have H': "c_in_c'_symb c c' FT" "c_in_c'_symb c c' FF" "c_in_c'_symb c c' (FVar x)"
by simp+
}
moreover {
fix ψ :: "'v propo"
have "ψ ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ ⟹ ∃ψ'. push_conn_inside c c' ψ ψ'"
by (auto simp: assms(2) c' c_in_c'_symb_step_exists)
}
ultimately show ?thesis using noTB no_test_symb_step_exists[of "c_in_c'_symb c c'"]
unfolding c_in_c'_only_def by metis
qed
lemma push_conn_insidec_in_c'_symb_no_T_F:
fixes φ ψ :: "'v propo"
shows "propo_rew_step (push_conn_inside c c') φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
case (global_rel φ ψ)
then show "no_T_F ψ"
by (cases rule: push_conn_inside.cases, auto)
next
case (propo_rew_one_step_lift φ φ' c ξ ξ')
note rel = this(1) and IH = this(2) and wf = this(3) and no_T_F = this(4)
have "no_T_F φ"
using wf no_T_F no_T_F_def subformula_into_subformula subformula_all_subformula_st
subformula_refl by (metis (no_types) in_set_conv_decomp)
then have φ': "no_T_F φ'" using IH by blast
have "∀ζ ∈ set (ξ @ φ # ξ'). no_T_F ζ" by (metis wf no_T_F no_T_F_def all_subformula_st_decomp)
then have n: "∀ζ ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using φ' by auto
then have n': "∀ζ ∈ set (ξ @ φ' # ξ'). ζ ≠ FF ∧ ζ ≠ FT"
using φ' by (metis no_T_F_symb_false(1) no_T_F_symb_false(2) no_T_F_def
all_subformula_st_test_symb_true_phi)
have wf': "wf_conn c (ξ @ φ' # ξ')"
using wf wf_conn_no_arity_change by (metis wf_conn_no_arity_change_helper)
{
fix x :: "'v"
assume "c = CT ∨ c = CF ∨ c = CVar x"
then have "False" using wf by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))" by blast
}
moreover {
assume c: "c = CNot"
then have "ξ = []" "ξ' = []" using wf by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))"
using c by (metis φ' conn.simps(4) no_T_F_symb_false(1,2) no_T_F_symb_fnot no_T_F_def
all_subformula_st_decomp_explicit(3) all_subformula_st_test_symb_true_phi self_append_conv2)
}
moreover {
assume c: "c ∈ binary_connectives"
then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))" using wf' n' no_T_F_symb.simps by fastforce
then have "no_T_F (conn c (ξ @ φ' # ξ'))"
by (metis all_subformula_st_decomp_imp wf' n no_T_F_def)
}
ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using connective_cases_arity by auto
qed
lemma simple_propo_rew_step_push_conn_inside_inv:
"propo_rew_step (push_conn_inside c c') φ ψ ⟹ simple φ ⟹ simple ψ"
apply (induct rule: propo_rew_step.induct)
apply (rename_tac φ, case_tac φ, auto simp: push_conn_inside.simps)[]
by (metis append_is_Nil_conv list.distinct(1) simple.elims(2) wf_conn_list(1-3))
lemma simple_propo_rew_step_inv_push_conn_inside_simple_not:
fixes c c' :: "'v connective" and φ ψ :: "'v propo"
shows "propo_rew_step (push_conn_inside c c') φ ψ ⟹ simple_not φ ⟹ simple_not ψ"
proof (induct rule: propo_rew_step.induct)
case (global_rel φ ψ)
then show ?case by (cases φ, auto simp: push_conn_inside.simps)
next
case (propo_rew_one_step_lift φ φ' ca ξ ξ') note rew = this(1) and IH = this(2) and wf = this(3)
and simple = this(4)
show ?case
proof (cases ca rule: connective_cases_arity)
case nullary
then show ?thesis using propo_rew_one_step_lift by auto
next
case binary note ca = this
obtain a b where ab: "ξ @ φ' # ξ' = [a, b]"
using wf ca list_length2_decomp wf_conn_bin_list_length
by (metis (no_types) wf_conn_no_arity_change_helper)
have "∀ζ ∈ set (ξ @ φ # ξ'). simple_not ζ"
by (metis wf all_subformula_st_decomp simple simple_not_def)
then have "∀ζ ∈ set (ξ @ φ' # ξ'). simple_not ζ" using IH by simp
moreover have "simple_not_symb (conn ca (ξ @ φ' # ξ'))" using ca
by (metis ab conn.simps(5-8) helper_fact simple_not_symb.simps(5) simple_not_symb.simps(6)
simple_not_symb.simps(7) simple_not_symb.simps(8))
ultimately show ?thesis
by (simp add: ab all_subformula_st_decomp ca)
next
case unary
then show ?thesis
using rew simple_propo_rew_step_push_conn_inside_inv[OF rew] IH local.wf simple by auto
qed
qed
lemma propo_rew_step_push_conn_inside_simple_not:
fixes φ φ' :: "'v propo" and ξ ξ' :: "'v propo list" and c :: "'v connective"
assumes
"propo_rew_step (push_conn_inside c c') φ φ'" and
"wf_conn c (ξ @ φ # ξ')" and
"simple_not_symb (conn c (ξ @ φ # ξ'))" and
"simple_not_symb φ'"
shows "simple_not_symb (conn c (ξ @ φ' # ξ'))"
using assms
proof (induction rule: propo_rew_step.induct)
print_cases
case (global_rel)
then show ?case
by (metis conn.simps(12,17) list.discI push_conn_inside.cases simple_not_symb.elims(3)
wf_conn_helper_facts(5) wf_conn_list(2) wf_conn_list(8) wf_conn_no_arity_change
wf_conn_no_arity_change_helper)
next
case (propo_rew_one_step_lift φ φ' c' χs χs') note tel = this(1) and wf = this(2) and
IH = this(3) and wf' = this(4) and simple' = this(5) and simple = this(6)
then show ?case
proof (cases c' rule: connective_cases_arity)
case nullary
then show ?thesis using wf simple simple' by auto
next
case binary note c = this(1)
have corr': "wf_conn c (ξ @ conn c' (χs @ φ' # χs') # ξ')"
using wf wf_conn_no_arity_change
by (metis wf' wf_conn_no_arity_change_helper)
then show ?thesis
using c propo_rew_one_step_lift wf
by (metis conn.simps(17) connective.distinct(37) propo_rew_step_subformula_imp
push_conn_inside.cases simple_not_symb.elims(3) wf_conn.simps wf_conn_list(2,8))
next
case unary
then have empty: "χs = []" "χs' = []" using wf by auto
then show ?thesis using simple unary simple' wf wf'
by (metis connective.distinct(37) connective.distinct(39) propo_rew_step_subformula_imp
push_conn_inside.cases simple_not_symb.elims(3) tel wf_conn_list(8)
wf_conn_no_arity_change wf_conn_no_arity_change_helper)
qed
qed
lemma push_conn_inside_not_true_false:
"push_conn_inside c c' φ ψ ⟹ ψ ≠ FT ∧ ψ ≠ FF"
by (induct rule: push_conn_inside.induct, auto)
lemma push_conn_inside_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step (push_conn_inside c c')) φ ψ"
and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
proof -
{
{
fix φ ψ :: "'v propo"
have H: "push_conn_inside c c' φ ψ ⟹ all_subformula_st simple_not_symb φ
⟹ all_subformula_st simple_not_symb ψ"
by (induct φ ψ rule: push_conn_inside.induct, auto)
} note H = this
fix φ ψ :: "'v propo"
have H: "propo_rew_step (push_conn_inside c c') φ ψ ⟹ all_subformula_st simple_not_symb φ
⟹ all_subformula_st simple_not_symb ψ"
apply (induct φ ψ rule: propo_rew_step.induct)
using H apply simp
proof (rename_tac φ φ' ca ψs ψs', case_tac ca rule: connective_cases_arity)
fix φ φ' :: "'v propo" and c:: "'v connective" and ξ ξ':: "'v propo list"
and x:: "'v"
assume "wf_conn c (ξ @ φ # ξ')"
and " c = CT ∨ c = CF ∨ c = CVar x"
then have "ξ @ φ # ξ' = []" by auto
then have False by auto
then show "all_subformula_st simple_not_symb (conn c (ξ @ φ' # ξ'))" by blast
next
fix φ φ' :: "'v propo" and ca:: "'v connective" and ξ ξ':: "'v propo list"
and x :: "'v"
assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
and φ_φ': "all_subformula_st simple_not_symb φ ⟹ all_subformula_st simple_not_symb φ'"
and corr: "wf_conn ca (ξ @ φ # ξ')"
and n: "all_subformula_st simple_not_symb (conn ca (ξ @ φ # ξ'))"
and c: "ca = CNot"
have empty: "ξ = []" "ξ' = []" using c corr by auto
then have simple_not:"all_subformula_st simple_not_symb (FNot φ)" using corr c n by auto
then have "simple φ"
using all_subformula_st_test_symb_true_phi simple_not_symb.simps(1) by blast
then have "simple φ'"
using rel simple_propo_rew_step_push_conn_inside_inv by blast
then show "all_subformula_st simple_not_symb (conn ca (ξ @ φ' # ξ'))" using c empty
by (metis simple_not φ_φ' append_Nil conn.simps(4) all_subformula_st_decomp_explicit(3)
simple_not_symb.simps(1))
next
fix φ φ' :: "'v propo" and ca :: "'v connective" and ξ ξ' :: "'v propo list"
and x :: "'v"
assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
and nφ: "all_subformula_st simple_not_symb φ ⟹ all_subformula_st simple_not_symb φ'"
and corr: "wf_conn ca (ξ @ φ # ξ')"
and n: "all_subformula_st simple_not_symb (conn ca (ξ @ φ # ξ'))"
and c: "ca ∈ binary_connectives"
have "all_subformula_st simple_not_symb φ"
using n c corr all_subformula_st_decomp by fastforce
then have φ': " all_subformula_st simple_not_symb φ'" using nφ by blast
obtain a b where ab: "[a, b] = (ξ @ φ # ξ')"
using corr c list_length2_decomp wf_conn_bin_list_length by metis
then have "ξ @ φ' # ξ' = [a, φ'] ∨ (ξ @ φ' # ξ') = [φ', b]"
using ab by (metis (no_types, hide_lams) append_Cons append_Nil append_Nil2
append_is_Nil_conv butlast.simps(2) butlast_append list.sel(3) tl_append2)
moreover
{
fix χ :: "'v propo"
have wf': "wf_conn ca [a, b]"
using ab corr by presburger
have "all_subformula_st simple_not_symb (conn ca [a, b])"
using ab n by presburger
then have "all_subformula_st simple_not_symb χ ∨ χ ∉ set (ξ @ φ' # ξ')"
using wf' by (metis (no_types) φ' all_subformula_st_decomp calculation insert_iff
list.set(2))
}
then have "∀φ. φ ∈ set (ξ @ φ' # ξ') ⟶ all_subformula_st simple_not_symb φ"
by (metis (no_types))
moreover have "simple_not_symb (conn ca (ξ @ φ' # ξ'))"
using ab conn_inj_not(1) corr wf_conn_list_decomp(4) wf_conn_no_arity_change
not_Cons_self2 self_append_conv2 simple_not_symb.elims(3) by (metis (no_types) c
calculation(1) wf_conn_binary)
moreover have "wf_conn ca (ξ @ φ' # ξ')" using c calculation(1) by auto
ultimately show "all_subformula_st simple_not_symb (conn ca (ξ @ φ' # ξ'))"
by (metis all_subformula_st_decomp_imp)
qed
}
moreover {
fix ca :: "'v connective" and ξ ξ' :: "'v propo list" and φ φ' :: "'v propo"
have "propo_rew_step (push_conn_inside c c') φ φ' ⟹ wf_conn ca (ξ @ φ # ξ')
⟹ simple_not_symb (conn ca (ξ @ φ # ξ')) ⟹ simple_not_symb φ'
⟹ simple_not_symb (conn ca (ξ @ φ' # ξ'))"
by (metis append_self_conv2 conn.simps(4) conn_inj_not(1) simple_not_symb.elims(3)
simple_not_symb.simps(1) simple_propo_rew_step_push_conn_inside_inv
wf_conn_no_arity_change_helper wf_conn_list_decomp(4) wf_conn_no_arity_change)
}
ultimately show "simple_not ψ"
using full_propo_rew_step_inv_stay'[of "push_conn_inside c c'" "simple_not_symb"] assms
unfolding no_T_F_except_top_level_def simple_not_def full_unfold by metis
next
{
fix φ ψ :: "'v propo"
have H: "propo_rew_step (push_conn_inside c c') φ ψ ⟹ no_T_F_except_top_level φ
⟹ no_T_F_except_top_level ψ"
proof -
assume rel: "propo_rew_step (push_conn_inside c c') φ ψ"
and "no_T_F_except_top_level φ"
then have "no_T_F φ ∨ φ = FF ∨ φ = FT"
by (metis no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
moreover {
assume "φ = FF ∨ φ = FT"
then have False using rel propo_rew_step_push_conn_inside by blast
then have "no_T_F_except_top_level ψ" by blast
}
moreover {
assume "no_T_F φ ∧ φ ≠ FF ∧ φ ≠ FT"
then have "no_T_F ψ" using rel push_conn_insidec_in_c'_symb_no_T_F by blast
then have "no_T_F_except_top_level ψ" using no_T_F_no_T_F_except_top_level by blast
}
ultimately show "no_T_F_except_top_level ψ" by blast
qed
}
moreover {
fix ca :: "'v connective" and ξ ξ' :: "'v propo list" and φ φ' :: "'v propo"
assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
assume corr: "wf_conn ca (ξ @ φ # ξ')"
then have c: "ca ≠ CT ∧ ca ≠ CF" by auto
assume no_T_F: "no_T_F_symb_except_toplevel (conn ca (ξ @ φ # ξ'))"
have "no_T_F_symb_except_toplevel (conn ca (ξ @ φ' # ξ'))"
proof
have c: "ca ≠ CT ∧ ca ≠ CF" using corr by auto
have ζ: "∀ζ∈ set (ξ @ φ # ξ'). ζ≠FT ∧ ζ ≠ FF"
using corr no_T_F no_T_F_symb_except_toplevel_if_is_a_true_false by blast
then have "φ ≠ FT ∧ φ ≠ FF" by auto
from rel this have "φ' ≠ FT ∧ φ' ≠ FF"
apply (induct rule: propo_rew_step.induct)
by (metis append_is_Nil_conv conn.simps(2) conn_inj list.distinct(1)
wf_conn_helper_facts(3) wf_conn_list(1) wf_conn_no_arity_change
wf_conn_no_arity_change_helper push_conn_inside_not_true_false)+
then have "∀ζ ∈ set (ξ @ φ' # ξ'). ζ ≠ FT ∧ ζ ≠ FF" using ζ by auto
moreover have "wf_conn ca (ξ @ φ' # ξ')"
using corr wf_conn_no_arity_change by (metis wf_conn_no_arity_change_helper)
ultimately show "no_T_F_symb (conn ca (ξ @ φ' # ξ'))" using no_T_F_symb.intros c by metis
qed
}
ultimately show "no_T_F_except_top_level ψ"
using full_propo_rew_step_inv_stay'[of "push_conn_inside c c'" "no_T_F_symb_except_toplevel"]
assms unfolding no_T_F_except_top_level_def full_unfold by metis
next
{
fix φ ψ :: "'v propo"
have H: "push_conn_inside c c' φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
by (induct φ ψ rule: push_conn_inside.induct, auto)
}
then show "no_equiv ψ"
using full_propo_rew_step_inv_stay_conn[of "push_conn_inside c c'" no_equiv_symb] assms
no_equiv_symb_conn_characterization unfolding no_equiv_def by metis
next
{
fix φ ψ :: "'v propo"
have H: "push_conn_inside c c' φ ψ ⟹ no_imp φ ⟹ no_imp ψ"
by (induct φ ψ rule: push_conn_inside.induct, auto)
}
then show "no_imp ψ"
using full_propo_rew_step_inv_stay_conn[of "push_conn_inside c c'" no_imp_symb] assms
no_imp_symb_conn_characterization unfolding no_imp_def by metis
qed
lemma push_conn_inside_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes
"no_equiv φ" and
"no_imp φ" and
"full (propo_rew_step (push_conn_inside c c')) φ ψ" and
"no_T_F_except_top_level φ" and
"simple_not φ" and
"c = CAnd ∨ c = COr" and
"c' = CAnd ∨ c' = COr"
shows "c_in_c'_only c c' ψ"
using c_in_c'_symb_rew assms full_propo_rew_step_subformula by blast
subsubsection ‹Only one type of connective in the formula (+ not)›
inductive only_c_inside_symb :: "'v connective ⇒ 'v propo ⇒ bool" for c :: "'v connective" where
simple_only_c_inside[simp]: "simple φ ⟹ only_c_inside_symb c φ" |
simple_cnot_only_c_inside[simp]: "simple φ ⟹ only_c_inside_symb c (FNot φ)" |
only_c_inside_into_only_c_inside: "wf_conn c l ⟹ only_c_inside_symb c (conn c l)"
lemma only_c_inside_symb_simp[simp]:
"only_c_inside_symb c FF" "only_c_inside_symb c FT" "only_c_inside_symb c (FVar x)" by auto
definition only_c_inside where "only_c_inside c = all_subformula_st (only_c_inside_symb c)"
lemma only_c_inside_symb_decomp:
"only_c_inside_symb c ψ ⟷ (simple ψ
∨ (∃ φ'. ψ = FNot φ' ∧ simple φ')
∨ (∃l. ψ = conn c l ∧ wf_conn c l))"
by (auto simp: only_c_inside_symb.intros(3)) (induct rule: only_c_inside_symb.induct, auto)
lemma only_c_inside_symb_decomp_not[simp]:
fixes c :: "'v connective"
assumes c: "c ≠ CNot"
shows "only_c_inside_symb c (FNot ψ) ⟷ simple ψ"
apply (auto simp: only_c_inside_symb.intros(3))
by (induct "FNot ψ" rule: only_c_inside_symb.induct, auto simp: wf_conn_list(8) c)
lemma only_c_inside_decomp_not[simp]:
assumes c: "c ≠ CNot"
shows "only_c_inside c (FNot ψ) ⟷ simple ψ"
by (metis (no_types, hide_lams) all_subformula_st_def all_subformula_st_test_symb_true_phi c
only_c_inside_def only_c_inside_symb_decomp_not simple_only_c_inside
subformula_conn_decomp_simple)
lemma only_c_inside_decomp:
"only_c_inside c φ ⟷
(∀ψ. ψ ≼ φ ⟶ (simple ψ ∨ (∃ φ'. ψ = FNot φ' ∧ simple φ')
∨ (∃l. ψ = conn c l ∧ wf_conn c l)))"
unfolding only_c_inside_def by (auto simp: all_subformula_st_def only_c_inside_symb_decomp)
lemma only_c_inside_c_c'_false:
fixes c c' :: "'v connective" and l :: "'v propo list" and φ :: "'v propo"
assumes cc': "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
and only: "only_c_inside c φ" and incl: "conn c' l ≼ φ" and wf: "wf_conn c' l"
shows False
proof -
let ?ψ = "conn c' l"
have "simple ?ψ ∨ (∃ φ'. ?ψ = FNot φ' ∧ simple φ') ∨ (∃l. ?ψ = conn c l ∧ wf_conn c l)"
using only_c_inside_decomp only incl by blast
moreover have "¬ simple ?ψ"
using wf simple_decomp by (metis c' connective.distinct(19) connective.distinct(7,9,21,29,31)
wf_conn_list(1-3))
moreover
{
fix φ'
have "?ψ ≠ FNot φ'" using c' conn_inj_not(1) wf by blast
}
ultimately obtain l :: "'v propo list" where "?ψ = conn c l ∧ wf_conn c l" by metis
then have "c = c'" using conn_inj wf by metis
then show False using cc' by auto
qed
lemma only_c_inside_implies_c_in_c'_symb:
assumes δ: "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
shows "only_c_inside c φ ⟹ c_in_c'_symb c c' φ"
apply (rule ccontr)
apply (cases rule: not_c_in_c'_symb.cases, auto)
by (metis δ c c' connective.distinct(37,39) list.distinct(1) only_c_inside_c_c'_false
subformula_in_binary_conn(1,2) wf_conn.simps)+
lemma c_in_c'_symb_decomp_level1:
fixes l :: "'v propo list" and c c' ca :: "'v connective"
shows "wf_conn ca l ⟹ ca ≠ c ⟹ c_in_c'_symb c c' (conn ca l)"
proof -
have "not_c_in_c'_symb c c' (conn ca l) ⟹ wf_conn ca l ⟹ ca = c"
by (induct "conn ca l" rule: not_c_in_c'_symb.induct, auto simp: conn_inj)
then show "wf_conn ca l ⟹ ca ≠ c ⟹ c_in_c'_symb c c' (conn ca l)" by blast
qed
lemma only_c_inside_implies_c_in_c'_only:
assumes δ: "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
shows "only_c_inside c φ ⟹ c_in_c'_only c c' φ"
unfolding c_in_c'_only_def all_subformula_st_def
using only_c_inside_implies_c_in_c'_symb
by (metis all_subformula_st_def assms(1) c c' only_c_inside_def subformula_trans)
lemma c_in_c'_symb_c_implies_only_c_inside:
assumes δ: "c = CAnd ∨ c = COr" "c' = CAnd ∨ c' = COr" "c ≠ c'" and wf: "wf_conn c [φ, ψ]"
and inv: "no_equiv (conn c l)" "no_imp (conn c l)" "simple_not (conn c l)"
shows "wf_conn c l ⟹ c_in_c'_only c c' (conn c l) ⟹ (∀ψ∈ set l. only_c_inside c ψ)"
using inv
proof (induct "conn c l" arbitrary: l rule: propo_induct_arity)
case (nullary x)
then show ?case by (auto simp: wf_conn_list assms)
next
case (unary φ la)
then have "c = CNot ∧ la = [φ]" by (metis (no_types) wf_conn_list(8))
then show ?case using assms(2) assms(1) by blast
next
case (binary φ1 φ2)
note IHφ1 = this(1) and IHφ2 = this(2) and φ = this(3) and only = this(5) and wf = this(4)
and no_equiv = this(6) and no_imp = this(7) and simple_not = this(8)
then have l: "l = [φ1, φ2]" by (meson wf_conn_list(4-7))
let ?φ = "conn c l"
obtain c1 l1 c2 l2 where φ1: "φ1 = conn c1 l1" and wfφ1: "wf_conn c1 l1"
and φ2: "φ2 = conn c2 l2" and wfφ2: "wf_conn c2 l2" using exists_c_conn by metis
then have c_in_onlyφ1: "c_in_c'_only c c' (conn c1 l1)" and "c_in_c'_only c c' (conn c2 l2)"
using only l unfolding c_in_c'_only_def using assms(1) by auto
have incφ1: "φ1 ≼ ?φ" and incφ2: "φ2 ≼ ?φ"
using φ1 φ2 φ local.wf by (metis conn.simps(5-8) helper_fact subformula_in_binary_conn(1,2))+
have c1_eq: "c1 ≠ CEq" and c2_eq: "c2 ≠ CEq"
unfolding no_equiv_def using incφ1 incφ2 by (metis φ1 φ2 wfφ1 wfφ2 assms(1) no_equiv
no_equiv_eq(1) no_equiv_symb.elims(3) no_equiv_symb_conn_characterization wf_conn_list(4,5)
no_equiv_def subformula_all_subformula_st)+
have c1_imp: "c1 ≠ CImp" and c2_imp: "c2 ≠ CImp"
using no_imp by (metis φ1 φ2 all_subformula_st_decomp_explicit_imp(2,3) assms(1)
conn.simps(5,6) l no_imp_Imp(1) no_imp_symb.elims(3) no_imp_symb_conn_characterization
wfφ1 wfφ2 all_subformula_st_decomp no_imp_symb_conn_characterization)+
have c1c: "c1 ≠ c'"
proof
assume c1c: "c1 = c'"
then obtain ξ1 ξ2 where l1: "l1 = [ξ1, ξ2]"
by (metis assms(2) connective.distinct(37,39) helper_fact wfφ1 wf_conn.simps
wf_conn_list_decomp(1-3))
have "c_in_c'_only c c' (conn c [conn c' l1, φ2])" using c1c l only φ1 by auto
moreover have "not_c_in_c'_symb c c' (conn c [conn c' l1, φ2])"
using l1 φ1 c1c l local.wf not_c_in_c'_symb_l wfφ1 by blast
ultimately show False using φ1 c1c l l1 local.wf not_c_in_c'_simp(4) wfφ1 by blast
qed
then have "(φ1 = conn c l1 ∧ wf_conn c l1) ∨ (∃ψ1. φ1 = FNot ψ1) ∨ simple φ1"
by (metis φ1 assms(1-3) c1_eq c1_imp simple.elims(3) wfφ1 wf_conn_list(4) wf_conn_list(5-7))
moreover {
assume "φ1 = conn c l1 ∧ wf_conn c l1"
then have "only_c_inside c φ1"
by (metis IHφ1 φ1 all_subformula_st_decomp_imp incφ1 no_equiv no_equiv_def no_imp no_imp_def
c_in_onlyφ1 only_c_inside_def only_c_inside_into_only_c_inside simple_not simple_not_def
subformula_all_subformula_st)
}
moreover {
assume "∃ψ1. φ1 = FNot ψ1"
then obtain ψ1 where "φ1 = FNot ψ1" by metis
then have "only_c_inside c φ1"
by (metis all_subformula_st_def assms(1) connective.distinct(37,39) incφ1
only_c_inside_decomp_not simple_not simple_not_def simple_not_symb.simps(1))
}
moreover {
assume "simple φ1"
then have "only_c_inside c φ1"
by (metis all_subformula_st_decomp_explicit(3) assms(1) connective.distinct(37,39)
only_c_inside_decomp_not only_c_inside_def)
}
ultimately have only_c_insideφ1: "only_c_inside c φ1" by metis
have c_in_onlyφ2: "c_in_c'_only c c' (conn c2 l2)"
using only l φ2 wfφ2 assms unfolding c_in_c'_only_def by auto
have c2c: "c2 ≠ c'"
proof
assume c2c: "c2 = c'"
then obtain ξ1 ξ2 where l2: "l2 = [ξ1, ξ2]"
by (metis assms(2) wfφ2 wf_conn.simps connective.distinct(7,9,19,21,29,31,37,39))
then have "c_in_c'_symb c c' (conn c [φ1, conn c' l2])"
using c2c l only φ2 all_subformula_st_test_symb_true_phi unfolding c_in_c'_only_def by auto
moreover have "not_c_in_c'_symb c c' (conn c [φ1, conn c' l2])"
using assms(1) c2c l2 not_c_in_c'_symb_r wfφ2 wf_conn_helper_facts(5,6) by metis
ultimately show False by auto
qed
then have "(φ2 = conn c l2 ∧ wf_conn c l2) ∨ (∃ψ2. φ2 = FNot ψ2) ∨ simple φ2"
using c2_eq by (metis φ2 assms(1-3) c2_eq c2_imp simple.elims(3) wfφ2 wf_conn_list(4-7))
moreover {
assume "φ2 = conn c l2 ∧ wf_conn c l2"
then have "only_c_inside c φ2"
by (metis IHφ2 φ2 all_subformula_st_decomp incφ2 no_equiv no_equiv_def no_imp no_imp_def
c_in_onlyφ2 only_c_inside_def only_c_inside_into_only_c_inside simple_not simple_not_def
subformula_all_subformula_st)
}
moreover {
assume "∃ψ2. φ2 = FNot ψ2"
then obtain ψ2 where "φ2 = FNot ψ2" by metis
then have "only_c_inside c φ2"
by (metis all_subformula_st_def assms(1-3) connective.distinct(38,40) incφ2
only_c_inside_decomp_not simple_not simple_not_def simple_not_symb.simps(1))
}
moreover {
assume "simple φ2"
then have "only_c_inside c φ2"
by (metis all_subformula_st_decomp_explicit(3) assms(1) connective.distinct(37,39)
only_c_inside_decomp_not only_c_inside_def)
}
ultimately have only_c_insideφ2: "only_c_inside c φ2" by metis
show ?case using l only_c_insideφ1 only_c_insideφ2 by auto
qed
subsubsection ‹Push Conjunction›
definition pushConj where "pushConj = push_conn_inside CAnd COr"
lemma pushConj_consistent: "preserve_models pushConj"
unfolding pushConj_def by (simp add: push_conn_inside_consistent)
definition and_in_or_symb where "and_in_or_symb = c_in_c'_symb CAnd COr"
definition and_in_or_only where
"and_in_or_only = all_subformula_st (c_in_c'_symb CAnd COr)"
lemma pushConj_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step pushConj) φ ψ"
and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
using push_conn_inside_inv assms unfolding pushConj_def by metis+
lemma pushConj_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes
"no_equiv φ" and
"no_imp φ" and
"full (propo_rew_step pushConj) φ ψ" and
"no_T_F_except_top_level φ" and
"simple_not φ"
shows "and_in_or_only ψ"
using assms push_conn_inside_full_propo_rew_step
unfolding pushConj_def and_in_or_only_def c_in_c'_only_def by (metis (no_types))
subsubsection ‹Push Disjunction›
definition pushDisj where "pushDisj = push_conn_inside COr CAnd"
lemma pushDisj_consistent: "preserve_models pushDisj"
unfolding pushDisj_def by (simp add: push_conn_inside_consistent)
definition or_in_and_symb where "or_in_and_symb = c_in_c'_symb COr CAnd"
definition or_in_and_only where
"or_in_and_only = all_subformula_st (c_in_c'_symb COr CAnd)"
lemma not_or_in_and_only_or_and[simp]:
"~or_in_and_only (FOr (FAnd ψ1 ψ2) φ')"
unfolding or_in_and_only_def
by (metis all_subformula_st_test_symb_true_phi conn.simps(5-6) not_c_in_c'_symb_l
wf_conn_helper_facts(5) wf_conn_helper_facts(6))
lemma pushDisj_inv:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step pushDisj) φ ψ"
and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
using push_conn_inside_inv assms unfolding pushDisj_def by metis+
lemma pushDisj_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes
"no_equiv φ" and
"no_imp φ" and
"full (propo_rew_step pushDisj) φ ψ" and
"no_T_F_except_top_level φ" and
"simple_not φ"
shows "or_in_and_only ψ"
using assms push_conn_inside_full_propo_rew_step
unfolding pushDisj_def or_in_and_only_def c_in_c'_only_def by (metis (no_types))
section ‹The Full Transformations›
subsection ‹Abstract Definition›
text ‹The normal form is a super group of groups›
inductive grouped_by :: "'a connective ⇒ 'a propo ⇒ bool" for c where
simple_is_grouped[simp]: "simple φ ⟹ grouped_by c φ" |
simple_not_is_grouped[simp]: "simple φ ⟹ grouped_by c (FNot φ)" |
connected_is_group[simp]: "grouped_by c φ ⟹ grouped_by c ψ ⟹ wf_conn c [φ, ψ]
⟹ grouped_by c (conn c [φ, ψ])"
lemma simple_clause[simp]:
"grouped_by c FT"
"grouped_by c FF"
"grouped_by c (FVar x)"
"grouped_by c (FNot FT)"
"grouped_by c (FNot FF)"
"grouped_by c (FNot (FVar x))"
by simp+
lemma only_c_inside_symb_c_eq_c':
"only_c_inside_symb c (conn c' [φ1, φ2]) ⟹ c' = CAnd ∨ c' = COr ⟹ wf_conn c' [φ1, φ2]
⟹ c' = c"
by (induct "conn c' [φ1, φ2]" rule: only_c_inside_symb.induct, auto simp: conn_inj)
lemma only_c_inside_c_eq_c':
"only_c_inside c (conn c' [φ1, φ2]) ⟹ c' = CAnd ∨ c' = COr ⟹ wf_conn c' [φ1, φ2] ⟹ c = c'"
unfolding only_c_inside_def all_subformula_st_def using only_c_inside_symb_c_eq_c' subformula_refl
by blast
lemma only_c_inside_imp_grouped_by:
assumes c: "c ≠ CNot" and c': "c' = CAnd ∨ c' = COr"
shows "only_c_inside c φ ⟹ grouped_by c φ" (is "?O φ ⟹ ?G φ")
proof (induct φ rule: propo_induct_arity)
case (nullary φ x)
then show "?G φ" by auto
next
case (unary ψ)
then show "?G (FNot ψ)" by (auto simp: c)
next
case (binary φ φ1 φ2)
note IHφ1 = this(1) and IHφ2 = this(2) and φ = this(3) and only = this(4)
have φ_conn: "φ = conn c [φ1, φ2]" and wf: "wf_conn c [φ1, φ2]"
proof -
obtain c'' l'' where φ_c'': "φ = conn c'' l''" and wf: "wf_conn c'' l''"
using exists_c_conn by metis
then have l'': "l'' = [φ1, φ2]" using φ by (metis wf_conn_list(4-7))
have "only_c_inside_symb c (conn c'' [φ1, φ2])"
using only all_subformula_st_test_symb_true_phi
unfolding only_c_inside_def φ_c'' l'' by metis
then have "c = c''"
by (metis φ φ_c'' conn_inj conn_inj_not(2) l'' list.distinct(1) list.inject wf
only_c_inside_symb.cases simple.simps(5-8))
then show "φ = conn c [φ1, φ2]" and "wf_conn c [φ1, φ2]" using φ_c'' wf l'' by auto
qed
have "grouped_by c φ1" using wf IHφ1 IHφ2 φ_conn only φ unfolding only_c_inside_def by auto
moreover have "grouped_by c φ2"
using wf φ IHφ1 IHφ2 φ_conn only unfolding only_c_inside_def by auto
ultimately show "?G φ" using φ_conn connected_is_group local.wf by blast
qed
lemma grouped_by_false:
"grouped_by c (conn c' [φ, ψ]) ⟹ c ≠ c' ⟹ wf_conn c' [φ, ψ] ⟹ False"
apply (induct "conn c' [φ, ψ]" rule: grouped_by.induct)
apply (auto simp: simple_decomp wf_conn_list, auto simp: conn_inj)
by (metis list.distinct(1) list.sel(3) wf_conn_list(8))+
text ‹Then the CNF form is a conjunction of clauses: every clause is in CNF form and two formulas in
CNF form can be related by an and.›
inductive super_grouped_by:: "'a connective ⇒ 'a connective ⇒ 'a propo ⇒ bool" for c c' where
grouped_is_super_grouped[simp]: "grouped_by c φ ⟹ super_grouped_by c c' φ" |
connected_is_super_group: "super_grouped_by c c' φ ⟹ super_grouped_by c c' ψ ⟹ wf_conn c [φ, ψ]
⟹ super_grouped_by c c' (conn c' [φ, ψ])"
lemma simple_cnf[simp]:
"super_grouped_by c c' FT"
"super_grouped_by c c' FF"
"super_grouped_by c c' (FVar x)"
"super_grouped_by c c' (FNot FT)"
"super_grouped_by c c' (FNot FF)"
"super_grouped_by c c' (FNot (FVar x))"
by auto
lemma c_in_c'_only_super_grouped_by:
assumes c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr" and cc': "c ≠ c'"
shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ c_in_c'_only c c' φ
⟹ super_grouped_by c c' φ"
(is "?NE φ ⟹ ?NI φ ⟹ ?SN φ ⟹ ?C φ ⟹ ?S φ")
proof (induct φ rule: propo_induct_arity)
case (nullary φ x)
then show "?S φ" by auto
next
case (unary φ)
then have "simple_not_symb (FNot φ)"
using all_subformula_st_test_symb_true_phi unfolding simple_not_def by blast
then have "φ = FT ∨ φ = FF ∨ (∃ x. φ = FVar x)" by (cases φ, auto)
then show "?S (FNot φ)" by auto
next
case (binary φ φ1 φ2)
note IHφ1 = this(1) and IHφ2 = this(2) and no_equiv = this(4) and no_imp = this(5)
and simpleN = this(6) and c_in_c'_only = this(7) and φ' = this(3)
{
assume "φ = FImp φ1 φ2 ∨ φ = FEq φ1 φ2"
then have False using no_equiv no_imp by auto
then have "?S φ" by auto
}
moreover {
assume φ: "φ = conn c' [φ1, φ2] ∧ wf_conn c' [φ1, φ2]"
have c_in_c'_only: "c_in_c'_only c c' φ1 ∧ c_in_c'_only c c' φ2 ∧ c_in_c'_symb c c' φ"
using c_in_c'_only φ' unfolding c_in_c'_only_def by auto
have "super_grouped_by c c' φ1" using φ c' no_equiv no_imp simpleN IHφ1 c_in_c'_only by auto
moreover have "super_grouped_by c c' φ2"
using φ c' no_equiv no_imp simpleN IHφ2 c_in_c'_only by auto
ultimately have "?S φ"
using super_grouped_by.intros(2) φ by (metis c wf_conn_helper_facts(5,6))
}
moreover {
assume φ: "φ = conn c [φ1, φ2] ∧ wf_conn c [φ1, φ2]"
then have "only_c_inside c φ1 ∧ only_c_inside c φ2"
using c_in_c'_symb_c_implies_only_c_inside c c' c_in_c'_only list.set_intros(1)
wf_conn_helper_facts(5,6) no_equiv no_imp simpleN last_ConsL last_ConsR last_in_set
list.distinct(1) by (metis (no_types, hide_lams) cc')
then have "only_c_inside c (conn c [φ1, φ2])"
unfolding only_c_inside_def using φ
by (simp add: only_c_inside_into_only_c_inside all_subformula_st_decomp)
then have "grouped_by c φ" using φ only_c_inside_imp_grouped_by c by blast
then have "?S φ" using super_grouped_by.intros(1) by metis
}
ultimately show "?S φ" by (metis φ' c c' cc' conn.simps(5,6) wf_conn_helper_facts(5,6))
qed
subsection ‹Conjunctive Normal Form›
subsubsection ‹Definition›
definition is_conj_with_TF where "is_conj_with_TF == super_grouped_by COr CAnd"
lemma or_in_and_only_conjunction_in_disj:
shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ or_in_and_only φ ⟹ is_conj_with_TF φ"
using c_in_c'_only_super_grouped_by
unfolding is_conj_with_TF_def or_in_and_only_def c_in_c'_only_def
by (simp add: c_in_c'_only_def c_in_c'_only_super_grouped_by)
definition is_cnf where
"is_cnf φ ≡ is_conj_with_TF φ ∧ no_T_F_except_top_level φ"
subsubsection ‹Full CNF transformation›
text ‹The full1 CNF transformation consists simply in chaining all the transformation defined
before.›
definition cnf_rew where "cnf_rew =
(full (propo_rew_step elim_equiv)) OO
(full (propo_rew_step elim_imp)) OO
(full (propo_rew_step elimTB)) OO
(full (propo_rew_step pushNeg)) OO
(full (propo_rew_step pushDisj))"
lemma cnf_rew_equivalent: "preserve_models cnf_rew"
by (simp add: cnf_rew_def elimEquv_lifted_consistant elim_imp_lifted_consistant elimTB_consistent
preserve_models_OO pushDisj_consistent pushNeg_lifted_consistant)
lemma cnf_rew_is_cnf: "cnf_rew φ φ' ⟹ is_cnf φ'"
apply (unfold cnf_rew_def OO_def)
apply auto
proof -
fix φ φEq φImp φTB φNeg φDisj :: "'v propo"
assume Eq: "full (propo_rew_step elim_equiv) φ φEq"
then have no_equiv: "no_equiv φEq" using no_equiv_full_propo_rew_step_elim_equiv by blast
assume Imp: "full (propo_rew_step elim_imp) φEq φImp"
then have no_imp: "no_imp φImp" using no_imp_full_propo_rew_step_elim_imp by blast
have no_imp_inv: "no_equiv φImp" using no_equiv Imp elim_imp_inv by blast
assume TB: "full (propo_rew_step elimTB) φImp φTB"
then have noTB: "no_T_F_except_top_level φTB"
using no_imp_inv no_imp elimTB_full_propo_rew_step by blast
have noTB_inv: "no_equiv φTB" "no_imp φTB" using elimTB_inv TB no_imp no_imp_inv by blast+
assume Neg: "full (propo_rew_step pushNeg) φTB φNeg"
then have noNeg: "simple_not φNeg"
using noTB_inv noTB pushNeg_full_propo_rew_step by blast
have noNeg_inv: "no_equiv φNeg" "no_imp φNeg" "no_T_F_except_top_level φNeg"
using pushNeg_inv Neg noTB noTB_inv by blast+
assume Disj: "full (propo_rew_step pushDisj) φNeg φDisj"
then have no_Disj: "or_in_and_only φDisj"
using noNeg_inv noNeg pushDisj_full_propo_rew_step by blast
have noDisj_inv: "no_equiv φDisj" "no_imp φDisj" "no_T_F_except_top_level φDisj"
"simple_not φDisj"
using pushDisj_inv Disj noNeg noNeg_inv by blast+
moreover have "is_conj_with_TF φDisj"
using or_in_and_only_conjunction_in_disj noDisj_inv no_Disj by blast
ultimately show "is_cnf φDisj" unfolding is_cnf_def by blast
qed
subsection ‹Disjunctive Normal Form›
subsubsection ‹Definition›
definition is_disj_with_TF where "is_disj_with_TF ≡ super_grouped_by CAnd COr"
lemma and_in_or_only_conjunction_in_disj:
shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ and_in_or_only φ ⟹ is_disj_with_TF φ"
using c_in_c'_only_super_grouped_by
unfolding is_disj_with_TF_def and_in_or_only_def c_in_c'_only_def
by (simp add: c_in_c'_only_def c_in_c'_only_super_grouped_by)
definition is_dnf :: "'a propo ⇒ bool" where
"is_dnf φ ⟷ is_disj_with_TF φ ∧ no_T_F_except_top_level φ"
subsubsection ‹Full DNF transform›
text ‹The full1 DNF transformation consists simply in chaining all the transformation defined
before.›
definition dnf_rew where "dnf_rew ≡
(full (propo_rew_step elim_equiv)) OO
(full (propo_rew_step elim_imp)) OO
(full (propo_rew_step elimTB)) OO
(full (propo_rew_step pushNeg)) OO
(full (propo_rew_step pushConj))"
lemma dnf_rew_consistent: "preserve_models dnf_rew"
by (simp add: dnf_rew_def elimEquv_lifted_consistant elim_imp_lifted_consistant elimTB_consistent
preserve_models_OO pushConj_consistent pushNeg_lifted_consistant)
theorem dnf_transformation_correction:
"dnf_rew φ φ' ⟹ is_dnf φ'"
apply (unfold dnf_rew_def OO_def)
by (meson and_in_or_only_conjunction_in_disj elimTB_full_propo_rew_step elimTB_inv(1,2)
elim_imp_inv is_dnf_def no_equiv_full_propo_rew_step_elim_equiv
no_imp_full_propo_rew_step_elim_imp pushConj_full_propo_rew_step pushConj_inv(1-4)
pushNeg_full_propo_rew_step pushNeg_inv(1-3))
section ‹More aggressive simplifications: Removing true and false at the beginning›
subsection ‹Transformation›
text ‹We should remove @{term FT} and @{term FF} at the beginning and not in the middle of the
algorithm. To do this, we have to use more rules (one for each connective):›
inductive elimTBFull where
ElimTBFull1[simp]: "elimTBFull (FAnd φ FT) φ" |
ElimTBFull1'[simp]: "elimTBFull (FAnd FT φ) φ" |
ElimTBFull2[simp]: "elimTBFull (FAnd φ FF) FF" |
ElimTBFull2'[simp]: "elimTBFull (FAnd FF φ) FF" |
ElimTBFull3[simp]: "elimTBFull (FOr φ FT) FT" |
ElimTBFull3'[simp]: "elimTBFull (FOr FT φ) FT" |
ElimTBFull4[simp]: "elimTBFull (FOr φ FF) φ" |
ElimTBFull4'[simp]: "elimTBFull (FOr FF φ) φ" |
ElimTBFull5[simp]: "elimTBFull (FNot FT) FF" |
ElimTBFull5'[simp]: "elimTBFull (FNot FF) FT" |
ElimTBFull6_l[simp]: "elimTBFull (FImp FT φ) φ" |
ElimTBFull6_l'[simp]: "elimTBFull (FImp FF φ) FT" |
ElimTBFull6_r[simp]: "elimTBFull (FImp φ FT) FT" |
ElimTBFull6_r'[simp]: "elimTBFull (FImp φ FF) (FNot φ)" |
ElimTBFull7_l[simp]: "elimTBFull (FEq FT φ) φ" |
ElimTBFull7_l'[simp]: "elimTBFull (FEq FF φ) (FNot φ)" |
ElimTBFull7_r[simp]: "elimTBFull (FEq φ FT) φ" |
ElimTBFull7_r'[simp]: "elimTBFull (FEq φ FF) (FNot φ)"
text ‹The transformation is still consistent.›
lemma elimTBFull_consistent: "preserve_models elimTBFull"
proof -
{
fix φ ψ:: "'b propo"
have "elimTBFull φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
by (induct_tac rule: elimTBFull.inducts, auto)
}
then show ?thesis using preserve_models_def by auto
qed
text ‹Contrary to the theorem @{thm [source] no_T_F_symb_except_toplevel_step_exists}, we do not
need the assumption @{term "no_equiv φ"} and @{term "no_imp φ"}, since our transformation is
more general.›
lemma no_T_F_symb_except_toplevel_step_exists':
fixes φ :: "'v propo"
shows "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTBFull ψ ψ'"
proof (induct ψ rule: propo_induct_arity)
case (nullary φ')
then have False using no_T_F_symb_except_toplevel_true no_T_F_symb_except_toplevel_false by auto
then show "Ex (elimTBFull φ')" by blast
next
case (unary ψ)
then have "ψ = FF ∨ ψ = FT" using no_T_F_symb_except_toplevel_not_decom by blast
then show "Ex (elimTBFull (FNot ψ))" using ElimTBFull5 ElimTBFull5' by blast
next
case (binary φ' ψ1 ψ2)
then have "ψ1 = FT ∨ ψ2 = FT ∨ ψ1 = FF ∨ ψ2 = FF"
by (metis binary_connectives_def conn.simps(5-8) insertI1 insert_commute
no_T_F_symb_except_toplevel_bin_decom binary.hyps(3))
then show "Ex (elimTBFull φ')" using elimTBFull.intros binary.hyps(3) by blast
qed
text ‹The same applies here. We do not need the assumption, but the deep link between
@{term "¬ no_T_F_except_top_level φ"} and the existence of a rewriting step, still exists.›
lemma no_T_F_except_top_level_rew':
fixes φ :: "'v propo"
assumes noTB: "¬ no_T_F_except_top_level φ"
shows "∃ψ ψ'. ψ ≼ φ ∧ elimTBFull ψ ψ'"
proof -
have test_symb_false_nullary:
"∀x. no_T_F_symb_except_toplevel (FF:: 'v propo) ∧ no_T_F_symb_except_toplevel FT
∧ no_T_F_symb_except_toplevel (FVar (x:: 'v))"
by auto
moreover {
fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
have H: "elimTBFull (conn c l) ψ ⟹ ¬no_T_F_symb_except_toplevel (conn c l)"
by (cases "conn c l" rule: elimTBFull.cases) auto
}
ultimately show ?thesis
using no_test_symb_step_exists[of no_T_F_symb_except_toplevel φ elimTBFull] noTB
no_T_F_symb_except_toplevel_step_exists' unfolding no_T_F_except_top_level_def by metis
qed
lemma elimTBFull_full_propo_rew_step:
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step elimTBFull) φ ψ"
shows "no_T_F_except_top_level ψ"
using full_propo_rew_step_subformula no_T_F_except_top_level_rew' assms by fastforce
subsection ‹More invariants›
text ‹As the aim is to use the transformation as the first transformation, we have to show some more
invariants for @{term elim_equiv} and @{term elim_imp}. For the other transformation, we have
already proven it.›
lemma propo_rew_step_ElimEquiv_no_T_F: "propo_rew_step elim_equiv φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
fix φ' :: "'v propo" and ψ' :: "'v propo"
assume a1: "no_T_F φ'"
assume a2: "elim_equiv φ' ψ'"
have "∀x0 x1. (¬ elim_equiv (x1 :: 'v propo) x0 ∨ (∃v2 v3 v4 v5 v6 v7. x1 = FEq v2 v3
∧ x0 = FAnd (FImp v4 v5) (FImp v6 v7) ∧ v2 = v4 ∧ v4 = v7 ∧ v3 = v5 ∧ v3 = v6))
= (¬ elim_equiv x1 x0 ∨ (∃v2 v3 v4 v5 v6 v7. x1 = FEq v2 v3
∧ x0 = FAnd (FImp v4 v5) (FImp v6 v7) ∧ v2 = v4 ∧ v4 = v7 ∧ v3 = v5 ∧ v3 = v6))"
by meson
then have "∀p pa. ¬ elim_equiv (p :: 'v propo) pa ∨ (∃pb pc pd pe pf pg. p = FEq pb pc
∧ pa = FAnd (FImp pd pe) (FImp pf pg) ∧ pb = pd ∧ pd = pg ∧ pc = pe ∧ pc = pf)"
using elim_equiv.cases by force
then show "no_T_F ψ'" using a1 a2 by fastforce
next
fix φ φ' :: "'v propo" and ξ ξ' :: "'v propo list" and c :: "'v connective"
assume rel: "propo_rew_step elim_equiv φ φ'"
and IH: "no_T_F φ ⟹ no_T_F φ'"
and corr: "wf_conn c (ξ @ φ # ξ')"
and no_T_F: "no_T_F (conn c (ξ @ φ # ξ'))"
{
assume c: "c = CNot"
then have empty: "ξ = []" "ξ' = []" using corr by auto
then have "no_T_F φ" using no_T_F c no_T_F_decomp_not by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))" using c empty no_T_F_comp_not IH by auto
}
moreover {
assume c: "c ∈ binary_connectives"
obtain a b where ab: "ξ @ φ # ξ' = [a, b]"
using corr c list_length2_decomp wf_conn_bin_list_length by metis
then have φ: "φ = a ∨ φ = b"
by (metis append.simps(1) append_is_Nil_conv list.distinct(1) list.sel(3) nth_Cons_0
tl_append2)
have ζ: "∀ζ∈ set (ξ @ φ # ξ'). no_T_F ζ"
using no_T_F unfolding no_T_F_def using corr all_subformula_st_decomp by blast
then have φ': "no_T_F φ'" using ab IH φ by auto
have l': "ξ @ φ' # ξ' = [φ', b] ∨ ξ @ φ' # ξ' = [a, φ']"
by (metis (no_types, hide_lams) ab append_Cons append_Nil append_Nil2 butlast.simps(2)
butlast_append list.distinct(1) list.sel(3))
then have "∀ζ ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using ζ φ' ab by fastforce
moreover
have "∀ζ ∈ set (ξ @ φ # ξ'). ζ ≠ FT ∧ ζ ≠ FF"
using ζ corr no_T_F no_T_F_except_top_level_false no_T_F_no_T_F_except_top_level by blast
then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))"
by (metis φ' l' ab all_subformula_st_test_symb_true_phi c list.distinct(1)
list.set_intros(1,2) no_T_F_symb_except_toplevel_bin_decom
no_T_F_symb_except_toplevel_no_T_F_symb no_T_F_symb_false(1,2) no_T_F_def wf_conn_binary
wf_conn_list(1,2))
ultimately have "no_T_F (conn c (ξ @ φ' # ξ'))"
by (metis l' all_subformula_st_decomp_imp c no_T_F_def wf_conn_binary)
}
moreover {
fix x
assume "c = CVar x ∨ c = CF ∨ c = CT"
then have False using corr by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))" by auto
}
ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using corr wf_conn.cases by metis
qed
lemma elim_equiv_inv':
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step elim_equiv) φ ψ" and "no_T_F_except_top_level φ"
shows "no_T_F_except_top_level ψ"
proof -
{
fix φ ψ :: "'v propo"
have "propo_rew_step elim_equiv φ ψ ⟹ no_T_F_except_top_level φ
⟹ no_T_F_except_top_level ψ"
proof -
assume rel: "propo_rew_step elim_equiv φ ψ"
and no: "no_T_F_except_top_level φ"
{
assume "φ = FT ∨ φ = FF"
from rel this have False
apply (induct rule: propo_rew_step.induct, auto simp: wf_conn_list(1,2))
using elim_equiv.simps by blast+
then have "no_T_F_except_top_level ψ" by blast
}
moreover {
assume "φ ≠ FT ∧ φ ≠ FF"
then have "no_T_F φ"
by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
then have "no_T_F ψ" using propo_rew_step_ElimEquiv_no_T_F rel by blast
then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
}
ultimately show "no_T_F_except_top_level ψ" by metis
qed
}
moreover {
fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
assume rel: "propo_rew_step elim_equiv ζ ζ'"
and incl: "ζ ≼ φ"
and corr: "wf_conn c (ξ @ ζ # ξ')"
and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
and n: "no_T_F_symb_except_toplevel ζ'"
have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
proof
have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
using corr wf_conn_list(1) wf_conn_list(2) no_T_F_symb_except_toplevel_no_T_F_symb no_T_F
by blast
have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
using corr wf_conn_no_T_F_symb_iff p by blast
from rel incl have "ζ'≠FT ∧ζ'≠FF"
apply (induction ζ ζ' rule: propo_rew_step.induct)
apply (cases rule: elim_equiv.cases, auto simp: elim_equiv.simps)
by (metis append_is_Nil_conv list.distinct wf_conn_list(1,2) wf_conn_no_arity_change
wf_conn_no_arity_change_helper)+
then have "∀φ ∈ set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
by (metis corr wf_conn_no_arity_change wf_conn_no_arity_change_helper no_T_F_symb_comp)
qed
}
ultimately show "no_T_F_except_top_level ψ"
using full_propo_rew_step_inv_stay_with_inc[of "elim_equiv" "no_T_F_symb_except_toplevel" "φ"]
assms subformula_refl unfolding no_T_F_except_top_level_def by metis
qed
lemma propo_rew_step_ElimImp_no_T_F: "propo_rew_step elim_imp φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
case (global_rel φ' ψ')
then show "no_T_F ψ'"
using elim_imp.cases no_T_F_comp_not no_T_F_decomp(1,2)
by (metis no_T_F_comp_expanded_explicit(2))
next
case (propo_rew_one_step_lift φ φ' c ξ ξ')
note rel = this(1) and IH = this(2) and corr = this(3) and no_T_F = this(4)
{
assume c: "c = CNot"
then have empty: "ξ = []" "ξ' = []" using corr by auto
then have "no_T_F φ" using no_T_F c no_T_F_decomp_not by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))" using c empty no_T_F_comp_not IH by auto
}
moreover {
assume c: "c ∈ binary_connectives"
then obtain a b where ab: "ξ @ φ # ξ' = [a, b]"
using corr list_length2_decomp wf_conn_bin_list_length by metis
then have φ: "φ = a ∨ φ = b"
by (metis append_self_conv2 wf_conn_list_decomp(4) wf_conn_unary list.discI list.sel(3)
nth_Cons_0 tl_append2)
have ζ: "∀ζ ∈ set (ξ @ φ # ξ'). no_T_F ζ" using ab c propo_rew_one_step_lift.prems by auto
then have φ': "no_T_F φ'"
using ab IH φ corr no_T_F no_T_F_def all_subformula_st_decomp_explicit by auto
have χ: "ξ @ φ' # ξ' = [φ', b] ∨ ξ @ φ' # ξ' = [a, φ']"
by (metis (no_types, hide_lams) ab append_Cons append_Nil append_Nil2 butlast.simps(2)
butlast_append list.distinct(1) list.sel(3))
then have "∀ζ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using ζ φ' ab by fastforce
moreover
have "no_T_F (last (ξ @ φ' # ξ'))" by (simp add: calculation)
then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))"
by (metis χ φ' ζ ab all_subformula_st_test_symb_true_phi c last.simps list.distinct(1)
list.set_intros(1) no_T_F_bin_decomp no_T_F_def)
ultimately have "no_T_F (conn c (ξ @ φ' # ξ'))" using c χ by fastforce
}
moreover {
fix x
assume "c = CVar x ∨ c = CF ∨ c = CT"
then have False using corr by auto
then have "no_T_F (conn c (ξ @ φ' # ξ'))" by auto
}
ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using corr wf_conn.cases by blast
qed
lemma elim_imp_inv':
fixes φ ψ :: "'v propo"
assumes "full (propo_rew_step elim_imp) φ ψ" and "no_T_F_except_top_level φ"
shows"no_T_F_except_top_level ψ"
proof -
{
{
fix φ ψ :: "'v propo"
have H: "elim_imp φ ψ ⟹ no_T_F_except_top_level φ ⟹ no_T_F_except_top_level ψ"
by (induct φ ψ rule: elim_imp.induct, auto)
} note H = this
fix φ ψ :: "'v propo"
have "propo_rew_step elim_imp φ ψ ⟹ no_T_F_except_top_level φ ⟹ no_T_F_except_top_level ψ"
proof -
assume rel: "propo_rew_step elim_imp φ ψ"
and no: "no_T_F_except_top_level φ"
{
assume "φ = FT ∨ φ = FF"
from rel this have False
apply (induct rule: propo_rew_step.induct)
by (cases rule: elim_imp.cases, auto simp: wf_conn_list(1,2))
then have "no_T_F_except_top_level ψ" by blast
}
moreover {
assume "φ ≠ FT ∧ φ ≠ FF"
then have "no_T_F φ"
by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
then have "no_T_F ψ"
using rel propo_rew_step_ElimImp_no_T_F by blast
then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
}
ultimately show "no_T_F_except_top_level ψ" by metis
qed
}
moreover {
fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
assume rel: "propo_rew_step elim_imp ζ ζ'"
and incl: "ζ ≼ φ"
and corr: "wf_conn c (ξ @ ζ # ξ')"
and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
and n: "no_T_F_symb_except_toplevel ζ'"
have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
proof
have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
by (simp add: corr no_T_F no_T_F_symb_except_toplevel_no_T_F_symb wf_conn_list(1,2))
have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
using corr wf_conn_no_T_F_symb_iff p by blast
from rel incl have "ζ'≠FT ∧ζ'≠FF"
apply (induction ζ ζ' rule: propo_rew_step.induct)
apply (cases rule: elim_imp.cases, auto)
using wf_conn_list(1,2) wf_conn_no_arity_change wf_conn_no_arity_change_helper
by (metis append_is_Nil_conv list.distinct(1))+
then have "∀φ∈set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
using corr wf_conn_no_arity_change no_T_F_symb_comp
by (metis wf_conn_no_arity_change_helper)
qed
}
ultimately show "no_T_F_except_top_level ψ"
using full_propo_rew_step_inv_stay_with_inc[of "elim_imp" "no_T_F_symb_except_toplevel" "φ"]
assms subformula_refl unfolding no_T_F_except_top_level_def by metis
qed
subsection ‹The new CNF and DNF transformation›
text ‹The transformation is the same as before, but the order is not the same.›
definition dnf_rew' :: "'a propo ⇒ 'a propo ⇒ bool" where
"dnf_rew' =
(full (propo_rew_step elimTBFull)) OO
(full (propo_rew_step elim_equiv)) OO
(full (propo_rew_step elim_imp)) OO
(full (propo_rew_step pushNeg)) OO
(full (propo_rew_step pushConj))"
lemma dnf_rew'_consistent: "preserve_models dnf_rew'"
by (simp add: dnf_rew'_def elimEquv_lifted_consistant elim_imp_lifted_consistant
elimTBFull_consistent preserve_models_OO pushConj_consistent pushNeg_lifted_consistant)
theorem cnf_transformation_correction:
"dnf_rew' φ φ' ⟹ is_dnf φ'"
unfolding dnf_rew'_def OO_def
by (meson and_in_or_only_conjunction_in_disj elimTBFull_full_propo_rew_step elim_equiv_inv'
elim_imp_inv elim_imp_inv' is_dnf_def no_equiv_full_propo_rew_step_elim_equiv
no_imp_full_propo_rew_step_elim_imp pushConj_full_propo_rew_step pushConj_inv(1-4)
pushNeg_full_propo_rew_step pushNeg_inv(1-3))
text ‹Given all the lemmas before the CNF transformation is easy to prove:›
definition cnf_rew' :: "'a propo ⇒ 'a propo ⇒ bool" where
"cnf_rew' =
(full (propo_rew_step elimTBFull)) OO
(full (propo_rew_step elim_equiv)) OO
(full (propo_rew_step elim_imp)) OO
(full (propo_rew_step pushNeg)) OO
(full (propo_rew_step pushDisj))"
lemma cnf_rew'_consistent: "preserve_models cnf_rew'"
by (simp add: cnf_rew'_def elimEquv_lifted_consistant elim_imp_lifted_consistant
elimTBFull_consistent preserve_models_OO pushDisj_consistent pushNeg_lifted_consistant)
theorem cnf'_transformation_correction:
"cnf_rew' φ φ' ⟹ is_cnf φ'"
unfolding cnf_rew'_def OO_def
by (meson elimTBFull_full_propo_rew_step elim_equiv_inv' elim_imp_inv elim_imp_inv' is_cnf_def
no_equiv_full_propo_rew_step_elim_equiv no_imp_full_propo_rew_step_elim_imp
or_in_and_only_conjunction_in_disj pushDisj_full_propo_rew_step pushDisj_inv(1-4)
pushNeg_full_propo_rew_step pushNeg_inv(1) pushNeg_inv(2) pushNeg_inv(3))
end