Email Gateway (Oct 14 2022 at 14:59): Email Gateway (Oct 14 2022 at 14:59):From: Peter Lammich <lammich@in.tum.de>
Hello List,
I just ran into an effect where Isabelle syntax-highlights statements in
an inconsistent way, that suggests a different statement from what is
actually proved!
When trying to use constant names as pattern variables in case
expressions, something in Isabelle's parser goes utterly wrong:
definition "b = 0"
...
Here the b in the pattern is highlighted black (indicating a constant),
the type is inferred from the !!-bound variable, but in the actual
statement that is proved, the b in "b=fst a" refers to the variable
bound by the case pattern!
The effect occurs in 2021-1 and 2022-RC2
-- Peter
More details and variations of this effect:
definition "b≡0"
lemma "case a of (b,c) ⇒ b = fst a" *** Not a datatype constructor:
"Scratch.b"
lemma foo: "case a of (b,c) ⇒ b = fst a" for b by auto
All fine, proves "case ?a of (bxx,c) ⇒ bxx = fst ?a", but the b in the
pattern is pretty-printed as constant (black), but not linked to
Scratch.b (via ctrl click). The b on the rhs (in b = ...) is, however,
ctrl-click linked to the "for b" clause.
lemma "⋀b. case a of (b,c) ⇒ b=fst a" by auto
// same as above. b in pattern highlighted as constant, b on rhs
ctrl-click linked to !!b, but lemma proved is "case ?a of (bxx, c) ⇒ bxx
= fst ?a"
Even worse, the parsing error even makes it into the type inference:
lemma "⋀b::nat. case a of (b,c) ⇒ b=fst a" by auto
proves a statement for a::(nat * _)
term ‹λb. b=0› *** highlighted as expected
term ‹λ(b,c). b=0› *** highlighted as expected
term ‹λ(b,c) ⇒ b=0› *** Not a datatype constructor: "Scratch.b"
If you change b to be a datatype constructor, things slightly change,
but still go wrong:
datatype foo = b
lemma "case a of (b,c) ⇒ b = fst a" by (auto split: foo.split) ** as
expected
lemma foo: "case a of (b,c) ⇒ b = fst a" for b :: nat by auto
** b in pattern still highlighted black, statement proved is "case ?a of
(bxx::nat,c) ⇒ bxx = fst ?a"
isabelle_strange2.png
isabelle_strange2.png
isabelle_strange1.png
Last updated: Jan 04 2025 at 20:18 UTC