37 |
37 |
38 Goalw [int_def,real_zero_def] "real (int 0) = 0"; |
38 Goalw [int_def,real_zero_def] "real (int 0) = 0"; |
39 by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1); |
39 by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1); |
40 qed "real_of_int_zero"; |
40 qed "real_of_int_zero"; |
41 |
41 |
42 Goalw [int_def,real_one_def] "real (int 1) = (1::real)"; |
42 Goal "real (1::int) = (1::real)"; |
|
43 by (stac (int_1 RS sym) 1); |
43 by (auto_tac (claset(), |
44 by (auto_tac (claset(), |
44 simpset() addsimps [real_of_int, |
45 simpset() addsimps [int_def, real_one_def, real_of_int, |
45 preal_of_prat_add RS sym,pnat_two_eq, |
46 preal_of_prat_add RS sym,pnat_two_eq, |
46 prat_of_pnat_add RS sym,pnat_one_iff RS sym])); |
47 prat_of_pnat_add RS sym, pnat_one_iff RS sym])); |
47 qed "real_of_int_one"; |
48 qed "real_of_one"; |
48 |
49 |
49 Goal "real (x::int) + real y = real (x + y)"; |
50 Goal "real (x::int) + real y = real (x + y)"; |
50 by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
51 by (res_inst_tac [("z","x")] eq_Abs_Integ 1); |
51 by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
52 by (res_inst_tac [("z","y")] eq_Abs_Integ 1); |
52 by (auto_tac (claset(), |
53 by (auto_tac (claset(), |
79 mult_ac @ add_ac @ pnat_add_ac)); |
80 mult_ac @ add_ac @ pnat_add_ac)); |
80 qed "real_of_int_mult"; |
81 qed "real_of_int_mult"; |
81 Addsimps [real_of_int_mult RS sym]; |
82 Addsimps [real_of_int_mult RS sym]; |
82 |
83 |
83 Goal "real (int (Suc n)) = real (int n) + (1::real)"; |
84 Goal "real (int (Suc n)) = real (int n) + (1::real)"; |
84 by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @ |
85 by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @ |
85 zadd_ac) 1); |
86 zadd_ac) 1); |
86 qed "real_of_int_Suc"; |
87 qed "real_of_int_Suc"; |
87 |
88 |
88 (* relating two of the embeddings *) |
89 (* relating two of the embeddings *) |
89 Goal "real (int n) = real n"; |
90 Goal "real (int n) = real n"; |