equal
deleted
inserted
replaced
180 |
180 |
181 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
181 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
182 by (split_all_tac 1); |
182 by (split_all_tac 1); |
183 by (Asm_simp_tac 1); |
183 by (Asm_simp_tac 1); |
184 qed "Pair_fst_snd_eq"; |
184 qed "Pair_fst_snd_eq"; |
|
185 |
|
186 Goal "fst p = fst q ==> snd p = snd q ==> p = q"; |
|
187 by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1); |
|
188 qed "prod_eqI"; |
|
189 AddXIs [prod_eqI]; |
185 |
190 |
186 (*Prevents simplification of c: much faster*) |
191 (*Prevents simplification of c: much faster*) |
187 Goal "p=q ==> split c p = split c q"; |
192 Goal "p=q ==> split c p = split c q"; |
188 by (etac arg_cong 1); |
193 by (etac arg_cong 1); |
189 qed "split_weak_cong"; |
194 qed "split_weak_cong"; |