[isabelle] print_cases shows non-existing schematic variable



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 ...
      ...
  next
    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:

  cases:
    a:
      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
'case_conclusion':

  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.

Cheers
Lars




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