|
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\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>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\<Colon>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\<Colon>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\<Colon>rat) = floor q" |
|
40 end |
|
41 |
|
42 overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int" |
|
43 begin |
|
44 definition "real_to_int (x\<Colon>real) = floor x" |
|
45 end |
|
46 |
|
47 overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat" |
|
48 begin |
|
49 definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)" |
|
50 end |
|
51 |
|
52 overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat" |
|
53 begin |
|
54 definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)" |
|
55 end |
|
56 |
|
57 overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real" |
|
58 begin |
|
59 definition "int_to_real (n\<Colon>int) = real n" |
|
60 end |
|
61 |
|
62 overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real" |
|
63 begin |
|
64 definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>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\<Colon>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\<Colon>int))" |
|
82 by (metis Ints_real_of_int int_to_real_def real_is_int_def) |
|
83 |
|
84 lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>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\<Colon>rat\<Rightarrow>real)" |
|
88 by (metis injI of_rat_eq_iff rat_to_real_def) |
|
89 |
|
90 end |