# [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
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
--
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.*