RealFieldContextScript.sml
1Theory RealFieldContext[bare]
2Ancestors
3 real marker
4Libs
5 HolKernel Parse boolLib bossLib
6 jrhUtils RealArith realSimps
7
8(* ------------------------------------------------------------------------- *)
9(* Lemmas RealField.sml formerly proved as it loaded. *)
10(* ------------------------------------------------------------------------- *)
11
12Theorem REAL_INT_RAT_pth:
13 (&x = &x / (&1 :real)) /\
14 (~(&x) = ~(&x) / &1) /\
15 (unint (&x / &y :real) = &x / &y) /\
16 (~unint (&x / &y :real) = ~(&x) / &y)
17Proof
18 REWRITE_TAC [REAL_OVER1, markerTheory.unint_def] THEN
19 REWRITE_TAC [real_div, REAL_MUL_LNEG]
20QED
21
22Theorem REAL_RAT_LE_pth:
23 &0 < y1 ==> &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)
24Proof REWRITE_TAC [AND_IMP_INTRO, RAT_LEMMA4]
25QED
26
27Theorem REAL_RAT_LT_pth:
28 &0 < y1 ==> &0 < y2 ==> (x1 / y1 < x2 / y2 <=> x1 * y2 < x2 * y1)
29Proof
30 REWRITE_TAC [AND_IMP_INTRO] THEN
31 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
32 [GSYM REAL_NOT_LE] THEN
33 SIMP_TAC bool_ss [tautLib.TAUT `(~a <=> ~b) <=> (a <=> b)`, RAT_LEMMA4]
34QED
35
36Theorem REAL_RAT_EQ_pth:
37 &0 < y1 ==> &0 < y2 ==> ((x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1))
38Proof REWRITE_TAC [AND_IMP_INTRO, RAT_LEMMA5]
39QED
40
41Theorem REAL_RAT_NEG_pth:
42 (~(&0) = &0) /\
43 (~(~(&n)) = &n) /\
44 (~(&m / &n) = ~(&m) / &n) /\
45 (~(~(&m) / &n) = &m / &n) /\
46 (~(unint (&m / &n :real)) = ~(&m) / &n)
47Proof
48 REWRITE_TAC [real_div, REAL_INV_NEG, REAL_MUL_LNEG, REAL_NEG_NEG,
49 REAL_NEG_0, markerTheory.unint_def]
50QED
51
52Theorem REAL_RAT_ABS_pth:
53 (abs(&n) = &n) /\
54 (abs(~(&n)) = &n) /\
55 (abs(&m / &n) = &m / &n) /\
56 (abs(~(&m) / &n) = &m / &n) /\
57 (abs(unint (&m / &n :real)) = &m / &n) /\
58 (abs(~(unint (&m / &n :real))) = &m / &n)
59Proof
60 REWRITE_TAC [markerTheory.unint_def, REAL_ABS_DIV,
61 realaxTheory.REAL_ABS_NEG, realaxTheory.REAL_ABS_NUM]
62QED
63
64Theorem REAL_RAT_INV_pth1:
65 (inv(&0) = &0) /\
66 (inv(&1) = &1) /\
67 (inv(~&1) = ~(&1)) /\
68 (inv(&1 / &n) = &n) /\
69 (inv(~&1 / &n) = ~&n)
70Proof
71 REWRITE_TAC [REAL_INV_0, REAL_INV_1, REAL_INV_NEG,
72 REAL_INV_DIV', REAL_OVER1] THEN
73 REWRITE_TAC [real_div, REAL_INV_NEG, REAL_MUL_RNEG, REAL_INV_1,
74 REAL_MUL_RID]
75QED
76
77Theorem REAL_RAT_INV_pth2:
78 (inv(&n) = &1 / &n) /\
79 (inv(~(&n)) = ~(&1) / &n) /\
80 (inv(&m / &n) = &n / &m) /\
81 (inv(~(&m) / &n) = ~(&n) / &m) /\
82 (inv(unint (&m / &n :real)) = &n / &m) /\
83 (inv(~(unint (&m / &n :real))) = ~(&n) / &m)
84Proof
85 REWRITE_TAC [markerTheory.unint_def, REAL_INV_DIV'] THEN
86 REWRITE_TAC [REAL_INV_NEG, real_div, REAL_MUL_RNEG,
87 REAL_MUL_LID, REAL_MUL_LNEG, REAL_INV_MUL', REAL_INV_INV] THEN
88 REWRITE_TAC [Once REAL_MUL_COMM]
89QED
90
91Theorem REAL_RAT_ADD_pth:
92 (&0 :real) < y1 ==> &0 < y2 ==> &0 < y3 ==>
93 ((x1 * y2 + x2 * y1) * y3 = x3 * (y1 * y2))
94 ==> (x1 / y1 + x2 / y2 = x3 / y3)
95Proof
96 REPEAT DISCH_TAC THEN
97 MP_TAC RAT_LEMMA2 THEN
98 ASM_REWRITE_TAC [] THEN
99 DISCH_THEN SUBST1_TAC THEN
100 ONCE_REWRITE_TAC [GSYM REAL_MUL_ASSOC] THEN
101 REWRITE_TAC [GSYM REAL_INV_MUL', GSYM real_div] THEN
102 Q.SUBGOAL_THEN `&0 < y1 * y2 /\ &0 < y3` MP_TAC THENL [
103 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC REAL_LT_MUL THEN
104 ASM_REWRITE_TAC [],
105 DISCH_THEN (fn th => ASM_REWRITE_TAC [MATCH_MP RAT_LEMMA5 th])
106 ]
107QED
108
109Theorem REAL_RAT_SUB_pth: x - y = x + ~y
110Proof REWRITE_TAC [real_sub]
111QED
112
113Theorem REAL_RAT_MUL_pth_nocancel:
114 (x1 / y1) * (x2 / y2) = (x1 * x2) / (y1 * y2 :real)
115Proof
116 SIMP_TAC bool_ss [real_div, REAL_INV_MUL',
117 simpLib.AC REAL_MUL_ASSOC REAL_MUL_COMM]
118QED
119
120Theorem REAL_RAT_MUL_pth_cancel:
121 ~(d1 = (&0 :real)) /\ ~(d2 = &0) /\
122 (d1 * u1 = x1) /\ (d2 * u2 = x2) /\
123 (d2 * v1 = y1) /\ (d1 * v2 = y2)
124 ==> ((x1 / y1) * (x2 / y2) = (u1 * u2) / (v1 * v2))
125Proof
126 rpt strip_tac >>
127 RW_TAC (bool_ss ++ RMULCANON_ss) [real_div, REAL_INV_MUL', nonzerop_def]
128QED
129
130Theorem REAL_RAT_DIV_pth: x / y = x * inv(y)
131Proof REWRITE_TAC [real_div]
132QED
133
134Theorem REAL_RAT_POW_pth: (x / y) pow n = (x pow n) / (y pow n)
135Proof REWRITE_TAC [REAL_POW_DIV]
136QED
137
138Theorem REAL_INTEGRAL:
139 (!(x :real). &0 * x = &0) /\
140 (!(x :real) y z. (x + y = x + z) <=> (y = z)) /\
141 (!(w :real) x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))
142Proof
143 ONCE_REWRITE_TAC [GSYM REAL_SUB_0] THEN
144 REWRITE_TAC [GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC
145QED
146
147Theorem REAL_RABINOWITSCH:
148 !x y:real. ~(x = y) <=> ?z. (x - y) * z = &1
149Proof
150 REWRITE_TAC [EQ_IMP_THM] >> rpt strip_tac >>
151 FULL_SIMP_TAC std_ss [EQ_IMP_THM, REAL_SUB_REFL, REAL_MUL_LZERO, REAL_10] >>
152 irule_at Any REAL_MUL_RINV >> ASM_REWRITE_TAC [REAL_SUB_0]
153QED
154
155Theorem REAL_FIELD_pth:
156 x pow n <> 0 <=> x <> 0 \/ &n = 0r \/ x pow n <> 0
157Proof
158 SIMP_TAC bool_ss [REAL_POW_EQ_0, DE_MORGAN_THM, EQ_IMP_THM, DISJ_IMP_THM,
159 REAL_OF_NUM_EQ]
160QED