[isabelle] print_cases shows non-existing schematic variable
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] print_cases shows non-existing schematic variable
- From: Lars Hupel <hupel at in.tum.de>
- Date: Wed, 22 Apr 2015 10:41:27 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0
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
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
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