[isabelle-dev] Nested "case" statements and "show" getting stuck

[Makarius]

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 
bindings inaccessible.

Here is an example of nested cases:

lemma True
proof

   have A
   proof (cases A)
     case True then have a: "A" .
     have B
     proof (cases B)
       case True then have b: "B" .
       oops

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

One of the examples happen to work, if a 'defer' step is inserted in the 
right spot.

I still need to figure out, which technical details pose particular 
problems here.  We shall continue this discussion privately ...


 	Makarius