Lines Matching defs:missing
1553 (* Takes a list of function clauses and a list of missing clauses and *)
1555 (* -- The list of missing clauses is simply concatenated, the clauses *)
1563 (* Takes a list of missing clauses and determines whether the set of *)
1572 (* Returns a list of missing clauses *)
1592 (* (this case is missing from the definition) the algorithm returns the *)
1593 (* reflection of this clause and adds it to the list of missing calls. *)
1710 | alpha_match_clauses outermost [(thm,missing)] = (missing,[SPEC_ALL thm])
1743 fun condense_missing outermost missing =
1744 let val constructors = map (fn x => outermost (mk_eq (x,x))) missing
1748 of [] => missing
1759 (free_varsl missing)),x)
1760 val _ = trace 1 ("M:[" ^ int_to_string (length missing) ^ "]")
1761 in [subst (map (fn c => c |-> var) constructors) (hd missing)]
1763 else missing)
1781 val (missing,next_thm) = alpha_match_clauses outermost split_clauses
1783 val missing' = condense_missing outermost missing
1793 (HO_MATCH_MP rule thm,missing')
2993 (* Converts a missing clause to a limit *)
2999 fun clause_to_limit missing =
3000 let val (fconst,constructors) = strip_comb missing
3012 ("Missing clause: " ^ term_to_string missing ^
3020 (* Calculates the nested theorems required for a missing clause limit: *)
3228 val rlist = map2 (fn (name,limit) => fn (thm,missing) =>
4191 let val (function,missing) = clause_to_case thm
4192 val limits' = map clause_to_limit missing @ limits