author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 1208 | bc3093616ba4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/OrdQuant.thy |
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Authors: Krzysztof Grabczewski and L C Paulson |
991 | 4 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
5 |
Quantifiers and union operator for ordinals. |
991 | 6 |
*) |
7 |
||
8 |
open OrdQuant; |
|
9 |
||
10 |
(*** universal quantifier for ordinals ***) |
|
11 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
12 |
qed_goalw "oallI" thy [oall_def] |
991 | 13 |
"[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)" |
14 |
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]); |
|
15 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
16 |
qed_goalw "ospec" thy [oall_def] |
991 | 17 |
"[| ALL x<A. P(x); x<A |] ==> P(x)" |
18 |
(fn major::prems=> |
|
19 |
[ (rtac (major RS spec RS mp) 1), |
|
20 |
(resolve_tac prems 1) ]); |
|
21 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
22 |
qed_goalw "oallE" thy [oall_def] |
991 | 23 |
"[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q" |
24 |
(fn major::prems=> |
|
25 |
[ (rtac (major RS allE) 1), |
|
26 |
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]); |
|
27 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
28 |
qed_goal "rev_oallE" thy |
991 | 29 |
"[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q" |
30 |
(fn major::prems=> |
|
31 |
[ (rtac (major RS oallE) 1), |
|
32 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
33 |
||
34 |
(*Trival rewrite rule; (ALL x<a.P)<->P holds only if a is not 0!*) |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
35 |
qed_goal "oall_simp" thy "(ALL x<a. True) <-> True" |
991 | 36 |
(fn _=> [ (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ]); |
37 |
||
38 |
(*Congruence rule for rewriting*) |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
39 |
qed_goalw "oall_cong" thy [oall_def] |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
40 |
"[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')" |
991 | 41 |
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]); |
42 |
||
43 |
||
44 |
(*** existential quantifier for ordinals ***) |
|
45 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
46 |
qed_goalw "oexI" thy [oex_def] |
991 | 47 |
"[| P(x); x<A |] ==> EX x<A. P(x)" |
48 |
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]); |
|
49 |
||
50 |
(*Not of the general form for such rules; ~EX has become ALL~ *) |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
51 |
qed_goal "oexCI" thy |
991 | 52 |
"[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A.P(x)" |
53 |
(fn prems=> |
|
54 |
[ (rtac classical 1), |
|
55 |
(REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]); |
|
56 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
57 |
qed_goalw "oexE" thy [oex_def] |
991 | 58 |
"[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q \ |
59 |
\ |] ==> Q" |
|
60 |
(fn major::prems=> |
|
61 |
[ (rtac (major RS exE) 1), |
|
62 |
(REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]); |
|
63 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
64 |
qed_goalw "oex_cong" thy [oex_def] |
991 | 65 |
"[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) \ |
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
66 |
\ |] ==> oex(a,P) <-> oex(a',P')" |
991 | 67 |
(fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]); |
68 |
||
69 |
||
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
70 |
(*** Rules for Ordinal-Indexed Unions ***) |
991 | 71 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
72 |
qed_goalw "OUN_I" thy [OUnion_def] |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
73 |
"!!i. [| a<i; b: B(a) |] ==> b: (UN z<i. B(z))" |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
74 |
(fn _=> [ fast_tac (ZF_cs addSEs [ltE]) 1 ]); |
991 | 75 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
76 |
qed_goalw "OUN_E" thy [OUnion_def] |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
77 |
"[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R" |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
78 |
(fn major::prems=> |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
79 |
[ (rtac (major RS CollectE) 1), |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
80 |
(rtac UN_E 1), |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
81 |
(REPEAT (ares_tac (ltI::prems) 1)) ]); |
991 | 82 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
83 |
qed_goalw "OUN_iff" thy [oex_def] |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
84 |
"b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))" |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
85 |
(fn _=> [ (fast_tac (FOL_cs addIs [OUN_I] addSEs [OUN_E]) 1) ]); |
991 | 86 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
87 |
qed_goal "OUN_cong" thy |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
88 |
"[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i.C(x)) = (UN x<j.D(x))" |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
89 |
(fn prems=> |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
90 |
[ rtac equality_iffI 1, |
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
91 |
simp_tac (ZF_ss addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]); |
991 | 92 |
|
93 |
val OrdQuant_cs = ZF_cs |
|
1461 | 94 |
addSIs [oallI] |
95 |
addIs [oexI, OUN_I] |
|
96 |
addSEs [oexE, OUN_E] |
|
97 |
addEs [rev_oallE]; |
|
991 | 98 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
99 |
val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, |
1461 | 100 |
ZF_mem_pairs); |
991 | 101 |
|
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
102 |
val OrdQuant_ss = ZF_ss setmksimps (map mk_meta_eq o Ord_atomize o gen_all) |
1461 | 103 |
addsimps [oall_simp, ltD RS beta] |
1038
9458105037b6
Redefined OUnion in a definitional manner, and proved the
lcp
parents:
991
diff
changeset
|
104 |
addcongs [oall_cong, oex_cong, OUN_cong]; |