[isabelle] Transfer consumes and case_names declaration from local theory to global theory
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
inductive r and rs
a: "a = a d r 0"
| b: "rs  d r 0"
| c: "r x d rs [x]"
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and