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



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"
defs (overloaded)
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"

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)


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








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