|
1 val expand_all_PROD = prove_goal LCF.thy |
|
2 "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))" |
|
3 (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1, |
|
4 rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]); |
|
5 |
|
6 local |
|
7 val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing; |
|
8 val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing; |
|
9 in |
|
10 val PROD_less = prove_goal LCF.thy |
|
11 "p::'a*'b << q <-> FST(p) << FST(q) & SND(p) << SND(q)" |
|
12 (fn _ => [EVERY1[rtac iffI, |
|
13 rtac conjI, etac less_ap_term, etac less_ap_term, |
|
14 rtac (ppair RS subst), rtac (qpair RS subst), |
|
15 etac conjE, rtac mono, etac less_ap_term, atac]]); |
|
16 end; |
|
17 |
|
18 val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" |
|
19 (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1, |
|
20 rewrite_goals_tac [eq_def], |
|
21 asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]); |
|
22 |
|
23 val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d" |
|
24 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]); |
|
25 |
|
26 val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d" |
|
27 (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]); |
|
28 |
|
29 val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU" |
|
30 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1]) |
|
31 RS less_UU RS sym; |
|
32 |
|
33 val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU]; |