src/ZF/Univ.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
     1
(*  Title:      ZF/Univ
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 187
diff changeset
     4
    Copyright   1994  University of Cambridge
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    15
qed "Vfrom";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    31
qed "Vfrom_mono_lemma";
0
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)  *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    34
bind_thm ("Vfrom_mono", (Vfrom_mono_lemma RS spec RS mp));
0
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);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    43
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    44
qed "Vfrom_rank_subset1";
0
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);
15
6c6d2f6e3185 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);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    51
by (rtac UN_least 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    52
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    53
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1);
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    54
by (rtac subset_trans 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    55
by (etac UN_upper 2);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    56
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    57
by (etac (ltI RS le_imp_subset) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
    58
by (rtac (Ord_rank RS Ord_succ) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (etac bspec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    61
qed "Vfrom_rank_subset2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (rtac Vfrom_rank_subset2 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
by (rtac Vfrom_rank_subset1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    67
qed "Vfrom_rank_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(*** Basic closure properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    75
qed "zero_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
goal Univ.thy "i <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    81
qed "i_subset_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal Univ.thy "A <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (rtac Un_upper1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    86
qed "A_subset_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    88
bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
    89
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
    93
qed "subset_mem_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
(** Finite sets and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
by (safe_tac ZF_cs);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   100
qed "singleton_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (safe_tac ZF_cs);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   106
qed "doubleton_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
goalw Univ.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
\         <a,b> : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   112
qed "Pair_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val [prem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   119
qed "succ_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
(*** 0, successor and limit equations fof Vfrom ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal Univ.thy "Vfrom(A,0) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   126
qed "Vfrom_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (rtac (Vfrom RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   130
by (rtac (succI1 RS RepFunI RS Union_upper RSN
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   131
              (2, equalityI RS subst_context)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
by (rtac UN_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   134
by (etac (ltI RS le_imp_subset) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   135
by (etac Ord_succ 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   136
qed "Vfrom_succ_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (rtac (rank_succ RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   143
qed "Vfrom_succ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
(*first inclusion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
by (rtac Un_least 1);
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   152
by (rtac (A_subset_Vfrom RS subset_trans) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   153
by (rtac (prem RS UN_upper) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   154
by (rtac UN_least 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   155
by (etac UnionE 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   156
by (rtac subset_trans 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   157
by (etac UN_upper 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (rtac (Vfrom RS ssubst) 1);
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   159
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
(*opposite inclusion*)
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   161
by (rtac UN_least 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   164
qed "Vfrom_Union";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*** Vfrom applied to Limit ordinals ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
(*NB. limit ordinals are non-empty;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val [limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   172
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
by (rtac refl 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   175
qed "Limit_Vfrom_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   177
goal Univ.thy "!!a. [| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   178
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   179
by (REPEAT (ares_tac [ltD RS UN_I] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   180
qed "Limit_VfromI";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   181
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   182
val prems = goal Univ.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   183
    "[| a: Vfrom(A,i);  Limit(i);               \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   184
\       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R    \
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   185
\    |] ==> R";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   186
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   187
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   188
qed "Limit_VfromE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   190
val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   191
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
val [major,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   194
by (rtac ([major,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   195
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (etac (limiti RS Limit_has_succ) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   197
qed "singleton_in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
\    {a,b} : Vfrom(A,i)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   206
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   207
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   208
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   209
by (etac Vfrom_UnI1 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   210
by (etac Vfrom_UnI2 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   211
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   212
qed "doubleton_in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
\    <a,b> : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
(*Infer that a, b occur at ordinals x,xa < i.*)
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   218
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   219
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   220
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
(*Infer that succ(succ(x Un xa)) < i *)
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   222
by (etac Vfrom_UnI1 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   223
by (etac Vfrom_UnI2 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   224
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   225
qed "Pair_in_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   226
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   227
goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   228
by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   229
     ORELSE eresolve_tac [SigmaE, ssubst] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   230
qed "product_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   231
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   232
bind_thm ("Sigma_subset_VLimit",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   233
          [Sigma_mono, product_VLimit] MRS subset_trans);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   234
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   235
bind_thm ("nat_subset_VLimit", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   236
          [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   237
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   238
goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   239
by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   240
qed "nat_into_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   241
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   242
(** Closure under disjoint union **)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   243
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   244
bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   245
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   246
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   247
by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   248
qed "one_in_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   249
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   250
goalw Univ.thy [Inl_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   251
    "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   252
by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   253
qed "Inl_in_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   254
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   255
goalw Univ.thy [Inr_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   256
    "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   257
by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   258
qed "Inr_in_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   259
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   260
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   261
by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   262
qed "sum_VLimit";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   263
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   264
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   265
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(*** Properties assuming Transset(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   274
                            Transset_Pow]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   275
qed "Transset_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (rtac (Vfrom_succ RS trans) 1);
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   279
by (rtac (Un_upper2 RSN (2,equalityI)) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   280
by (rtac (subset_refl RSN (2,Un_least)) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   281
by (rtac (A_subset_Vfrom RS subset_trans) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   282
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   283
qed "Transset_Vfrom_succ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 187
diff changeset
   285
goalw Ordinal.thy [Pair_def,Transset_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
    "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   288
qed "Transset_Pair_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
    "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
\          <a,b> : Vfrom(A,i)";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   293
by (etac (Transset_Pair_subset RS conjE) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   294
by (etac Transset_Vfrom 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   295
by (REPEAT (ares_tac [Pair_in_VLimit] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   296
qed "Transset_Pair_subset_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
     is a model of simple type theory provided A is a transitive set
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
     and i is a limit ordinal
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   304
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   305
val [aprem,bprem,limiti,step] = goal Univ.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   306
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);                 \
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   307
\     !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   308
\              |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==>     \
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   309
\  h(a,b) : Vfrom(A,i)";
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   310
(*Infer that a, b occur at ordinals x,xa < i.*)
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   311
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   312
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
828
03d7bfa70289 Changed succ(1) to 2 in in_VLimit, two_in_univ
lcp
parents: 803
diff changeset
   313
by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   314
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   315
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   316
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   317
by (rtac (succI1 RS UnI2) 2);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   318
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   319
qed "in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
(** products **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
goal Univ.thy
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   324
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   325
\         a*b : Vfrom(A, succ(succ(succ(j))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   330
qed "prod_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
\  a*b : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   335
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   336
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   337
                      limiti RS Limit_has_succ] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   338
qed "prod_in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
(** Disjoint sums, aka Quine ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
goalw Univ.thy [sum_def]
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   343
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   344
\         a+b : Vfrom(A, succ(succ(succ(j))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   349
                           i_subset_Vfrom RS subsetD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   350
qed "sum_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
\  a+b : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   355
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   356
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   357
                      limiti RS Limit_has_succ] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   358
qed "sum_in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
(** function space! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
goalw Univ.thy [Pi_def]
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   363
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   364
\         a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
by (rtac (Collect_subset RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
by (rtac (subset_trans RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
by (rtac Un_upper2 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
by (rtac (succI1 RS UN_upper) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
by (rtac Pow_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   375
qed "fun_in_Vfrom";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
\  a->b : Vfrom(A,i)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   380
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   381
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   382
                      limiti RS Limit_has_succ] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   383
qed "fun_in_VLimit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
(*** The set Vset(i) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   391
qed "Vset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
val Transset_Vset = Transset_0 RS Transset_Vfrom;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
(** Characterisation of the elements of Vset(i) **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   399
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
by (rtac (Vset RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
by (rtac (rank RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   404
by (rtac UN_succ_least_lt 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   405
by (fast_tac ZF_cs 2);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   406
by (REPEAT (ares_tac [ltI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   407
qed "Vset_rank_imp1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   409
(*  [| Ord(i); x : Vset(i) |] ==> rank(x) < i  *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   410
bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
by (rtac allI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
by (rtac (Vset RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   416
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   417
qed "Vset_rank_imp2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   419
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   420
by (etac ltE 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   421
by (etac (Vset_rank_imp2 RS spec RS mp) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   422
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   423
qed "VsetI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   425
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
by (rtac iffI 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   427
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   428
qed "Vset_Ord_rank_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   430
goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
by (rtac (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   433
qed "Vset_rank_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
by (rtac (rank RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
by (safe_tac ZF_cs);
828
03d7bfa70289 Changed succ(1) to 2 in in_VLimit, two_in_univ
lcp
parents: 803
diff changeset
   439
by (EVERY' [rtac UN_I, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   440
            etac (i_subset_Vfrom RS subsetD),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   441
            etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   442
            assume_tac,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   443
            rtac succI1] 3);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   444
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   445
qed "rank_Vset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
(** Lemmas for reasoning about sets in terms of their elements' ranks **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
goal Univ.thy "a <= Vset(rank(a))";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   450
by (rtac subsetI 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   451
by (etac (rank_lt RS VsetI) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   452
qed "arg_subset_Vset_rank";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
val [iprem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   456
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   457
          Int_greatest RS subset_trans) 1);
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   458
by (rtac (Ord_rank RS iprem) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   459
qed "Int_Vset_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
(** Set up an environment for simplification **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   464
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   466
val rank_ss = ZF_ss 
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   467
    addsimps [case_Inl, case_Inr, VsetI]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   468
    addsimps rank_trans_rls;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
(** Recursion over Vset levels! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
(*NOT SUITABLE FOR REWRITING: recursive!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
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
   474
by (rtac (transrec RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 15
diff changeset
   475
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   476
                              VsetI RS beta, le_refl]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   477
qed "Vrec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
val rew::prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
    "[| !!x. h(x)==Vrec(x,H) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   483
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
by (rtac Vrec 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   485
qed "def_Vrec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
(*** univ(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
by (etac Vfrom_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
by (rtac subset_refl 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   493
qed "univ_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
by (etac Transset_Vfrom 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   497
qed "Transset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
(** univ(A) as a limit **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   502
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   503
qed "univ_eq_UN";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   504
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   506
by (rtac (subset_UN_iff_eq RS iffD1) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   507
by (etac (univ_eq_UN RS subst) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   508
qed "subset_univ_eq_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
val [aprem, iprem] = goal Univ.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   511
    "[| a <= univ(X);                           \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   512
\       !!i. i:nat ==> a Int Vfrom(X,i) <= b    \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
\    |] ==> a <= b";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   514
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   515
by (rtac UN_least 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   516
by (etac iprem 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   517
qed "univ_Int_Vfrom_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
val prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
    "[| a <= univ(X);   b <= univ(X);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   522
\    |] ==> a = b";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   523
by (rtac equalityI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   524
by (ALLGOALS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   525
    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
     rtac Int_lower1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   528
qed "univ_Int_Vfrom_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   529
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   530
(** Closure properties **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   531
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   532
goalw Univ.thy [univ_def] "0 : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
by (rtac (nat_0I RS zero_in_Vfrom) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   534
qed "zero_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
goalw Univ.thy [univ_def] "A <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
by (rtac A_subset_Vfrom 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   538
qed "A_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
val A_into_univ = A_subset_univ RS subsetD;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
(** Closure under unordered and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   545
by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   546
qed "singleton_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
goalw Univ.thy [univ_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   550
by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   551
qed "doubleton_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
goalw Univ.thy [univ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   555
by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   556
qed "Pair_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   558
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   559
by (rtac (Limit_nat RS product_VLimit) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   560
qed "product_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
(** The natural numbers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
goalw Univ.thy [univ_def] "nat <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
by (rtac i_subset_Vfrom 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   567
qed "nat_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
(* n:nat ==> n:univ(A) *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   570
bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
(** instances for 1 and 2 **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   574
goalw Univ.thy [univ_def] "1 : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   575
by (rtac (Limit_nat RS one_in_VLimit) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   576
qed "one_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   577
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
(*unused!*)
828
03d7bfa70289 Changed succ(1) to 2 in in_VLimit, two_in_univ
lcp
parents: 803
diff changeset
   579
goal Univ.thy "2 : univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   581
qed "two_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
goalw Univ.thy [bool_def] "bool <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   584
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   585
qed "bool_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   586
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   587
bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   589
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   590
(** Closure under disjoint union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   592
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   593
by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   594
qed "Inl_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   595
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   596
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   597
by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   598
qed "Inr_in_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   600
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   601
by (rtac (Limit_nat RS sum_VLimit) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 537
diff changeset
   602
qed "sum_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   604
bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   605
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   606
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
(** Closure under binary union -- use Un_least **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
(** Closure under RepFun -- use   RepFun_subset  **)
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   610
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   611
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   612
(*** Finite Branching Closure Properties ***)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   613
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   614
(** Closure under finite powerset **)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   615
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   616
goal Univ.thy
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   617
   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   618
by (etac Fin_induct 1);
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   619
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   620
by (safe_tac ZF_cs);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   621
by (etac Limit_VfromE 1);
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   622
by (assume_tac 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   623
by (res_inst_tac [("x", "xa Un j")] exI 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   624
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   625
                           Un_least_lt]) 1);
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   626
val Fin_Vfrom_lemma = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   627
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   628
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   629
by (rtac subsetI 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   630
by (dtac Fin_Vfrom_lemma 1);
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   631
by (safe_tac ZF_cs);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   632
by (resolve_tac [Vfrom RS ssubst] 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   633
by (fast_tac (ZF_cs addSDs [ltD]) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   634
val Fin_VLimit = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   635
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   636
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   637
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   638
goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   639
by (rtac (Limit_nat RS Fin_VLimit) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   640
val Fin_univ = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   641
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   642
(** Closure under finite powers (functions from a fixed natural number) **)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   643
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   644
goal Univ.thy
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   645
    "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   646
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   647
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   648
                      nat_subset_VLimit, subset_refl] 1));
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   649
val nat_fun_VLimit = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   650
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   651
bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   652
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   653
goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   654
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   655
val nat_fun_univ = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   656
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   657
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   658
(** Closure under finite function space **)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   659
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   660
(*General but seldom-used version; normally the domain is fixed*)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   661
goal Univ.thy
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   662
    "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   663
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   664
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   665
val FiniteFun_VLimit1 = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   666
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   667
goalw Univ.thy [univ_def] "univ(A) -||> univ(A) <= univ(A)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   668
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   669
val FiniteFun_univ1 = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   670
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   671
(*Version for a fixed domain*)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   672
goal Univ.thy
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   673
   "!!i.  [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   674
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 853
diff changeset
   675
by (etac FiniteFun_VLimit1 1);
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   676
val FiniteFun_VLimit = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   677
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   678
goalw Univ.thy [univ_def]
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   679
    "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   680
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   681
val FiniteFun_univ = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   682
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   683
goal Univ.thy
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   684
    "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   685
by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   686
by (assume_tac 1);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   687
val FiniteFun_in_univ = result();
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   688
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   689
(*Remove <= from the rule above*)
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   690
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   691
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   692