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



I finish this off and post it here in case there's something I should know about what I've done up to this point, though it is pretty much what it is.

I started with an ordered pair of type (int * int), where in practice I mainly care, hypothetically, that I can make statements about three other types, (nat*nat), (nat*int), and (int*nat). But, since the infrastructure is already there, I finally figured out how to generalize using this type:

('a::linordered_idom * 'b::linordered_ab_group_add)

Part of that is enforcing the type class in the datatype:

datatype ('a::linordered_idom,'b::linordered_ab_group_add) oI

That's nice.

If I was going to ask someone a question, it would be, "Where's the conversion function of type ('a => nat)? I couldn't find it, so I made my own."

What actually ends up coming for free, which I didn't know at first, is that I can use type nat in place of type int, even though the set of nats is not an integral domain or even a group. I surmise, from what I glanced at in the HOL source, that it's because the nats are embedded in the integers. The result is that coercions are done with the function "int".

The software figures out it should coerce nat to int, even though the constructor is using type ('a::linordered_idom * 'b::linordered_ab_group_add).

Actually, the features of jEdit can help teach one what the software does.

With `term "- (2::nat)"`, int coercion is done, and cntl-clicking on "-" takes me to the class "uminus".

With `term "0 - (2::nat)"`, no coercion is done, and cntl-clicking takes me to class "minus". Somewhere, something is registered with those type classes to allow me to use nat as types linordered_idom and linordered_ab_group_add.

Regards,
GB



(*Comments:
1) I found no general conversion function ('a => nat), so I made
   "a_nat::'a => nat" and defined it for "(int => nat)".
2) I get by default what I initially thought I had to work to get, the default part being that nat is coerced to int even though the set of nats is not an
   integral domain or a additive group.
3) I generalize and enforce the ordered pair of the datatype to be
   ('a::linordered_idom * 'b::linordered_ab_group_add).
*)

consts rat :: "'a => rat"

defs (overloaded)
  rat_of_nat_def [simp,code_unfold]: "rat == rat_of_nat"
  rat_of_int_def [simp,code_unfold]: "rat == rat_of_int"

consts a_nat :: "'a => nat"

abbreviation (input) int_of_nat :: "int => nat" where
  "int_of_nat == nat"

defs (overloaded)
  int_of_nat_def [simp,code_unfold]: "a_nat == int_of_nat"

datatype ('a::linordered_idom,'b::linordered_ab_group_add) oI =
  oIf "'a * 'b"
 |oIF "('a,'b) oI list"

fun oICq :: "('a::linordered_idom,'b::linordered_ab_group_add) oI => rat" where
  "oICq (oIf p) = (if (snd p) < 0
                     then 1/rat(fst p ^ a_nat(- snd p))
                     else rat(fst p ^ a_nat(snd p)))"
 |"oICq (oIF[]) = 1"
 |"oICq (oIF (x#xs)) = oICq x * oICq (oIF xs)"

(* (int * int) *)
theorem "oICq(oIf(a::int,b::int)) = rat(a ^ nat(b)) |
         oICq(oIf(a::int,b::int)) = (1/rat(a ^ nat(-b)))"
  by(simp)

(* (nat * int) *)
theorem "oICq(oIf(a::nat,b::int)) = rat(a ^ nat(b)) |
         oICq(oIf(a::nat,b::int)) = (1/rat(a ^ nat(-b)))"
  by(simp add: zpower_int)

(* (int * nat) *)
theorem "oICq(oIf(a::int,b::nat)) = rat(a ^ b)"
  by(simp)

(* (nat * nat) *)
theorem "oICq(oIf(a::nat,b::nat)) = rat(a ^ b)"
  by(simp add: zpower_int)





theory i131031a__v4_linordered_idom_1st_linordered_ab_group_add_2nd
imports Complex_Main
begin

(*Comments:
1) I found no general conversion function ('a => nat), so I made 
   "a_nat::'a => nat" and defined it for "(int => nat)". 
2) I get by default what I initially thought I had to work to get, the default 
   part being that nat is coerced to int even though the set of nats is not an 
   integral domain or a additive group.
3) I generalize and enforce the ordered pair of the datatype to be
   ('a::linordered_idom * 'b::linordered_ab_group_add).
*)

consts rat :: "'a => rat"

defs (overloaded)
  rat_of_nat_def [simp,code_unfold]: "rat == rat_of_nat"
  rat_of_int_def [simp,code_unfold]: "rat == rat_of_int"

consts a_nat :: "'a => nat"

abbreviation (input) int_of_nat :: "int => nat" where 
  "int_of_nat == nat"
  
defs (overloaded)
  int_of_nat_def [simp,code_unfold]: "a_nat == int_of_nat"

datatype ('a::linordered_idom,'b::linordered_ab_group_add) oI =
  oIf "'a * 'b"
 |oIF "('a,'b) oI list"
 
fun oICq :: "('a::linordered_idom,'b::linordered_ab_group_add) oI => rat" where
  "oICq (oIf p) = (if (snd p) < 0 
                     then 1/rat(fst p ^ a_nat(- snd p)) 
                     else rat(fst p ^ a_nat(snd p)))" 
 |"oICq (oIF[]) = 1"
 |"oICq (oIF (x#xs)) = oICq x * oICq (oIF xs)"

(* (int * int) *)
theorem "oICq(oIf(a::int,b::int)) = rat(a ^ nat(b)) | 
         oICq(oIf(a::int,b::int)) = (1/rat(a ^ nat(-b)))"
  by(simp) 

(* (nat * int) *)
theorem "oICq(oIf(a::nat,b::int)) = rat(a ^ nat(b)) | 
         oICq(oIf(a::nat,b::int)) = (1/rat(a ^ nat(-b)))"
  by(simp add: zpower_int)

(* (int * nat) *)  
theorem "oICq(oIf(a::int,b::nat)) = rat(a ^ b)"
  by(simp)
  
(* (nat * nat) *)  
theorem "oICq(oIf(a::nat,b::nat)) = rat(a ^ b)"
  by(simp add: zpower_int)

(******************************************************************************)
end
(******************************************************************************)








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