TFL/post.ML
changeset 15150 c7af682b9ee5
parent 14240 d3843feb9de7
child 15171 e0cd537c4325
equal deleted inserted replaced
15149:c5c4884634b7 15150:c7af682b9ee5
   193    end
   193    end
   194   handle U.ERR {mesg,func,module} =>
   194   handle U.ERR {mesg,func,module} =>
   195                error (mesg ^
   195                error (mesg ^
   196                       "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   196                       "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   197 
   197 
       
   198 
       
   199 (* Derive the initial equations from the case-split rules to meet the
       
   200 users specification of the recursive function. 
       
   201  Note: We don't do this if the wf conditions fail to be solved, as each
       
   202 case may have a different wf condition. We could group the conditions
       
   203 together and say that they must be true to solve the general case,
       
   204 but that would hide from the user which sub-case they were related
       
   205 to. Probably this is not important, and it would work fine, but, for now, I
       
   206 prefer leaving more fine-grain control to the user. *)
       
   207 local
       
   208   fun get_related_thms i = 
       
   209       mapfilter ((fn (r,x) => if x = i then Some r else None));
       
   210 
       
   211   fun solve_eq (th, [], i) = 
       
   212       raise ERROR_MESSAGE "derive_init_eqs: missing rules"
       
   213     | solve_eq (th, [a], i) = [(a, i)]
       
   214     | solve_eq (th, splitths as (_ :: _), i) = 
       
   215       [((standard o ObjectLogic.rulify_no_asm)
       
   216           (CaseSplit.splitto splitths th), i)]
       
   217       (* if there's an error, pretend nothing happened with this definition 
       
   218          We should probably print something out so that the user knows...? *)
       
   219       handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
       
   220 in
       
   221 fun derive_init_eqs sgn rules eqs = 
       
   222     let 
       
   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
       
   224                       eqs
       
   225       fun countlist l = 
       
   226           (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
       
   227     in
       
   228       flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
       
   229                 (countlist eqths))
       
   230     end;
       
   231 end;
       
   232 
       
   233 
   198 (*---------------------------------------------------------------------------
   234 (*---------------------------------------------------------------------------
   199  * Defining a function with an associated termination relation.
   235  * Defining a function with an associated termination relation.
   200  *---------------------------------------------------------------------------*)
   236  *---------------------------------------------------------------------------*)
   201 fun define_i strict thy cs ss congs wfs fid R eqs =
   237 fun define_i strict thy cs ss congs wfs fid R eqs =
   202   let val {functional,pats} = Prim.mk_functional thy eqs
   238   let val {functional,pats} = Prim.mk_functional thy eqs