Theory Logic

(*  Author:     Tobias Nipkow, 2007  *)

section‹Logic›

theory Logic
imports Main "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 (atoms: 'a) fm =
  TrueF | FalseF | Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
  Neg "'a fm" | ExQ "'a fm"

notation map_fm ("mapfm")

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)"

lemmas atoms_map_fm[simp] = fm.set_map

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 (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 (mapfm f φ) = qfree φ"
by (induct φ) simp_all

lemma atoms_list_disjE:
  "a ∈ atoms(list_disj fs) ⟹ a ∈ (⋃φ ∈ set fs. atoms φ)"
apply(induct fs)
 apply (simp add:list_disj_def)
apply (auto simp add:list_disj_def Logic.or_def split:if_split_asm)
done

lemma atoms_list_conjE:
  "a ∈ atoms(list_conj fs) ⟹ a ∈ (⋃φ ∈ set fs. atoms φ)"
apply(induct fs)
 apply (simp add:list_conj_def)
apply (auto simp add:list_conj_def Logic.and_def split:if_split_asm)
done


fun dnf :: "'a fm ⇒ 'a list list" where
"dnf TrueF = [[]]" |
"dnf FalseF = []" |
"dnf (Atom φ) = [[φ]]" |
"dnf (And φ1 φ2) = [d1 @ d2. d1 ← dnf φ1, d2 ← 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 φ) (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 (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 fastforce
apply (metis anormal_aneg atoms_dnf nqfree_aneg)
done

end

end