*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Looking for rat & int powers to use with linordered_idom*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 04 Nov 2013 01:30:07 -0600*In-reply-to*: <52770894.8000805@gmx.com>*References*: <52770894.8000805@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

('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.

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

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)".

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"

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

**References**:**[isabelle] Looking for rat & int powers to use with linordered_idom***From:*Gottfried Barrow

- Previous by Date: [isabelle] Looking for rat & int powers to use with linordered_idom
- Next by Date: [isabelle] Code generation for "int" in Isabelle 2013-1 RC3
- Previous by Thread: [isabelle] Looking for rat & int powers to use with linordered_idom
- Next by Thread: [isabelle] Code generation for "int" in Isabelle 2013-1 RC3
- 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