Theory Propositional_Proof_Systems.Formulas

section ‹Formulas›

theory Formulas
imports Main "HOL-Library.Countable"
begin

(* unrelated, but I need this in too many places. *)
notation insert (‹_ ▹ _› [56,55] 55)

datatype (atoms: 'a) formula = 
    Atom 'a
  | Bot                              (‹⊥›)  
  | Not "'a formula"                 (‹❙¬›)
  | And "'a formula" "'a formula"    (infix ‹❙∧› 68)
  | Or "'a formula" "'a formula"     (infix ‹❙∨› 68)
  | Imp "'a formula" "'a formula"    (infixr ‹❙→› 68)
(* In a standard Isabelle/jEdit config, bold can be done with C-e rightarrow.
   I learned that way too late. *)
(* I'm not sure I'm happy about the definition of what is an atom.
   I'm inclined to treat 'a as our atom type and call an Atom k an "atom formula",
   but this goes against anything the literature does. So, Atom k will be an atom,
   k its index, but there are probably a few cases where I call 'a an atom… *)
(* like here: *)
lemma atoms_finite[simp,intro!]: "finite (atoms F)" by(induction F; simp)

primrec subformulae where
"subformulae ⊥ = [⊥]" |
"subformulae (Atom k) = [Atom k]" |
"subformulae (Not F) = Not F # subformulae F" |
"subformulae (And F G) = And F G # subformulae F @ subformulae G" |
"subformulae (Imp F G) = Imp F G # subformulae F @ subformulae G" |
"subformulae (Or F G) = Or F G # subformulae F @ subformulae G"

lemma atoms_are_subformulae: "Atom ` atoms F ⊆ set (subformulae F)"
  by (induction F) auto
    
lemma subsubformulae: "G ∈ set (subformulae F) ⟹ H ∈ set (subformulae G) ⟹ H ∈ set (subformulae F)"
  by(induction F; force)
    
lemma subformula_atoms: "G ∈ set (subformulae F) ⟹ atoms G ⊆ atoms F"
  by(induction F) auto
    
lemma subformulae_self[simp,intro]: "F ∈ set (subformulae F)"
  by(induction F; simp)

lemma subformulas_in_subformulas:
  "G ❙∧ H ∈ set (subformulae F) ⟹ G ∈ set (subformulae F) ∧ H ∈ set (subformulae F)"
  "G ❙∨ H ∈ set (subformulae F) ⟹ G ∈ set (subformulae F) ∧ H ∈ set (subformulae F)"
  "G ❙→ H ∈ set (subformulae F) ⟹ G ∈ set (subformulae F) ∧ H ∈ set (subformulae F)"
  "❙¬ G ∈ set (subformulae F) ⟹ G ∈ set (subformulae F)"
  by(fastforce elim: subsubformulae)+

lemma length_subformulae: "length (subformulae F) = size F" by(induction F; simp)

subsection‹Derived Connectives›
    
definition Top (‹⊤›) where
"⊤ ≡ ⊥ ❙→ ⊥"
lemma top_atoms_simp[simp]: "atoms ⊤ = {}" unfolding Top_def by simp

primrec BigAnd :: "'a formula list ⇒ 'a formula" (‹❙⋀_›) where
"❙⋀Nil = (❙¬⊥)" ― ‹essentially, it doesn't matter what I use here. But since I want to use this in CNFs, implication is not a nice thing to have.› |
"❙⋀(F#Fs) = F ❙∧ ❙⋀Fs"

lemma atoms_BigAnd[simp]: "atoms (❙⋀Fs) = ⋃(atoms ` set Fs)"
  by(induction Fs; simp)

primrec BigOr :: "'a formula list ⇒ 'a formula" (‹❙⋁_›) where
"❙⋁Nil = ⊥" |
"❙⋁(F#Fs) = F ❙∨ ❙⋁Fs"

text‹Formulas are countable if their atoms are, and @{method countable_datatype} is really helpful with that.› 
instance formula :: (countable) countable by countable_datatype

definition "prod_unions A B ≡ case A of (a,b) ⇒ case B of (c,d) ⇒ (a ∪ c, b ∪ d)"
primrec pn_atoms where
"pn_atoms (Atom A) = ({A},{})" |
"pn_atoms Bot = ({},{})" |
"pn_atoms (Not F) = prod.swap (pn_atoms F)" |
"pn_atoms (And F G) = prod_unions (pn_atoms F) (pn_atoms G)" |
"pn_atoms (Or F G) = prod_unions (pn_atoms F) (pn_atoms G)" |
"pn_atoms (Imp F G) = prod_unions (prod.swap (pn_atoms F)) (pn_atoms G)"
lemma pn_atoms_atoms: "atoms F = fst (pn_atoms F) ∪ snd (pn_atoms F)"
  by(induction F) (auto simp add: prod_unions_def split: prod.splits)

text‹A very trivial simplifier.
Does wonders as a postprocessor for the Harrison-style Craig interpolations.›
context begin
definition "isstop F ≡ F = ❙¬⊥ ∨ F = ⊤"
fun simplify_consts where
"simplify_consts (Atom k) = Atom k" |
"simplify_consts ⊥ = ⊥" |
"simplify_consts (Not F) = (let S = simplify_consts F in case S of (Not G) ⇒ G | _ ⇒
  if isstop S then ⊥ else ❙¬ S)" |
"simplify_consts (And F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S = ⊥ then ⊥ else
  if isstop S then T ― ‹not ‹⊤›, ‹T›› else
  if T = ⊥ then ⊥ else
  if isstop T then S else
  if S = T then S else
  S ❙∧ T))" |
"simplify_consts (Or F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S = ⊥ then T else
  if isstop S then ⊤ else
  if T = ⊥ then S else
  if isstop T then ⊤ else
  if S = T then S else
  S ❙∨ T))" |
"simplify_consts (Imp F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S = ⊥ then ⊤ else
  if isstop S then T else
  if isstop T then ⊤ else
  if T = ⊥ then ❙¬ S else
  if S = T then ⊤ else
  case S of Not H ⇒ (case T of Not I ⇒ 
    I ❙→ H | _ ⇒ 
    H ❙∨ T) | _ ⇒
    S ❙→ T))"

lemma simplify_consts_size_le: "size (simplify_consts F) ≤ size F"
proof -
  have [simp]: "Suc (Suc 0) ≤ size F + size G" for F G :: "'a formula" by(cases F; cases G; simp)
  show ?thesis by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)
qed

lemma simplify_const: "atoms F = {} ⟹ isstop (simplify_consts F) ∨ (simplify_consts F) = ⊥"
  by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)
value "(size ⊤, size (❙¬⊥))" (* this is why I need isstop in this lemma and can't write simplify_consts
  in a way that this lemma can say ∈ {⊤, ⊥} *)

end
  
(*
Here's a useful little function for testing a conjecture on "a few" examples: 
*)
fun all_formulas_of_size where
"all_formulas_of_size K 0 = {⊥} ∪ Atom ` K" |
"all_formulas_of_size K (Suc n) = (
  let af = ⋃(set [all_formulas_of_size K m. m ← [0..<Suc n]]) in
  (⋃F∈af.
    (⋃G∈af. if size F + size G ≤ Suc n then {And F G, Or F G, Imp F G} else {}) 
   ∪ (if size F ≤ Suc n then {Not F} else {})) 
  ∪ af)"
(* this set obviously grows exponentially (with a base of 5 approximately).
   size 7 produces 26032 formulas, which is probably the last value
   where I can test anything meaningfully with this implementation. *)

lemma all_formulas_of_size: "F ∈ all_formulas_of_size K n ⟷ (size F ≤ Suc n ∧ atoms F ⊆ K)" (is "?l ⟷ ?r")
proof -
  have rl: "?r ⟹ ?l"
  proof(induction F arbitrary: n)
    case (Atom x)
    have *: "Atom x ∈ all_formulas_of_size K 0" using Atom by simp
    hence **: "Atom x ∈ ⋃ (all_formulas_of_size K ` set [0..<Suc m])" for m
      by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
    thus ?case using Atom by(cases n; simp)
  next
    case Bot
    have *: "Bot ∈ all_formulas_of_size K 0" by simp
    hence **: "Bot ∈ ⋃ (all_formulas_of_size K ` set [0..<Suc m])" for m
      by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
    then show ?case using Bot by(cases n; simp)
  next
    case (Not F)
    have *: "size F ≤ n" using Not by simp
    then obtain m where n[simp]: "n = Suc m" by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Not have IH: "F ∈ all_formulas_of_size K m" by simp
    then show ?case using * by(simp add: bexI[where x=F])
  next
    case (And F G)
    with And have *: "size F + size G ≤ n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F ≤ nF" "size G ≤ nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with And have IH: "F ∈ all_formulas_of_size K mF" "G ∈ all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "⋃(set [all_formulas_of_size K m. m ← [0..<Suc m]])"
    have r: "F ∈ all_formulas_of_size K mF ⟹ mF ≤ n ⟹ F ∈ ⋃(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F ∈ ?af" "G ∈ ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "F ❙∧ G ∈ (if size F + size G ≤ Suc m then {F ❙∧ G, F ❙∨ G, F ❙→ G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  next
    case (Or F G) case (Imp F G) ― ‹analogous› (*<*)
  next
    case (Or F G)
    with Or have *: "size F + size G ≤ n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F ≤ nF" "size G ≤ nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Or have IH: "F ∈ all_formulas_of_size K mF" "G ∈ all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "⋃(set [all_formulas_of_size K m. m ← [0..<Suc m]])"
    have r: "F ∈ all_formulas_of_size K mF ⟹ mF ≤ n ⟹ F ∈ ⋃(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F ∈ ?af" "G ∈ ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "Or F G ∈ (if size F + size G ≤ Suc m then {F ❙∧ G, F ❙∨ G, F ❙→ G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  next
    case (Imp F G)
    with Imp have *: "size F + size G ≤ n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F ≤ nF" "size G ≤ nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Imp have IH: "F ∈ all_formulas_of_size K mF" "G ∈ all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "⋃(set [all_formulas_of_size K m. m ← [0..<Suc m]])"
    have r: "F ∈ all_formulas_of_size K mF ⟹ mF ≤ n ⟹ F ∈ ⋃(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F ∈ ?af" "G ∈ ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "Imp F G ∈ (if size F + size G ≤ Suc m then {F ❙∧ G, F ❙∨ G, F ❙→ G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  (*>*)
  qed
  have lr: ?r if l: ?l 
  proof
    have *: "F ∈ all_formulas_of_size K x ⟹ F ∈ all_formulas_of_size K (x + n)" for x n
      by(induction n; simp)
    show "size F ≤ Suc n" using l
      by(induction n; auto split: if_splits) (metis "*" le_SucI le_eq_less_or_eq le_iff_add)
    show "atoms F ⊆ K" using l
      proof(induction n arbitrary: F rule: less_induct)
        case (less x)
        then show ?case proof(cases x)
          case 0 with less show ?thesis by force
        next
          case (Suc y) with less show ?thesis 
            by(simp only: all_formulas_of_size.simps Let_def) (fastforce simp add: less_Suc_eq split: if_splits)
        qed
      qed
  qed
  from lr rl show ?thesis proof qed
qed
(* At first I thought: why would I prove anything about all_formulas_of_size, I only want to test a conjecture with it.
   Guess why: it was broken.
   Granted, I spent too much time on this. *)

end