Re: [isabelle] Decision procedures through computation & code_reflect



Hi Wenda,

> When building a decision procedure though computation in Isabelle, one
> way is to rely on the command Code_Runtime.dynamic_holds_conv, which
> compiles the goal into SML using code generation mechanism, and then
> prove by evaluation. However, one drawback of this method is that the
> same computable functions are compiled each time the decision procedure
> is called.

the short answer is: use
	code_reflect
plus
	Code_Runtime.static_holds_conv

Details can be found in the Tutorial on Code Generation.

If this does not work as expected, give a link to your examples.

> code_reflect Rat
>   datatypes rat = Frct
>   functions Fract
>     "(plus :: rat ⇒ rat ⇒ rat)" "(minus :: rat ⇒ rat ⇒ rat)"
>     "(times :: rat ⇒ rat ⇒ rat)" "(divide :: rat ⇒ rat ⇒ rat)"
>   file "rat.ML"

This works relative to the current working directory, which is an a
little bit arbitrary notion.  Usually it is best to leave out the file
clause entirely and thus to compile directly in the runtime environment.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.