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

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

Here is an example of nested cases:

lemma True

   have A
   proof (cases A)
     case True then have a: "A" .
     have B
     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 
right spot.

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 mailing list