equal
deleted
inserted
replaced
166 Goalw [congruent2_def] |
166 Goalw [congruent2_def] |
167 "congruent2 intrel (%p1 p2. \ |
167 "congruent2 intrel (%p1 p2. \ |
168 \ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; |
168 \ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; |
169 (*Proof via congruent2_commuteI seems longer*) |
169 (*Proof via congruent2_commuteI seems longer*) |
170 by Safe_tac; |
170 by Safe_tac; |
171 by (asm_simp_tac (simpset() addsimps [add_assoc]) 1); |
171 by (Asm_simp_tac 1); |
172 (*The rest should be trivial, but rearranging terms is hard*) |
|
173 by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1); |
|
174 by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); |
|
175 qed "zadd_congruent2"; |
172 qed "zadd_congruent2"; |
176 |
173 |
177 (*Resolve th against the corresponding facts for zadd*) |
174 (*Resolve th against the corresponding facts for zadd*) |
178 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
175 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
179 |
176 |