0
|
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];
|