15 |
15 |
16 Goalw [real_number_of_def] "(0::real) = Numeral0"; |
16 Goalw [real_number_of_def] "(0::real) = Numeral0"; |
17 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1); |
17 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1); |
18 qed "zero_eq_numeral_0"; |
18 qed "zero_eq_numeral_0"; |
19 |
19 |
20 Goalw [real_number_of_def] "1r = Numeral1"; |
20 Goalw [real_number_of_def] "(1::real) = Numeral1"; |
21 by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1); |
21 by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1); |
22 qed "one_eq_numeral_1"; |
22 qed "one_eq_numeral_1"; |
23 |
23 |
24 (** Addition **) |
24 (** Addition **) |
25 |
25 |
107 by (rtac (linorder_not_less RS sym) 1); |
107 by (rtac (linorder_not_less RS sym) 1); |
108 qed "le_real_number_of_eq_not_less"; |
108 qed "le_real_number_of_eq_not_less"; |
109 |
109 |
110 Addsimps [le_real_number_of_eq_not_less]; |
110 Addsimps [le_real_number_of_eq_not_less]; |
111 |
111 |
112 (*** New versions of existing theorems involving 0, 1r ***) |
112 (*** New versions of existing theorems involving 0, 1 ***) |
113 |
113 |
114 Goal "- Numeral1 = (-1::real)"; |
114 Goal "- Numeral1 = (-1::real)"; |
115 by (Simp_tac 1); |
115 by (Simp_tac 1); |
116 qed "minus_numeral_one"; |
116 qed "minus_numeral_one"; |
117 |
117 |
118 |
118 |
119 (*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*) |
119 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) |
120 val real_numeral_ss = |
120 val real_numeral_ss = |
121 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, |
121 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, |
122 minus_numeral_one]; |
122 minus_numeral_one]; |
123 |
123 |
124 fun rename_numerals th = |
124 fun rename_numerals th = |
125 asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th); |
125 asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th); |
126 |
126 |
127 |
127 |
128 (*Now insert some identities previously stated for 0 and 1r*) |
128 (*Now insert some identities previously stated for 0 and 1*) |
129 |
129 |
130 (** RealDef & Real **) |
130 (** RealDef & Real **) |
131 |
131 |
132 Addsimps (map rename_numerals |
132 Addsimps (map rename_numerals |
133 [real_minus_zero, real_minus_zero_iff, |
133 [real_minus_zero, real_minus_zero_iff, |