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