section ‹Preliminaries›
theory Preliminaries
  imports 
    Main
    HOL.Real
    "HOL-Library.FuncSet"
begin

lemma exists_subset_between: 
  assumes 
    "card A ≤ n" 
    "n ≤ card C"
    "A ⊆ C"
    "finite C"
  shows "∃B. A ⊆ B ∧ B ⊆ C ∧ card B = n" 
  using assms 
proof (induct n arbitrary: A C)
  case 0
  thus ?case using finite_subset[of A C] by (intro exI[of _ "{}"], auto)
next
  case (Suc n A C)
  show ?case
  proof (cases "A = {}")
    case True
    from obtain_subset_with_card_n[OF Suc(3)]
    obtain B where "B ⊆ C" "card B = Suc n" by metis
    thus ?thesis unfolding True by blast
  next
    case False
    then obtain a where a: "a ∈ A" by auto
    let ?A = "A - {a}" 
    let ?C = "C - {a}" 
    have 1: "card ?A ≤ n" using Suc(2-) a 
      using finite_subset by fastforce 
    have 2: "card ?C ≥ n" using Suc(2-) a by auto
    from Suc(1)[OF 1 2 _ finite_subset[OF _ Suc(5)]] Suc(2-)
    obtain B where "?A ⊆ B" "B ⊆ ?C" "card B = n" by blast
    thus ?thesis using a Suc(2-) 
      by (intro exI[of _ "insert a B"], auto intro!: card_insert_disjoint finite_subset[of B C])
  qed
qed

lemma fact_approx_add: "fact (l + n) ≤ fact l * (real l + real n) ^ n" 
proof (induct n arbitrary: l)
  case (Suc n l)
  have "fact (l + Suc n) = (real l + Suc n) * fact (l + n)" by simp
  also have "… ≤ (real l + Suc n) * (fact l * (real l + real n) ^ n)" 
    by (intro mult_left_mono[OF Suc], auto)
  also have "… = fact l * ((real l + Suc n) * (real l + real n) ^ n)" by simp
  also have "… ≤ fact l * ((real l + Suc n) * (real l + real (Suc n)) ^ n)" 
    by (rule mult_left_mono, rule mult_left_mono, rule power_mono, auto)
  finally show ?case by simp
qed simp

lemma fact_approx_minus: assumes "k ≥ n"
  shows "fact k ≤ fact (k - n) * (real k ^ n)"
proof -
  define l where "l = k - n" 
  from assms have k: "k = l + n" unfolding l_def by auto
  show ?thesis unfolding k using fact_approx_add[of l n] by simp
qed

lemma fact_approx_upper_add: assumes al: "a ≤ Suc l" shows "fact l * real a ^ n ≤ fact (l + n)" 
proof (induct n)
  case (Suc n)
  have "fact l * real a ^ (Suc n) = (fact l * real a ^ n) * real a" by simp
  also have "… ≤ fact (l + n) * real a" 
    by (rule mult_right_mono[OF Suc], auto)
  also have "… ≤ fact (l + n) * real (Suc (l + n))" 
    by (intro mult_left_mono, insert al, auto)
  also have "… = fact (Suc (l + n))" by simp
  finally show ?case by simp
qed simp

lemma fact_approx_upper_minus: assumes "n ≤ k" and "n + a ≤ Suc k" 
  shows "fact (k - n) * real a ^ n ≤ fact k" 
proof -
  define l where "l = k - n" 
  from assms have k: "k = l + n" unfolding l_def by auto
  show ?thesis using assms unfolding k 
    apply simp
    apply (rule fact_approx_upper_add, insert assms, auto simp: l_def)
    done
qed

lemma choose_mono: "n ≤ m ⟹ n choose k ≤ m choose k" 
  unfolding binomial_def
  by (rule card_mono, auto)

lemma div_mult_le: "(a div b) * c ≤ (a * c) div (b :: nat)"
  by (metis div_mult2_eq div_mult_mult2 mult.commute mult_0_right times_div_less_eq_dividend)

lemma div_mult_pow_le: "(a div b)^n ≤ a^n div (b :: nat)^n"  
proof (cases "b = 0")
  case True
  thus ?thesis by (cases n, auto)
next
  case b: False  
  then obtain c d where a: "a = b * c + d" and id: "c = a div b" "d = a mod b" by auto
  have "(a div b)^n = c^n" unfolding id by simp
  also have "… = (b * c)^n div b^n" using b
    by (metis div_power dvd_triv_left nonzero_mult_div_cancel_left)
  also have "… ≤ (b * c + d)^n div b^n" 
    by (rule div_le_mono, rule power_mono, auto)
  also have "… = a^n div b^n " unfolding a by simp
  finally show ?thesis .
qed

lemma choose_inj_right:
  assumes id: "(n choose l) = (k choose l)" 
    and n0: "n choose l ≠ 0" 
    and l0:  "l ≠ 0" 
  shows "n = k"
proof (rule ccontr)
  assume nk: "n ≠ k" 
  define m where "m = min n k" 
  define M where "M = max n k" 
  from nk have mM: "m < M" unfolding m_def M_def by auto
  let ?new = "insert (M - 1) {0..< l - 1}" 
  let ?m = "{K ∈ Pow {0..<m}. card K = l}" 
  let ?M = "{K ∈ Pow {0..<M}. card K = l}" 
  from id n0 have lM :"l ≤ M" unfolding m_def M_def by auto
  from id have id: "(m choose l) = (M choose l)" 
    unfolding m_def M_def by auto
  from this[unfolded binomial_def]
  have "card ?M < Suc (card ?m)" 
    by auto
  also have "… = card (insert ?new ?m)" 
    by (rule sym, rule card_insert_disjoint, force, insert mM, auto)
  also have "… ≤ card (insert ?new ?M)" 
    by (rule card_mono, insert mM, auto)
  also have "insert ?new ?M = ?M" 
    by (insert mM lM l0, auto)
  finally show False by simp
qed

lemma card_funcsetE: "finite A ⟹ card (A →⇩E B) = card B ^ card A" 
  by (subst card_PiE, auto)

lemma card_inj_on_subset_funcset: assumes finB: "finite B"
  and finC: "finite C" 
  and AB: "A ⊆ B" 
shows "card { f. f ∈ B →⇩E C ∧ inj_on f A} = 
  card C^(card B - card A) * prod ((-) (card C)) {0 ..< card A}"
proof -
  define D where "D = B - A" 
  from AB have B: "B = A ∪ D" and disj: "A ∩ D = {}" unfolding D_def by auto
  have sub: "card B - card A = card D" unfolding D_def using finB AB
    by (metis card_Diff_subset finite_subset)
  have "finite A" "finite D" using finB unfolding B by auto
  thus ?thesis unfolding sub unfolding B using disj
  proof (induct A rule: finite_induct)
    case empty
    from card_funcsetE[OF this(1), of C] show ?case by auto
  next
    case (insert a A)
    have "{f. f ∈ insert a A ∪ D →⇩E C ∧ inj_on f (insert a A)}
      = {f(a := c) | f c. f ∈ A ∪ D →⇩E C ∧ inj_on f A ∧ c ∈ C - f ` A}" 
      (is "?l = ?r")
    proof
      show "?r ⊆ ?l" 
        by (auto intro: inj_on_fun_updI split: if_splits) 
      {
        fix f
        assume f: "f ∈ ?l" 
        let ?g = "f(a := undefined)" 
        let ?h = "?g(a := f a)" 
        have mem: "f a ∈ C - ?g ` A" using insert(1,2,4,5) f by auto
        from f have f: "f ∈ insert a A ∪ D →⇩E C" "inj_on f (insert a A)" by auto
        hence "?g ∈ A ∪ D →⇩E C" "inj_on ?g A" using ‹a ∉ A› ‹insert a A ∩ D = {}›
          by (auto split: if_splits simp: inj_on_def)
        with mem have "?h ∈ ?r" by blast
        also have "?h = f" by auto
        finally have "f ∈ ?r" .
      }
      thus "?l ⊆ ?r" by auto
    qed
    also have "… = (λ (f, c). f (a := c)) ` 
         (Sigma {f . f ∈ A ∪ D →⇩E C ∧ inj_on f A} (λ f. C - f ` A))"
      by auto
    also have "card (...) = card (Sigma {f . f ∈ A ∪ D →⇩E C ∧ inj_on f A} (λ f. C - f ` A))" 
    proof (rule card_image, intro inj_onI, clarsimp, goal_cases) 
      case (1 f c g d)
      let ?f = "f(a := c, a := undefined)" 
      let ?g = "g(a := d, a := undefined)" 
      from 1 have id: "f(a := c) = g(a := d)" by auto
      from fun_upd_eqD[OF id] 
      have cd: "c = d" by auto
      from id have "?f = ?g" by auto
      also have "?f = f" using `f ∈ A ∪ D →⇩E C` insert(1,2,4,5) 
        by (intro ext, auto)
      also have "?g = g" using `g ∈ A ∪ D →⇩E C` insert(1,2,4,5) 
        by (intro ext, auto)
      finally show "f = g ∧ c = d" using cd by auto
    qed
    also have "… = (∑f∈{f ∈ A ∪ D →⇩E C. inj_on f A}. card (C - f ` A))" 
      by (rule card_SigmaI, rule finite_subset[of _ "A ∪ D →⇩E C"],
          insert ‹finite C› ‹finite D› ‹finite A›, auto intro!: finite_PiE)
    also have "… = (∑f∈{f ∈ A ∪ D →⇩E C. inj_on f A}. card C - card A)"
      by (rule sum.cong[OF refl], subst card_Diff_subset, insert ‹finite A›, auto simp: card_image)
    also have "… = (card C - card A) * card {f ∈ A ∪ D →⇩E C. inj_on f A}" 
      by simp
    also have "… = card C ^ card D * ((card C - card A) * prod ((-) (card C)) {0..<card A})" 
      using insert by (auto simp: ac_simps)
    also have "(card C - card A) * prod ((-) (card C)) {0..<card A} =
      prod ((-) (card C)) {0..<Suc (card A)}" by simp
    also have "Suc (card A) = card (insert a A)" using insert by auto
    finally show ?case .
  qed
qed


end

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