Re: [isabelle] print_cases shows non-existing schematic variable
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
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