acl2/ml/tutorial.ml

26 (* Such functions are translated using the function:                         *)
29 (* The first argument relates function constants to the names of translated  *)
32 (* The function EXP:                                                         *)
58 (* functionEncodeLib.rewrites, using the function                            *)
61 (* The function LENGTH (instantiated to operate on concrete lists of natural *)
106 (* 'listnum' is created using the function:                                  *)
108 (* function creates recognition functions, suitable for export to ACL2, for  *)
111 (* We can create a different translation using this function directly:       *)
180 (* The function 'i2n' is defined as follows:                                 *)
261 (* their entire range. In the case of SEG this is because the function       *)
263 (* function LOG this is given explicitly:                                    *)
273 (* When non-clausal functions are given (a) is not required. If the function *)
285 (*     When a recursive call is made in a clausal function the function is   *)
287 (* t, using the function call:                                               *)
305 (* The function SEG can be converted by provided theorems to state that:     *)
312 (* SEG is translated using the function:                                     *)
316 (* This acts like translate_conditional_function, except for each function   *)
319 (* These are presented as limits to the resulting function. If the theorem   *)
366 (* The LOG function is translated in a similar manner to SEG. However, as it *)
421 (* the function definition as an instantiation, so the same technique works  *)
425 (* function determining whether all elements are non-zero:                   *)
453 (* The extra theorem supplied demonstrates that the function preserves map   *)
527 (* theorems. However, they take a general function to recognise the type     *)
539 (* the function, preserves the map. In the case of SEG, this requires the    *)
602 (* be created. To do this, the following function is used:                   *)
634 (* We define the function 'FLATTEN_TREE' to convert trees to a lists, in a   *)
640 (* As this function is polymorphic, we must prove a map theorem. However,    *)
641 (* the map function was created automatically, so we must find it from the   *)
667 (* We can then translate the function as follows:                            *)
694 (* the translation of the function. Then, this term is proven termination    *)
699 (* An example of this procedure is the translation of the function word_div: *)
701 (* This function is only valid for ~(w = 0w), so we translate as a limit     *)
702 (* function. The FCP functions do not operate on mutually recursive          *)
737 (*        function itself.                                                   *)
743 (*        proved to match the HOL function.                                  *)
752 (* In the translation of word_div the recognition function, word_detect, is  *)
754 (* created by flattening the definition. As with normal types, the function  *)
795 (* When converting a recursive FCP function two tactics must also be         *)
801 (* Here, we are trying to translate the function 'addn' that adds the ith    *)
876 (* the following function call we translate 'addn' under the limit ensuring  *)