Email Gateway (Aug 18 2022 at 13:53): Email Gateway (Aug 18 2022 at 13:53):From: Randy Pollack <rpollack@inf.ed.ac.uk>
This is ok:
lemma
fixes F::"nat \<Rightarrow> nat"
defines "P == (F = Suc)"
assumes h:"... P ..."
shows "... P ..."
where I might want to use P several times in the assumes and shows.
What is the intended way to make a definition for local use in the
assumes of a locale? This is rejected:
locale PF = (***)
fixes F::"nat \<Rightarrow> nat"
defines "P == (F = Suc)"
assumes PFa:"P"
*** Bad head of lhs: bound variable "P"
This is accepted
locale PF2 =
fixes F::"nat \<Rightarrow> nat"
and P :: bool
defines "P == (F = Suc)"
assumes PFa:"P"
but doesn't seem to mean what I wanted to express in (***).
A different, but related question. Consider the (partial)
interpretation:
interpretation PF2I: PF2 Suc
gives goal
PF2 Suc &&& P == Suc = Suc
^ this P is blue
I guess the blue P is generalized, so this can never be proved, which
is probably intended for partial interpretation.
but consider this:
abbreviation P :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
where "P F == \<forall>(n::nat). \<exists>(z::nat). F n = z + 1"
locale PF =
fixes F::"nat \<Rightarrow> nat"
assumes PFa[rule_format]:"P F"
locale PFm = PF + fixes m :: nat
begin
definition F0 :: "nat \<Rightarrow> nat" where "F0 x = (F x) + m"
lemma Flem: shows "P F0"
sorry
end
Now the partial interpretation
interpretation PFmSuc: PFm Suc
by (unfold_locales, auto)
is accepted.
thm PFmSuc.Flem
shows
P (PFm.F0 Suc m)
^ thus is black on a yellow background
What does that mean?
Randy
Email Gateway (Aug 18 2022 at 13:54):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:
This is ok:
lemma
fixes F::"nat \<Rightarrow> nat"
defines "P == (F = Suc)"
assumes h:"... P ..."
shows "... P ..."where I might want to use P several times in the assumes and shows.
What is the intended way to make a definition for local use in the
assumes of a locale? This is rejected:locale PF = (***)
fixes F::"nat \<Rightarrow> nat"
defines "P == (F = Suc)"
assumes PFa:"P"*** Bad head of lhs: bound variable "P"
This is accepted
locale PF2 =
fixes F::"nat \<Rightarrow> nat"
and P :: bool
defines "P == (F = Suc)"
assumes PFa:"P"but doesn't seem to mean what I wanted to express in (***).
The treatment of "free" variables is different in "lemma" and
"locale". In "lemma" they are automatically fixed (and generalised
when the statement is turned into a theorem), in "locale" they are
universally quantified for the term they occur in. The distinction
might seem a bit arbitrary but I guess one wanted "x * y = y * x" to
mean "!x y. x * y = y * x" in a locale assumption.
A different, but related question. Consider the (partial)
interpretation:interpretation PF2I: PF2 Suc
gives goal
PF2 Suc &&& P == Suc = Suc
^ this P is blueI guess the blue P is generalized, so this can never be proved, which
is probably intended for partial interpretation.
Indeed, in a top-level interpretation there is no context where "P"
could be bound and it is thus generalised. If you did
interpretation FP2I: PF2 Suc x
you would get a blue x instead. (In contrary to what I said in my
previous e-mail, I think the implementation accepts such an unbound
variable also on the right hand side of sublocale, but it may then get
lost as what to do with it when applying the interpretation.)
but consider this:
abbreviation P :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
where "P F == \<forall>(n::nat). \<exists>(z::nat). F n = z + 1"locale PF =
fixes F::"nat \<Rightarrow> nat"
assumes PFa[rule_format]:"P F"locale PFm = PF + fixes m :: nat
begin
definition F0 :: "nat \<Rightarrow> nat" where "F0 x = (F x) + m"
This creates a constant "PFm.F0" with two arguments and in the locale
"PFm.F0 F m" is abbreviated by "F0".
lemma Flem: shows "P F0"
sorryend
Now the partial interpretation
interpretation PFmSuc: PFm Suc
by (unfold_locales, auto)is accepted.
It should be equivalent to
interpretation PFmSuc: PFm Suc m
thm PFmSuc.Flem
shows
P (PFm.F0 Suc m)
^ thus is black on a yellow background
I'm not sure what black on yellow means. I believe it is a warning
that you might have done something unintended. However, I expect the
result to be the same if you make an interpretation with full arguments.
Clemens
Email Gateway (Aug 18 2022 at 13:54):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Clemens Ballarin wrote:
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:
What is the intended way to make a definition for local use in the
assumes of a locale?
In Isabelle 2008 and earlier, "defines" allowed you to make a definition
that gets unfolded automatically in interpretations and need not be
specified, although you still had to explicitly fix the defined
parameter. In particular, at interpretations, you did not have to
instantiate the parameter. Since Isabelle 2009, you can still fix the
parameter, but at all interpretations, you must specify the defined
parameter as well.
In your example, this would be:
locale PF2 =
fixes F::"nat \<Rightarrow> nat"
and P :: bool
defines "P == (F = Suc)"
assumes PFa:"P"
interpretation PF2I: PF2 Suc "Suc = Suc"
or
interpretation PF2I: PF2 Suc True
Unfortunately, unfold_locales does not work well with defines, so you
typically have to get rid of the goals due to defines first.
Now the partial interpretation
interpretation PFmSuc: PFm Suc
by (unfold_locales, auto)is accepted.
thm PFmSuc.Flemshows
P (PFm.F0 Suc m)
^ thus is black on a yellow backgroundI'm not sure what black on yellow means. I believe it is a warning that
you might have done something unintended. However, I expect the result
to be the same if you make an interpretation with full arguments.
It does have the same result. In this example, m is not bound by the
context, i.e. a new parameter that should be declared as such. However,
interpretation has an unusual behaviour regarding undeclared new
parameters. As far as I have been able to track it down, it does the
following for undeclared parameters:
If the undeclared parameter in the expression is the same as one in
the locale that is not instantiated, then it is not generalised.
If is a new undeclared parameter (e.g. some argument to a function),
then it is generalised iff there are assumptions to be shown at the
interpretation.
Anyway, the correct way to do the above interpretation is:
interpretation PFmSuc: PFm Suc m for m
You can also omit the m parameter:
interpretation PFmSuc: PFm Suc for m
The black on yellow background tells you that there is a variable that
is not bound by the context, but neither generalised. You can turn it
into a free (generalised) variable by applying the attribute standard to
the theorem, but this can also do much more to it.
Andreas
Last updated: May 03 2024 at 12:27 UTC