equal
deleted
inserted
replaced
156 lemma hypnat_add_zero_left: "(0::hypnat) + z = z" |
156 lemma hypnat_add_zero_left: "(0::hypnat) + z = z" |
157 apply (cases z) |
157 apply (cases z) |
158 apply (simp add: hypnat_zero_def hypnat_add) |
158 apply (simp add: hypnat_zero_def hypnat_add) |
159 done |
159 done |
160 |
160 |
161 instance hypnat :: plus_ac0 |
161 instance hypnat :: comm_monoid_add |
162 by intro_classes |
162 by intro_classes |
163 (assumption | |
163 (assumption | |
164 rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+ |
164 rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+ |
165 |
165 |
166 |
166 |
278 lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)" |
278 lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)" |
279 by (auto simp add: hypnat_zero_def hypnat_one_def) |
279 by (auto simp add: hypnat_zero_def hypnat_one_def) |
280 declare hypnat_zero_not_eq_one [THEN not_sym, simp] |
280 declare hypnat_zero_not_eq_one [THEN not_sym, simp] |
281 |
281 |
282 |
282 |
283 text{*The Hypernaturals Form A Semiring*} |
283 text{*The Hypernaturals Form A comm_semiring_1_cancel*} |
284 instance hypnat :: semiring |
284 instance hypnat :: comm_semiring_1_cancel |
285 proof |
285 proof |
286 fix i j k :: hypnat |
286 fix i j k :: hypnat |
287 show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc) |
|
288 show "i + j = j + i" by (rule hypnat_add_commute) |
|
289 show "0 + i = i" by simp |
|
290 show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc) |
287 show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc) |
291 show "i * j = j * i" by (rule hypnat_mult_commute) |
288 show "i * j = j * i" by (rule hypnat_mult_commute) |
292 show "1 * i = i" by (rule hypnat_mult_1) |
289 show "1 * i = i" by (rule hypnat_mult_1) |
293 show "(i + j) * k = i * k + j * k" by (simp add: hypnat_add_mult_distrib) |
290 show "(i + j) * k = i * k + j * k" by (simp add: hypnat_add_mult_distrib) |
294 show "0 \<noteq> (1::hypnat)" by (rule hypnat_zero_not_eq_one) |
291 show "0 \<noteq> (1::hypnat)" by (rule hypnat_zero_not_eq_one) |
350 apply (simp add: hypnat_zero_def hypnat_mult linorder_not_le [symmetric]) |
347 apply (simp add: hypnat_zero_def hypnat_mult linorder_not_le [symmetric]) |
351 apply (auto simp add: hypnat_le, ultra) |
348 apply (auto simp add: hypnat_le, ultra) |
352 done |
349 done |
353 |
350 |
354 |
351 |
355 subsection{*The Hypernaturals Form an Ordered Semiring*} |
352 subsection{*The Hypernaturals Form an Ordered comm_semiring_1_cancel*} |
356 |
353 |
357 instance hypnat :: ordered_semiring |
354 instance hypnat :: ordered_semidom |
358 proof |
355 proof |
359 fix x y z :: hypnat |
356 fix x y z :: hypnat |
360 show "0 < (1::hypnat)" |
357 show "0 < (1::hypnat)" |
361 by (simp add: hypnat_zero_def hypnat_one_def linorder_not_le [symmetric], |
358 by (simp add: hypnat_zero_def hypnat_one_def linorder_not_le [symmetric], |
362 simp add: hypnat_le) |
359 simp add: hypnat_le) |
454 thus ?thesis |
451 thus ?thesis |
455 by (auto simp add: linorder_not_less dest: order_le_less_trans) |
452 by (auto simp add: linorder_not_less dest: order_le_less_trans) |
456 qed |
453 qed |
457 |
454 |
458 |
455 |
459 subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and |
456 subsection{*The Embedding @{term hypnat_of_nat} Preserves comm_ring_1 and |
460 Order Properties*} |
457 Order Properties*} |
461 |
458 |
462 constdefs |
459 constdefs |
463 |
460 |
464 hypnat_of_nat :: "nat => hypnat" |
461 hypnat_of_nat :: "nat => hypnat" |