src/ZF/univ.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 27 0e152fe9571e
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/univ
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   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
The cumulative hierarchy and a small universe for recursive types
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 Univ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    14
by (simp_tac ZF_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(** Monotonicity **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (etac Un_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (rtac UN_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (rtac Pow_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (etac (bspec RS spec RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val Vfrom_mono_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
(** A fundamental equality: Vfrom does not require ordinals! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (eps_ind_tac "x" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
val Vfrom_rank_subset1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (eps_ind_tac "x" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (rtac (Vfrom RS ssubst) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    50
by (rtac (subset_refl RS Un_mono) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    51
by (rtac UN_least 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (etac (rank_implies_mem RS bexE) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    53
by (rtac subset_trans 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    54
by (etac UN_upper 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (etac bspec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val Vfrom_rank_subset2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (rtac Vfrom_rank_subset2 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (rtac Vfrom_rank_subset1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
val Vfrom_rank_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(*** Basic closure properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val zero_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
goal Univ.thy "i <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val i_subset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
goal Univ.thy "A <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (rtac Un_upper1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val A_subset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val subset_mem_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(** Finite sets and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val singleton_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
val doubleton_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
goalw Univ.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
\         <a,b> : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val Pair_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
val [prem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
    "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val succ_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(*** 0, successor and limit equations fof Vfrom ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
goal Univ.thy "Vfrom(A,0) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val Vfrom_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (rtac (Vfrom RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   125
by (rtac (succI1 RS RepFunI RS Union_upper RSN
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   126
	      (2, equalityI RS subst_context)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
by (rtac UN_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (etac member_succD 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val Vfrom_succ_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
by (rtac (rank_succ RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Vfrom_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(*first inclusion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (rtac Un_least 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   147
by (rtac (A_subset_Vfrom RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   148
by (rtac (prem RS UN_upper) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   149
by (rtac UN_least 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   150
by (etac UnionE 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   151
by (rtac subset_trans 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   152
by (etac UN_upper 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (rtac (Vfrom RS ssubst) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   154
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
(*opposite inclusion*)
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   156
by (rtac UN_least 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val Vfrom_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
(*** Limit ordinals -- general properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
by (fast_tac (eq_cs addEs [Ord_trans]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
val Limit_Union_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
by (etac conjunct1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
val Limit_is_Ord = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 : i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
val Limit_has_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j:i |] ==> succ(j) : i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
val Limit_has_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
goalw Univ.thy [Limit_def] "Limit(nat)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
by (REPEAT (ares_tac [conjI, ballI, nat_0I, nat_succI, Ord_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val Limit_nat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
goalw Univ.thy [Limit_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    "!!i. [| Ord(i);  0:i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (safe_tac subset_cs);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   186
by (rtac Ord_member 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   188
          ORELSE' dtac Ord_succ_subsetI ));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (fast_tac (subset_cs addSIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
val non_succ_LimitI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_member_iff RS iffD2]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
val Ord_cases_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
val major::prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
    "[| Ord(i);			\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
\       i=0            ==> P;	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
\       !!j. i=succ(j) ==> P;	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
\       Limit(i)       ==> P	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
by (cut_facts_tac [major RS Ord_cases_lemma] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
val Ord_cases = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(*** Vfrom applied to Limit ordinals ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
(*NB. limit ordinals are non-empty;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val [limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (rtac (limiti RS Limit_has_0 RS Vfrom_Union RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val Limit_Vfrom_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
val Limit_VfromE = standard (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
val [major,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
by (rtac (limiti RS Limit_VfromE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
by (rtac major 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (rtac UN_I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
by (etac singleton_in_Vfrom 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (etac (limiti RS Limit_has_succ) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
val singleton_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
\    {a,b} : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
by (rtac UN_I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (rtac doubleton_in_Vfrom 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
by (etac Vfrom_UnI1 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
by (etac Vfrom_UnI2 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
val doubleton_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
\    <a,b> : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
(*Infer that a, b occur at ordinals x,xa < i.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
by (rtac UN_I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
by (rtac Pair_in_Vfrom 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
(*Infer that succ(succ(x Un xa)) < i *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
by (etac Vfrom_UnI1 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
by (etac Vfrom_UnI2 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
val Pair_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
(*** Properties assuming Transset(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
			    Transset_Pow]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val Transset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (rtac (Vfrom_succ RS trans) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   274
by (rtac (Un_upper2 RSN (2,equalityI)) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   275
by (rtac (subset_refl RSN (2,Un_least)) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   276
by (rtac (A_subset_Vfrom RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   277
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
val Transset_Vfrom_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
goalw Ord.thy [Pair_def,Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
    "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
val Transset_Pair_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
    "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
\          <a,b> : Vfrom(A,i)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   288
by (etac (Transset_Pair_subset RS conjE) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   289
by (etac Transset_Vfrom 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
val Transset_Pair_subset_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
     is a model of simple type theory provided A is a transitive set
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
     and i is a limit ordinal
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
(*There are three nearly identical proofs below -- needs a general theorem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
  for proving  ...a...b : Vfrom(A,i) where i is a limit ordinal*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(** products **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
\         a*b : Vfrom(A, succ(succ(succ(i))))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
val prod_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
\  a*b : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
(*Infer that a, b occur at ordinals x,xa < i.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
by (rtac UN_I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
by (rtac prod_in_Vfrom 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
(*Infer that succ(succ(succ(x Un xa))) < i *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
by (REPEAT (ares_tac [limiti RS Limit_has_succ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
val prod_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
(** Disjoint sums, aka Quine ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
goalw Univ.thy [sum_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A);  1:i |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
\         a+b : Vfrom(A, succ(succ(succ(i))))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
			   i_subset_Vfrom RS subsetD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
val sum_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
\  a+b : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
(*Infer that a, b occur at ordinals x,xa < i.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
by (rtac UN_I 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   349
by (rtac sum_in_Vfrom 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (rtac (succI1 RS UnI1) 5);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
(*Infer that succ(succ(succ(x Un xa))) < i *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
by (REPEAT (ares_tac [limiti RS Limit_has_0, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
		      limiti RS Limit_has_succ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
val sum_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
(** function space! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
goalw Univ.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
\         a->b : Vfrom(A, succ(succ(succ(succ(i)))))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
by (rtac (Collect_subset RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (rtac (subset_trans RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
by (rtac Un_upper2 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
by (rtac (succI1 RS UN_upper) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
by (rtac Pow_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
val fun_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
\  a->b : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
(*Infer that a, b occur at ordinals x,xa < i.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
by (rtac UN_I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
by (rtac fun_in_Vfrom 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
(*Infer that succ(succ(succ(x Un xa))) < i *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
by (REPEAT (ares_tac [limiti RS Limit_has_succ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
val fun_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
(*** The set Vset(i) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
val Vset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
val Transset_Vset = Transset_0 RS Transset_Vfrom;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
(** Characterisation of the elements of Vset(i) **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) : i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
by (rtac (Vset RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
by (rtac (rank RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
by (rtac sup_least2 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
val Vset_rank_imp1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
(*  [| Ord(i); x : Vset(i) |] ==> rank(x) : i  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
val Vset_D = standard (Vset_rank_imp1 RS spec RS mp);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   421
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
by (rtac allI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
by (rtac (Vset RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
val Vset_rank_imp2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
(*  [| Ord(i); rank(x) : i |] ==> x : Vset(i)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
val VsetI = standard (Vset_rank_imp2 RS spec RS mp);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
val [ordi] = goal Univ.thy "Ord(i) ==> b : Vset(i) <-> rank(b) : i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
by (etac (ordi RS Vset_D) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
by (etac (ordi RS VsetI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
val Vset_Ord_rank_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
goal Univ.thy "b : Vset(a) <-> rank(b) : rank(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
by (rtac (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
val Vset_rank_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
by (rtac (rank RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
by (EVERY' [rtac UN_I, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
	    etac (i_subset_Vfrom RS subsetD),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
	    assume_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
	    rtac succI1] 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
by (REPEAT (eresolve_tac [asm_rl,Vset_D,Ord_trans] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
val rank_Vset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
(** Lemmas for reasoning about sets in terms of their elements' ranks **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
(*  rank(x) : rank(a) ==> x : Vset(rank(a))  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
val Vset_rankI = Ord_rank RS VsetI;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
goal Univ.thy "a <= Vset(rank(a))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   459
by (rtac subsetI 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   460
by (etac (rank_lt RS Vset_rankI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
val arg_subset_Vset_rank = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
val [iprem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   465
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   466
by (rtac (Ord_rank RS iprem) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
val Int_Vset_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
(** Set up an environment for simplification **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
val rank_ss = ZF_ss 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   475
    addsimps [case_Inl, case_Inr, Vset_rankI]
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   476
    addsimps rank_trans_rls;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
(** Recursion over Vset levels! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
(*NOT SUITABLE FOR REWRITING: recursive!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
by (rtac (transrec RS ssubst) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   483
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   484
			      VsetI RS beta]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
val Vrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
val rew::prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
    "[| !!x. h(x)==Vrec(x,H) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
by (rtac Vrec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
val def_Vrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
(*** univ(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
by (etac Vfrom_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
val univ_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   504
by (etac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
val Transset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
(** univ(A) as a limit **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   508
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   510
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   511
val univ_eq_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   514
by (rtac (subset_UN_iff_eq RS iffD1) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   515
by (etac (univ_eq_UN RS subst) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   516
val subset_univ_eq_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
val [aprem, iprem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
    "[| a <= univ(X);			 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
\       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
\    |] ==> a <= b";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   522
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   523
by (rtac UN_least 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   524
by (etac iprem 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   525
val univ_Int_Vfrom_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
val prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   528
    "[| a <= univ(X);   b <= univ(X);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   529
\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   530
\    |] ==> a = b";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   531
by (rtac equalityI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   532
by (ALLGOALS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
     rtac Int_lower1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
val univ_Int_Vfrom_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   538
(** Closure properties **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
goalw Univ.thy [univ_def] "0 : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
by (rtac (nat_0I RS zero_in_Vfrom) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
val zero_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
goalw Univ.thy [univ_def] "A <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
by (rtac A_subset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
val A_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
val A_into_univ = A_subset_univ RS subsetD;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
(** Closure under unordered and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
by (rtac singleton_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
val singleton_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   556
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
goalw Univ.thy [univ_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   559
by (rtac doubleton_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
val doubleton_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
goalw Univ.thy [univ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
by (rtac Pair_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
val Pair_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
goal Univ.thy "univ(A)*univ(A) <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   570
by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
     ORELSE eresolve_tac [SigmaE, ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
val product_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
val Sigma_subset_univ = standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   575
    (Sigma_mono RS (product_univ RSN (2,subset_trans)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   577
goalw Univ.thy [univ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
    "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   579
by (etac Transset_Pair_subset_Vfrom_limit 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   581
val Transset_Pair_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   584
(** The natural numbers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   585
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   586
goalw Univ.thy [univ_def] "nat <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   587
by (rtac i_subset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
val nat_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   589
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   590
(* n:nat ==> n:univ(A) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591
val nat_into_univ = standard (nat_subset_univ RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   592
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   593
(** instances for 1 and 2 **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   594
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   595
goal Univ.thy "1 : univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   596
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
val one_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
(*unused!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   600
goal Univ.thy "succ(succ(0)) : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
val two_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
goalw Univ.thy [bool_def] "bool <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   605
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   606
val bool_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
val bool_into_univ = standard (bool_subset_univ RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   610
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   611
(** Closure under disjoint union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   612
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   613
goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   614
by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   615
val Inl_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   616
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   617
goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   618
by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   619
val Inr_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   620
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   621
goal Univ.thy "univ(C)+univ(C) <= univ(C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   622
by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   623
     ORELSE eresolve_tac [sumE, ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   624
val sum_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   625
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   626
val sum_subset_univ = standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   627
    (sum_mono RS (sum_univ RSN (2,subset_trans)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   628
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   629
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   630
(** Closure under binary union -- use Un_least **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   631
(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   632
(** Closure under RepFun -- use   RepFun_subset  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   633
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   634