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