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