Re: [isabelle] Illegal schematic variable(s) in case



Hi Lars,

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 write

proof(induction taking: foo rule: ienv_relatedE)
  case none

Whether this is better than

proof(rule ienv_relatedE)
  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".

Best,
Andreas


On 20/04/15 14:59, Lars Hupel wrote:
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.