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

Hi Andreas,

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

thanks for the hint, this works nicely.

> 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.

It probably incites more head-scratching from readers of the proof as to
why exactly induction is used there.

> Alternatively, you can see whether the cases method
> can be easily extended with "taking".

I will keep this in mind for later when I'm done with my current
formalization :-)


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