Email Gateway (Aug 18 2022 at 18:27): Email Gateway (Aug 18 2022 at 18:27):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
In the script bellow, I was expecting to solve lemmas 01 and 04 directly by
reflexivity of equality, like the
other ones, since both terms are the same.. But the simplifier tells me
that I have to use also the equation len01, to substitute len(Empty) for Z.
What (basic fact) am I missing here?
Many thanks,
theory equality
imports Main
begin
datatype Nat = Z | suc Nat
datatype 'a List = Empty | cons 'a "'a List"
primrec add :: "Nat => Nat => Nat"
where
add01: "(add x Z) = x" |
add02: "(add x (suc y)) = suc (add x y)"
primrec cat :: "'a List => 'a List => 'a List"
where
cat01: "(cat Empty list) = list" |
cat02: "(cat (cons head tail) list) = cons head (cat tail list)"
primrec len :: "'a List => Nat"
where
len01: "(len Empty) = Z" |
len02: "(len (cons head tail)) = suc(len tail)"
thm "refl"
(* lemma 00 *)
lemma "cat Empty Empty = cat Empty Empty" by (rule refl)
(* lemma 01 *)
lemma "len Empty = len Empty" by (simp only:len01)
(*lemma 02 *)
lemma "add (len x) (len y) = add (len x) (len y)" by (rule refl)
(* lemma 03 *)
lemma "add (len x) (len y) = add (len x) (len y)" by (simp only: refl)
(* lemma 04 *)
lemma "add (len Empty) (len Empty) = add (len Empty) (len Empty)"
by (simp only: len01)
end
Email Gateway (Aug 18 2022 at 18:27):From: Lawrence Paulson <lp15@cam.ac.uk>
The two terms are not identical. Each instance of Empty in len Empty has a separate type.
Larry Paulson
Email Gateway (Aug 18 2022 at 18:27):From: Alfio Martini <alfio.martini@acm.org>
Very well!!
Thank you!
Email Gateway (Aug 18 2022 at 18:27):From: Lars Noschinski <noschinl@in.tum.de>
No, the two subtterms left and right of the equality sign are not
exactly the same. Unfortunately, it is a bit misleading how this goal is
presented by Isabelle. If you enable the display of types, you get at
least a hint about what is going wrong:
lemma "len Empty = len Empty"
using [[show_types]]
outputs
proof (prove): step 0
goal (1 subgoal):
1. len Empty = len Empty
type variables:
'a, 'b :: type
As you see, there are two type variables occuring in this term: Empty is
polymorphic, but there are no constraints, which would enforce a
particular instantiation of the polymorphic type variable -- not even
that the types of the left and right Empty should be the same.
For this reason, refl is not applicable here.
-- Lars
Last updated: Apr 27 2024 at 01:05 UTC