# [isabelle] On the use of the rule HOL.refl(exive)

```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

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

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.