|
1 (* Title: ZF/AC/OrdQuant.thy |
|
2 ID: $Id$ |
|
3 Authors: Krzysztof Grabczewski and L C Paulson |
|
4 |
|
5 Quantifiers and union operator for ordinals. |
|
6 *) |
|
7 |
|
8 open OrdQuant; |
|
9 |
|
10 (*** universal quantifier for ordinals ***) |
|
11 |
|
12 qed_goalw "oallI" thy [oall_def] |
|
13 "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)" |
|
14 (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]); |
|
15 |
|
16 qed_goalw "ospec" thy [oall_def] |
|
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 |
|
22 qed_goalw "oallE" thy [oall_def] |
|
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 |
|
28 qed_goal "rev_oallE" thy |
|
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!*) |
|
35 qed_goal "oall_simp" thy "(ALL x<a. True) <-> True" |
|
36 (fn _=> [ (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ]); |
|
37 |
|
38 (*Congruence rule for rewriting*) |
|
39 qed_goalw "oall_cong" thy [oall_def] |
|
40 "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')" |
|
41 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
|
42 |
|
43 |
|
44 (*** existential quantifier for ordinals ***) |
|
45 |
|
46 qed_goalw "oexI" thy [oex_def] |
|
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~ *) |
|
51 qed_goal "oexCI" thy |
|
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 |
|
57 qed_goalw "oexE" thy [oex_def] |
|
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 |
|
64 qed_goalw "oex_cong" thy [oex_def] |
|
65 "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) \ |
|
66 \ |] ==> oex(a,P) <-> oex(a',P')" |
|
67 (fn prems=> [ (simp_tac (!simpset addsimps prems addcongs [conj_cong]) 1) ]); |
|
68 |
|
69 |
|
70 (*** Rules for Ordinal-Indexed Unions ***) |
|
71 |
|
72 qed_goalw "OUN_I" thy [OUnion_def] |
|
73 "!!i. [| a<i; b: B(a) |] ==> b: (UN z<i. B(z))" |
|
74 (fn _=> [ fast_tac (!claset addSEs [ltE]) 1 ]); |
|
75 |
|
76 qed_goalw "OUN_E" thy [OUnion_def] |
|
77 "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R" |
|
78 (fn major::prems=> |
|
79 [ (rtac (major RS CollectE) 1), |
|
80 (rtac UN_E 1), |
|
81 (REPEAT (ares_tac (ltI::prems) 1)) ]); |
|
82 |
|
83 qed_goalw "OUN_iff" thy [oex_def] |
|
84 "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))" |
|
85 (fn _=> [ (fast_tac (!claset addIs [OUN_I] addSEs [OUN_E]) 1) ]); |
|
86 |
|
87 qed_goal "OUN_cong" thy |
|
88 "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i.C(x)) = (UN x<j.D(x))" |
|
89 (fn prems=> |
|
90 [ rtac equality_iffI 1, |
|
91 simp_tac (!simpset addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]); |
|
92 |
|
93 AddSIs [oallI]; |
|
94 AddIs [oexI, OUN_I]; |
|
95 AddSEs [oexE, OUN_E]; |
|
96 AddEs [rev_oallE]; |
|
97 |
|
98 val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, |
|
99 ZF_mem_pairs); |
|
100 |
|
101 simpset := !simpset setmksimps (map mk_meta_eq o Ord_atomize o gen_all) |
|
102 addsimps [oall_simp, ltD RS beta] |
|
103 addcongs [oall_cong, oex_cong, OUN_cong]; |
|
104 |
|
105 val major::prems = goalw thy [lt_def, oall_def] |
|
106 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) \ |
|
107 \ |] ==> P(i)"; |
|
108 by (rtac (major RS conjE) 1); |
|
109 by (etac Ord_induct 1 THEN assume_tac 1); |
|
110 by (fast_tac (!claset addIs prems) 1); |
|
111 qed "lt_induct"; |
|
112 |