Email Gateway (Aug 18 2022 at 18:31): Email Gateway (Aug 18 2022 at 18:31):From: Steve Wong <s.wong.731@gmail.com>
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
Last updated: Apr 20 2024 at 08:16 UTC