[isabelle] Fwd: Re: Decision procedures through computation & code_reflect



(this should have been posted on the user mailing list also)


-------- Weitergeleitete Nachricht --------
Betreff: Re: [isabelle] Decision procedures through computation &
code_reflect
Datum: Sat, 31 Jan 2015 09:43:02 +0100
Von: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
Organisation: TU Munich
An: Renà Thiemann <rene.thiemann at uibk.ac.at>
Kopie (CC): Manuel Eberl <eberlm at in.tum.de>,
cl-isabelle-users at lists.cam.ac.uk

Hi RenÃ,

after reading your mail twice, I finally got the point

> Sure, I can also give you a short version of what is going on.
> 
> We have an executable function ceta_checker with the following soundness property
> (slightly simplified from the real theorem)
> 
> lemma sound: ceta_checker ?input ?certificate ==> SN (rstep ?input)
> 
> to use this result with code generation, we do the following:
> 
> lemma "SN (rstep example_input)"
> apply (rule sound[where certificate = "example_certificate"])
> (* get proof obligation "ceta_checker example_input example_certificate" *)
> apply eval
> done

This is indeed no surprise: code_reflect essentially provides a target
language setup, but does not influence preprocessing etc. at all.  Ie.
during the call of eval the whole preprocessing of code equations is
issued, the code equations are translated, although when generation ML
code they are not used (any more) at all.  Hence the magical speedup
after deleting the critical code equation.

This seems to be a suitable candidate for
Code_Runtime.static_holds_conv.  Have you ever tried this?

Cheers,
	Florian

-- 

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



-- 

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.