13 by (auto_tac (claset(), |
13 by (auto_tac (claset(), |
14 simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym, |
14 simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym, |
15 preal_of_prat_add RS sym])); |
15 preal_of_prat_add RS sym])); |
16 qed "real_of_int_congruent"; |
16 qed "real_of_int_congruent"; |
17 |
17 |
18 val real_of_int_ize = RSLIST [equiv_intrel, real_of_int_congruent]; |
|
19 |
|
20 Goalw [real_of_int_def] |
18 Goalw [real_of_int_def] |
21 "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \ |
19 "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \ |
22 \ Abs_real(realrel ^^ \ |
20 \ Abs_real(realrel ^^ \ |
23 \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
21 \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
24 \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"; |
22 \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"; |
25 by (res_inst_tac [("f","Abs_real")] arg_cong 1); |
23 by (res_inst_tac [("f","Abs_real")] arg_cong 1); |
26 by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse, |
24 by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse, |
27 real_of_int_ize UN_equiv_class]) 1); |
25 [equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1); |
28 qed "real_of_int"; |
26 qed "real_of_int"; |
29 |
27 |
30 Goal "inj(real_of_int)"; |
28 Goal "inj(real_of_int)"; |
31 by (rtac injI 1); |
29 by (rtac injI 1); |
32 by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
30 by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |