(******************************************************************************)
(* FILE          : clausal_form.ml                                            *)
(* DESCRIPTION   : Functions for putting a formula into clausal form.         *)
(*                                                                            *)
(* READS FILES   : <none>                                                     *)
(* WRITES FILES  : <none>                                                     *)
(*                                                                            *)
(* AUTHOR        : R.J.Boulton                                                *)
(* DATE          : 13th May 1991                                              *)
(*                                                                            *)
(* LAST MODIFIED : R.J.Boulton                                                *)
(* DATE          : 12th October 1992                                          *)
(*                                                                            *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
(* DATE          : 2008                                                       *)
(******************************************************************************)

let IMP_DISJ_THM = TAUT `!t1 t2. t1 ==> t2 <=> ~t1 \/ t2`;;
let RIGHT_OR_OVER_AND = TAUT `!t1 t2 t3. t2 /\ t3 \/ t1 <=> (t2 \/ t1) /\ (t3 \/ t1)`;;
let LEFT_OR_OVER_AND = TAUT `!t1 t2 t3. t1 \/ t2 /\ t3 <=> (t1 \/ t2) /\ (t1 \/ t3)`;;

(*============================================================================*)
(* Theorems for normalizing Boolean terms                                     *)
(*============================================================================*)

(*----------------------------------------------------------------------------*)
(* EQ_EXPAND = |- (x = y) = ((~x \/ y) /\ (~y \/ x))                          *)
(*----------------------------------------------------------------------------*)

let EQ_EXPAND = 
prove
  (`(x = y) = ((~x \/ y) /\ (~y \/ x))`,

   BOOL_CASES_TAC `x:bool` THEN
   BOOL_CASES_TAC `y:bool` THEN
   REWRITE_TAC []);;
(*----------------------------------------------------------------------------*)
(* IMP_EXPAND = |- (x ==> y) = (~x \/ y)                                      *)
(*----------------------------------------------------------------------------*)

let IMP_EXPAND = SPEC `y:bool` (SPEC `x:bool` IMP_DISJ_THM);;

(*----------------------------------------------------------------------------*)
(* COND_EXPAND = |- (x => y | z) = ((~x \/ y) /\ (x \/ z))                    *)
(*----------------------------------------------------------------------------*)

let COND_EXPAND = 
prove
  (`(if x then y else z) = ((~x \/ y) /\ (x \/ z))`,

   BOOL_CASES_TAC `x:bool` THEN
   BOOL_CASES_TAC `y:bool` THEN
   BOOL_CASES_TAC `z:bool` THEN
   REWRITE_TAC []);;
(*----------------------------------------------------------------------------*)
(* NOT_NOT_NORM = |- ~~x = x                                                  *)
(*----------------------------------------------------------------------------*)

let NOT_NOT_NORM = SPEC `x:bool` (CONJUNCT1 NOT_CLAUSES);;

(*----------------------------------------------------------------------------*)
(* NOT_CONJ_NORM = |- ~(x /\ y) = (~x \/ ~y)                                  *)
(*----------------------------------------------------------------------------*)

let NOT_CONJ_NORM = CONJUNCT1 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;

(*----------------------------------------------------------------------------*)
(* NOT_DISJ_NORM = |- ~(x \/ y) = (~x /\ ~y)                                  *)
(*----------------------------------------------------------------------------*)

let NOT_DISJ_NORM = CONJUNCT2 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;

(*----------------------------------------------------------------------------*)
(* LEFT_DIST_NORM = |- x \/ (y /\ z) = (x \/ y) /\ (x \/ z)                   *)
(*----------------------------------------------------------------------------*)

let LEFT_DIST_NORM =
 SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` LEFT_OR_OVER_AND));;

(*----------------------------------------------------------------------------*)
(* RIGHT_DIST_NORM = |- (x /\ y) \/ z = (x \/ z) /\ (y \/ z)                  *)
(*----------------------------------------------------------------------------*)

let RIGHT_DIST_NORM =
 SPEC `y:bool` (SPEC `x:bool` (SPEC `z:bool` RIGHT_OR_OVER_AND));;

(*----------------------------------------------------------------------------*)
(* CONJ_ASSOC_NORM = |- (x /\ y) /\ z = x /\ (y /\ z)                         *)
(*----------------------------------------------------------------------------*)

let CONJ_ASSOC_NORM =
 SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` CONJ_ASSOC)));;

(*----------------------------------------------------------------------------*)
(* DISJ_ASSOC_NORM = |- (x \/ y) \/ z = x \/ (y \/ z)                         *)
(*----------------------------------------------------------------------------*)

let DISJ_ASSOC_NORM =
 SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` DISJ_ASSOC)));;

(*============================================================================*)
(* Conversions for rewriting Boolean terms                                    *)
(*============================================================================*)

let COND_EXPAND_CONV = REWR_CONV COND_EXPAND;;
let CONJ_ASSOC_NORM_CONV = REWR_CONV CONJ_ASSOC_NORM;;
let DISJ_ASSOC_NORM_CONV = REWR_CONV DISJ_ASSOC_NORM;;
let EQ_EXPAND_CONV = REWR_CONV EQ_EXPAND;;
let IMP_EXPAND_CONV = REWR_CONV IMP_EXPAND;;
let LEFT_DIST_NORM_CONV = REWR_CONV LEFT_DIST_NORM;;
let NOT_CONJ_NORM_CONV = REWR_CONV NOT_CONJ_NORM;;
let NOT_DISJ_NORM_CONV = REWR_CONV NOT_DISJ_NORM;;
let NOT_NOT_NORM_CONV = REWR_CONV NOT_NOT_NORM;;
let RIGHT_DIST_NORM_CONV = REWR_CONV RIGHT_DIST_NORM;;

(*----------------------------------------------------------------------------*)
(* NOT_CONV : conv                                                            *)
(*                                                                            *)
(*    |- !t. ~~t = t                                                          *)
(*    |- ~T = F                                                               *)
(*    |- ~F = T                                                               *)
(*----------------------------------------------------------------------------*)

let NOT_CONV =
try (
 let [th1;th2;th3] = CONJUNCTS NOT_CLAUSES
 in fun tm ->
 (let arg = dest_neg tm
  in  if (is_T arg) then th2
      else if (is_F arg) then th3
      else SPEC (dest_neg arg) th1
 )
) with Failure _ -> failwith "NOT_CONV";;

(*----------------------------------------------------------------------------*)
(* AND_CONV : conv                                                            *)
(*                                                                            *)
(*    |- T /\ t = t                                                           *)
(*    |- t /\ T = t                                                           *)
(*    |- F /\ t = F                                                           *)
(*    |- t /\ F = F                                                           *)
(*    |- t /\ t = t                                                           *)
(*----------------------------------------------------------------------------*)

let AND_CONV =
try (
 let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES))
 in fun tm ->
 (let (arg1,arg2) = dest_conj tm
  in  if (is_T arg1) then SPEC arg2 th1
      else if (is_T arg2) then SPEC arg1 th2
      else if (is_F arg1) then SPEC arg2 th3
      else if (is_F arg2) then SPEC arg1 th4
      else if (arg1 = arg2) then SPEC arg1 th5
      else failwith ""
  )
 ) with Failure _ -> failwith "AND_CONV" ;;

(*----------------------------------------------------------------------------*)
(* OR_CONV : conv                                                             *)
(*                                                                            *)
(*    |- T \/ t = T                                                           *)
(*    |- t \/ T = T                                                           *)
(*    |- F \/ t = t                                                           *)
(*    |- t \/ F = t                                                           *)
(*    |- t \/ t = t                                                           *)
(*----------------------------------------------------------------------------*)

let OR_CONV =
try (
 let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
 in fun tm ->
 (let (arg1,arg2) = dest_disj tm
  in  if (is_T arg1) then SPEC arg2 th1
      else if (is_T arg2) then SPEC arg1 th2
      else if (is_F arg1) then SPEC arg2 th3
      else if (is_F arg2) then SPEC arg1 th4
      else if (arg1 = arg2) then SPEC arg1 th5
      else failwith ""
 )
) with Failure _ -> failwith "OR_CONV";;

(*============================================================================*)
(* Conversions for obtaining `clausal' form                                   *)
(*============================================================================*)

(*----------------------------------------------------------------------------*)
(* EQ_IMP_COND_ELIM_CONV : (term -> bool) -> conv                             *)
(*                                                                            *)
(* Eliminates Boolean equalities, Boolean conditionals, and implications from *)
(* terms consisting of =,==>,COND,/\,\/,~ and atoms. The atoms are specified  *)
(* by the predicate that the conversion takes as its first argument.          *)
(*----------------------------------------------------------------------------*)

let rec EQ_IMP_COND_ELIM_CONV is_atom tm =
try
 (if (is_atom tm) then ALL_CONV tm
  else if (is_neg tm) then (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) tm
  else if (is_eq tm) then
     ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
      (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
      EQ_EXPAND_CONV) tm
  else if (is_imp tm) then
     ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
      (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
      IMP_EXPAND_CONV) tm
  else if (is_cond tm) then
     ((RATOR_CONV
        (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)))) THENC
      (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
      (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
      COND_EXPAND_CONV) tm
  else ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
        (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) tm
 ) with Failure _ -> failwith "EQ_IMP_COND_ELIM_CONV";;

(*----------------------------------------------------------------------------*)
(* MOVE_NOT_DOWN_CONV : (term -> bool) -> conv -> conv                        *)
(*                                                                            *)
(* Moves negations down through a term consisting of /\,\/,~ and atoms. The   *)
(* atoms are specified by a predicate (first argument). When a negation has   *)
(* reached an atom, the conversion `conv' (second argument) is applied to the *)
(* negation of the atom. `conv' is also applied to any non-negated atoms      *)
(* encountered. T and F are eliminated.                                       *)
(*----------------------------------------------------------------------------*)

let rec MOVE_NOT_DOWN_CONV is_atom conv tm =
try
 (if (is_atom tm) then (conv tm)
  else if (is_neg tm)
  then ((let tm' = rand tm
         in  if (is_atom tm') then ((conv THENC (TRY_CONV NOT_CONV)) tm)
             else if (is_neg tm') then (NOT_NOT_NORM_CONV THENC
                                   (MOVE_NOT_DOWN_CONV is_atom conv)) tm
             else if (is_conj tm') then
                (NOT_CONJ_NORM_CONV THENC
                 (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
                                                                          THENC
                 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
                 (TRY_CONV AND_CONV)) tm
             else if (is_disj tm') then
                (NOT_DISJ_NORM_CONV THENC
                 (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
                                                                          THENC
                 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
                 (TRY_CONV OR_CONV)) tm
             else failwith ""))
  else if (is_conj tm) then
     ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
      (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
      (TRY_CONV AND_CONV)) tm
  else if (is_disj tm) then
     ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
      (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
      (TRY_CONV OR_CONV)) tm
  else failwith ""
 ) with Failure _ -> failwith "MOVE_NOT_DOWN_CONV";;

(*----------------------------------------------------------------------------*)
(* CONJ_LINEAR_CONV : conv                                                    *)
(*                                                                            *)
(* Linearizes conjuncts using the following conversion applied recursively:   *)
(*                                                                            *)
(*    "(x /\ y) /\ z"                                                         *)
(*    ================================                                        *)
(*    |- (x /\ y) /\ z = x /\ (y /\ z)                                        *)
(*----------------------------------------------------------------------------*)

let rec CONJ_LINEAR_CONV tm =
try
 (if ((is_conj tm) & (is_conj (rand (rator tm))))
  then (CONJ_ASSOC_NORM_CONV THENC
        (RAND_CONV (TRY_CONV CONJ_LINEAR_CONV)) THENC
        (TRY_CONV CONJ_LINEAR_CONV)) tm
  else failwith ""
 ) with Failure _ -> failwith "CONJ_LINEAR_CONV";;

(*----------------------------------------------------------------------------*)
(* CONJ_NORM_FORM_CONV : conv                                                 *)
(*                                                                            *)
(* Puts a term involving /\ and \/ into conjunctive normal form. Anything     *)
(* other than /\ and \/ is taken to be an atom and is not processed.          *)
(*                                                                            *)
(* The conjunction returned is linear, i.e. the conjunctions are associated   *)
(* to the right. Each conjunct is a linear disjunction.                       *)
(*----------------------------------------------------------------------------*)

let rec CONJ_NORM_FORM_CONV tm =
try
 (if (is_disj tm) then
     (if (is_conj (rand (rator tm))) then
         ((RATOR_CONV
              (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
                          (RAND_CONV CONJ_NORM_FORM_CONV)))) THENC
          (RAND_CONV CONJ_NORM_FORM_CONV) THENC
          RIGHT_DIST_NORM_CONV THENC
          (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
          (RAND_CONV CONJ_NORM_FORM_CONV) THENC
          (TRY_CONV CONJ_LINEAR_CONV)) tm
      else if (is_conj (rand tm)) then
         ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
          (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
                      (RAND_CONV CONJ_NORM_FORM_CONV))) THENC
          LEFT_DIST_NORM_CONV THENC
          (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
          (RAND_CONV CONJ_NORM_FORM_CONV) THENC
          (TRY_CONV CONJ_LINEAR_CONV)) tm
      else if (is_disj (rand (rator tm))) then
         (DISJ_ASSOC_NORM_CONV THENC CONJ_NORM_FORM_CONV) tm
      else (let th = RAND_CONV CONJ_NORM_FORM_CONV tm
            in  let tm' = rhs (concl th)
            in  if (is_conj (rand tm'))
                then (TRANS th (CONJ_NORM_FORM_CONV tm'))
                else th))
  else if (is_conj tm) then
     ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
      (RAND_CONV CONJ_NORM_FORM_CONV) THENC
      (TRY_CONV CONJ_LINEAR_CONV)) tm
  else ALL_CONV tm
 ) with Failure _ -> failwith "CONJ_NORM_FORM_CONV";;

(*----------------------------------------------------------------------------*)
(* has_boolean_args_and_result : term -> bool                                 *)
(*                                                                            *)
(* Yields true if and only if the term is of type ":bool", and if it is a     *)
(* function application, all the arguments are of type ":bool".               *)
(*----------------------------------------------------------------------------*)

let has_boolean_args_and_result tm =
try
 (let args = snd (strip_comb tm)
  in  let types = (type_of tm)::(map type_of args)
  in  (subtract (setify types) [`:bool`]) = [] )
 with Failure _ -> (type_of tm = `:bool`);;

(*----------------------------------------------------------------------------*)
(* CLAUSAL_FORM_CONV : conv                                                   *)
(*                                                                            *)
(* Puts into clausal form terms consisting of =,==>,COND,/\,\/,~ and atoms.   *)
(*----------------------------------------------------------------------------*)

let CLAUSAL_FORM_CONV tm =
try (
 let is_atom tm =
    (not (has_boolean_args_and_result tm)) or (is_var tm) or (is_const tm)
 in
 ((EQ_IMP_COND_ELIM_CONV is_atom) THENC
  (MOVE_NOT_DOWN_CONV is_atom ALL_CONV) THENC
  CONJ_NORM_FORM_CONV) tm
 ) with Failure _ -> failwith "CLAUSAL_FORM_CONV";;