Email Gateway (Aug 22 2022 at 16:26): Email Gateway (Aug 22 2022 at 16:26):From: Andreas Halkjær From <andro.from@gmail.com>
Hey,
I ran into this issue in a larger theory (*) but it can be boiled down at
least to the following (silly) theory:
theory THM0_741 imports Main begin
datatype 'a s = S 'a
datatype 'a t = T ‹'a s›
primrec f :: ‹'a s ⇒ 'a set› where
‹f (S x) = {x}›
primrec g :: ‹'a t ⇒ 'a set› where
‹g (T x) = f x›
lemma trigger: ‹f t ⊆ UNIV›
by blast
lemma ‹g p ⊆ UNIV›
using trigger (* raises: *)
proof (induct p)
case (T x) (* exception THM 0 raised (line 741 of "thm.ML"):
assume: variables *)
then show ?case
by simp
qed
end
Also available here:
https://gist.github.com/andreasfrom/d4b87d0bbac6d94742ecdfd8605369f7
It's unclear from the error what the problem is.
In the larger theory I worked around it by moving the using into each
case that needed it.
Andreas
Email Gateway (Aug 22 2022 at 16:26):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Andreas,
I agree that the error message is suboptimal. It occurs when the subgoal corresponding to
the case contains schematic (type) variables. In your example, the lemma trigger
introduces a schematic type variable ?'a into the goal state, on which the "case" command
chokes. If you instantiate the type variable, the error goes away. For example:
lemma ‹g p ⊆ UNIV› for p :: "'a t"
using trigger[where ?'a='a]
For schematic term variables, the induct(ion) proof method has an optional argument
"taking: ..." where the instantiations can be given. Unfortunately, there is no equivalent
for type variables.
A general remark: You should feed only those assumptions into the induction proof method
that are consumed by the induction rule or mention some of the induction variables.
Eveything else such as the trigger should really be added with "using" in the relevant
cases. Every non-inductive assumption just makes the goal state much larger and the proof
checking and pretty printing slower.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 16:26):From: Andreas Halkjær From <andro.from@gmail.com>
That makes good sense. Thank you.
And thank you for the general remark!
Andreas
Last updated: Apr 26 2024 at 04:17 UTC