# Theory Logic

Up to index of Isabelle/HOL/LinearQuantifierElim

theory Logic
imports FuncSet
(*  Author:     Tobias Nipkow, 2007  *)header{* Logic *}theory Logicimports Main "~~/src/HOL/Library/FuncSet"begintext{* \noindentWe start with a generic formalization of quantified logical formulaeusing 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 φ) autofun 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) autolemma 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)qedlemma 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)qedlemma qfree_map_fm: "qfree (map⇘fm⇙ f φ) = qfree φ"by (induct φ) simp_alllemma 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)donelemma 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)donefun 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_alllemma nqfree_map_fm: "nqfree (map⇘fm⇙ f φ) = nqfree φ"by (induct φ) simp_allfun "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 thegeneric formulation of theory-independent algorithms, in particularquantifier 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)"beginfun 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)qedlemma 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)qedlemma 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)donelemma normal_nnf: "normal φ ==> normal(nnf φ)"by(induct φ rule:nnf.induct) simp_alllemma normal_map_fm:  "∀a. anormal(f a) = anormal(a) ==> normal (map⇘fm⇙ f φ) = normal φ"by(induct φ) autolemma 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)+donelemma 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 fastforceapply (metis anormal_aneg atoms_dnf nqfree_aneg)doneendend`