Re: [isabelle] print_cases shows non-existing schematic variable

Hi Lars,

I don't know the design choices for cases, as I have not implemented them, but here are my comments: cases assumes that you give it a conventional case analysis rules. These rules do not change the conclusion, so cases has some point in not providing any term abbreviations for the conclusions. Anyway, you are trying to use sophisticated proof methods just to benefit from a certain side effect. I used to do that regularly, too (and sometimes still do, but much less).

I guess that it should be fairly easy to implement your own method that does nothing but applying a rule and setting up the cases. The infrastructure should be all there.


On 22/04/15 10:41, Lars Hupel wrote:
I have an introduction rule which has a lot of premises. These premises
also have some assumptions. It is very tedious to fix all the variables
and assume all the assumptions over and over again, so I decided to
investigate whether I can leverage Isar's 'case' notation for proofs
using this rule.

My first attempt was to start my proof like this:

   lemmas irule_cases = irulesI[case_names a b c d e]

   proof (cases rule: irule_cases)

This works out almost as I expected. I can write down

     case a
     show ...
     case b
     show ...

However, the schematic variable '?case' does not exist. In other
situations, I can just use 'show ?thesis', but this is not applicable here.

Strangely enough, this is what 'print_cases' prints:

       let "?case" = "is_fmap ?rs"

But the variable is just not there, which can be confirmed via
'Query/Print Context'.

I've browsed through the Isar reference and found the attribute

   lemmas irule_cases =
     irulesI[case_names a b c d e,
             case_conclusion a foo, ...]

Now, 'print_cases' claims that '?foo' exists, but it doesn't.

Now, if I change the initial proof step to use 'induct' instead of
'cases', I get the '?case' variable. However, I would argue, that using
'induct' for this situation feels even more unnatural than using 'cases'.

In Â6.6.1 of the Isar reference, it is stated about the 'case' command
that "Term bindings may be covered as well, notably ?case for the main
conclusion." I haven't found anything about when exactly '?case' is
present or absent.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.