Re: [isabelle] Illegal schematic variable(s) in case
The problem really is the schematic ?x in the goal state. The case syntax cannot deal with
such schematics. The proof methods for induction support the argument "taking: foo" with
which such variables can be instantiated for the proof. Unfortunately, the cases method
does not support taking. As elimination rules usually also work with induction, you could
proof(induction taking: foo rule: ienv_relatedE)
Whether this is better than
assume "nenv foo = None" "penv foo = None"
is debatable, as induction is normally a much stronger proof principle than case analysis.
Alternatively, you can see whether the cases method can be easily extended with "taking".
On 20/04/15 14:59, Lars Hupel wrote:
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