Email Gateway (Aug 18 2022 at 11:11): Email Gateway (Aug 18 2022 at 11:11):From: Carsten Varming <cvarming@cs.cmu.edu>
I get some strange sorts using the new Isabelle 2007.
The constant funZip declared below somehow doesn't get the right type.
I specify that 'a should be of sort type, but when I try to use the
constant, 'a is of sort complete_lattice.
The constant got the right sort in the beta release of July 21st 2007 and
I don't think I had any problems in Isabelle 2005 either.
Is this a bug in Isabelle or am I missing something very basic?
Carsten
theory test imports Main
begin
consts funZip :: "(('b::type) => ('a::type)) => (('b::type) list) =>
(('a::type) list) => ('b::type) => ('a::type)"
primrec
"funZip b [] l v1 = b v1"
"funZip b ((v::'b::type) # r) l v1 =
(case l of Nil => b v1
| Cons e l' => if v1 = v
then (e::'a::type)
else (funZip b r l' v1))"
lemma "funZip bot (v # a) (v' # b) v = v'" by auto
end
Email Gateway (Aug 18 2022 at 11:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Carsten,
lemma "funZip bot (v # a) (v' # b) v = v'" by auto
the point is that "bot" is now a constant, namely the bottom element in
a complete lattice. Adding a "hide const bot" at the beginning of your
theory will avoid a renaming.
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:13):From: Makarius <makarius@sketis.net>
After stating this lemma the proof state output displays a non-hilighted
"bot", which indicates that it is a constant (of class complete_lattice).
In order to avoid this capturing of a free variable in the statement, you
may specify a local context explicitly as follows:
lemma
fixes bot
shows "funZip bot (v # a) (v' # b) v = v'"
Of course you can also just rename "bot" apart from the theory context, or
tweak the latter by hiding "bot" in the name space permanantly.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC