Structure normalForms


Source File Identifier index Theory binding index

(* ========================================================================= *)
(* HOL NORMALIZATION FUNCTIONS.                                              *)
(* Created by Joe Hurd, October 2001                                         *)
(* ========================================================================= *)

signature normalForms =
sig

include Abbrev
type ssfrag  = simpLib.ssfrag
type simpset = simpLib.simpset

(* ------------------------------------------------------------------------- *)
(* Replace genvars with variants on `v`.                                     *)
(*                                                                           *)
(* Example:                                                                  *)
(*   ?%%genvar%%20744 %%genvar%%20745 %%genvar%%20746.                       *)
(*     (%%genvar%%20744 \/ %%genvar%%20745 \/ ~%%genvar%%20746) /\           *)
(*     (%%genvar%%20746 \/ ~%%genvar%%20744) /\                              *)
(*     (%%genvar%%20746 \/ ~%%genvar%%20745) /\ (~q \/ ~%%genvar%%20745) /\  *)
(*     (r \/ ~%%genvar%%20745) /\ (%%genvar%%20745 \/ q \/ ~r) /\            *)
(*     (q \/ ~p \/ ~%%genvar%%20744) /\ (p \/ ~q \/ ~%%genvar%%20744) /\     *)
(*     (%%genvar%%20744 \/ ~p \/ ~q) /\ (%%genvar%%20744 \/ p \/ q) /\       *)
(*     %%genvar%%20746                                                       *)
(*   =                                                                       *)
(*   ?v v1 v2.                                                               *)
(*     (v \/ v1 \/ ~v2) /\ (v2 \/ ~v) /\ (v2 \/ ~v1) /\ (q \/ ~v1) /\        *)
(*     (r \/ ~v1) /\ (v1 \/ ~q \/ ~r) /\ (q \/ ~p \/ ~v) /\                  *)
(*     (p \/ ~q \/ ~v) /\ (v \/ ~p \/ ~q) /\ (v \/ p \/ q) /\ v2             *)
(* ------------------------------------------------------------------------- *)

val prettify_vars      : term -> term
val PRETTIFY_VARS_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Conversion to combinators {S,K,I}.                                        *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (?f. !y. f y = y + 1)                                                   *)
(*   =                                                                       *)
(*   $? (S (K $!) (S (S (K S) (S (K (S (K $=))) I)) (K (S $+ (K 1)))))       *)
(* ------------------------------------------------------------------------- *)

val SKI_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Conversion to combinators {S,K,I,C,o}.                                    *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (?f. !y. f y = y + 1)                                                   *)
(*   =                                                                       *)
(*   $? ($! o C (S o $o $= o I) (C $+ 1))                                    *)
(* ------------------------------------------------------------------------- *)

val SKICo_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Beta reduction and simplifying boolean rewrites.                          *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (!x y. P x \/ (P y /\ F)) ==> ?z. P z                                   *)
(*   =                                                                       *)
(*   (!x. P x) ==> ?z. P z                                                   *)
(* ------------------------------------------------------------------------- *)

val simplify_ss   : simpset             (* pure + BOOL *)
val SIMPLIFY_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Negation normal form.                                                     *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (!x. P x) ==> ((?y. Q y) = ?z. P z /\ Q z)                              *)
(*   =                                                                       *)
(*   ((?y. Q y) /\ (?z. P z /\ Q z) \/ (!y. ~Q y) /\ !z. ~P z \/ ~Q z) \/    *)
(*   ?x. ~P x                                                                *)
(* ------------------------------------------------------------------------- *)

val PURE_NNF_CONV' : conv -> conv       (* takes a 'leaf conversion' *)
val PURE_NNF_CONV  : conv
val NNF_CONV'      : conv -> conv       (* takes a 'leaf conversion' *)
val NNF_CONV       : conv

(* ------------------------------------------------------------------------- *)
(* General NNF conversion. The user supplies some conversion to be applied   *)
(* to atomic formulas.                                                       *)
(*                                                                           *)
(* "Iff"s are split conjunctively or disjunctively according to the flag     *)
(* argument (conjuctively = true) until a universal quantifier (modulo       *)
(* current parity) is passed; after that they are split conjunctively. This  *)
(* is appropriate when the result is passed to a disjunctive splitter        *)
(* followed by a clausal form inner core, such as MESON.                     *)
(*                                                                           *)
(* To avoid some duplicate computation, this function will in general        *)
(* enter a recursion where it simultaneously computes NNF representations    *)
(* for "p" and "~p", so the user needs to supply an atomic "conversion"      *)
(* that does the same.                                                       *)
(* ------------------------------------------------------------------------- *)

val GEN_NNF_CONV   : bool -> conv * (term -> thm * thm) -> conv

(* A trivial application of GEN_NNF_CONV which splits "Iff"s conjuctively.
   NOTE: The above NNF_CONV has the same behavior with NNF_CONV on "Iff"s. *)
val NNFC_CONV      : conv

(* A trivial application of GEN_NNF_CONV which splits "Iff"s disjuctively.
   NOTE: this is the HOL-Light's "NNF_CONV" (canon.ml). *)
val NNFD_CONV      : conv

(* ------------------------------------------------------------------------- *)
(* Skolemization.                                                            *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (!x. (?y. Q y \/ !z. ~P z \/ ~Q z) \/ ~P x)                             *)
(*   =                                                                       *)
(*   ?y. !x. (Q (y x) \/ !z. ~P z \/ ~Q z) \/ ~P x                           *)
(* ------------------------------------------------------------------------- *)

val SKOLEMIZE_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Prenex Normal Form.                                                       *)
(* ------------------------------------------------------------------------- *)

val PRENEX_CONV      : conv
val ANTI_PRENEX_CONV : conv

(* ------------------------------------------------------------------------- *)
(* A basic tautology prover and simplifier for clauses                       *)
(*                                                                           *)
(* Examples:                                                                 *)
(*   TAUTOLOGY_CONV:   p \/ r \/ ~p \/ ~q   =  T                             *)
(*   CONTRACT_CONV:    (p \/ r) \/ p \/ ~q  =  p \/ r \/ ~q                  *)
(* ------------------------------------------------------------------------- *)

val TAUTOLOGY_CONV : conv
val CONTRACT_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Conjunctive Normal Form.                                                  *)
(*                                                                           *)
(* Example:                                                                  *)
(*  (!x. P x ==> ?y z. Q y \/ ~?z. P z \/ Q z)                               *)
(*  =                                                                        *)
(*  ?y. (!x x'. Q (y x) \/ ~P x' \/ ~P x) /\ !x x'. Q (y x) \/ ~Q x' \/ ~P x *)
(* ------------------------------------------------------------------------- *)

val tautology_checking : bool ref
val PURE_CNF_CONV  : conv
val CNF_CONV'      : conv -> conv       (* takes a 'leaf conversion' *)
val CNF_CONV       : conv

(* ------------------------------------------------------------------------- *)
(* Disjunctive Normal Form.                                                  *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (!x. P x ==> ?y z. Q y \/ ~?z. P z \/ Q z)                              *)
(*   =                                                                       *)
(*   !x z. (?y. Q y) \/ (?y. ~P (z y) /\ ~Q (z y)) \/ ~P x                   *)
(* ------------------------------------------------------------------------- *)

val DNF_CONV'      : conv -> conv       (* takes a 'leaf conversion' *)
val DNF_CONV       : conv

(* ------------------------------------------------------------------------- *)
(* Definitional Negation Normal Form                                         *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
(*   =                                                                       *)
(*   ((p = (q = r)) = ((p = ~q) = ~r))                                       *)
(* ------------------------------------------------------------------------- *)

val DEF_NNF_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Definitional Conjunctive Normal Form                                      *)
(*                                                                           *)
(* Example:                                                                  *)
(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
(*   =                                                                       *)
(*   ?v v1 v2 v3 v4.                                                         *)
(*     (v4 \/ v1 \/ v3) /\ (v4 \/ ~v1 \/ ~v3) /\ (v1 \/ ~v3 \/ ~v4) /\       *)
(*     (v3 \/ ~v1 \/ ~v4) /\ (v3 \/ v2 \/ ~r) /\ (v3 \/ ~v2 \/ r) /\         *)
(*     (v2 \/ r \/ ~v3) /\ (~r \/ ~v2 \/ ~v3) /\ (v2 \/ p \/ ~q) /\          *)
(*     (v2 \/ ~p \/ q) /\ (p \/ q \/ ~v2) /\ (~q \/ ~p \/ ~v2) /\            *)
(*     (v1 \/ p \/ v) /\ (v1 \/ ~p \/ ~v) /\ (p \/ ~v \/ ~v1) /\             *)
(*     (v \/ ~p \/ ~v1) /\ (v \/ q \/ r) /\ (v \/ ~q \/ ~r) /\               *)
(*     (q \/ ~r \/ ~v) /\ (r \/ ~q \/ ~v) /\ v4                              *)
(* ------------------------------------------------------------------------- *)

val PURE_DEF_CNF_CONV    : conv         (* Introduces definitions *)
val CLEANUP_DEF_CNF_CONV : conv         (* Converts defns to CNF *)
val DEF_CNF_CONV         : conv         (* NNF + PURE + CLEANUP *)

val ORACLE_PURE_DEF_CNF_CONV : conv     (* Simply asserts the conversion thm *)
val ORACLE_DEF_CNF_CONV      : conv     (* NNF + ORACLE_PURE + CLEANUP *)

(* ------------------------------------------------------------------------- *)
(* Removes leading existential quantifiers from a theorem, by introducing a  *)
(* new skolem constant with an appropriate assumption.                       *)
(*                                                                           *)
(* Examples:                                                                 *)
(*   SKOLEM_CONST_RULE   ``a``   |- ?x. P x y z                              *)
(*   ---->  [a = @x. P x y z] |- P a y                                       *)
(*                                                                           *)
(*   SKOLEM_CONST_RULE   ``a y z``   |- ?x. P x y                            *)
(*   ---->  [a = \y z. @x. P x y z] |- P (a y z) y                           *)
(*                                                                           *)
(* NEW_SKOLEM_CONST generates an argument for SKOLEM_CONST_RULE, and         *)
(* NEW_SKOLEM_CONST_RULE puts the two functions together.                    *)
(* CLEANUP_SKOLEM_CONSTS_RULE tries to eliminate as many 'skolem             *)
(* assumptions' as possible.                                                 *)
(* ------------------------------------------------------------------------- *)

val SKOLEM_CONST_RULE          : term -> rule
val NEW_SKOLEM_CONST           : thm -> term
val NEW_SKOLEM_CONST_RULE      : rule
val CLEANUP_SKOLEM_CONSTS_RULE : rule

(* ------------------------------------------------------------------------- *)
(* Eliminates some lambdas to make terms "as first-order as possible".       *)
(*                                                                           *)
(* Example:  ((\x. f x z) = g z)  =  !x. f x z = g z x                       *)
(* ------------------------------------------------------------------------- *)

val DELAMB_CONV : conv

(* ------------------------------------------------------------------------- *)
(* Eliminating Hilbert's epsilon operator.                                   *)
(*                                                                           *)
(* Example:                                                                  *)
(*                                                                           *)
(*   ((?n. f n = 0) ==> (f n = 0)) ==> 3 < n                                 *)
(*   ---------------------------------------  SELECT_TAC                     *)
(*               3 < @n. f n = 0                                             *)
(* ------------------------------------------------------------------------- *)

val SELECT_TAC : tactic

(* ------------------------------------------------------------------------- *)
(* Remove all Abbrev terms from a goal by rewriting them away (Abbrev = I)   *)
(* ------------------------------------------------------------------------- *)

val REMOVE_ABBR_TAC : tactic

(* ------------------------------------------------------------------------- *)
(* Lifting conditionals through function applications.                       *)
(*                                                                           *)
(* Example:  f (if x then y else z)  =  (if x then f y else f z)             *)
(* ------------------------------------------------------------------------- *)

val cond_lift_SS : ssfrag
val cond_lift_ss : simpset      (* pure + cond_lift *)

(* ------------------------------------------------------------------------- *)
(* Converting boolean connectives to conditionals.                           *)
(*                                                                           *)
(* Example:  x /\ ~(y ==> ~z)  =  (if x then (if y then z else F) else F)    *)
(* ------------------------------------------------------------------------- *)

val condify_SS : ssfrag
val condify_ss : simpset      (* pure + condify *)

(* ------------------------------------------------------------------------- *)
(* Definitional CNF minimizing number of clauses.                            *)
(*                                                                           *)
(* Example:                                                                  *)
(* |- (p /\ q /\ r) \/ (s /\ t /\ u)                                         *)
(*    -->                                                                    *)
(* ([``d``],                                                                 *)
(*   [[.] |- (d \/ s) /\ (d \/ t) /\ (d \/ u),                               *)
(*    [.] |- (d \/ ~p \/ ~q \/ ~r) /\ (~d \/ p) /\ (~d \/ q) /\ (~d \/ r)])  *)
(*                                                                           *)
(* where the assumption [.] in both theorems is d = (p /\ q /\ r).           *)
(* ------------------------------------------------------------------------- *)

val MIN_CNF : thm list -> term list * thm list

(* ------------------------------------------------------------------------- *)
(* Some conversions ported from HOL-Light's canon.ml                         *)
(* ------------------------------------------------------------------------- *)

val CONJ_CANON_CONV  : conv
val CONDS_ELIM_CONV  : conv
val CONDS_CELIM_CONV : conv
val WEAK_DNF_CONV    : conv
val STRONG_DNF_CONV  : conv
val WEAK_CNF_CONV    : conv
val STRONG_CNF_CONV  : conv

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1