Email Gateway (Aug 22 2022 at 11:17): Email Gateway (Aug 22 2022 at 11:17):From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Hello mailing-list!
When I try the following minimal example in Isabelle2015
theory Test
imports Main
begin
datatype (funs : 'f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
type_synonym ('f, 'v) trs = "(('f, 'v) term × ('f, 'v) term) set"
context
fixes F and R :: "('f, 'v) trs"
assumes "R ⊆ F"
begin
fun star :: "('f, 'v) term ⇒ ('f, 'v) term"
where
"star (Fun f ts) = Fun f (map star ts)"
end
end
I get the error message:
exception THM 0 raised (line 744 of "thm.ML"):
forall_intr: variable "R" free in assumptions
wf R ⟹
(⋀f ts x. x ∈ set ts ⟹ (x, Fun f ts) ∈ R) ⟹
∀x. Wellfounded.accp star_rel x
[star_rel ≡ ??.Test.star_rel]
Which leaves me quite puzzled. I do neither understand the error
message nor why there is an error at all. Can somebody explain what
happens here, please?
Cheers, Thomas
Email Gateway (Aug 22 2022 at 11:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Thomas,
I have run into this problem before. The issue is that the function package does not seem
to properly respect the fixed variables in unnamed contexts. If you change the variable
name in the context from R to something else, then the function definition should work.
Internally, fun uses the name "R" for the termination relation in the termination proof.
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:20):From: Christian Sternagel <c.sternagel@gmail.com>
A related question: Who is the maintainer of the function package these
days?
If my suspicion is correct this (slightly) confusing error could be
avoided by using the existing Isabelle/ML machinery for inventing fresh
names at the right point in the function package (wherever this is ;)).
cheers
chris
Email Gateway (Aug 22 2022 at 11:41):From: Makarius <makarius@sketis.net>
It means that the function package is not fully localized, even though it
happens to be one of the first local theory packages in history.
I have refined that in Isabelle/ce74c00de6b7, so it should work better in
the coming release.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC