[isabelle] Illegal schematic variable(s) in case



I have proved the following elimination rule (which is surprisingly
similar to option.rel_cases):

  lemma ienv_relatedE:
    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`
  show ?case
    proof (cases rule: ienv_relatedE)
      case none

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'?

Cheers
Lars




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