equal
deleted
inserted
replaced
224 Goalw [pnat_add_def] "!(y::pnat). x + y ~= x"; |
224 Goalw [pnat_add_def] "!(y::pnat). x + y ~= x"; |
225 by (rtac (Rep_pnat_inverse RS subst) 1); |
225 by (rtac (Rep_pnat_inverse RS subst) 1); |
226 by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] |
226 by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] |
227 addSDs [add_eq_self_zero], |
227 addSDs [add_eq_self_zero], |
228 simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse, |
228 simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse, |
229 Rep_pnat_gt_zero RS less_not_refl2])); |
229 Rep_pnat_gt_zero RS less_not_refl2] |
|
230 delsimprocs Nat_Numeral_Simprocs.cancel_numerals)); |
230 qed "pnat_no_add_ident"; |
231 qed "pnat_no_add_ident"; |
231 |
232 |
232 |
233 |
233 (***) (***) (***) (***) (***) (***) (***) (***) (***) |
234 (***) (***) (***) (***) (***) (***) (***) (***) (***) |
234 |
235 |