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
  (Faf.
    (Gaf. 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