[isabelle] Transfer consumes and case_names declaration from local theory to global theory



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.