[isabelle-dev] Nested "case" statements and "show" getting stuck
makarius at sketis.net
Mon Dec 14 18:00:35 CET 2009
On Thu, 10 Dec 2009, Simon Meier wrote:
> 1. It seems that case environments are global instead of local to
> subproofs. Hence, reusing case names in a subproof is impossible.
The name space for case elements is indeed flat, but the results nest
within a proof context in the usual way, potentially making some earlier
Here is an example of nested cases:
proof (cases A)
case True then have a: "A" .
proof (cases B)
case True then have b: "B" .
Of course you can always rebind particular results from an earlier case
invocations, such as "a" above. You can also use 'note' for facts or
'let' for terms to avoid repeating text.
> 2. Sometimes in a more deeoply nested position (like four calls of
> the "sources" proof method) the "show" command gets stuck while
> checking if the proven goal solves an open subgoal.
In the example that you've shown me privately, the system has a hard time
to match the result from without a cascade of case invocations against one
of the pending subgoals. Isar has no explicit goal focus, so the
propositions are reconsidered explicitly, trying subgoals 1, 2, 3, ... in
One of the examples happen to work, if a 'defer' step is inserted in the
I still need to figure out, which technical details pose particular
problems here. We shall continue this discussion privately ...
More information about the isabelle-dev