author | paulson |
Thu, 06 Mar 2003 15:02:51 +0100 | |
changeset 13849 | 2584233cf3ef |
parent 12613 | 279facb4253a |
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] |
|
10834 | 10 |
"congruent intrel (%p. (%(i,j). realrel `` \ |
7292 | 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 |
Goalw [real_of_int_def] |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
19 |
"real (Abs_Integ (intrel `` {(i, j)})) = \ |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
20 |
\ Abs_REAL(realrel `` \ |
7292 | 21 |
\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
22 |
\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"; |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
23 |
by (res_inst_tac [("f","Abs_REAL")] arg_cong 1); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
24 |
by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse, |
9391 | 25 |
[equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1); |
7292 | 26 |
qed "real_of_int"; |
27 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
28 |
Goal "inj(real :: int => real)"; |
7292 | 29 |
by (rtac injI 1); |
30 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
|
31 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
32 |
by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD, |
|
9069 | 33 |
inj_prat_of_pnat RS injD, inj_pnat_of_nat RS injD], |
34 |
simpset() addsimps [real_of_int,preal_of_prat_add RS sym, |
|
35 |
prat_of_pnat_add RS sym,pnat_of_nat_add])); |
|
7292 | 36 |
qed "inj_real_of_int"; |
37 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
38 |
Goalw [int_def,real_zero_def] "real (int 0) = 0"; |
7292 | 39 |
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1); |
40 |
qed "real_of_int_zero"; |
|
41 |
||
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
42 |
Goal "real (1::int) = (1::real)"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
43 |
by (stac (int_1 RS sym) 1); |
7292 | 44 |
by (auto_tac (claset(), |
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
45 |
simpset() addsimps [int_def, real_one_def, real_of_int, |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
46 |
preal_of_prat_add RS sym,pnat_two_eq, |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
47 |
prat_of_pnat_add RS sym, pnat_one_iff RS sym])); |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
48 |
qed "real_of_one"; |
7292 | 49 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
50 |
Goal "real (x::int) + real y = real (x + y)"; |
7292 | 51 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
52 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
53 |
by (auto_tac (claset(), |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
54 |
simpset() addsimps [real_of_int, preal_of_prat_add RS sym, |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
55 |
prat_of_pnat_add RS sym, zadd,real_add, |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
56 |
pnat_of_nat_add] @ pnat_add_ac)); |
7292 | 57 |
qed "real_of_int_add"; |
10784 | 58 |
Addsimps [real_of_int_add RS sym]; |
7292 | 59 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
60 |
Goal "-real (x::int) = real (-x)"; |
7292 | 61 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
9069 | 62 |
by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus])); |
7292 | 63 |
qed "real_of_int_minus"; |
10784 | 64 |
Addsimps [real_of_int_minus RS sym]; |
7292 | 65 |
|
66 |
Goalw [zdiff_def,real_diff_def] |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
67 |
"real (x::int) - real y = real (x - y)"; |
10784 | 68 |
by (simp_tac (HOL_ss addsimps [real_of_int_add, real_of_int_minus]) 1); |
7292 | 69 |
qed "real_of_int_diff"; |
10784 | 70 |
Addsimps [real_of_int_diff RS sym]; |
7292 | 71 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
72 |
Goal "real (x::int) * real y = real (x * y)"; |
7292 | 73 |
by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
74 |
by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
|
10784 | 75 |
by (auto_tac (claset(), |
76 |
simpset() addsimps [real_of_int, real_mult,zmult, |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
77 |
preal_of_prat_mult RS sym,pnat_of_nat_mult, |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
78 |
prat_of_pnat_mult RS sym,preal_of_prat_add RS sym, |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
79 |
prat_of_pnat_add RS sym,pnat_of_nat_add] @ |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
80 |
mult_ac @ add_ac @ pnat_add_ac)); |
7292 | 81 |
qed "real_of_int_mult"; |
10784 | 82 |
Addsimps [real_of_int_mult RS sym]; |
7292 | 83 |
|
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11597
diff
changeset
|
84 |
Goal "real (int (Suc n)) = real (int n) + (1::real)"; |
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
85 |
by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @ |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
86 |
zadd_ac) 1); |
7292 | 87 |
qed "real_of_int_Suc"; |
88 |
||
89 |
(* relating two of the embeddings *) |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
90 |
Goal "real (int n) = real n"; |
7292 | 91 |
by (induct_tac "n" 1); |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
92 |
by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, real_of_nat_zero, |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
93 |
real_of_int_Suc,real_of_nat_Suc]))); |
8856 | 94 |
by (Simp_tac 1); |
7292 | 95 |
qed "real_of_int_real_of_nat"; |
96 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
97 |
Goal "~neg z ==> real (nat z) = real z"; |
13849 | 98 |
by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1); |
7292 | 99 |
qed "real_of_nat_real_of_int"; |
100 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
101 |
Goal "(real x = 0) = (x = int 0)"; |
7292 | 102 |
by (auto_tac (claset() addIs [inj_real_of_int RS injD], |
9069 | 103 |
HOL_ss addsimps [real_of_int_zero])); |
7292 | 104 |
qed "real_of_int_zero_cancel"; |
105 |
Addsimps [real_of_int_zero_cancel]; |
|
106 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
107 |
Goal "real (x::int) < real y ==> x < y"; |
7292 | 108 |
by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); |
109 |
by (auto_tac (claset(), |
|
110 |
simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym, |
|
111 |
real_of_int_real_of_nat, |
|
9069 | 112 |
linorder_not_le RS sym])); |
7292 | 113 |
qed "real_of_int_less_cancel"; |
114 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
115 |
Goal "(real (x::int) = real y) = (x = y)"; |
9069 | 116 |
by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1); |
11597
cd6d2eddf75f
renamed real_of_int_eq_iff to real_of_int_inject;
wenzelm
parents:
10919
diff
changeset
|
117 |
qed "real_of_int_inject"; |
cd6d2eddf75f
renamed real_of_int_eq_iff to real_of_int_inject;
wenzelm
parents:
10919
diff
changeset
|
118 |
AddIffs [real_of_int_inject]; |
9069 | 119 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
120 |
Goal "x < y ==> (real (x::int) < real y)"; |
9069 | 121 |
by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
122 |
by (auto_tac (claset() addSDs [real_of_int_less_cancel], |
|
123 |
simpset() addsimps [order_le_less])); |
|
7292 | 124 |
qed "real_of_int_less_mono"; |
125 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
126 |
Goal "(real (x::int) < real y) = (x < y)"; |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
127 |
by (blast_tac (claset() addDs [real_of_int_less_cancel] |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
128 |
addIs [real_of_int_less_mono]) 1); |
7292 | 129 |
qed "real_of_int_less_iff"; |
9069 | 130 |
AddIffs [real_of_int_less_iff]; |
7292 | 131 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
132 |
Goal "(real (x::int) <= real y) = (x <= y)"; |
9069 | 133 |
by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
7292 | 134 |
qed "real_of_int_le_iff"; |
135 |
Addsimps [real_of_int_le_iff]; |
|
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
136 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
137 |
Addsimps [real_of_one]; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11713
diff
changeset
|
138 |