header{* Logic *}
theory Logic
imports Main FuncSet
begin
text{* \noindent
We start with a generic formalization of quantified logical formulae
using de Bruijn notation. The syntax is parametric in the type of atoms. *}
declare Let_def[simp]
datatype 'a fm =
TrueF | FalseF | Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
Neg "'a fm" | ExQ "'a fm"
abbreviation Imp where "Imp φ1 φ2 ≡ Or (Neg φ1) φ2"
abbreviation AllQ where "AllQ φ ≡ Neg(ExQ(Neg φ))"
definition neg where
"neg φ = (if φ=TrueF then FalseF else if φ=FalseF then TrueF else Neg φ)"
definition "and" :: "'a fm => 'a fm => 'a fm" where
"and φ1 φ2 =
(if φ1=TrueF then φ2 else if φ2=TrueF then φ1 else
if φ1=FalseF ∨ φ2=FalseF then FalseF else And φ1 φ2)"
definition or :: "'a fm => 'a fm => 'a fm" where
"or φ1 φ2 =
(if φ1=FalseF then φ2 else if φ2=FalseF then φ1 else
if φ1=TrueF ∨ φ2=TrueF then TrueF else Or φ1 φ2)"
definition list_conj :: "'a fm list => 'a fm" where
"list_conj fs = foldr and fs TrueF"
definition list_disj :: "'a fm list => 'a fm" where
"list_disj fs = foldr or fs FalseF"
abbreviation "Disj is f ≡ list_disj (map f is)"
fun atoms :: "'a fm => 'a set" where
"atoms TrueF = {}" |
"atoms FalseF = {}" |
"atoms (Atom a) = {a}" |
"atoms (And φ1 φ2) = atoms φ1 ∪ atoms φ2" |
"atoms (Or φ1 φ2) = atoms φ1 ∪ atoms φ2" |
"atoms (Neg φ) = atoms φ" |
"atoms (ExQ φ) = atoms φ"
fun map_fm :: "('a => 'b) => 'a fm => 'b fm" ("mapfm") where
"mapfm h TrueF = TrueF" |
"mapfm h FalseF = FalseF" |
"mapfm h (Atom a) = Atom(h a)" |
"mapfm h (And φ1 φ2) = And (mapfm h φ1) (mapfm h φ2)" |
"mapfm h (Or φ1 φ2) = Or (mapfm h φ1) (mapfm h φ2)" |
"mapfm h (Neg φ) = Neg (mapfm h φ)" |
"mapfm h (ExQ φ) = ExQ (mapfm h φ)"
lemma atoms_map_fm[simp]: "atoms(mapfm f φ) = f ` atoms φ"
by(induct φ) auto
fun amap_fm :: "('a => 'b fm) => 'a fm => 'b fm" ("amapfm") where
"amapfm h TrueF = TrueF" |
"amapfm h FalseF = FalseF" |
"amapfm h (Atom a) = h a" |
"amapfm h (And φ1 φ2) = and (amapfm h φ1) (amapfm h φ2)" |
"amapfm h (Or φ1 φ2) = or (amapfm h φ1) (amapfm h φ2)" |
"amapfm h (Neg φ) = neg (amapfm h φ)"
lemma amap_fm_list_disj:
"amapfm h (list_disj fs) = list_disj (map (amapfm h) fs)"
by(induct fs) (auto simp:list_disj_def or_def)
fun qfree :: "'a fm => bool" where
"qfree(ExQ f) = False" |
"qfree(And φ1 φ2) = (qfree φ1 ∧ qfree φ2)" |
"qfree(Or φ1 φ2) = (qfree φ1 ∧ qfree φ2)" |
"qfree(Neg φ) = (qfree φ)" |
"qfree φ = True"
lemma qfree_and[simp]: "[| qfree φ1; qfree φ2 |] ==> qfree(and φ1 φ2)"
by(simp add:and_def)
lemma qfree_or[simp]: "[| qfree φ1; qfree φ2 |] ==> qfree(or φ1 φ2)"
by(simp add:or_def)
lemma qfree_neg[simp]: "qfree(neg φ) = qfree φ"
by(simp add:neg_def)
lemma qfree_foldr_Or[simp]:
"qfree(foldr Or fs φ) = (qfree φ ∧ (∀φ ∈ set fs. qfree φ))"
by (induct fs) auto
lemma qfree_list_conj[simp]:
assumes "∀φ ∈ set fs. qfree φ" shows "qfree(list_conj fs)"
proof -
{ fix fs φ
have "[| ∀φ ∈ set fs. qfree φ; qfree φ |] ==> qfree(foldr and fs φ)"
by (induct fs) auto
} thus ?thesis using assms by (fastsimp simp add:list_conj_def)
qed
lemma qfree_list_disj[simp]:
assumes "∀φ ∈ set fs. qfree φ" shows "qfree(list_disj fs)"
proof -
{ fix fs φ
have "[| ∀φ ∈ set fs. qfree φ; qfree φ |] ==> qfree(foldr or fs φ)"
by (induct fs) auto
} thus ?thesis using assms by (fastsimp simp add:list_disj_def)
qed
lemma qfree_map_fm: "qfree (mapfm f φ) = qfree φ"
by (induct φ) simp_all
lemma atoms_list_disjE:
"a : atoms(list_disj fs) ==> a : (\<Union>φ ∈ set fs. atoms φ)"
apply(induct fs)
apply (simp add:list_disj_def)
apply (auto simp add:list_disj_def Logic.or_def split:split_if_asm)
done
lemma atoms_list_conjE:
"a : atoms(list_conj fs) ==> a : (\<Union>φ ∈ set fs. atoms φ)"
apply(induct fs)
apply (simp add:list_conj_def)
apply (auto simp add:list_conj_def Logic.and_def split:split_if_asm)
done
fun dnf :: "'a fm => 'a list list" where
"dnf TrueF = [[]]" |
"dnf FalseF = []" |
"dnf (Atom φ) = [[φ]]" |
"dnf (And φ1 φ2) = [d1 @ d2. d1 \<leftarrow> dnf φ1, d2 \<leftarrow> dnf φ2]" |
"dnf (Or φ1 φ2) = dnf φ1 @ dnf φ2"
fun nqfree :: "'a fm => bool" where
"nqfree(Atom a) = True" |
"nqfree TrueF = True" |
"nqfree FalseF = True" |
"nqfree (And φ1 φ2) = (nqfree φ1 ∧ nqfree φ2)" |
"nqfree (Or φ1 φ2) = (nqfree φ1 ∧ nqfree φ2)" |
"nqfree φ = False"
lemma nqfree_qfree[simp]: "nqfree φ ==> qfree φ"
by (induct φ) simp_all
lemma nqfree_map_fm: "nqfree (mapfm f φ) = nqfree φ"
by (induct φ) simp_all
fun "interpret" :: "('a => 'b list => bool) => 'a fm => 'b list => bool" where
"interpret h TrueF xs = True" |
"interpret h FalseF xs = False" |
"interpret h (Atom a) xs = h a xs" |
"interpret h (And φ1 φ2) xs = (interpret h φ1 xs ∧ interpret h φ2 xs)" |
"interpret h (Or φ1 φ2) xs = (interpret h φ1 xs | interpret h φ2 xs)" |
"interpret h (Neg φ) xs = (¬ interpret h φ xs)" |
"interpret h (ExQ φ) xs = (∃x. interpret h φ (x#xs))"
subsection{*Atoms*}
text{* The locale ATOM of atoms provides a minimal framework for the
generic formulation of theory-independent algorithms, in particular
quantifier elimination. *}
locale ATOM =
fixes aneg :: "'a => 'a fm"
fixes anormal :: "'a => bool"
assumes nqfree_aneg: "nqfree(aneg a)"
assumes anormal_aneg: "anormal a ==> ∀b∈atoms(aneg a). anormal b"
fixes Ia :: "'a => 'b list => bool"
assumes Ia_aneg: "interpret Ia (aneg a) xs = (¬ Ia a xs)"
fixes depends0 :: "'a => bool"
and decr :: "'a => 'a"
assumes not_dep_decr: "¬depends0 a ==> Ia a (x#xs) = Ia (decr a) xs"
assumes anormal_decr: "¬ depends0 a ==> anormal a ==> anormal(decr a)"
begin
fun atoms0 :: "'a fm => 'a list" where
"atoms0 TrueF = []" |
"atoms0 FalseF = []" |
"atoms0 (Atom a) = (if depends0 a then [a] else [])" |
"atoms0 (And φ1 φ2) = atoms0 φ1 @ atoms0 φ2" |
"atoms0 (Or φ1 φ2) = atoms0 φ1 @ atoms0 φ2" |
"atoms0 (Neg φ) = atoms0 φ"
abbreviation I where "I ≡ interpret Ia"
fun nnf :: "'a fm => 'a fm" where
"nnf (And φ1 φ2) = And (nnf φ1) (nnf φ2)" |
"nnf (Or φ1 φ2) = Or (nnf φ1) (nnf φ2)" |
"nnf (Neg TrueF) = FalseF" |
"nnf (Neg FalseF) = TrueF" |
"nnf (Neg (Neg φ)) = (nnf φ)" |
"nnf (Neg (And φ1 φ2)) = (Or (nnf (Neg φ1)) (nnf (Neg φ2)))" |
"nnf (Neg (Or φ1 φ2)) = (And (nnf (Neg φ1)) (nnf (Neg φ2)))" |
"nnf (Neg (Atom a)) = aneg a" |
"nnf φ = φ"
lemma nqfree_nnf: "qfree φ ==> nqfree(nnf φ)"
by(induct φ rule:nnf.induct)
(simp_all add: nqfree_aneg and_def or_def)
lemma qfree_nnf[simp]: "qfree(nnf φ) = qfree φ"
by (induct φ rule:nnf.induct)(simp_all add: nqfree_aneg)
lemma I_neg[simp]: "I (neg φ) xs = I (Neg φ) xs"
by(simp add:neg_def)
lemma I_and[simp]: "I (and φ1 φ2) xs = I (And φ1 φ2) xs"
by(simp add:and_def)
lemma I_list_conj[simp]:
"I (list_conj fs) xs = (∀φ ∈ set fs. I φ xs)"
proof -
{ fix fs φ
have "I (foldr and fs φ) xs = (I φ xs ∧ (∀φ ∈ set fs. I φ xs))"
by (induct fs) auto
} thus ?thesis by(simp add:list_conj_def)
qed
lemma I_or[simp]: "I (or φ1 φ2) xs = I (Or φ1 φ2) xs"
by(simp add:or_def)
lemma I_list_disj[simp]:
"I (list_disj fs) xs = (∃φ ∈ set fs. I φ xs)"
proof -
{ fix fs φ
have "I (foldr or fs φ) xs = (I φ xs ∨ (∃φ ∈ set fs. I φ xs))"
by (induct fs) auto
} thus ?thesis by(simp add:list_disj_def)
qed
lemma I_nnf: "I (nnf φ) xs = I φ xs"
by(induct rule:nnf.induct)(simp_all add: Ia_aneg)
lemma I_dnf:
"nqfree φ ==> (∃as∈set (dnf φ). ∀a∈set as. Ia a xs) = I φ xs"
by (induct φ) (fastsimp)+
definition "normal φ = (∀a ∈ atoms φ. anormal a)"
lemma normal_simps[simp]:
"normal TrueF"
"normal FalseF"
"normal (Atom a) <-> anormal a"
"normal (And φ1 φ2) <-> normal φ1 ∧ normal φ2"
"normal (Or φ1 φ2) <-> normal φ1 ∧ normal φ2"
"normal (Neg φ) <-> normal φ"
"normal (ExQ φ) <-> normal φ"
by(auto simp:normal_def)
lemma normal_aneg[simp]: "anormal a ==> normal (aneg a)"
by (simp add:anormal_aneg normal_def)
lemma normal_and[simp]:
"normal φ1 ==> normal φ2 ==> normal (and φ1 φ2)"
by (simp add:Logic.and_def)
lemma normal_or[simp]:
"normal φ1 ==> normal φ2 ==> normal (or φ1 φ2)"
by (simp add:Logic.or_def)
lemma normal_list_disj[simp]:
"∀φ∈set fs. normal φ ==> normal (list_disj fs)"
apply(induct fs)
apply (simp add:list_disj_def normal_simps)
apply (simp add:list_disj_def normal_simps)
done
lemma normal_nnf: "normal φ ==> normal(nnf φ)"
by(induct φ rule:nnf.induct) simp_all
lemma normal_map_fm:
"∀a. anormal(f a) = anormal(a) ==> normal (mapfm f φ) = normal φ"
by(induct φ) auto
lemma anormal_nnf:
"qfree φ ==> normal φ ==> ∀a∈atoms(nnf φ). anormal a"
apply(induct φ rule:nnf.induct)
apply(unfold normal_def)
apply(simp_all)
apply (blast dest:anormal_aneg)+
done
lemma atoms_dnf: "nqfree φ ==> as : set(dnf φ) ==> a : set as ==> a : atoms φ"
by(induct φ arbitrary: as a rule:nqfree.induct)(auto)
lemma anormal_dnf_nnf:
"as : set(dnf(nnf φ)) ==> qfree φ ==> normal φ ==> a : set as ==> anormal a"
apply(induct φ arbitrary: a as rule:nnf.induct)
apply(simp_all add: normal_def)
apply clarify
apply (metis UnE set_append)
apply metis
apply metis
apply fastsimp
apply (metis anormal_aneg atoms_dnf nqfree_aneg)
done
end
end