Email Gateway (Aug 19 2022 at 12:51): Email Gateway (Aug 19 2022 at 12:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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)
i131031a__v3_simple_fun_linordered_idom_to_rat.thy
Last updated: Apr 24 2024 at 01:07 UTC