# [isabelle] Looking for rat & int powers to use with linordered_idom

• 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,

```
What I did is create a function based on integers. I then decided to generalize it using linordered_idom, which is the type class linear ordered integral domain.
```
```
A general question is, if you want to look at my theory, is there something I should be doing to do things better? I guess I got some of the basics right.
```
My three basic questions are:

1) Is there an integer powers operator?

```
2) Is there a rat::('a => rat) function, like there's a real::('a => real) function. I didn't find one, so I had to add a few commands to get one.
```
```
3) The "value" for my function is a complicated expression. Is there an easy way to get "value" to simplify it, like when I use "simp" with "theorem".
```
```
I attach a simplified theory with comments, and I include the text in this email, where I repeat the questions I just asked.
```
Thanks,
GB

(*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 ⇒ real" where "real_of_int == of_int"
real_of_int_def [code_unfold]: "real == real_of_int"
declare [[coercion_enabled]]
declare [[coercion "real::int⇒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"

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)

```
```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"
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"

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

```

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