author  lcp 
Mon, 31 Oct 1994 15:35:43 +0100  
changeset 660  7fe6ec24d842 
parent 442  13ac1fd0a14d 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
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]; 