author | paulson |
Wed, 14 Jun 2000 18:21:25 +0200 | |
changeset 9069 | e8d530582061 |
parent 9043 | ca761fe227d8 |
child 9365 | 0cced1b20d68 |
permissions | -rw-r--r-- |
7292 | 1 |
(* Title: RealInt.ML |
2 |
ID: $Id$ |
|
3 |
Author: Jacques D. Fleuriot |
|
4 |
Copyright: 1999 University of Edinburgh |
|
5 |
Description: Embedding the integers in the reals |
|
6 |
*) |
|
7 |
||
8 |
||
9 |
Goalw [congruent_def] |
|
10 |
"congruent intrel (%p. split (%i j. realrel ^^ \ |
|
11 |
\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
|
12 |
\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"; |
|
9069 | 13 |
by (auto_tac (claset(), |
14 |
simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym, |
|
15 |
preal_of_prat_add RS sym])); |
|
7292 | 16 |
qed "real_of_int_congruent"; |
17 |
||
18 |
val real_of_int_ize = RSLIST [equiv_intrel, real_of_int_congruent]; |
|
19 |
||
20 |
Goalw [real_of_int_def] |
|
21 |
"real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \ |
|
22 |
\ Abs_real(realrel ^^ \ |
|
23 |
\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
|
24 |
\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"; |
|
25 |
by (res_inst_tac [("f","Abs_real")] arg_cong 1); |
|
9069 | 26 |
by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse, |
27 |
real_of_int_ize UN_equiv_class]) 1); |
|
7292 | 28 |
qed "real_of_int"; |
29 |
||
30 |
Goal "inj(real_of_int)"; |
|
31 |
by (rtac injI 1); |
|
32 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
|
33 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
34 |
by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD, |
|
9069 | 35 |
inj_prat_of_pnat RS injD, inj_pnat_of_nat RS injD], |
36 |
simpset() addsimps [real_of_int,preal_of_prat_add RS sym, |
|
37 |
prat_of_pnat_add RS sym,pnat_of_nat_add])); |
|
7292 | 38 |
qed "inj_real_of_int"; |
39 |
||
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
8856
diff
changeset
|
40 |
Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0"; |
7292 | 41 |
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1); |
42 |
qed "real_of_int_zero"; |
|
43 |
||
44 |
Goalw [int_def,real_one_def] "real_of_int (int 1) = 1r"; |
|
45 |
by (auto_tac (claset(), |
|
46 |
simpset() addsimps [real_of_int, |
|
47 |
preal_of_prat_add RS sym,pnat_two_eq, |
|
48 |
prat_of_pnat_add RS sym,pnat_one_iff RS sym])); |
|
49 |
qed "real_of_int_one"; |
|
50 |
||
51 |
Goal "real_of_int x + real_of_int y = real_of_int (x + y)"; |
|
52 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
|
53 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
54 |
by (auto_tac (claset(),simpset() addsimps [real_of_int, |
|
55 |
preal_of_prat_add RS sym,prat_of_pnat_add RS sym, |
|
56 |
zadd,real_add,pnat_of_nat_add] @ pnat_add_ac)); |
|
57 |
qed "real_of_int_add"; |
|
58 |
||
59 |
Goal "-real_of_int x = real_of_int (-x)"; |
|
60 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
|
9069 | 61 |
by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus])); |
7292 | 62 |
qed "real_of_int_minus"; |
63 |
||
64 |
Goalw [zdiff_def,real_diff_def] |
|
65 |
"real_of_int x - real_of_int y = real_of_int (x - y)"; |
|
9069 | 66 |
by (simp_tac (simpset() addsimps [real_of_int_add, real_of_int_minus]) 1); |
7292 | 67 |
qed "real_of_int_diff"; |
68 |
||
69 |
Goal "real_of_int x * real_of_int y = real_of_int (x * y)"; |
|
70 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
|
71 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
72 |
by (auto_tac (claset(),simpset() addsimps [real_of_int, |
|
73 |
real_mult,zmult,preal_of_prat_mult RS sym,pnat_of_nat_mult, |
|
74 |
prat_of_pnat_mult RS sym,preal_of_prat_add RS sym, |
|
75 |
prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac |
|
76 |
@ pnat_add_ac)); |
|
77 |
qed "real_of_int_mult"; |
|
78 |
||
79 |
Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r"; |
|
80 |
by (simp_tac (simpset() addsimps [real_of_int_one RS sym, |
|
8856 | 81 |
real_of_int_add,zadd_int] @ zadd_ac) 1); |
7292 | 82 |
qed "real_of_int_Suc"; |
83 |
||
84 |
(* relating two of the embeddings *) |
|
85 |
Goal "real_of_int (int n) = real_of_nat n"; |
|
86 |
by (induct_tac "n" 1); |
|
8856 | 87 |
by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, |
88 |
real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc]))); |
|
89 |
by (Simp_tac 1); |
|
7292 | 90 |
qed "real_of_int_real_of_nat"; |
91 |
||
92 |
Goal "~neg z ==> real_of_nat (nat z) = real_of_int z"; |
|
93 |
by (asm_simp_tac (simpset() addsimps [not_neg_nat, |
|
9069 | 94 |
real_of_int_real_of_nat RS sym]) 1); |
7292 | 95 |
qed "real_of_nat_real_of_int"; |
96 |
||
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
8856
diff
changeset
|
97 |
Goal "(real_of_int x = 0) = (x = int 0)"; |
7292 | 98 |
by (auto_tac (claset() addIs [inj_real_of_int RS injD], |
9069 | 99 |
HOL_ss addsimps [real_of_int_zero])); |
7292 | 100 |
qed "real_of_int_zero_cancel"; |
101 |
Addsimps [real_of_int_zero_cancel]; |
|
102 |
||
103 |
Goal "real_of_int x < real_of_int y ==> x < y"; |
|
104 |
by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); |
|
105 |
by (auto_tac (claset(), |
|
106 |
simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym, |
|
107 |
real_of_int_real_of_nat, |
|
9069 | 108 |
linorder_not_le RS sym])); |
7292 | 109 |
qed "real_of_int_less_cancel"; |
110 |
||
9069 | 111 |
Goal "(real_of_int x = real_of_int y) = (x = y)"; |
112 |
by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1); |
|
113 |
qed "real_of_int_eq_iff"; |
|
114 |
AddIffs [real_of_int_eq_iff]; |
|
115 |
||
7292 | 116 |
Goal "x < y ==> (real_of_int x < real_of_int y)"; |
9069 | 117 |
by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
118 |
by (auto_tac (claset() addSDs [real_of_int_less_cancel], |
|
119 |
simpset() addsimps [order_le_less])); |
|
7292 | 120 |
qed "real_of_int_less_mono"; |
121 |
||
122 |
Goal "(real_of_int x < real_of_int y) = (x < y)"; |
|
9069 | 123 |
by (blast_tac (claset() addIs [real_of_int_less_cancel, |
124 |
real_of_int_less_mono]) 1); |
|
7292 | 125 |
qed "real_of_int_less_iff"; |
9069 | 126 |
AddIffs [real_of_int_less_iff]; |
7292 | 127 |
|
128 |
Goal "(real_of_int x <= real_of_int y) = (x <= y)"; |
|
9069 | 129 |
by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
7292 | 130 |
qed "real_of_int_le_iff"; |
131 |
Addsimps [real_of_int_le_iff]; |