theory i131031a__q1b_context_slower__needs_qualified_simp__numeral_print
imports Complex_Main
begin

(*Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
Answer by Andreas Lochbihler:
> 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. 

And part of my answer:
As you talk about, the type variable 'a is special in the class context. If I try
`fun foo_f :: "'a::linordered_idom foo_d => real"`, I get the error `Sort 
constraint linordered_idom inconsistent with default type for type variable "'a"`. 
Using 'b works, and the two print statements show I get what I want. 
I could also be confused about instantiation.*)

datatype 'a foo_d = Foo_d 'a
context linordered_idom begin
fun foo_f :: "'b::linordered_idom foo_d => real" where
  "foo_f (Foo_d x) = real x"
  
theorem "foo_f (Foo_d (1::int)) = (1::real)"
print_statement foo_f.simps
print_statement linordered_idom_class.foo_f.simps
by(simp)
end

(*Andreas' answer about numerals not printing nice with "value":
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. 

GB: From "[isabelle] Looking for rat & int powers to use with linordered_idom",
and the examples I was working on, I create a simple example to show that
`value "nat_of(1::int)"` gets simplified, but `value "foo_g(Foo(1::int))"`
doesn't, even though it's a simple use of nat_of(x).
*)

consts nat_of :: "'a => nat"

abbreviation (input) nat_of_int :: "int => nat" where 
  "nat_of_int == nat"
  
defs (overloaded)
  nat_of_int_def [simp,code_unfold]: "nat_of == nat_of_int"

datatype 'a foo_d2 = Foo_d2 'a
 
fun foo_g :: "'a foo_d2 => nat" where 
  "foo_g (Foo_d2 x) = nat_of(x)"

value "nat_of(1::int)"
  (* Output: "(Suc (0::nat))" :: "nat" *)
  (* With simp_trace, this is the first rewrite:
    [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
    (term_of_class.term_of (nat_of (1::int))) 
    [1]Applying instance of rewrite rule "??.unknown":
    (nat_of == nat) 
    [1]Rewriting:
    (nat_of == nat) *)

value "foo_g(Foo_d2(1::int))"
  (* Output: "(nat_of (1::int))" :: "nat" *)
  (* With simp_trace, this is the last rewrite:
    [1]Rewriting:
    (Numeral1 == (1::int)) 
    "(nat_of (1::int))" :: "nat" *)


(******************************************************************************)
end
(******************************************************************************)