equal
deleted
inserted
replaced
57 by (sstac [fst_conv, snd_conv] 1); |
57 by (sstac [fst_conv, snd_conv] 1); |
58 by (rtac refl 1); |
58 by (rtac refl 1); |
59 val split = result(); |
59 val split = result(); |
60 |
60 |
61 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq]; |
61 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq]; |
|
62 |
|
63 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
|
64 by(res_inst_tac[("p","s")]PairE 1); |
|
65 by(res_inst_tac[("p","t")]PairE 1); |
|
66 by(asm_simp_tac pair_ss 1); |
|
67 val pair_eq = result(); |
62 |
68 |
63 (*Prevents simplification of c: much faster*) |
69 (*Prevents simplification of c: much faster*) |
64 val split_weak_cong = prove_goal Prod.thy |
70 val split_weak_cong = prove_goal Prod.thy |
65 "p=q ==> split(p,c) = split(q,c)" |
71 "p=q ==> split(p,c) = split(q,c)" |
66 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
72 (fn [prem] => [rtac (prem RS arg_cong) 1]); |