*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 04 Nov 2013 11:03:48 -0600*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <527778FA.4080209@inf.ethz.ch>*References*: <5276C6E4.9050903@gmx.com> <527778FA.4080209@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 11/4/2013 4:37 AM, Andreas Lochbihler wrote:

You are confused by Isabelle's type inference. Inside a type classcontext, 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". Inyour theorem, you try to instantiate 'a to int. This makes Isabellethink that you want to refer to the exported version of foo_f, so youhave to add the exported foo_f.simps rules as well.

Andreas,

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

value uses a different set of different equations for normalisingterms, 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.

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.

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

**Follow-Ups**:**Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Florian Haftmann

**References**:**[isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Gottfried Barrow

**Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Date: Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer
- Previous by Thread: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Thread: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list