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



On 11/4/2013 4:37 AM, Andreas Lochbihler wrote:
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.

Andreas,

Thanks for the help. It helps to get help to understand the subtleties. What I was doing in those other emails helped me here to experiment with the type variables in the class context:

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

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.

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.

The printing of numerals is bigger than me, but getting "value" to work by using [code] is something I want to start doing.

Related to those other emails, I've created these commands:

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"

These are based on the "real::'a => real" function in Real.thy.

The problem is that `value "nat_of(1::int)"` gets rewritten as "Suc 0", but a slightly more complicated use of "nat_of" doesn't get simplified with "value".

I don't know the relationship of "simp" to "code", but with "declare[[simp_trace]]", when I use "value", the output panel shows the rewriting that's being done.

Below, I give the simple example I just mentioned, along with the output of the two "value"s, and some of the simp trace. I attach the THY, which just duplicates the source I've put in this email.

Thanks for the help,
GB


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


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








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