theory i131031a__context_slower__needs_qualified_simp__numeral_print
imports Complex_Main
        "~~/src/HOL/Library/Code_Target_Numeral"
(******************************************************************************)
begin
(******************************************************************************)

(*I have three questions related to the 6 comments in the source below, and which 
  are marked 1a, 1b, 2a, 2b, 3a, and 3b, though the comments aren't in that order.

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?
   
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?*)


datatype 'a foo_d = Foo_d 'a

context linordered_idom
begin
(*___1a__ It takes about 0.7 second to process foo_f in this context.*)
 
fun foo_f :: "'a foo_d => real" where
  "foo_f (Foo_d x) = real x"

(*___2a__ Inside, foo_f.simps must be used with the fully qualified name, even
  though the output message shows it's present as a rewrite rule.*)  
  
theorem "foo_f (Foo_d (1::int)) = (1::real)"
apply(simp add: foo_f.simps)
  (*OUTPUT: Ignoring duplicate rewrite rule... Failed to apply proof method...*)
apply(simp add: linordered_idom_class.foo_f.simps)
done
end

(*___2b__ Outside, foo_f.simps works without the fully qualified name.*)

theorem "foo_f (Foo_d (1::int)) = (1::real)"
  by(simp)

(*___1b__ It takes about 0.1 second to process foo_f2 in the global context.*)  

fun foo_f2 :: "'a::linordered_idom foo_d => real" where
  "foo_f2 (Foo_d x) = real x"
  
(*___3a__ Value prints numerals as sums of 1. Importing Code_Target_Numeral.thy
  doesn't help.*)
declare[[show_sorts=true]]
value "foo_f(Foo_d(2 * 2))"
  (*OUTPUT:
    "real (((1::'a::linordered_idom) + (1::'a::linordered_idom)) *
           ((1::'a::linordered_idom) + (1::'a::linordered_idom)))"
      :: "real"*)

(*___3b__ But simp prints numerals in the nice form.*)
theorem "foo_f(Foo_d(2 * 2)) = (4::real)"
apply(simp)
  (*OUTPUT:
    goal (1 subgoal):
    1. real (4\<Colon>'a) = (4\<Colon>real)*)  
oops


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