Theory THF_Arith

theory THF_Arith
imports Complex_Main
(*  Title:      HOL/TPTP/THF_Arith.thy
Author: Jasmin Blanchette
Copyright 2011, 2012

Experimental setup for THF arithmetic. This is not connected with the TPTP
parser yet.
*)


theory THF_Arith
imports Complex_Main
begin

consts
is_int :: "'a => bool"
is_rat :: "'a => bool"

overloading rat_is_int "is_int :: rat => bool"
begin
definition "rat_is_int (q::rat) <-> (∃n::int. q = of_int n)"
end

overloading real_is_int "is_int :: real => bool"
begin
definition "real_is_int (x::real) <-> x ∈ \<int>"
end

overloading real_is_rat "is_rat :: real => bool"
begin
definition "real_is_rat (x::real) <-> x ∈ \<rat>"
end

consts
to_int :: "'a => int"
to_rat :: "'a => rat"
to_real :: "'a => real"

overloading rat_to_int "to_int :: rat => int"
begin
definition "rat_to_int (q::rat) = floor q"
end

overloading real_to_int "to_int :: real => int"
begin
definition "real_to_int (x::real) = floor x"
end

overloading int_to_rat "to_rat :: int => rat"
begin
definition "int_to_rat (n::int) = (of_int n::rat)"
end

overloading real_to_rat "to_rat :: real => rat"
begin
definition "real_to_rat (x::real) = (inv real x::rat)"
end

overloading int_to_real "to_real :: int => real"
begin
definition "int_to_real (n::int) = real n"
end

overloading rat_to_real "to_real :: rat => real"
begin
definition "rat_to_real (x::rat) = (of_rat x::real)"
end

declare
rat_is_int_def [simp]
real_is_int_def [simp]
real_is_rat_def [simp]
rat_to_int_def [simp]
real_to_int_def [simp]
int_to_rat_def [simp]
real_to_rat_def [simp]
int_to_real_def [simp]
rat_to_real_def [simp]

lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n::int))"
by (metis int_to_rat_def rat_is_int_def)

lemma to_real_is_int [intro, simp]: "is_int (to_real (n::int))"
by (metis Ints_real_of_int int_to_real_def real_is_int_def)

lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q::rat))"
by (metis Rats_of_rat rat_to_real_def real_is_rat_def)

lemma inj_of_rat [intro, simp]: "inj (of_rat::rat=>real)"
by (metis injI of_rat_eq_iff rat_to_real_def)

end