acl2/ml/acl2encodeLib.sig

2 (* Information and trouble shooting guide for encoding to ACL2.              *)
9 (*    flatten_recognizers is used to do this.                                *)
15 (*    The two common reasons for the encoding process to fail are:           *)
51 (*    Recursive calls are characterised by the limit being applied to        *)
64 (*    Prints all definitions, up until the definition given, to a file.      *)
70 (*    is occasionally unable to prove termination / verify guards. This will *)
80 (*    Set the destructors for a given type to the theorems given.            *)
93 (*    Initialises a type so that functions over it can be translated to ACL2 *)
108 (*    This function should be used to encode types added via hol_datatype.   *)
109 (*    Failure to do so may introduce unexpected errors into the translation  *)
120 (*         a) Convert to clause form, using                                  *)
129 (*    Each function takes an associative list, mapping function constants to *)
132 (*    Lists are used throughout to support mutually recursive function       *)
143 (*        The second argument to this function is then a list of helper      *)
144 (*    theorems. For example, if a call to HD is guarded by '~(x = [])`, then *)
155 (*    NOTE: The system is designed to work with constructors given           *)
187 (*     In this case, we must also supply a fusion theorem for CONS, to the   *)
208 (*    These functions are designed to work with functions that use           *)
211 (*    The encoding process for such functions is subtly different to that    *)
213 (*    to represent the encoded function, and a function defined to match it  *)
215 (*    definitions, two tactics must be supplied. The first to prove that the *)
216 (*    definition terminates, and the second to prove the propagation theorem.*)
221 (*    is designed to act as WF_REL_TAC, except the relation is combined with *)
222 (*    encoding functions to produce a relation over s-expressions.           *)
244 (*     Creates functions to 'recognise' the type, suitable for export to     *)
245 (*     ACL2. This *must* be used before attempting to translate functions    *)
249 (*     Both functions require a 'naming' function to produce names for       *)
262 (* Tactics to assist proof of recursive FCP functions:                       *)