Quellcode-Bibliothek THF_Arith.thy Sprache: Isabelle

(*  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 \<equiv> "is_int :: rat \<Rightarrow> bool"
begin
  definition "rat_is_int (q::rat) \ (\n::int. q = of_int n)"
end

overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool"
begin
  definition "real_is_int (x::real) \ x \ \"
end

overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool"
begin
  definition "real_is_rat (x::real) \ x \ \"
end

consts
  to_int :: "'a \ int"
  to_rat :: "'a \ rat"
  to_real :: "'a \ real"

overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
begin
  definition "rat_to_int (q::rat) = \q\"
end

overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
begin
  definition "real_to_int (x::real) = \x\"
end

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

overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
begin
  definition "real_to_rat (x::real) = (inv of_rat x::rat)"
end

overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
begin
  definition "int_to_real (n::int) = real_of_int n"
end

overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> 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_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)

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.