acl2/ml/polytypicLib.sml

205 (*    Recognisers for different terms, 'is_conjunction_of' and               *)
387 (*    Like UNBETA_CONV but operates on a list of terms                       *)
878 (*     Returns true if the term is a conjunction of terms of the form:       *)
886 (*     Returns true if the term is a conjunction of terms of the form:       *)
891 (*     also returns true if terms are singly constructed, eg:                *)
1727         (* Extra terms for inclusion from single constructed terms, ie: !x. P0 x ==> P1 x *)
1746                 val terms = strip_conj ante
1750                                 DISCH_ALL (ASSUME t)) terms
1759         (* Finds all terms in the clause such that there is a function call:          *)
1792                                 ("Extra terms cannot be resolved, no theorem in the set:\n  " ^
2286                 (size_err "result of theorem is not a conjunction of a < b terms")
2288                 (size_err "left of < terms are not measures '(size x)'")
2290                 (size_err "right of < terms are not measures '(size x)'")
2734 (*     Given a list mapping function terms to types and a theorem            *)
2735 (*     prove_all_split_terms removes all split terms from the hypothese      *)
2739 (*     Given a pair function, the list of proved split terms and a the       *)
2859         val terms = map (mk_term o fst) recursive_types handle e => wrap e
2863         val term = list_mk_conj (flatten (map strip_conj terms)) handle e => wrap e
3060         let     val terms = find_terms (fn t => (exists (curry op= (rator t) o snd o snd) equivs handle _ => false))
3064                         (first (curry op= (rator t) o snd o snd) equivs)) terms
3085         val terms = (strip_conj o fst o dest_imp_only o concl) inst handle e => wrap e
3100                 if can (tryfind (dest_neg o fst o dest_imp_only o snd o strip_forall)) terms
3124                         (MATCH_IND_TERM t) (final_assums @ extra_assums)) terms)))
3171         val terms = filter is_imp_only (hyp thm)
3178                                 andalso (can dom_rng o type_of o lhs o snd o strip_forall) x))] term) terms
3181           | do_all matches terms =
3182         let     val (found,notfound) = mappartition (fn t => (get_type t matches,t)) terms
3184                 val _ = type_trace 1 (int_to_string (length terms) ^ "-")
3193                 if null terms then [] else
3194                 (type_trace 1 "Proving uniqueness terms: " ;
3195                  do_all matches terms
3199                                  xlist_to_string term_to_string terms ^
3259                         ("The terms: " ^ xlist_to_string (term_to_string o concl) kept ^
3260                          " do not match terms in the hypothesis set"))