list_FOLD_CONV : thm -> conv -> conv

- STRUCTURE
- SYNOPSIS
- Computes by inference the result of applying a function to the elements of a list.
- DESCRIPTION
- Evaluating list_FOLD_CONV fthm conv tm returns a theoremThe first argument fthm should be a theorem of the form
|- CONST x0' ... xi' ... xn' = tm'

where FOLD[LR] means either FOLDL or FOLDR. The last argument tm is a term of the following form:|- !x0 ... xi ... xn. CONST x0 ... xi ... xn = FOLD[LR] f e xi

where xi' is a concrete list. list_FOLD_CONV first instantiates the input theorem using tm. It then calls either FOLDL_CONV or FOLDR_CONV with the user supplied conversion conv on the right-hand side.CONST x0' ... xi' ... xn'

- FAILURE
- list_FOLD_CONV fthm conv tm fails if fthm or tm is not of the form described above, or if they do not agree, or the call to FOLDL_CONV OR FOLDR_CONV fails.
- USES
- This function is used to implement conversions for logical constants which can be expressed in terms of the fold operators. For example, the constant SUM can be expressed in terms of FOLDR as in the following theorem:The conversion for SUM, SUM_CONV can be implemented as
|- !l. SUM l = FOLDR $+ 0 l

Then, evaluating SUM_CONV “SUM [0;1;2;3]” will return the following theorem:load_library_in_place num_lib; val SUM_CONV = list_FOLD_CONV (theorem "list" "SUM_FOLDR") Num_lib.ADD_CONV;

|- SUM [0;1;2;3] = 6

- SEEALSO

HOL Kananaskis-14