acl2/ml/polytypicLib.sml

1100         val func =  snd (EQ_IMP_RULE (STRIP_QUANT_CONV (RAND_CONV (REWR_CONV pair_def))
1106                                         (UNDISCH_ONLY func) handle e => wrapd e)
1107                         else FUN_EQ_RULE (UNDISCH_ONLY func handle e => wrapd e)
1109         (repeat rator new_term :: fvs,(GSYM rewrite,fst (dest_imp_only (concl func)))) handle e => wrapd e
1274         fun find_names_of X (func,def) =
1275         let     val var = rand func
1354 fun FTERM_CONV func_types func var term =
1360         if mem (type_of term) (map snd func_types) andalso can (match_term func) tm then
1439 fun instantiate_clause term_subst ((n,(func,body)),(thm,mthm)) =
1457                                 (term_to_string (mk_eq (func,body))),
1458                          (not o free_in (rand func) o repeat rator o rhs o concl))] term_rec_thm
1466                         STRIP_QUANT_CONV (FORK_CONV (UNBETA_LIST_CONV (snd (strip_comb func)),
1489                 unzip (map2 (fn tc => fn (func,body) =>
1490                         let     val args = with_exn (snd o strip_comb o rator) func exn1
1493                                 (res_t |-> list_mk_fun(map type_of args,type_of func),args)
1505                 map2 (fn tc => fn (func,body) =>
1508                                 (repeat rator func |-> list_mk_abs(tl args,(mk_abs(hd args,lhs (concl tc))))) end)
2839 fun wrap_conv source func conv term =
2855 fun mk_eq_thm func mk_term get_def get_func conv t =
2856 let     fun wrap e = wrapException ("mk_split_" ^ func ^ "_function (mk_eq_thm)") e
3291         fun find_type func =
3292                 case (assoc1 func alist)
3293                 of NONE => if can (match_term pt) func
3294                                 then list_mk_prod(mapfilter find_type (snd (strip_comb func)))
3296                                                 ("Could not find type for function: " ^ term_to_string func))
3380 fun check_defs func get_def t =
3384         (raise (mkStandardExn func
3615                                 of ([],func) => foldl (uncurry PROVE_HYP) (func []) (map ASSUME assums)
3616                                 |  (x::xs,func) => raise (clause_err ""))
3724                                 of ([],func) => func []
3725                                 |  (x::xs,func) =>
3731                                 of ([],func) => func []
3732                                 |  (x::xs,func) =>