[isabelle] --> vs. == for simp



Hi,

I'm having a bit of a problem with an axiomatization. For example

axiomatization
myless :: "['a::ord,'a] => bool" where
myless [simp] : "a < b == myless a b"

lemma "myless (1::nat) 2"

I cannot use simp, but rather by (metis Suc_eq_plus1 lessI myless
nat_1_add_1).

But if the axiomatization was weaker:

axiomatization
myless :: "['a::ord,'a] => bool" where
myless [simp] : "a < b --> myless a b"

then I can simply do

lemma "myless (1::nat) 2"
by simp

How come simp works only if the axiom was weaker?

Steve




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