acl2/ml/functionEncodeLib.sml

38 (*        often in the trace. First of all: why, secondly, it can be proved! *)
328 (*          A |- t is resolved against all P for |- P ==> Q in extras:       *)
332 (*          A |- t is also resolved against all other assumptions, A' |- t': *)
828     if all (curry op= residue o #residue) match1
909 (*     Applies the rewrite given as (name,thm) by encoding all of the        *)
925 (*     assumption list of all subsequent encodings and resolved at the end.  *)
1045     else (if all (fn tm => not (exists (C free_in tm) fvsr))
1054                "Could not remove all hypothesese from the theorem:\n" ^
1180     fun all [] thm = raise Empty
1181       | all (p::ps) thm =
1182     (let val x = single p thm in (BOOL_RULE x  handle _ => all ps x) end)
1183     handle _ => all ps thm;
1185     all poss finished
1565 (*     contains all the constructors for that type:                          *)
1578 (*       2. Alpha convert the clauses so that bound variables all match up   *)
1641                                         "Theorems are not all of the form: \"|- !a0 .. an. F = X\"")
1718              "Clauses must all be of the form: \"|- !a0..an. f X = Y\"")
1752     if all (all is_var o snd o strip_comb) constructors andalso
2467 (*    If a term is of the form: I M and all subterms of M are functions from *)
2474         all (curry op= target)
2477         both ((all (curry op= target o type_of) o pairSyntax.strip_pair ##
2559            orelse all (not o can dom_rng o type_of) (constructors_of t)
2569         else if all (not o can dom_rng o type_of) (constructors_of t) then
2576            all (not o can dom_rng o type_of) (constructors_of t) then ([],[])
2778                   ("Could not prove all terms in the conjunction:\n" ^
2801         if all (fn x => is_var x orelse mem x (snd (strip_comb function_term)))
3386 (*     Returns the list of all types in recursion, or nested recursion,      *)