Re: [isabelle] Decision procedures through computation & code_reflect



Hi Wenda,

the order must be:

> code_reflect Foo
> datatypes real="_" and rat = "_"  and int="_" and poly="_"
> functions sgn_at

> declare [[code drop: sgn_at]]

> method_setup eval_sgn_at_static = {*
>       Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds ctxt)))
> *}

It is the very nature of static conversions that they don't take notice
of any code setup after their position.

Cheers,
	Florian



> 
> lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
>   (*almost instant*)
>   apply eval_sgn_at_dynamic
> oops
> 
> lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
>   (*0.5s-1s*)
>   apply eval_sgn_at_static
> oops
> 
> end
> 
> Thanks,
> Wenda
> 

-- 

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.