equal
deleted
inserted
replaced
91 by (dtac eq_equiv_class 1); |
91 by (dtac eq_equiv_class 1); |
92 by (rtac equiv_intrel 1); |
92 by (rtac equiv_intrel 1); |
93 by (Fast_tac 1); |
93 by (Fast_tac 1); |
94 by Safe_tac; |
94 by Safe_tac; |
95 by (Asm_full_simp_tac 1); |
95 by (Asm_full_simp_tac 1); |
96 qed "inj_nat"; |
96 qed "inj_int"; |
97 |
97 |
98 |
98 |
99 (**** zminus: unary negation on Integ ****) |
99 (**** zminus: unary negation on Integ ****) |
100 |
100 |
101 Goalw [congruent_def] |
101 Goalw [congruent_def] |
471 |
471 |
472 (*** eliminates ~= in premises ***) |
472 (*** eliminates ~= in premises ***) |
473 bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE); |
473 bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE); |
474 |
474 |
475 Goal "(int m = int n) = (m = n)"; |
475 Goal "(int m = int n) = (m = n)"; |
476 by (fast_tac (claset() addSEs [inj_nat RS injD]) 1); |
476 by (fast_tac (claset() addSEs [inj_int RS injD]) 1); |
477 qed "int_int_eq"; |
477 qed "int_int_eq"; |
478 AddIffs [int_int_eq]; |
478 AddIffs [int_int_eq]; |
479 |
479 |
480 Goal "(int m < int n) = (m<n)"; |
480 Goal "(int m < int n) = (m<n)"; |
481 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, |
481 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, |