author | lcp |
Fri, 16 Dec 1994 13:30:34 +0100 | |
changeset 793 | 0b5c5f568d74 |
parent 660 | 7fe6ec24d842 |
child 1461 | 6bcb44e4d6e5 |
permissions | -rw-r--r-- |
660 | 1 |
(* Title: LCF/pair |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
Theory of ordered pairs and products |
|
7 |
*) |
|
8 |
||
0 | 9 |
val expand_all_PROD = prove_goal LCF.thy |
10 |
"(ALL p. P(p)) <-> (ALL x y. P(<x,y>))" |
|
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]); |
|
13 |
||
14 |
local |
|
15 |
val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing; |
|
16 |
val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing; |
|
17 |
in |
|
18 |
val PROD_less = prove_goal LCF.thy |
|
442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
0
diff
changeset
|
19 |
"(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" |
0 | 20 |
(fn _ => [EVERY1[rtac iffI, |
21 |
rtac conjI, etac less_ap_term, etac less_ap_term, |
|
22 |
rtac (ppair RS subst), rtac (qpair RS subst), |
|
23 |
etac conjE, rtac mono, etac less_ap_term, atac]]); |
|
24 |
end; |
|
25 |
||
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, |
|
28 |
rewrite_goals_tac [eq_def], |
|
29 |
asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]); |
|
30 |
||
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]); |
|
33 |
||
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]); |
|
36 |
||
37 |
val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU" |
|
38 |
(fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1]) |
|
39 |
RS less_UU RS sym; |
|
40 |
||
41 |
val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU]; |