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



Hello,

I have to revisit this rather old thread ...

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

I've now run into a situation where even with a fully instantiated rule,
I get "illegal schematic variable in case".

Here's the output of "print_cases":

cases:
  Closure:
    fix env_ n_ e_
    let "?case" = "?thesis"
    assume "cl = Closure env_ n_ e_"
  Recclosure:
    fix env_ funs_ n_ n'_ e_
    let "?case" = "?thesis"
    assume "cl = Recclosure env_ funs_ n_" "allDistinct (map (Î(f, uu_,
uu_). f) funs_)" "find_recfun n_ funs_ = Some (n'_, e)"

I fail to see the schematic variable. It seems fully instantiated to me.

Cheers
Lars




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