1 (* Title: LCF/pair |
1 (* Title: LCF/pair |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Theory of ordered pairs and products |
6 Theory of ordered pairs and products |
7 *) |
7 *) |
8 |
8 |
9 val expand_all_PROD = prove_goal LCF.thy |
9 val expand_all_PROD = prove_goal LCF.thy |
10 "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))" |
10 "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))" |
11 (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1, |
11 (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1, |
12 rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]); |
12 rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]); |
13 |
13 |
14 local |
14 local |
15 val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing; |
15 val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing; |
16 val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing; |
16 val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing; |
17 in |
17 in |
18 val PROD_less = prove_goal LCF.thy |
18 val PROD_less = prove_goal LCF.thy |
19 "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" |
19 "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" |
20 (fn _ => [EVERY1[rtac iffI, |
20 (fn _ => [EVERY1[rtac iffI, |
21 rtac conjI, etac less_ap_term, etac less_ap_term, |
21 rtac conjI, etac less_ap_term, etac less_ap_term, |
22 rtac (ppair RS subst), rtac (qpair RS subst), |
22 rtac (ppair RS subst), rtac (qpair RS subst), |
23 etac conjE, rtac mono, etac less_ap_term, atac]]); |
23 etac conjE, rtac mono, etac less_ap_term, atac]]); |
24 end; |
24 end; |
25 |
25 |
26 val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" |
26 val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" |
27 (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1, |
27 (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1, |
28 rewrite_goals_tac [eq_def], |
28 rewtac eq_def, |
29 asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]); |
29 asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]); |
30 |
30 |
31 val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d" |
31 val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d" |
32 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]); |
32 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]); |
33 |
33 |
34 val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d" |
34 val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d" |
35 (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]); |
35 (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]); |
36 |
36 |
37 val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU" |
37 val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU" |
38 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1]) |
38 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1]) |
39 RS less_UU RS sym; |
39 RS less_UU RS sym; |
40 |
40 |
41 val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU]; |
41 val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU]; |