diff -r c5c4884634b7 -r c7af682b9ee5 TFL/post.ML --- a/TFL/post.ML Thu Aug 19 12:35:45 2004 +0200 +++ b/TFL/post.ML Fri Aug 20 12:20:09 2004 +0200 @@ -195,6 +195,42 @@ error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); + +(* Derive the initial equations from the case-split rules to meet the +users specification of the recursive function. + Note: We don't do this if the wf conditions fail to be solved, as each +case may have a different wf condition. We could group the conditions +together and say that they must be true to solve the general case, +but that would hide from the user which sub-case they were related +to. Probably this is not important, and it would work fine, but, for now, I +prefer leaving more fine-grain control to the user. *) +local + fun get_related_thms i = + mapfilter ((fn (r,x) => if x = i then Some r else None)); + + fun solve_eq (th, [], i) = + raise ERROR_MESSAGE "derive_init_eqs: missing rules" + | solve_eq (th, [a], i) = [(a, i)] + | solve_eq (th, splitths as (_ :: _), i) = + [((standard o ObjectLogic.rulify_no_asm) + (CaseSplit.splitto splitths th), i)] + (* if there's an error, pretend nothing happened with this definition + We should probably print something out so that the user knows...? *) + handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; +in +fun derive_init_eqs sgn rules eqs = + let + val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) + eqs + fun countlist l = + (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) + in + flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) + (countlist eqths)) + end; +end; + + (*--------------------------------------------------------------------------- * Defining a function with an associated termination relation. *---------------------------------------------------------------------------*)