Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Predicate compiler inside a locale

Email Gateway (Aug 22 2022 at 15:00):

From: Lars Hupel <hupel@in.tum.de>
Dear list,

is it at all possible to use the predicate compiler for inductive
definitions inside a locale? So far I have tried

context my_locale begin
code_pred veval'
end

and

global_interpretation ...
code_pred ...

both of which fail ("not a constant" and "no such predicate", respectively).

The locale itself has no assumptions, so I naively thought I could also try

code_pred my_locale.veval'

but that fails with "exception Subscript".

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:00):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,

It is possible when the locale has no assumptions. Before invoking code_pred, you must
re-declare all the intro rules using [code_pred_intros]. Then, you'll have to prove a huge
elimination rule when you invoke code_pred, but this is usually easy.

There's an example at the end of J/Smallstep.thy in my JinjaThreads AFP entry that should
get you started.

Best,
Andreas

Email Gateway (Aug 22 2022 at 15:00):

From: Lars Hupel <hupel@in.tum.de>
Hi Andreas,

thanks, that worked (and I wanted to use [code_pred_intro] anyway). Now
I just need to convince mode inference ...

Cheers
Lars

Last updated: Apr 25 2024 at 04:18 UTC