Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals

Hi Gottfried,

1) In the linordered_idom class context, the function foo_f takes 0.7 seconds to
process, where an identical function, foo_f2, in the global context takes
only about 0.1 second. Is there any advantage to defining foo_f in the
linordered_idom class context, other than it will localize its name?
As the definition of foo_f does not depend on any parameter of the linordered_idom type class, I don't see a point in defining foo_f inside the type class context.

2) Inside the class context, the simp method will not use foo_f.simps, even
though the output message shows that foo_f.simps are available as rewrite
rules. Inside, linordered_idom_class.foo_f.simps must be added as a simp rule.
Is there something I can do to get it to use foo_f.simps, without having to
add the qualified name linordered_idom_class.foo_f.simps as a simp rule?
You are confused by Isabelle's type inference. Inside a type class context, the type variable 'a is fixed, i.e., inside linorderd_idom, foo_f.simps only works for instances of foo_f with type "'a foo_d". In your theorem, you try to instantiate 'a to int. This makes Isabelle think that you want to refer to the exported version of foo_f, so you have to add the exported foo_f.simps rules as well.

3) The value method prints linordered_idom numerals as sums of 1, even though
I import Code_Target_Numeral.thy. The simp method prints numerals in the nice
form. Is there something I can do to get the value method to print
linordered_idom numerals as single numbers rather than sums of 1?*)

value uses a different set of different equations for normalising terms, namely those declared as [code], whereas the simp method uses [simp]. You can, of course, try to change the setup of code generator, but that requires considerable effort.


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