*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Looking for rat & int powers to use with linordered_idom*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Sun, 03 Nov 2013 20:38:12 -0600*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Hi,

My three basic questions are: 1) Is there an integer powers operator?

Thanks, GB (*Questions:

function oZCq, which I use after comment __2__. 2) Is there a rat function of type ('a => rat), as I talk about in comments 4, 5, and 6. As I talk about, I used the function real::('a => real) as an example on how to define my rat below.

answer when I use my oICq function, as it is used after comment __8__. 4) Is there something I should be doing here that would make it better? *) (*__1__) I start with a non-generalized datatype based on (int * int).*) datatype oZ = oZf "int * int" |oZF "oZ list"

to do integer powers, so I use an if/then statement.*) fun oZCq :: "oZ => rat" where "oZCq (oZf p) = (if (snd p) < 0 then 1/of_int(fst p ^ nat(- snd p)) else of_int(fst p ^ nat(snd p)))" |"oZCq (oZF[]) = 1" |"oZCq (oZF(x#xs)) = oZCq x * oZCq (oZF xs)" value "oZCq(oZF[oZf(2,-2),oZf(2,3)])" (* 2 *) value "oZCq(oZF[oZf(2,-3),oZf(2,2)])" (* 1/2 *)

which is a linear ordered integral domain. The problem is that I found no function ('a => rat). There is, however, the function real::('a => real). I

to know how to create my rat function.*)

conversion, and for the real::(int => real) definition. It is taken from lines 1021-1042. consts (*overloaded constant for injecting other types into "real"*) real :: "'a => real" abbreviation real_of_int :: "int ⇒ real" where "real_of_int == of_int" defs (overloaded) real_of_int_def [code_unfold]: "real == real_of_int" declare [[coercion_enabled]] declare [[coercion "real::int⇒real"]] *)

it shows that rat_of_int::(int => rat) has already been defined. 0758: abbreviation rat_of_int :: "int => rat" where "rat_of_int == of_int" 0898: definition of_int :: "int => rat" where [code_abbrev]: "of_int = Int.of_int" *)

consts rat :: "'a => rat" defs (overloaded) rat_of_int_def [simp,code_unfold]: "rat == rat_of_int"

computation function to be of type ('a::linordered_idom oI => rat).*) datatype 'a oI = oIf "'a * int" |oIF "'a oI list" fun oICq :: "'a::linordered_idom oI => rat" where "oICq (oIf p) = (if (snd p) < 0 then 1/rat(fst p ^ nat(- snd p)) else rat(fst p ^ nat(snd p)))" |"oICq (oIF[]) = 1" |"oICq (oIF (x#xs)) = oICq x * oICq (oIF xs)"

done is a total loser. It's hard to tell. The return values are partially simplified, but they are still complicated expressions.*) value "rat(1::int)" value "rat(1::'a::linordered_idom)" value "oICq(oIF[oIf(2,-2),oIf(2,3)])" (* SB 2 *) value "oICq(oIF[oIf(2,-3),oIf(2,2)])" (* SB 1/2 *) value "oICq(oIF[oIf(2::int,-2),oIf(2,3)])" (* SB 2 rat *) value "oICq(oIF[oIf(2::int,-3),oIf(2,2)])" (* SB 1/2 rat *)

expression, so I resort to using simp to look at the computations.*)

apply(simp) oops

apply(simp) oops theorem "oICq(oIF[oIf(2::int,-2),oIf(2,3)]) = z" (* z = (2::rat) *) apply(simp) oops

apply(simp) oops theorem "oICq(oIF[oIf(2::int,-2),oIf(2,3)]) = 2" by(simp)

theory i131031a__v3_simple_fun_linordered_idom_to_rat imports Complex_Main begin (*Questions: 1) Is there an integer powers operator I can use to get rid of my if/then in the function oZCq, which I use after comment __2__. 2) Is there a rat function of type ('a => rat), as I talk about in comments 4, 5, and 6. As I talk about, I used the function real::('a => real) as an example on how to define my rat below. 3) Is there something easy I can do to get the value method to return a simplified answer when I use my oICq function, as it is used after comment __8__. 4) Is there something I should be doing here that would make it better? *) (*__1__) I start with a non-generalized datatype based on (int * int).*) datatype oZ = oZf "int * int" |oZF "oZ list" (*__2__) I compute a recursive list or pairs of int. I found no HOL operator to do integer powers, so I use an if/then statement.*) fun oZCq :: "oZ => rat" where "oZCq (oZf p) = (if (snd p) < 0 then 1/of_int(fst p ^ nat(- snd p)) else of_int(fst p ^ nat(snd p)))" |"oZCq (oZF[]) = 1" |"oZCq (oZF(x#xs)) = oZCq x * oZCq (oZF xs)" value "oZCq(oZF[oZf(2,-2),oZf(2,3)])" (* 2 *) value "oZCq(oZF[oZf(2,-3),oZf(2,2)])" (* 1/2 *) (*__3__) Instead of using integers, I want to use type class linordered_idom, which is a linear ordered integral domain. The problem is that I found no function ('a => rat). There is, however, the function real::('a => real). I use that as an example to make me an overloaded rat::('a => rat), and I define rat::(int => rat). The following shows what I found from Rat.thy and Real.thy to know how to create my rat function.*) (*__4__) From Real.thy: Here is source showing what's done for the ('a => real) conversion, and for the real::(int => real) definition. It is taken from lines 1021-1042. consts (*overloaded constant for injecting other types into "real"*) real :: "'a => real" abbreviation real_of_int :: "int \<Rightarrow> real" where "real_of_int == of_int" defs (overloaded) real_of_int_def [code_unfold]: "real == real_of_int" declare [[coercion_enabled]] declare [[coercion "real::int\<Rightarrow>real"]] *) (*__5__) In Rat.thy, I found nothing implemented for ('a => rat) conversion, but it shows that rat_of_int::(int => rat) has already been defined. 0758: abbreviation rat_of_int :: "int => rat" where "rat_of_int == of_int" 0898: definition of_int :: "int => rat" where [code_abbrev]: "of_int = Int.of_int" *) (*__6__) I decide that maybe I only need to add the following two commands.*) consts rat :: "'a => rat" defs (overloaded) rat_of_int_def [simp,code_unfold]: "rat == rat_of_int" (*__7__) I make a new datatype, "'a oI", and it seems I can now generalize my computation function to be of type ('a::linordered_idom oI => rat).*) datatype 'a oI = oIf "'a * int" |oIF "'a oI list" fun oICq :: "'a::linordered_idom oI => rat" where "oICq (oIf p) = (if (snd p) < 0 then 1/rat(fst p ^ nat(- snd p)) else rat(fst p ^ nat(snd p)))" |"oICq (oIF[]) = 1" |"oICq (oIF (x#xs)) = oICq x * oICq (oIF xs)" (*__8__) I try out a few examples, some using int, to find out whether what I've done is a total loser. It's hard to tell. The return values are partially simplified, but they are still complicated expressions.*) value "rat(1::int)" value "rat(1::'a::linordered_idom)" value "oICq(oIF[oIf(2,-2),oIf(2,3)])" (* SB 2 *) value "oICq(oIF[oIf(2,-3),oIf(2,2)])" (* SB 1/2 *) value "oICq(oIF[oIf(2::int,-2),oIf(2,3)])" (* SB 2 rat *) value "oICq(oIF[oIf(2::int,-3),oIf(2,2)])" (* SB 1/2 rat *) (*__9__) As I said, the output of value when I use oICq is a big complicated expression, so I resort to using simp to look at the computations.*) theorem "oICq(oIF[oIf(2,-2),oIf(2,3)])=z" (* (rat(8::'a))/(rat (4::'a)) = z *) apply(simp) oops theorem "oICq(oIF[oIf(2,2),oIf(2,-3)])=z" (* (rat(8::'a))/(rat (4::'a)) = z *) apply(simp) oops theorem "oICq(oIF[oIf(2::int,-2),oIf(2,3)]) = z" (* z = (2::rat) *) apply(simp) oops theorem "oICq(oIF[oIf(2::int,-3),oIf(2,2)]) = z" (* (z * (2::rat)) = (1::rat) *) apply(simp) oops theorem "oICq(oIF[oIf(2::int,-2),oIf(2,3)]) = 2" by(simp) (******************************************************************************) end (******************************************************************************)

**Follow-Ups**:**Re: [isabelle] Looking for rat & int powers to use with linordered_idom***From:*Gottfried Barrow

- Previous by Date: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Date: Re: [isabelle] Looking for rat & int powers to use with linordered_idom
- Previous by Thread: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Thread: Re: [isabelle] Looking for rat & int powers to use with linordered_idom
- 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