# Theory Monotone_Formula

```section ‹Monotone Formulas›

text ‹We define monotone formulas, i.e., without negation,
and show that usually the constant TRUE is not required.›

theory Monotone_Formula
imports Main
begin

subsection ‹Definition›

datatype 'a mformula =
TRUE | FALSE |            ― ‹True and False›
Var 'a |                  ― ‹propositional variables›
Conj "'a mformula" "'a mformula" |  ― ‹conjunction›
Disj "'a mformula" "'a mformula"    ― ‹disjunction›

text ‹the set of subformulas of a mformula›

fun SUB :: "'a mformula ⇒ 'a mformula set" where
"SUB (Conj φ ψ) = {Conj φ ψ} ∪ SUB φ ∪ SUB ψ"
| "SUB (Disj φ ψ) = {Disj φ ψ} ∪ SUB φ ∪ SUB ψ"
| "SUB (Var x) = {Var x}"
| "SUB FALSE = {FALSE}"
| "SUB TRUE = {TRUE}"

text ‹the variables of a mformula›

fun vars :: "'a mformula ⇒ 'a set" where
"vars (Var x) = {x}"
| "vars (Conj φ ψ) = vars φ ∪ vars ψ"
| "vars (Disj φ ψ) = vars φ ∪ vars ψ"
| "vars FALSE = {}"
| "vars TRUE = {}"

lemma finite_SUB[simp, intro]: "finite (SUB φ)"
by (induct φ, auto)

text ‹The circuit-size of a mformula: number of subformulas›

definition cs :: "'a mformula ⇒ nat" where
"cs φ = card (SUB φ)"

text ‹variable assignments›

type_synonym 'a VAS = "'a ⇒ bool"

text ‹evaluation of mformulas›

fun eval :: "'a VAS ⇒ 'a mformula ⇒ bool" where
"eval θ FALSE = False"
| "eval θ TRUE = True"
| "eval θ (Var x) = θ x"
| "eval θ (Disj φ ψ) = (eval θ φ ∨ eval θ ψ)"
| "eval θ (Conj φ ψ) = (eval θ φ ∧ eval θ ψ)"

lemma eval_vars: assumes "⋀ x. x ∈ vars φ ⟹ θ1 x = θ2 x"
shows "eval θ1 φ = eval θ2 φ"
using assms by (induct φ, auto)

subsection ‹Conversion of mformulas to true-free mformulas›

inductive_set tf_mformula :: "'a mformula set" where
tf_False: "FALSE ∈ tf_mformula"
| tf_Var: "Var x ∈ tf_mformula"
| tf_Disj: "φ ∈ tf_mformula ⟹ ψ ∈ tf_mformula ⟹ Disj φ ψ ∈ tf_mformula"
| tf_Conj: "φ ∈ tf_mformula ⟹ ψ ∈ tf_mformula ⟹ Conj φ ψ ∈ tf_mformula"

fun to_tf_formula where
"to_tf_formula (Disj phi psi) = (let phi' = to_tf_formula phi; psi' = to_tf_formula psi
in (if phi' = TRUE ∨ psi' = TRUE then TRUE else Disj phi' psi'))"
| "to_tf_formula (Conj phi psi) = (let phi' = to_tf_formula phi; psi' = to_tf_formula psi
in (if phi' = TRUE then psi' else if psi' = TRUE then phi' else Conj phi' psi'))"
| "to_tf_formula phi = phi"

lemma eval_to_tf_formula: "eval θ (to_tf_formula φ) = eval θ φ"
by (induct φ rule: to_tf_formula.induct, auto simp: Let_def)

lemma to_tf_formula: "to_tf_formula φ ≠ TRUE ⟹ to_tf_formula φ ∈ tf_mformula"
by (induct φ, auto simp: Let_def intro: tf_mformula.intros)

lemma vars_to_tf_formula: "vars (to_tf_formula φ) ⊆ vars φ"
by (induct φ rule: to_tf_formula.induct, auto simp: Let_def)

lemma SUB_to_tf_formula: "SUB (to_tf_formula φ) ⊆ to_tf_formula ` SUB φ"
by (induct φ rule: to_tf_formula.induct, auto simp: Let_def)

lemma cs_to_tf_formula: "cs (to_tf_formula φ) ≤ cs φ"
proof -
have "cs (to_tf_formula φ) ≤ card (to_tf_formula ` SUB φ)"
unfolding cs_def by (rule card_mono[OF finite_imageI[OF finite_SUB] SUB_to_tf_formula])
also have "… ≤ cs φ" unfolding cs_def
by (rule card_image_le[OF finite_SUB])
finally show "cs (to_tf_formula φ) ≤ cs φ" .
qed

lemma to_tf_mformula: assumes "¬ eval θ φ"
shows "∃ ψ ∈ tf_mformula. (∀ θ. eval θ φ = eval θ ψ) ∧ vars ψ ⊆ vars φ ∧ cs ψ ≤ cs φ"
proof (intro bexI[of _ "to_tf_formula φ"] conjI allI eval_to_tf_formula[symmetric] vars_to_tf_formula to_tf_formula)
from assms have "¬ eval θ (to_tf_formula φ)" by (simp add: eval_to_tf_formula)
thus "to_tf_formula φ ≠ TRUE" by auto
show "cs (to_tf_formula φ) ≤ cs φ" by (rule cs_to_tf_formula)
qed

end```