Email Gateway (Aug 22 2022 at 12:15): Email Gateway (Aug 22 2022 at 12:15):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
in Isabelle 2015, I could write:
lemma "X"
proof (rule Y)
case goal1
In Isabelle 2016, I can write:
lemma "X"
apply (rule Y)
proof(goal_cases)
case 1
Or I could write
proof(rule Y, goal_cases)
Is there a nicer way to combine the rule and goal_cases method? Is
this the intended usage?
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:28):From: Makarius <makarius@sketis.net>
Yes, the second form is the intended usage. Method "goal_cases" bypasses
the "using" facts, so the comma is always right.
Since the preceeding proof method in this example is just "rule", it might
be also possible to say:
proof (cases rule: Y)
Details depend on the shape of Y.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC