src/ZF/ord.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ordinal.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For ordinal.thy.  Ordinals in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Ord;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*** Rules for Transset ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(** Two neat characterisations of Transset **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
goalw Ord.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val Transset_iff_Pow = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goalw Ord.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
val Transset_iff_Union_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(** Consequences of downwards closure **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val Transset_doubleton_D = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val [prem1,prem2] = goalw Ord.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
by (cut_facts_tac [prem2] 1);	
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val Transset_Pair_D = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val prem1::prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
    "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val Transset_includes_domain = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val prem1::prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val Transset_includes_range = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (REPEAT (etac (prem1 RS Transset_includes_range) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
     ORELSE resolve_tac [conjI, singletonI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val Transset_includes_summands = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
br (Int_Un_distrib RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val Transset_sum_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(** Closure properties **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
goalw Ord.thy [Transset_def] "Transset(0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val Transset_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val Transset_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val Transset_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val Transset_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val Transset_Pow = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
goalw Ord.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val Transset_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val [Transprem] = goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val Transset_Union_family = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val [prem,Transprem] = goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
by (cut_facts_tac [prem] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
val Transset_Inter_family = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*** Natural Deduction rules for Ord ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val prems = goalw Ord.thy [Ord_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i) ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val OrdI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val [major] = goalw Ord.thy [Ord_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
    "Ord(i) ==> Transset(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (rtac (major RS conjunct1) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val Ord_is_Transset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val [major,minor] = goalw Ord.thy [Ord_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
    "[| Ord(i);  j:i |] ==> Transset(j) ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
val Ord_contains_Transset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*** Lemmas for ordinals ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| Ord(i);  j:i |] ==> Ord(j) ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val Ord_in_Ord = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal Ord.thy "!!i j. [| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (REPEAT (ares_tac [OrdI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
     ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val Ord_subset_Ord = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val OrdmemD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
goal Ord.thy "!!i j k. [| i:j;  j:k;  Ord(k) |] ==> i:k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val Ord_trans = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goal Ord.thy "!!i j. [| i:j;  Ord(j) |] ==> succ(i) <= j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Ord_succ_subsetI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(*** The construction of ordinals: 0, succ, Union ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
goal Ord.thy "Ord(0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
val Ord_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
goal Ord.thy "!!i. Ord(i) ==> Ord(succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
by (REPEAT (ares_tac [OrdI,Transset_succ] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
     ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
			  Ord_contains_Transset] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
val Ord_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
val nonempty::prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
by (rtac Ord_is_Transset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
     ORELSE etac InterD 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val Ord_Inter = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val jmemA::prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
by (etac RepFunE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
val Ord_INT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
(*** Natural Deduction rules for Memrel ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
val Memrel_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
val prems = goal Ord.thy "[| a: b;  a: A;  b: A |]  ==>  <a,b> : Memrel(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
val MemrelI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
val [major,minor] = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
    "[| <a,b> : Memrel(A);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
\       [| a: A;  b: A;  a:b |]  ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
\    |]  ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (etac conjE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (rtac minor 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
val MemrelE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
(*The membership relation (as a set) is well-founded.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
  Proof idea: show A<=B by applying the foundation axiom to A-B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
goalw Ord.thy [wf_def] "wf(Memrel(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
by (EVERY1 [rtac (foundation RS disjE RS allI),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
	    etac disjI1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
	    etac bexE, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
	    rtac (impI RS allI RS bexI RS disjI2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
	    etac MemrelE,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
	    etac bspec,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
	    REPEAT o assume_tac]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val wf_Memrel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(*** Transfinite induction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
(*Epsilon induction over a transitive set*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val major::prems = goalw Ord.thy [Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
    "[| i: k;  Transset(k);                          \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
\       !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
\    |]  ==>  P(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (fast_tac (ZF_cs addEs [MemrelE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
by (fast_tac (ZF_cs addIs [MemrelI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
val Transset_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
(*Induction over an ordinal*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
val [major,indhyp] = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    "[| Ord(i); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
\       !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
\    |]  ==>  P(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
by (rtac indhyp 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (rtac (major RS Ord_succ RS Ord_in_Ord) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
val trans_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
fun trans_ind_tac a prems i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
    EVERY [res_inst_tac [("i",a)] trans_induct i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
	   rename_last_tac a ["1"] (i+1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
	   ares_tac prems i];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
(*Finds contradictions for the following proof*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
(** Proving that "member" is a linear ordering on the ordinals **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
val prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
    "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
by (trans_ind_tac "i" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
by (trans_ind_tac "j" [] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
by (DEPTH_SOLVE (swap_res_tac [disjCI,equalityI,subsetI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
     ORELSE ball_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
     ORELSE eresolve_tac [impE,disjE,allE] 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
     ORELSE hyp_subst_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
     ORELSE Ord_trans_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val Ord_linear_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
val ordi::ordj::prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
    "[| Ord(i);  Ord(j);  i:j ==> P;  i=j ==> P;  j:i ==> P |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
\    ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
by (rtac ordj 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1)); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
val Ord_linear = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val prems = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
    "[| Ord(i);  Ord(j);  i<=j ==> P;  j<=i ==> P |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
\    ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
          ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
val Ord_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
goal Ord.thy "!!i j. [| j<=i;  ~ i<=j;  Ord(i);  Ord(j) |] ==> j:i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (etac Ord_linear 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (REPEAT (ares_tac [subset_refl] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
     ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
val Ord_member = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
by (rtac (empty_subsetI RS Ord_member) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (rtac (prem RS Ord_succ) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (rtac Ord_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
val Ord_0_mem_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
by (rtac conjI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
by (etac OrdmemD 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
by (rtac (mem_anti_refl RS notI) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
by (etac subsetD 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
val Ord_member_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
goal Ord.thy "!!i. Ord(i) ==> 0:i  <-> ~ i=0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val Ord_0_member_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
(** For ordinals, i: succ(j) means 'less-than or equals' **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
goal Ord.thy "!!i j. [| j<=i;  Ord(i);  Ord(j) |] ==> j : succ(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
by (rtac Ord_member 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
by (REPEAT (ares_tac [Ord_succ] 3));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
by (rtac (mem_anti_refl RS notI) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
by (etac subsetD 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
by (ALLGOALS (fast_tac ZF_cs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
val member_succI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
goalw Ord.thy [Transset_def,Ord_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
    "!!i j. [| i : succ(j);  Ord(j) |] ==> i<=j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
val member_succD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:succ(i) <-> j<=i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
val member_succ_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
    "!!i j. [| Ord(i);  Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   321
by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
val subset_succ_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
goal Ord.thy "!!i j. [| i:succ(j);  j:k;  Ord(k) |] ==> i:k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
val Ord_trans1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
goal Ord.thy "!!i j. [| i:j;  j:succ(k);  Ord(k) |] ==> i:k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
val Ord_trans2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
goal Ord.thy "!!i jk. [| i:j;  j<=k;  Ord(k) |] ==> i:k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
val Ord_transsub2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
goal Ord.thy "!!i j. [| i:j;  Ord(j) |] ==> succ(i) : succ(j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
by (rtac member_succI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
     ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
val succ_mem_succI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
goal Ord.thy "!!i j. [| succ(i) : succ(j);  Ord(j) |] ==> i:j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
val succ_mem_succE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <-> i:j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
val succ_mem_succ_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
goal Ord.thy "!!i j. [| i<=j;  Ord(i);  Ord(j) |] ==> succ(i) <= succ(j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
by (rtac (member_succI RS succ_mem_succI RS member_succD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
by (REPEAT (ares_tac [Ord_succ] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
val Ord_succ_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   359
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
by (rtac (Un_commute RS ssubst) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   361
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
val Ord_member_UnI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Int j : k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   367
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (rtac (Int_commute RS ssubst) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   369
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
val Ord_member_IntI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
(*** Results about limits ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
val prems = goal Ord.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
val Ord_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
val prems = goal Ord.thy "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
by (rtac Ord_Union 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
by (etac RepFunE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
val Ord_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
(*The upper bound must be a successor ordinal --
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
  consider that (UN i:nat.i)=nat although nat is an upper bound of each i*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
val [ordi,limit] = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
    "[| Ord(i);  !!y. y:A ==> f(y): succ(i) |] ==> (UN y:A. f(y)) : succ(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
by (rtac (member_succD RS UN_least RS member_succI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
		      limit] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
val sup_least = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
val [jmemi,ordi,limit] = goal Ord.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
    "[| j: i;  Ord(i);  !!y. y:A ==> f(y): j |] ==> (UN y:A. succ(f(y))) : i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
by (rtac (sup_least RS Ord_trans2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
val sup_least2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
by (fast_tac (eq_cs addSEs [Ord_trans1]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
val Ord_equality = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
(*Holds for all transitive sets, not just ordinals*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
by (fast_tac (ZF_cs addSEs [Ord_trans]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
val Ord_Union_subset = result();