1 (* Title: RealInt.thy |
|
2 ID: $Id$ |
|
3 Author: Jacques D. Fleuriot |
|
4 Copyright: 1999 University of Edinburgh |
|
5 *) |
|
6 |
|
7 header{*Embedding the Integers into the Reals*} |
|
8 |
|
9 theory RealInt = RealDef: |
|
10 |
|
11 defs (overloaded) |
|
12 real_of_int_def: |
|
13 "real z == Abs_REAL(UN (i,j): Rep_Integ z. realrel `` |
|
14 {(preal_of_prat(prat_of_pnat(pnat_of_nat i)), |
|
15 preal_of_prat(prat_of_pnat(pnat_of_nat j)))})" |
|
16 |
|
17 |
|
18 lemma real_of_int_congruent: |
|
19 "congruent intrel (%p. (%(i,j). realrel `` |
|
20 {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), |
|
21 preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)" |
|
22 apply (unfold congruent_def) |
|
23 apply (auto simp add: pnat_of_nat_add prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]) |
|
24 done |
|
25 |
|
26 lemma real_of_int: |
|
27 "real (Abs_Integ (intrel `` {(i, j)})) = |
|
28 Abs_REAL(realrel `` |
|
29 {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), |
|
30 preal_of_prat (prat_of_pnat (pnat_of_nat j)))})" |
|
31 apply (unfold real_of_int_def) |
|
32 apply (rule_tac f = Abs_REAL in arg_cong) |
|
33 apply (simp add: realrel_in_real [THEN Abs_REAL_inverse] |
|
34 UN_equiv_class [OF equiv_intrel real_of_int_congruent]) |
|
35 done |
|
36 |
|
37 lemma inj_real_of_int: "inj(real :: int => real)" |
|
38 apply (rule inj_onI) |
|
39 apply (rule_tac z = x in eq_Abs_Integ) |
|
40 apply (rule_tac z = y in eq_Abs_Integ) |
|
41 apply (auto dest!: inj_preal_of_prat [THEN injD] inj_prat_of_pnat [THEN injD] |
|
42 inj_pnat_of_nat [THEN injD] |
|
43 simp add: real_of_int preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) |
|
44 done |
|
45 |
|
46 lemma real_of_int_zero: "real (int 0) = 0" |
|
47 apply (unfold int_def real_zero_def) |
|
48 apply (simp add: real_of_int preal_add_commute) |
|
49 done |
|
50 |
|
51 lemma real_of_one: "real (1::int) = (1::real)" |
|
52 apply (subst int_1 [symmetric]) |
|
53 apply (auto simp add: int_def real_one_def real_of_int preal_of_prat_add [symmetric] pnat_two_eq prat_of_pnat_add [symmetric] pnat_one_iff [symmetric]) |
|
54 done |
|
55 |
|
56 lemma real_of_int_add: "real (x::int) + real y = real (x + y)" |
|
57 apply (rule_tac z = x in eq_Abs_Integ) |
|
58 apply (rule_tac z = y in eq_Abs_Integ) |
|
59 apply (auto simp add: real_of_int preal_of_prat_add [symmetric] |
|
60 prat_of_pnat_add [symmetric] zadd real_add pnat_of_nat_add pnat_add_ac) |
|
61 done |
|
62 declare real_of_int_add [symmetric, simp] |
|
63 |
|
64 lemma real_of_int_minus: "-real (x::int) = real (-x)" |
|
65 apply (rule_tac z = x in eq_Abs_Integ) |
|
66 apply (auto simp add: real_of_int real_minus zminus) |
|
67 done |
|
68 declare real_of_int_minus [symmetric, simp] |
|
69 |
|
70 lemma real_of_int_diff: |
|
71 "real (x::int) - real y = real (x - y)" |
|
72 apply (unfold zdiff_def real_diff_def) |
|
73 apply (simp only: real_of_int_add real_of_int_minus) |
|
74 done |
|
75 declare real_of_int_diff [symmetric, simp] |
|
76 |
|
77 lemma real_of_int_mult: "real (x::int) * real y = real (x * y)" |
|
78 apply (rule_tac z = x in eq_Abs_Integ) |
|
79 apply (rule_tac z = y in eq_Abs_Integ) |
|
80 apply (auto simp add: real_of_int real_mult zmult |
|
81 preal_of_prat_mult [symmetric] pnat_of_nat_mult |
|
82 prat_of_pnat_mult [symmetric] preal_of_prat_add [symmetric] |
|
83 prat_of_pnat_add [symmetric] pnat_of_nat_add mult_ac add_ac pnat_add_ac) |
|
84 done |
|
85 declare real_of_int_mult [symmetric, simp] |
|
86 |
|
87 lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)" |
|
88 by (simp add: real_of_one [symmetric] zadd_int add_ac) |
|
89 |
|
90 declare real_of_one [simp] |
|
91 |
|
92 (* relating two of the embeddings *) |
|
93 lemma real_of_int_real_of_nat: "real (int n) = real n" |
|
94 apply (induct_tac "n") |
|
95 apply (simp_all only: real_of_int_zero real_of_nat_zero real_of_int_Suc real_of_nat_Suc) |
|
96 done |
|
97 |
|
98 lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z" |
|
99 by (simp add: not_neg_eq_ge_0 real_of_int_real_of_nat [symmetric]) |
|
100 |
|
101 lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = int 0)" |
|
102 by (auto intro: inj_real_of_int [THEN injD] |
|
103 simp only: real_of_int_zero) |
|
104 |
|
105 lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y" |
|
106 apply (rule ccontr, drule linorder_not_less [THEN iffD1]) |
|
107 apply (auto simp add: zle_iff_zadd real_of_int_add [symmetric] real_of_int_real_of_nat linorder_not_le [symmetric]) |
|
108 apply (subgoal_tac "~ real y + 0 \<le> real y + real n") |
|
109 prefer 2 apply simp |
|
110 apply (simp only: add_le_cancel_left, simp) |
|
111 done |
|
112 |
|
113 lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" |
|
114 by (blast dest!: inj_real_of_int [THEN injD]) |
|
115 |
|
116 lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)" |
|
117 apply (simp add: linorder_not_le [symmetric]) |
|
118 apply (auto dest!: real_of_int_less_cancel simp add: order_le_less) |
|
119 done |
|
120 |
|
121 lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)" |
|
122 by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono) |
|
123 |
|
124 lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)" |
|
125 by (simp add: linorder_not_less [symmetric]) |
|
126 |
|
127 ML |
|
128 {* |
|
129 val real_of_int_congruent = thm"real_of_int_congruent"; |
|
130 val real_of_int = thm"real_of_int"; |
|
131 val inj_real_of_int = thm"inj_real_of_int"; |
|
132 val real_of_int_zero = thm"real_of_int_zero"; |
|
133 val real_of_one = thm"real_of_one"; |
|
134 val real_of_int_add = thm"real_of_int_add"; |
|
135 val real_of_int_minus = thm"real_of_int_minus"; |
|
136 val real_of_int_diff = thm"real_of_int_diff"; |
|
137 val real_of_int_mult = thm"real_of_int_mult"; |
|
138 val real_of_int_Suc = thm"real_of_int_Suc"; |
|
139 val real_of_int_real_of_nat = thm"real_of_int_real_of_nat"; |
|
140 val real_of_nat_real_of_int = thm"real_of_nat_real_of_int"; |
|
141 val real_of_int_zero_cancel = thm"real_of_int_zero_cancel"; |
|
142 val real_of_int_less_cancel = thm"real_of_int_less_cancel"; |
|
143 val real_of_int_inject = thm"real_of_int_inject"; |
|
144 val real_of_int_less_mono = thm"real_of_int_less_mono"; |
|
145 val real_of_int_less_iff = thm"real_of_int_less_iff"; |
|
146 val real_of_int_le_iff = thm"real_of_int_le_iff"; |
|
147 *} |
|
148 |
|
149 |
|
150 end |
|