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