Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
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.
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?
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.
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?
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