I have declared an inductive predicate in an unnamed context like so:
context fixes a_convs :: "'a ⇒ 'a fm ⇒ 'a_conv_prf ⇒ bool" fixes aneg_convs :: "'a ⇒ 'a fm ⇒ 'aneg_conv_prf ⇒ bool" begin inductive fm_convs :: "'a fm ⇒ 'a fm ⇒ ('a_conv_prf, 'aneg_conv_prf) fm_conv_prf ⇒ bool" end
Suppose that I have instantiations for
aneg_convs. I can declare an abbreviation for
fm_convs.induct like so:
lemmas convs_induct = fm_convs.induct[of a_convs aneg_convs]
The problem now is that convs_induct does not have the case names attached to fm_convs.induct. Is there a way to transfer those case names automatically?
I don't know any automatic version, but the manual version should work:
lemmas convs_induct = fm_convs.induct[of a_convs aneg_convs, case_names c1 c2 c3]
You can name the cases with
and you probably want
consumes 1 also.
Last updated: Dec 07 2023 at 08:19 UTC