Stream: General

Topic: Keep case names with lemmas

Lukas Stevens (Mar 30 2020 at 11:30):

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 a_convs and 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?

Mathias Fleury (Mar 30 2020 at 13:39):

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 case_names.

Mathias Fleury (Mar 30 2020 at 15:26):

and you probably want consumes 1 also.

Last updated: Oct 26 2025 at 20:22 UTC