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