acl2/ml/functionEncodeLib.sml

195 val err1 = "some terms in the conclusion and second antecedent\n are not encoded terms"
237                 val terms = find_terms (fn x => (curry op= a' o rator) x handle _ => false) (concl thm')
241                         (PURE_REWRITE_CONV (map (fn t => ISPEC (rand t) I_THM) terms))))) (ISPEC t thm)
273     val terms = terms1;
276     val vars = map (mk_varv o implode o base26 o fst) (enumerate 0 terms)
278     val assums = mapfilter (ASSUME o mk_eq) (zip terms vars)
319 (*      of partial_resolve, the flag indicates whether terms in P can be     *)
470 (*     A list of terms is provided, and instantiated in the same manner as P *)
980 (*     any higher-order terms. Eg.:                                          *)
1082                      " the following terms have been added:\n" ^
1188 let val (terms,disjs) = (map strip_conj ## strip_disj) (strip_imp_only conj)
1193                          (map ASSUME (flatten terms) @ RR)) (sortf disjs)
1197        if dest_neg (concl solved) = conj andalso null (flatten terms)
1201                                     (flatten terms))] THENC
1205                     REWRITE_CONV []) (list_mk_disj disjs))) terms
1292     val terms = strip_conj (fst (dest_imp_only (concl thm)))
1296     val thms = map (fn x => backchain_rewrite 0 RR x before trace 3 "\n") terms
1534 (*         returns that function that returns the last argument from terms   *)
1660         val terms = map (fn y => (repeat rator (om (concl y)),y)) clauses
1661         val t = snd (strip_fun (type_of (fst (hd terms))))
1664                         ("Function to find constructed terms returned a term with a non-compound type: " ^
1666         val matched = map (fn c => (c,map snd (filter (same_const c o fst) terms))) cs
1670                                  "which are not constructed terms: " ^ xlist_to_string (term_to_string o fst) terms))
1894 let     val terms = map (length o strip_pair) (fst (strip_pabs tm))
1896         val names = for 0 (foldl op+ 0 terms) (String.implode o base26)
1897         val types = for 0 (foldl op+ 0 terms)
1900         val pairs = map list_mk_pair (compn terms vars) handle e => wrap e
2042     val terms = hyp negated
2044     map (C fix_term negated) terms
2502 (* decoded terms:                                                            *)
2778                   ("Could not prove all terms in the conjunction:\n" ^
3138 (*                              [limit terms]                                *)
3218     val terms = map (fst o strip_comb o lhs o snd o strip_imp o
3221     val name_list = map (Option.valOf o assoc name_map) terms
3226                                      terms)))
3227     val limit_list = map ((fn NONE => [] | SOME y => y) o assoc limits) terms
3308 (*     Returns the encoded term, along with a list of terminal terms for     *)
3639         val (terms,r) = encode_until_recursive [f o rand] ([],general_detects)
3641     in  (map snd (hd terms),RIGHT_CONV_RULE (ALLOW_CONV (REWR_CONV r)) thm)
3659 (*     Given terms L and R, proves a goal of the form:                       *)
3690 (*     Used to relate terms:                                                 *)
3819 fun mk_nested_rel terms =
3821                                         make_all_terms terms))
3980 (*     Attempts to define a list of terms as functions using the tactic      *)
4000 fun define_with_tactic is_single conv tactic terms =
4001 let val (singles,not_singles) = partition is_single terms
4028                (sdefs @ ultimate)) terms,induction)
4035 (*    Flattens the recognizers for the type given, abstracting terms that    *)
4042     val (props,thms,terms) = create_abstract_recognizers fname f target t
4045     val funcs = map lhs terms
4049                               WF_RECOGNIZER_TAC terms
4088 fun ENCODE_BOOL_UNTIL_CONV target terms term =
4091     val limits = map (fn t => can (match_term t) o rand) terms