TFL/post.ML
 changeset 15150 c7af682b9ee5 parent 14240 d3843feb9de7 child 15171 e0cd537c4325
equal 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`