1461

1 
(* Title: LCF/pair

660

2 
ID: $Id$

1461

3 
Author: Tobias Nipkow

660

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

1461

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

0

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

1461

19 
"(p::'a*'b) << q <> FST(p) << FST(q) & SND(p) << SND(q)"


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

0

24 
end;


25 


26 
val PROD_eq = prove_goal LCF.thy "p=q <> FST(p)=FST(q) & SND(p)=SND(q)"

1461

27 
(fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1,


28 
rewtac eq_def,


29 
asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]);

0

30 


31 
val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <> a<<c & b<<d"

1461

32 
(fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);

0

33 


34 
val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <> a=c & b=d"

1461

35 
(fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);

0

36 


37 
val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU"

1461

38 
(fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])


39 
RS less_UU RS sym;

0

40 


41 
val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU];
