Lines Matching refs:function
16 (* derivation of function type for encode/decode et al... *)
24 (* not collected. A function should be created to log this and use it *)
26 (* 2) (Minor) When a coding function is added its form is not checked *)
146 print "The term is not an instance of function application."
1312 (* a) If the term is matched by function in !terminals then REFL term *)
1314 (* b) If the term is matched by a polytypic theorem, ie. a function *)
1333 (* The add_extended_terminal function can also determine the list of *)
1531 (* Returns a function that finds the outermost leftmost constructed term *)
1534 (* returns that function that returns the last argument from terms *)
1536 (* Fails if the theorems supplied are not function clauses, or if the *)
1537 (* the function constants found in the term and clauses are not *)
1543 (* The function supplied strips the constructor out of the term *)
1545 (* function = ``f a b c`` then *)
1547 (* Fails if no clauses are given, the function used fails or returns *)
1549 (* clauses and the function term supplied are inconsistent. *)
1553 (* Takes a list of function clauses and a list of missing clauses and *)
1557 (* indicated by the function skipped. *)
1558 (* Fails if the function given fails or the clauses are not of the *)
1564 (* constructors determined by applying the function is complete, ie. *)
1568 (* The function given should always perform 'lhs' (historical) *)
1571 (* Converts a function defined using clause structure to use case *)
1575 (* 0. Group function clauses by the leftmost outermost constructor. *)
1585 (* When grouping by constructor, a function term is instantiated to *)
1595 (* Fails if the theorem given is not a proper function (conjunction of *)
1609 (* this function will fail. *)
1638 fun outermost_constructor function clauses =
1642 val normalised = map (fn x => inst (snd (match_term (repeat rator x) (repeat rator function))) x) stripped
1644 "Theorems and function term supplied use different function constants")
1645 val lists = mapfilter (find_mismatch function) normalised
1657 raise (mkStandardExn "group_by_constructor" "No function clauses given!")
1658 | group_by_constructor function outermost clauses =
1669 ("The argument pointed to by the function given contains values " ^
1671 val replace = om (mk_eq(function,function))
1672 val fvs = ref (map (fst o dest_var) (free_vars (mk_abs(replace,function))))
1682 (t,map (fn (a,b) => (sub a function,b)) matched) handle e => wrapException "group_by_constructor" e
1697 (* subst_om substitutes ONLY the term matching the function om (f term). *)
1770 fun ctc omc function [] = (REFL function,[function])
1771 | ctc omc (function:term) (clauses:thm list) : thm * term list =
1772 case (omc function clauses)
1776 "Two or more function clauses do not differ by constructors")
1778 let val grouped = (group_by_constructor function outermost clauses)
1807 val function = list_mk_comb(left,map (fn (a,b) => (mk_var(implode (base26 a),b)))
1811 fun omc function clauses =
1813 of [] => outermost_constructor function clauses
1815 let val a = find_comb x function
1818 " cannot find a sub-term in the current function: "
1819 ^ term_to_string function))
1823 " is selecting a constructed term: " ^ term_to_string function))
1827 ctc omc function clauses
1881 (* Proves the conclusion generated by the previous function. *)
1952 ("Tactic used by this function did not fully solve the term:\n" ^ term_to_string term))
2624 (* this function calls add_standard_rewrites then returns the *)
2854 fun MK_DEFINITION tvs target limits function =
2855 let val tfunction = INST_TYPE (map (fn x => x |-> target) tvs) function
2882 fun mk_analogue_definition_term target name limits function =
2886 thm_to_string function ^ "\n")
2889 MK_DEFINITION [] target limits function
2916 fun mk_analogue_definition target name tautologies limits function =
2920 thm_to_string function ^ "\n")
2923 MK_DEFINITION [] target limits function
2942 target name map_thm tautologies limits extras function =
2946 thm_to_string function ^ "\n")
2954 ((fst o strip_comb o map_lhs) function)
2957 ("The instantiated map theorem does not match function." ^
2960 "\nwhich does not match the function constant: " ^
2961 term_to_string ((fst o strip_comb o map_lhs) function)))
2966 MK_DEFINITION type_vars target limits function
3034 (* Groups a set of mutually recursive equations by function symbol *)
3038 fun group_function_clauses function =
3042 (CONJUNCTS function)))
3141 (* The name map maps function clauses to new names *)
3142 (* Limits map function constants (from the original definition) to *)
3147 (* the abstraction must exactly match the function arguments. *)
3223 ("No name has been supplied for the function clause: " ^
3266 let fun mad t s l1 l2 function =
3268 snd o strip_forall o concl) function))
3270 mk_polymorphic_analogue_definition t s map_thm l1 l2 extras function
3271 | NONE => mk_analogue_definition t s l1 l2 function
3280 (* Loads function definitions in from the theory given. *)
3307 (* Performs encoding until one of the function terminals is reached. *)
4036 (* match the function given as inputs to the recognizer. For example: *)
4139 f target name limits extras function =
4142 limits function))
4145 RAND_CONV (ONCE_REWRITE_CONV [function]))))) term;
4146 val (tfunc,left) = dest_eq (snd (strip_forall (concl function)));
4148 val extra_theorems = calculate_extra_theorems target [(function,limits)];
4191 let val (function,missing) = clause_to_case thm
4194 f target name limits' extras function