230 (*Positive Rational multiplication is an AC operator*) |
230 (*Positive Rational multiplication is an AC operator*) |
231 bind_thms ("prat_mult_ac", [prat_mult_assoc, |
231 bind_thms ("prat_mult_ac", [prat_mult_assoc, |
232 prat_mult_commute,prat_mult_left_commute]); |
232 prat_mult_commute,prat_mult_left_commute]); |
233 |
233 |
234 Goalw [prat_of_pnat_def] |
234 Goalw [prat_of_pnat_def] |
235 "(prat_of_pnat (Abs_pnat 1')) * z = z"; |
235 "(prat_of_pnat (Abs_pnat (Suc 0))) * z = z"; |
236 by (res_inst_tac [("z","z")] eq_Abs_prat 1); |
236 by (res_inst_tac [("z","z")] eq_Abs_prat 1); |
237 by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1); |
237 by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1); |
238 qed "prat_mult_1"; |
238 qed "prat_mult_1"; |
239 |
239 |
240 Goalw [prat_of_pnat_def] |
240 Goalw [prat_of_pnat_def] |
241 "z * (prat_of_pnat (Abs_pnat 1')) = z"; |
241 "z * (prat_of_pnat (Abs_pnat (Suc 0))) = z"; |
242 by (res_inst_tac [("z","z")] eq_Abs_prat 1); |
242 by (res_inst_tac [("z","z")] eq_Abs_prat 1); |
243 by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1); |
243 by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1); |
244 qed "prat_mult_1_right"; |
244 qed "prat_mult_1_right"; |
245 |
245 |
246 Goalw [prat_of_pnat_def] |
246 Goalw [prat_of_pnat_def] |
257 qed "prat_of_pnat_mult"; |
257 qed "prat_of_pnat_mult"; |
258 |
258 |
259 (*** prat_mult and qinv ***) |
259 (*** prat_mult and qinv ***) |
260 |
260 |
261 Goalw [prat_def,prat_of_pnat_def] |
261 Goalw [prat_def,prat_of_pnat_def] |
262 "qinv (q) * q = prat_of_pnat (Abs_pnat 1')"; |
262 "qinv (q) * q = prat_of_pnat (Abs_pnat (Suc 0))"; |
263 by (res_inst_tac [("z","q")] eq_Abs_prat 1); |
263 by (res_inst_tac [("z","q")] eq_Abs_prat 1); |
264 by (asm_full_simp_tac (simpset() addsimps [qinv, |
264 by (asm_full_simp_tac (simpset() addsimps [qinv, |
265 prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1); |
265 prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1); |
266 qed "prat_mult_qinv"; |
266 qed "prat_mult_qinv"; |
267 |
267 |
268 Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1')"; |
268 Goal "q * qinv (q) = prat_of_pnat (Abs_pnat (Suc 0))"; |
269 by (rtac (prat_mult_commute RS subst) 1); |
269 by (rtac (prat_mult_commute RS subst) 1); |
270 by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1); |
270 by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1); |
271 qed "prat_mult_qinv_right"; |
271 qed "prat_mult_qinv_right"; |
272 |
272 |
273 Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')"; |
273 Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat (Suc 0))"; |
274 by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1); |
274 by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1); |
275 qed "prat_qinv_ex"; |
275 qed "prat_qinv_ex"; |
276 |
276 |
277 Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')"; |
277 Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat (Suc 0))"; |
278 by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset())); |
278 by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset())); |
279 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1); |
279 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1); |
280 by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1); |
280 by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1); |
281 by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute, |
281 by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute, |
282 prat_mult_1,prat_mult_1_right]) 1); |
282 prat_mult_1,prat_mult_1_right]) 1); |
283 qed "prat_qinv_ex1"; |
283 qed "prat_qinv_ex1"; |
284 |
284 |
285 Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1')"; |
285 Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat (Suc 0))"; |
286 by (auto_tac (claset() addIs [prat_mult_qinv],simpset())); |
286 by (auto_tac (claset() addIs [prat_mult_qinv],simpset())); |
287 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1); |
287 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1); |
288 by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1); |
288 by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1); |
289 by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute, |
289 by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute, |
290 prat_mult_1,prat_mult_1_right]) 1); |
290 prat_mult_1,prat_mult_1_right]) 1); |
291 qed "prat_qinv_left_ex1"; |
291 qed "prat_qinv_left_ex1"; |
292 |
292 |
293 Goal "x * y = prat_of_pnat (Abs_pnat 1') ==> x = qinv y"; |
293 Goal "x * y = prat_of_pnat (Abs_pnat (Suc 0)) ==> x = qinv y"; |
294 by (cut_inst_tac [("q","y")] prat_mult_qinv 1); |
294 by (cut_inst_tac [("q","y")] prat_mult_qinv 1); |
295 by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1); |
295 by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1); |
296 by (Blast_tac 1); |
296 by (Blast_tac 1); |
297 qed "prat_mult_inv_qinv"; |
297 qed "prat_mult_inv_qinv"; |
298 |
298 |
504 prat_mult_less2_mono1 1); |
504 prat_mult_less2_mono1 1); |
505 by (assume_tac 1); |
505 by (assume_tac 1); |
506 by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")] |
506 by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")] |
507 prat_mult_left_less2_mono1 1); |
507 prat_mult_left_less2_mono1 1); |
508 by Auto_tac; |
508 by Auto_tac; |
509 by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1')")] prat_less_trans 1); |
509 by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] prat_less_trans 1); |
510 by (auto_tac (claset(),simpset() addsimps |
510 by (auto_tac (claset(),simpset() addsimps |
511 [prat_less_not_refl])); |
511 [prat_less_not_refl])); |
512 qed "lemma2_qinv_prat_less"; |
512 qed "lemma2_qinv_prat_less"; |
513 |
513 |
514 Goal "q1 < q2 ==> qinv (q2) < qinv (q1)"; |
514 Goal "q1 < q2 ==> qinv (q2) < qinv (q1)"; |
515 by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1); |
515 by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1); |
516 by (auto_tac (claset() addEs [lemma1_qinv_prat_less, |
516 by (auto_tac (claset() addEs [lemma1_qinv_prat_less, |
517 lemma2_qinv_prat_less],simpset())); |
517 lemma2_qinv_prat_less],simpset())); |
518 qed "qinv_prat_less"; |
518 qed "qinv_prat_less"; |
519 |
519 |
520 Goal "q1 < prat_of_pnat (Abs_pnat 1') \ |
520 Goal "q1 < prat_of_pnat (Abs_pnat (Suc 0)) \ |
521 \ ==> prat_of_pnat (Abs_pnat 1') < qinv(q1)"; |
521 \ ==> prat_of_pnat (Abs_pnat (Suc 0)) < qinv(q1)"; |
522 by (dtac qinv_prat_less 1); |
522 by (dtac qinv_prat_less 1); |
523 by (full_simp_tac (simpset() addsimps [qinv_1]) 1); |
523 by (full_simp_tac (simpset() addsimps [qinv_1]) 1); |
524 qed "prat_qinv_gt_1"; |
524 qed "prat_qinv_gt_1"; |
525 |
525 |
526 Goalw [pnat_one_def] |
526 Goalw [pnat_one_def] |
527 "q1 < prat_of_pnat 1p ==> prat_of_pnat 1p < qinv(q1)"; |
527 "q1 < prat_of_pnat 1p ==> prat_of_pnat 1p < qinv(q1)"; |
528 by (etac prat_qinv_gt_1 1); |
528 by (etac prat_qinv_gt_1 1); |
529 qed "prat_qinv_is_gt_1"; |
529 qed "prat_qinv_is_gt_1"; |
530 |
530 |
531 Goalw [prat_less_def] |
531 Goalw [prat_less_def] |
532 "prat_of_pnat (Abs_pnat 1') < prat_of_pnat (Abs_pnat 1') \ |
532 "prat_of_pnat (Abs_pnat (Suc 0)) < prat_of_pnat (Abs_pnat (Suc 0)) \ |
533 \ + prat_of_pnat (Abs_pnat 1')"; |
533 \ + prat_of_pnat (Abs_pnat (Suc 0))"; |
534 by (Fast_tac 1); |
534 by (Fast_tac 1); |
535 qed "prat_less_1_2"; |
535 qed "prat_less_1_2"; |
536 |
536 |
537 Goal "qinv(prat_of_pnat (Abs_pnat 1') + \ |
537 Goal "qinv(prat_of_pnat (Abs_pnat (Suc 0)) + \ |
538 \ prat_of_pnat (Abs_pnat 1')) < prat_of_pnat (Abs_pnat 1')"; |
538 \ prat_of_pnat (Abs_pnat (Suc 0))) < prat_of_pnat (Abs_pnat (Suc 0))"; |
539 by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1); |
539 by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1); |
540 by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1); |
540 by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1); |
541 qed "prat_less_qinv_2_1"; |
541 qed "prat_less_qinv_2_1"; |
542 |
542 |
543 Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1')"; |
543 Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat (Suc 0))"; |
544 by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1); |
544 by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1); |
545 by (Asm_full_simp_tac 1); |
545 by (Asm_full_simp_tac 1); |
546 qed "prat_mult_qinv_less_1"; |
546 qed "prat_mult_qinv_less_1"; |
547 |
547 |
548 Goal "(x::prat) < x + x"; |
548 Goal "(x::prat) < x + x"; |
699 "Abs_prat(ratrel``{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)"; |
699 "Abs_prat(ratrel``{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)"; |
700 by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left, |
700 by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left, |
701 pnat_mult_1])); |
701 pnat_mult_1])); |
702 qed "Abs_prat_mult_qinv"; |
702 qed "Abs_prat_mult_qinv"; |
703 |
703 |
704 Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1')})"; |
704 Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat (Suc 0))})"; |
705 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); |
705 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); |
706 by (rtac prat_mult_left_le2_mono1 1); |
706 by (rtac prat_mult_left_le2_mono1 1); |
707 by (rtac qinv_prat_le 1); |
707 by (rtac qinv_prat_le 1); |
708 by (pnat_ind_tac "y" 1); |
708 by (pnat_ind_tac "y" 1); |
709 by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] prat_add_le2_mono1 2); |
709 by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat (Suc 0))")] prat_add_le2_mono1 2); |
710 by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2); |
710 by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2); |
711 by (auto_tac (claset() addIs [prat_le_trans], |
711 by (auto_tac (claset() addIs [prat_le_trans], |
712 simpset() addsimps [prat_le_refl, |
712 simpset() addsimps [prat_le_refl, |
713 pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add])); |
713 pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add])); |
714 qed "lemma_Abs_prat_le1"; |
714 qed "lemma_Abs_prat_le1"; |
715 |
715 |
716 Goal "Abs_prat(ratrel``{(x,Abs_pnat 1')}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})"; |
716 Goal "Abs_prat(ratrel``{(x,Abs_pnat (Suc 0))}) <= Abs_prat(ratrel``{(x*y,Abs_pnat (Suc 0))})"; |
717 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); |
717 by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); |
718 by (rtac prat_mult_le2_mono1 1); |
718 by (rtac prat_mult_le2_mono1 1); |
719 by (pnat_ind_tac "y" 1); |
719 by (pnat_ind_tac "y" 1); |
720 by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2); |
720 by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2); |
721 by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self |
721 by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self |
724 simpset() addsimps [prat_le_refl, |
724 simpset() addsimps [prat_le_refl, |
725 pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2, |
725 pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2, |
726 prat_of_pnat_add,prat_of_pnat_mult])); |
726 prat_of_pnat_add,prat_of_pnat_mult])); |
727 qed "lemma_Abs_prat_le2"; |
727 qed "lemma_Abs_prat_le2"; |
728 |
728 |
729 Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})"; |
729 Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat (Suc 0))})"; |
730 by (fast_tac (claset() addIs [prat_le_trans, |
730 by (fast_tac (claset() addIs [prat_le_trans, |
731 lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1); |
731 lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1); |
732 qed "lemma_Abs_prat_le3"; |
732 qed "lemma_Abs_prat_le3"; |
733 |
733 |
734 Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1')}) * Abs_prat(ratrel``{(w,x)}) = \ |
734 Goal "Abs_prat(ratrel``{(x*y,Abs_pnat (Suc 0))}) * Abs_prat(ratrel``{(w,x)}) = \ |
735 \ Abs_prat(ratrel``{(w*y,Abs_pnat 1')})"; |
735 \ Abs_prat(ratrel``{(w*y,Abs_pnat (Suc 0))})"; |
736 by (full_simp_tac (simpset() addsimps [prat_mult, |
736 by (full_simp_tac (simpset() addsimps [prat_mult, |
737 pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1); |
737 pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1); |
738 qed "pre_lemma_gleason9_34"; |
738 qed "pre_lemma_gleason9_34"; |
739 |
739 |
740 Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1'*y)}) = \ |
740 Goal "Abs_prat(ratrel``{(y*x,Abs_pnat (Suc 0)*y)}) = \ |
741 \ Abs_prat(ratrel``{(x,Abs_pnat 1')})"; |
741 \ Abs_prat(ratrel``{(x,Abs_pnat (Suc 0))})"; |
742 by (auto_tac (claset(), |
742 by (auto_tac (claset(), |
743 simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac)); |
743 simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac)); |
744 qed "pre_lemma_gleason9_34b"; |
744 qed "pre_lemma_gleason9_34b"; |
745 |
745 |
746 Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)"; |
746 Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)"; |
758 |
758 |
759 (*** prove witness that will be required to prove non-emptiness ***) |
759 (*** prove witness that will be required to prove non-emptiness ***) |
760 (*** of preal type as defined using Dedekind Sections in PReal ***) |
760 (*** of preal type as defined using Dedekind Sections in PReal ***) |
761 (*** Show that exists positive real `one' ***) |
761 (*** Show that exists positive real `one' ***) |
762 |
762 |
763 Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1')}"; |
763 Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))}"; |
764 by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1); |
764 by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1); |
765 qed "lemma_prat_less_1_memEx"; |
765 qed "lemma_prat_less_1_memEx"; |
766 |
766 |
767 Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= {}"; |
767 Goal "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} ~= {}"; |
768 by (rtac notI 1); |
768 by (rtac notI 1); |
769 by (cut_facts_tac [lemma_prat_less_1_memEx] 1); |
769 by (cut_facts_tac [lemma_prat_less_1_memEx] 1); |
770 by (Asm_full_simp_tac 1); |
770 by (Asm_full_simp_tac 1); |
771 qed "lemma_prat_less_1_set_non_empty"; |
771 qed "lemma_prat_less_1_set_non_empty"; |
772 |
772 |
773 Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1')}"; |
773 Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))}"; |
774 by (asm_full_simp_tac (simpset() addsimps |
774 by (asm_full_simp_tac (simpset() addsimps |
775 [lemma_prat_less_1_set_non_empty RS not_sym]) 1); |
775 [lemma_prat_less_1_set_non_empty RS not_sym]) 1); |
776 qed "empty_set_psubset_lemma_prat_less_1_set"; |
776 qed "empty_set_psubset_lemma_prat_less_1_set"; |
777 |
777 |
778 (*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***) |
778 (*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***) |
779 Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1')}"; |
779 Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))}"; |
780 by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] exI 1); |
780 by (res_inst_tac [("x","prat_of_pnat (Abs_pnat (Suc 0))")] exI 1); |
781 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl])); |
781 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl])); |
782 qed "lemma_prat_less_1_not_memEx"; |
782 qed "lemma_prat_less_1_not_memEx"; |
783 |
783 |
784 Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= UNIV"; |
784 Goal "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} ~= UNIV"; |
785 by (rtac notI 1); |
785 by (rtac notI 1); |
786 by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1); |
786 by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1); |
787 by (Asm_full_simp_tac 1); |
787 by (Asm_full_simp_tac 1); |
788 qed "lemma_prat_less_1_set_not_rat_set"; |
788 qed "lemma_prat_less_1_set_not_rat_set"; |
789 |
789 |
790 Goalw [psubset_def,subset_def] |
790 Goalw [psubset_def,subset_def] |
791 "{x::prat. x < prat_of_pnat (Abs_pnat 1')} < UNIV"; |
791 "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} < UNIV"; |
792 by (asm_full_simp_tac |
792 by (asm_full_simp_tac |
793 (simpset() addsimps [lemma_prat_less_1_set_not_rat_set, |
793 (simpset() addsimps [lemma_prat_less_1_set_not_rat_set, |
794 lemma_prat_less_1_not_memEx]) 1); |
794 lemma_prat_less_1_not_memEx]) 1); |
795 qed "lemma_prat_less_1_set_psubset_rat_set"; |
795 qed "lemma_prat_less_1_set_psubset_rat_set"; |
796 |
796 |
797 (*** prove non_emptiness of type ***) |
797 (*** prove non_emptiness of type ***) |
798 Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : {A. {} < A & \ |
798 Goal "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} : {A. {} < A & \ |
799 \ A < UNIV & \ |
799 \ A < UNIV & \ |
800 \ (!y: A. ((!z. z < y --> z: A) & \ |
800 \ (!y: A. ((!z. z < y --> z: A) & \ |
801 \ (EX u: A. y < u)))}"; |
801 \ (EX u: A. y < u)))}"; |
802 by (auto_tac (claset() addDs [prat_less_trans], |
802 by (auto_tac (claset() addDs [prat_less_trans], |
803 simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set, |
803 simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set, |