src/LCF/pair.ML
author clasohm
Wed, 29 Jun 1994 12:03:41 +0200
changeset 442 13ac1fd0a14d
parent 0 a5a9c433f639
child 660 7fe6ec24d842
permissions -rw-r--r--
added parentheses made necessary by change of constrain's precedence
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
val expand_all_PROD = prove_goal LCF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
	"(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
	(fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
		  rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
val PROD_less = prove_goal LCF.thy
442
13ac1fd0a14d added parentheses made necessary by change of constrain's precedence
clasohm
parents: 0
diff changeset
    11
	"(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
	(fn _ => [EVERY1[rtac iffI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
		  rtac conjI, etac less_ap_term, etac less_ap_term,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
		  rtac (ppair RS subst), rtac (qpair RS subst),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
		  etac conjE, rtac mono, etac less_ap_term, atac]]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
	(fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
		  rewrite_goals_tac [eq_def],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
		  asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
	(fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
	(fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
		(fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
	RS less_UU RS sym;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU];