real_algebraScript.sml
1(* ------------------------------------------------------------------------- *)
2(* The monoids of addition and multiplication of real numbers. *)
3(* ------------------------------------------------------------------------- *)
4(* The groups of addition and multiplication of real numbers. *)
5(* ------------------------------------------------------------------------- *)
6(* Reals as a ring. *)
7(* ------------------------------------------------------------------------- *)
8Theory real_algebra
9Ancestors
10 pred_set real iterate real_sigma bag monoid group ring
11Libs
12 dep_rewrite
13
14
15Definition real_add_monoid_def:
16 real_add_monoid : real monoid =
17 <| carrier := UNIV; id := 0; op := (real_add) |>
18End
19
20Theorem real_add_monoid_simps[simp]:
21 real_add_monoid.carrier = UNIV /\
22 real_add_monoid.op = (real_add) /\
23 real_add_monoid.id = 0
24Proof
25 rw[real_add_monoid_def]
26QED
27
28Theorem real_add_monoid[simp]:
29 AbelianMonoid real_add_monoid
30Proof
31 rw[AbelianMonoid_def]
32 >- (
33 rewrite_tac[Monoid_def]
34 \\ simp[REAL_ADD_ASSOC] )
35 \\ simp[REAL_ADD_COMM]
36QED
37
38Definition real_mul_monoid_def:
39 real_mul_monoid : real monoid =
40 <| carrier := UNIV; id := 1; op := (real_mul) |>
41End
42
43Theorem real_mul_monoid_simps[simp]:
44 real_mul_monoid.carrier = UNIV /\
45 real_mul_monoid.op = (real_mul) /\
46 real_mul_monoid.id = 1
47Proof
48 rw[real_mul_monoid_def]
49QED
50
51Theorem real_mul_monoid[simp]:
52 AbelianMonoid real_mul_monoid
53Proof
54 rw[AbelianMonoid_def]
55 >- (
56 rewrite_tac[Monoid_def]
57 \\ simp[REAL_MUL_ASSOC] )
58 \\ simp[REAL_MUL_COMM]
59QED
60
61Theorem real_add_group[simp]:
62 AbelianGroup real_add_monoid
63Proof
64 mp_tac real_add_monoid
65 \\ rewrite_tac[AbelianMonoid_def]
66 \\ rw[AbelianGroup_def, Group_def]
67 \\ rw[monoid_invertibles_def]
68 \\ simp[Once EXTENSION]
69 \\ gen_tac \\ qexists_tac`-x`
70 \\ simp[]
71QED
72
73Theorem real_mul_group:
74 AbelianGroup (real_mul_monoid excluding 0)
75Proof
76 mp_tac real_mul_monoid
77 \\ rewrite_tac[AbelianMonoid_def]
78 \\ rw[AbelianGroup_def, Group_def]
79 >- (
80 full_simp_tac std_ss [Monoid_def]
81 \\ fs[excluding_def] )
82 \\ rw[monoid_invertibles_def]
83 \\ simp[excluding_def, Once EXTENSION]
84 \\ gen_tac \\ Cases_on`x = 0` \\ rw[]
85 \\ qexists_tac`realinv x`
86 \\ simp[realTheory.REAL_MUL_RINV]
87QED
88
89Definition Reals_def:
90 Reals =
91 <| carrier := UNIV;
92 sum := real_add_monoid;
93 prod := real_mul_monoid
94 |>
95End
96
97Theorem RingReals[simp]:
98 Ring Reals
99Proof
100 rewrite_tac[Ring_def]
101 \\ simp[Reals_def, REAL_LDISTRIB]
102QED
103
104Theorem Unit_Reals[simp]:
105 Unit Reals r <=> r <> 0
106Proof
107 simp[ring_unit_property]
108 \\ simp[Reals_def]
109 \\ rw[EQ_IMP_THM]
110 >- (strip_tac \\ fs[])
111 \\ qexists_tac`realinv r`
112 \\ simp[REAL_MUL_RINV]
113QED
114
115Theorem Inv_Reals[simp]:
116 r <> 0 ==> Inv Reals r = realinv r
117Proof
118 strip_tac
119 \\ irule EQ_SYM
120 \\ irule ring_unit_linv_unique
121 \\ simp[]
122 \\ simp[Reals_def, REAL_MUL_LINV, Invertibles_carrier]
123QED
124
125Theorem ring_divides_Reals:
126 ring_divides Reals p q <=> (p = 0 ==> q = 0)
127Proof
128 rw[ring_divides_def]
129 \\ rw[Reals_def]
130 \\ Cases_on`p = 0` \\ simp[]
131 \\ qexists_tac`q / p`
132 \\ simp[REAL_DIV_RMUL]
133QED
134
135Theorem ring_prime_Reals[simp]:
136 ring_prime Reals p
137Proof
138 rw[ring_prime_def]
139 \\ fs[ring_divides_Reals]
140 \\ fs[Reals_def]
141QED
142
143Theorem Reals_sum_inv:
144 Reals.sum.inv = real_neg
145Proof
146 rw[FUN_EQ_THM, Reals_def]
147 \\ DEP_REWRITE_TAC[GSYM group_linv_unique]
148 \\ simp[]
149 \\ metis_tac[real_add_group, AbelianGroup_def]
150QED
151
152Theorem GBAG_Reals_sum_BAG_IMAGE_BAG_OF_SET:
153 !f s. FINITE s ==>
154 GBAG Reals.sum (BAG_IMAGE f (BAG_OF_SET s)) =
155 REAL_SUM_IMAGE f s
156Proof
157 strip_tac
158 \\ ho_match_mp_tac FINITE_INDUCT
159 \\ rw[]
160 >- rw[Reals_def, real_sigmaTheory.REAL_SUM_IMAGE_THM]
161 \\ rw[real_sigmaTheory.REAL_SUM_IMAGE_THM]
162 \\ fs[DELETE_NON_ELEMENT]
163 \\ fs[GSYM DELETE_NON_ELEMENT]
164 \\ rw[BAG_OF_SET_INSERT_NON_ELEMENT]
165 \\ DEP_REWRITE_TAC[GBAG_INSERT]
166 \\ simp[]
167 \\ simp[Reals_def]
168QED
169
170Theorem GBAG_Reals_prod_BAG_OF_SET:
171 !f s. FINITE s ==>
172 GBAG Reals.prod (BAG_IMAGE f (BAG_OF_SET s)) =
173 product s f
174Proof
175 strip_tac
176 \\ ho_match_mp_tac FINITE_INDUCT
177 \\ rw[]
178 >- rw[Reals_def, PRODUCT_CLAUSES]
179 \\ rw[PRODUCT_CLAUSES]
180 \\ fs[DELETE_NON_ELEMENT]
181 \\ fs[GSYM DELETE_NON_ELEMENT]
182 \\ rw[BAG_OF_SET_INSERT_NON_ELEMENT]
183 \\ DEP_REWRITE_TAC[GBAG_INSERT]
184 \\ simp[]
185 \\ simp[Reals_def]
186QED
187