Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added pair_eq
authornipkow
Fri, 07 Jan 1994 14:22:37 +0100
changeset 31 04f43a28c97a
parent 30 2fdeeae553ac
child 32 4ea58120ef3d
added pair_eq
Prod.ML file | annotate | diff | comparison | revisions
prod.ML file | annotate | diff | comparison | revisions 
--- a/Prod.ML	Wed Jan 05 19:39:05 1994 +0100
+++ b/Prod.ML	Fri Jan 07 14:22:37 1994 +0100
@@ -60,6 +60,12 @@
 
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
+goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by(res_inst_tac[("p","s")]PairE 1);
+by(res_inst_tac[("p","t")]PairE 1);
+by(asm_simp_tac pair_ss 1);
+val pair_eq = result();
+
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy
   "p=q ==> split(p,c) = split(q,c)"
--- a/prod.ML	Wed Jan 05 19:39:05 1994 +0100
+++ b/prod.ML	Fri Jan 07 14:22:37 1994 +0100
@@ -60,6 +60,12 @@
 
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
+goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by(res_inst_tac[("p","s")]PairE 1);
+by(res_inst_tac[("p","t")]PairE 1);
+by(asm_simp_tac pair_ss 1);
+val pair_eq = result();
+
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy
   "p=q ==> split(p,c) = split(q,c)"
Old_HOL