equal
deleted
inserted
replaced
132 (*----------------------------------------------------------- |
132 (*----------------------------------------------------------- |
133 Addition for hyper naturals: hypnat_add |
133 Addition for hyper naturals: hypnat_add |
134 -----------------------------------------------------------*) |
134 -----------------------------------------------------------*) |
135 Goalw [congruent2_def] |
135 Goalw [congruent2_def] |
136 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})"; |
136 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})"; |
137 by (safe_tac (claset())); |
137 by Safe_tac; |
138 by (ALLGOALS(Fuf_tac)); |
138 by (ALLGOALS(Fuf_tac)); |
139 qed "hypnat_add_congruent2"; |
139 qed "hypnat_add_congruent2"; |
140 |
140 |
141 Goalw [hypnat_add_def] |
141 Goalw [hypnat_add_def] |
142 "Abs_hypnat(hypnatrel^^{%n. X n}) + Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
142 "Abs_hypnat(hypnatrel^^{%n. X n}) + Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
186 (*----------------------------------------------------------- |
186 (*----------------------------------------------------------- |
187 Subtraction for hyper naturals: hypnat_minus |
187 Subtraction for hyper naturals: hypnat_minus |
188 -----------------------------------------------------------*) |
188 -----------------------------------------------------------*) |
189 Goalw [congruent2_def] |
189 Goalw [congruent2_def] |
190 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})"; |
190 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})"; |
191 by (safe_tac (claset())); |
191 by Safe_tac; |
192 by (ALLGOALS(Fuf_tac)); |
192 by (ALLGOALS(Fuf_tac)); |
193 qed "hypnat_minus_congruent2"; |
193 qed "hypnat_minus_congruent2"; |
194 |
194 |
195 Goalw [hypnat_minus_def] |
195 Goalw [hypnat_minus_def] |
196 "Abs_hypnat(hypnatrel^^{%n. X n}) - Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
196 "Abs_hypnat(hypnatrel^^{%n. X n}) - Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
277 (*----------------------------------------------------------- |
277 (*----------------------------------------------------------- |
278 Multiplication for hyper naturals: hypnat_mult |
278 Multiplication for hyper naturals: hypnat_mult |
279 -----------------------------------------------------------*) |
279 -----------------------------------------------------------*) |
280 Goalw [congruent2_def] |
280 Goalw [congruent2_def] |
281 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})"; |
281 "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})"; |
282 by (safe_tac (claset())); |
282 by Safe_tac; |
283 by (ALLGOALS(Fuf_tac)); |
283 by (ALLGOALS(Fuf_tac)); |
284 qed "hypnat_mult_congruent2"; |
284 qed "hypnat_mult_congruent2"; |
285 |
285 |
286 Goalw [hypnat_mult_def] |
286 Goalw [hypnat_mult_def] |
287 "Abs_hypnat(hypnatrel^^{%n. X n}) * Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
287 "Abs_hypnat(hypnatrel^^{%n. X n}) * Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |