src/HOL/TPTP/THF_Arith.thy
author blanchet
Fri Apr 27 15:24:37 2012 +0200 (2012-04-27)
changeset 47792 804fdf0f6006
parent 47790 src/HOL/TPTP/CASC_Setup.thy@2e1636e45770
child 58042 ffa9e39763e3
permissions -rw-r--r--
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet@47792
     1
(*  Title:      HOL/TPTP/THF_Arith.thy
blanchet@42071
     2
    Author:     Jasmin Blanchette
blanchet@47792
     3
    Copyright   2011, 2012
blanchet@42071
     4
blanchet@47792
     5
Experimental setup for THF arithmetic. This is not connected with the TPTP
blanchet@47792
     6
parser yet.
blanchet@42071
     7
*)
blanchet@42071
     8
blanchet@47792
     9
theory THF_Arith
blanchet@43805
    10
imports Complex_Main
blanchet@43806
    11
begin
blanchet@43806
    12
blanchet@43806
    13
consts
blanchet@43806
    14
  is_int :: "'a \<Rightarrow> bool"
blanchet@43806
    15
  is_rat :: "'a \<Rightarrow> bool"
blanchet@43806
    16
blanchet@43806
    17
overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool"
blanchet@43806
    18
begin
blanchet@43806
    19
  definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)"
blanchet@43806
    20
end
blanchet@43806
    21
blanchet@43806
    22
overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool"
blanchet@43806
    23
begin
blanchet@43806
    24
  definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>"
blanchet@43806
    25
end
blanchet@43806
    26
blanchet@43806
    27
overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool"
blanchet@43806
    28
begin
blanchet@43806
    29
  definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>"
blanchet@43806
    30
end
blanchet@43806
    31
blanchet@43806
    32
consts
blanchet@43806
    33
  to_int :: "'a \<Rightarrow> int"
blanchet@43806
    34
  to_rat :: "'a \<Rightarrow> rat"
blanchet@43806
    35
  to_real :: "'a \<Rightarrow> real"
blanchet@43806
    36
blanchet@43806
    37
overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
blanchet@43806
    38
begin
blanchet@43806
    39
  definition "rat_to_int (q\<Colon>rat) = floor q"
blanchet@43806
    40
end
blanchet@43806
    41
blanchet@43806
    42
overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
blanchet@43806
    43
begin
blanchet@43806
    44
  definition "real_to_int (x\<Colon>real) = floor x"
blanchet@43806
    45
end
blanchet@43806
    46
blanchet@43806
    47
overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"
blanchet@42063
    48
begin
blanchet@43806
    49
  definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)"
blanchet@43806
    50
end
blanchet@43806
    51
blanchet@43806
    52
overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
blanchet@43806
    53
begin
blanchet@43806
    54
  definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)"
blanchet@43806
    55
end
blanchet@43806
    56
blanchet@43806
    57
overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
blanchet@43806
    58
begin
blanchet@43806
    59
  definition "int_to_real (n\<Colon>int) = real n"
blanchet@43806
    60
end
blanchet@43806
    61
blanchet@43806
    62
overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real"
blanchet@43806
    63
begin
blanchet@43806
    64
  definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)"
blanchet@43806
    65
end
blanchet@43806
    66
blanchet@43806
    67
declare
blanchet@43806
    68
  rat_is_int_def [simp]
blanchet@43806
    69
  real_is_int_def [simp]
blanchet@43806
    70
  real_is_rat_def [simp]
blanchet@43806
    71
  rat_to_int_def [simp]
blanchet@43806
    72
  real_to_int_def [simp]
blanchet@43806
    73
  int_to_rat_def [simp]
blanchet@43806
    74
  real_to_rat_def [simp]
blanchet@43806
    75
  int_to_real_def [simp]
blanchet@43806
    76
  rat_to_real_def [simp]
blanchet@43806
    77
blanchet@43806
    78
lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))"
blanchet@43806
    79
by (metis int_to_rat_def rat_is_int_def)
blanchet@43806
    80
blanchet@43806
    81
lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))"
blanchet@43806
    82
by (metis Ints_real_of_int int_to_real_def real_is_int_def)
blanchet@43806
    83
blanchet@43806
    84
lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))"
blanchet@43806
    85
by (metis Rats_of_rat rat_to_real_def real_is_rat_def)
blanchet@43806
    86
blanchet@43806
    87
lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
blanchet@43806
    88
by (metis injI of_rat_eq_iff rat_to_real_def)
blanchet@42063
    89
blanchet@42063
    90
end