Email Gateway (Aug 18 2022 at 15:47): Email Gateway (Aug 18 2022 at 15:47):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,
I use a locale without assumptions to hide multiple parameters to a
large (mutually recursive) inductive definition. Later on, I would like
to use the inductive rule generated for the predicate for an
instantiation of the locale, but without interpreting the locale because
the interpretation simply takes too long. Instead, I would like to use
the global version of the induction rule directly.
Here is a short example:
locale A =
fixes a :: 'a
begin
inductive r and rs
where
a: "a = a d r 0"
| b: "rs [0] d r 0"
| c: "r x d rs [x]"
end
lemma "A.r x (Suc 0) ==> True"
and "A.rs x [Suc 0] ==> True"
apply(induct rule: A.r_rs.inducts)
However, induct complains that it failed to join given rules into one
mutual rule. I figured out that A.r_rs.inducts is missing the
[consumes 1] declaration (as well as the case names).
How can I extract the consumes/case_names/case_conclusion declarations
of a theorem t in a local context C and transfer this information to the
global version C.t automatically? Is this possible at all?
Best regards,
Andreas
Last updated: Apr 24 2024 at 20:16 UTC