Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-RC0 - using goal_cases correctly


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC