Theory Logic

(*  Author:     Tobias Nipkow, 2007  *)

header{* Logic *}

theory Logic
imports Main "~~/src/HOL/Library/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" ("map⇘fm⇙") where
"map⇘fm⇙ h TrueF = TrueF" |
"map⇘fm⇙ h FalseF = FalseF" |
"map⇘fm⇙ h (Atom a) = Atom(h a)" |
"map⇘fm⇙ h (And φ⇣1 φ⇣2) = And (map⇘fm⇙ h φ⇣1) (map⇘fm⇙ h φ⇣2)" |
"map⇘fm⇙ h (Or φ⇣1 φ⇣2) = Or (map⇘fm⇙ h φ⇣1) (map⇘fm⇙ h φ⇣2)" |
"map⇘fm⇙ h (Neg φ) = Neg (map⇘fm⇙ h φ)" |
"map⇘fm⇙ h (ExQ φ) = ExQ (map⇘fm⇙ h φ)"

lemma atoms_map_fm[simp]: "atoms(map⇘fm⇙ f φ) = f ` atoms φ"
by(induct φ) auto

fun amap_fm :: "('a => 'b fm) => 'a fm => 'b fm" ("amap⇘fm⇙") where
"amap⇘fm⇙ h TrueF = TrueF" |
"amap⇘fm⇙ h FalseF = FalseF" |
"amap⇘fm⇙ h (Atom a) = h a" |
"amap⇘fm⇙ h (And φ⇣1 φ⇣2) = and (amap⇘fm⇙ h φ⇣1) (amap⇘fm⇙ h φ⇣2)" |
"amap⇘fm⇙ h (Or φ⇣1 φ⇣2) = or (amap⇘fm⇙ h φ⇣1) (amap⇘fm⇙ h φ⇣2)" |
"amap⇘fm⇙ h (Neg φ) = neg (amap⇘fm⇙ h φ)"

lemma amap_fm_list_disj:
  "amap⇘fm⇙ h (list_disj fs) = list_disj (map (amap⇘fm⇙ 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 (fastforce 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 (fastforce simp add:list_disj_def)
qed

lemma qfree_map_fm: "qfree (map⇘fm⇙ 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 (map⇘fm⇙ 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 I⇣a :: "'a => 'b list => bool"
assumes I⇣a_aneg: "interpret I⇣a (aneg a) xs = (¬ I⇣a a xs)"

fixes depends⇣0 :: "'a => bool"
and decr :: "'a => 'a" 
assumes not_dep_decr: "¬depends⇣0 a ==> I⇣a a (x#xs) = I⇣a (decr a) xs"
assumes anormal_decr: "¬ depends⇣0 a ==> anormal a ==> anormal(decr a)"

begin

fun atoms⇣0 :: "'a fm => 'a list" where
"atoms⇣0 TrueF = []" |
"atoms⇣0 FalseF = []" |
"atoms⇣0 (Atom a) = (if depends⇣0 a then [a] else [])" |
"atoms⇣0 (And φ⇣1 φ⇣2) = atoms⇣0 φ⇣1 @ atoms⇣0 φ⇣2" |
"atoms⇣0 (Or φ⇣1 φ⇣2) = atoms⇣0 φ⇣1 @ atoms⇣0 φ⇣2" |
"atoms⇣0 (Neg φ) = atoms⇣0 φ"

abbreviation I where "I ≡ interpret I⇣a"

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: I⇣a_aneg)

lemma I_dnf:
"nqfree φ ==> (∃as∈set (dnf φ). ∀a∈set as. I⇣a a xs) = I φ xs"
by (induct φ) (fastforce)+

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)
apply (simp add:list_disj_def)
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 (map⇘fm⇙ 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 fastforce
apply (metis anormal_aneg atoms_dnf nqfree_aneg)
done

end

end