[isabelle] Illegal schematic variable(s) in case
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Illegal schematic variable(s) in case
- From: Lars Hupel <hupel at in.tum.de>
- Date: Mon, 20 Apr 2015 14:59:22 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0
I have proved the following elimination rule (which is surprisingly
similar to option.rel_cases):
assumes "ienv_related nenv penv"
obtains (none) "nenv x = None" "penv x = None"
| (some) t u where "nenv x = Some t" "penv x = Some u" "P t u"
When trying to use it
from `ienv_related nenv penv`
proof (cases rule: ienv_relatedE)
I get the following error message:
Illegal schematic variable(s) in case "none"â
Presumably, the problem is that there are still uninstantiated schematic
variables in the assumption. It works if I instantiate the rule
explicitly with 'where'. My question now is, is this the recommended
style, or should I rather write an explicit 'assume'?
This archive was generated by a fusion of
Pipermail (Mailman edition) and