Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 09:18):

From: Lars Hupel <hupel@in.tum.de>
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

Email Gateway (Aug 22 2022 at 09:18):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 09:20):

From: Lars Hupel <hupel@in.tum.de>
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 :-)

Cheers
Lars

Email Gateway (Aug 22 2022 at 11:50):

From: Lars Hupel <hupel@in.tum.de>
Hello,

I have to revisit this rather old thread ...

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

Last updated: Nov 21 2024 at 12:39 UTC