Email Gateway (Aug 19 2022 at 17:24): Email Gateway (Aug 19 2022 at 17:24):From: Walther Neuper <wneuper@ist.tugraz.at>
working through Lars Hupel's paper [1] I run into a newbie's question:
lemma "(a::rat) < b ⟹ 0 < b ⟹ 0 < c ⟹ 0 < (c + c)/(b - a)"
by simp
works, but I cannot do that with more general types:
lemma "(a::'a::{zero,ord,plus,minus,inverse}) < b ⟹
0 < b ⟹ 0 < c ⟹ 0 < (c + c)/(b - a)"
by ???
How is the latter done, or: why I am wrong?
Walther
[1] https://www21.in.tum.de/~hupel/pub/simp-trace.pdf
Email Gateway (Aug 19 2022 at 17:24):From: Tobias Nipkow <nipkow@in.tum.de>
Your second lemma is just not true: the classes zero,ord,plus,minus,inverse
merely require the existence of 0,<,etc but impose no axioms on them. That's why
Isabelle tells you
Auto Quickcheck found a counterexample
and that's why no rewrite rules apply.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 17:25):From: Walther Neuper <wneuper@ist.tugraz.at>
thank you for help !
working through Lars Hupel's paper [1] I run into a newbie's question:
lemma "(a::rat) < b ⟹ 0 < b ⟹ 0 < c ⟹ 0 < (c + c)/(b - a)"
by simpworks, but I cannot do that with more general types:
lemma "(a::'a::{zero,ord,plus,minus,inverse}) < b ⟹
0 < b ⟹ 0 < c ⟹ 0 < (c + c)/(b - a)"
by ???Your second lemma is just not true: the classes
zero,ord,plus,minus,inverse merely require the existence of 0,<,etc
but impose no axioms on them.
More questions from playing with the wounderful simp_trace_new:
thm Fields.field_class.add_frac_eq
but some are not known (theory imports Complex_Main), e.g
thm Num.mult_1s_2
thm Divides.add_0s_1
Why is that ?
forced the simplifier into
c + c = Numeral1 / Numeral1 * (c / 1) + (Numeral1 / Numeral1 * (c / 1) + 0)
as shown in the attachment ?
Thanks,
Walther
[1] https://www21.in.tum.de/~hupel/pub/simp-trace.pdf
Screenshot-trace-1.png
Email Gateway (Aug 19 2022 at 17:25):From: Walther Neuper <wneuper@ist.tugraz.at>
just another question: given ...
... is there a way to get a trace convincing novices that
execution of functional programs is actually rewriting ?
Walther
Email Gateway (Aug 19 2022 at 17:29):From: Lars Hupel <hupel@in.tum.de>
Some theorems found in the trace are known in the context, eg.
thm Fields.field_class.add_frac_eq
but some are not known (theory imports Complex_Main), e.g
thm Num.mult_1s_2
thm Divides.add_0s_1
Why is that ?
The theorem names printed by the simp trace are not always "authentic".
My best guess here is that the above should be
thm Num.mult_1s(2)
thm Divides.add_0s(1)
What is the best way to find out, what sequence of rule applications
forced the simplifier into
c + c = Numeral1 / Numeral1 * (c / 1) + (Numeral1 / Numeral1 * (c / 1) + 0)
as shown in the attachment ?
I can't answer that question. Apparently, the "classic" simplifier trace
doesn't now either.
Cheers
Lars
Last updated: Apr 24 2024 at 20:16 UTC
