src/ZF/QUniv.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: 838
diff changeset
     1
(*  Title:      ZF/quniv
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For quniv.thy.  A small universe for lazy 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 QUniv;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
838
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    11
(** Properties involving Transset and Sum **)
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    12
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    13
val [prem1,prem2] = goalw QUniv.thy [sum_def]
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    14
    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    15
by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    16
by (REPEAT (etac (prem1 RS Transset_includes_range) 1
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    17
     ORELSE resolve_tac [conjI, singletonI] 1));
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    18
qed "Transset_includes_summands";
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    19
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    20
val [prem] = goalw QUniv.thy [sum_def]
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    21
    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    22
by (rtac (Int_Un_distrib RS ssubst) 1);
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    23
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    24
qed "Transset_sum_Int_subset";
120edb26ee93 Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents: 803
diff changeset
    25
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
(** Introduction and elimination rules avoid tiresome folding/unfolding **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
goalw QUniv.thy [quniv_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
    "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    30
by (etac PowI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    31
qed "qunivI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
goalw QUniv.thy [quniv_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    "!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    35
by (etac PowD 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    36
qed "qunivD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    40
qed "quniv_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(*** Closure properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (rtac (Transset_iff_Pow RS iffD1) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (rtac (Transset_eclose RS Transset_univ) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    47
qed "univ_eclose_subset_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
    49
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
goal QUniv.thy "univ(A) <= quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (rtac univ_eclose_subset_quniv 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    53
qed "univ_subset_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    55
bind_thm ("univ_into_quniv", univ_subset_quniv RS subsetD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    59
qed "Pow_univ_subset_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    61
bind_thm ("univ_subset_into_quniv", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
    62
          PowI RS (Pow_univ_subset_quniv RS subsetD));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    64
bind_thm ("zero_in_quniv", zero_in_univ RS univ_into_quniv);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    65
bind_thm ("one_in_quniv", one_in_univ RS univ_into_quniv);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    66
bind_thm ("two_in_quniv", two_in_univ RS univ_into_quniv);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
    68
bind_thm ("A_subset_quniv",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
    69
          [A_subset_univ, univ_subset_quniv] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val A_into_quniv = A_subset_quniv RS subsetD;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
(*** univ(A) closure for Quine-inspired pairs and injections ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*Quine ordered pairs*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
goalw QUniv.thy [QPair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "!!A a. [| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (REPEAT (ares_tac [sum_subset_univ] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    79
qed "QPair_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(** Quine disjoint sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (etac (empty_subsetI RS QPair_subset_univ) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    85
qed "QInl_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val naturals_subset_nat =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    RS bspec;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val naturals_subset_univ = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    [naturals_subset_nat, nat_subset_univ] MRS subset_trans;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
    96
qed "QInr_subset_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
(*** Closure for Quine-inspired products and sums ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*Quine ordered pairs*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
goalw QUniv.thy [quniv_def,QPair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
    "!!A a. [| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (REPEAT (dtac PowD 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   105
qed "QPair_in_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
     ORELSE eresolve_tac [QSigmaE, ssubst] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   110
qed "QSigma_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   112
bind_thm ("QSigma_subset_quniv",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   113
          [QSigma_mono, QSigma_quniv] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*The opposite inclusion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
goalw QUniv.thy [quniv_def,QPair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
129
dc50a4b96d7b expandshort and other trivial changes
lcp
parents: 120
diff changeset
   118
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   119
          Transset_includes_summands RS conjE) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (REPEAT (ares_tac [conjI,PowI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   121
qed "quniv_QPair_D";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   123
bind_thm ("quniv_QPair_E", quniv_QPair_D RS conjE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
     ORELSE etac conjE 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   128
qed "quniv_QPair_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
(** Quine disjoint sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   135
qed "QInl_in_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   139
qed "QInr_in_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
     ORELSE eresolve_tac [qsumE, ssubst] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   144
qed "qsum_quniv";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   146
bind_thm ("qsum_subset_quniv", [qsum_mono, qsum_quniv] MRS subset_trans);
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   147
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*** The natural numbers ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   151
bind_thm ("nat_subset_quniv",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   152
          [nat_subset_univ, univ_subset_quniv] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
(* n:nat ==> n:quniv(A) *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   155
bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   157
bind_thm ("bool_subset_quniv",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   158
          [bool_subset_univ, univ_subset_quniv] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   160
bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(**** Properties of Vfrom analogous to the "take-lemma" ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
(*** Intersecting a*b with Vfrom... ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
    "!!X. [| {a,b} : Vfrom(X,succ(i));  Transset(X) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   171
by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   172
by (assume_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   174
qed "doubleton_in_Vfrom_D";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
(*This weaker version says a, b exist at the same level*)
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   177
bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
      implies a, b : Vfrom(X,i), which is useless for induction.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
    The combination gives a reduction by precisely one level, which is
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
      most convenient for proofs.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
**)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
goalw Univ.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   191
qed "Pair_in_Vfrom_D";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
goal Univ.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   194
 "!!X. Transset(X) ==>          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   197
qed "product_Int_Vfrom_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
(*** Intersecting <a;b> with Vfrom... ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
goalw QUniv.thy [QPair_def,sum_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   202
 "!!X. Transset(X) ==>          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
\      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   204
by (rtac (Int_Un_distrib RS ssubst) 1);
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   205
by (rtac Un_mono 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   207
                      [Int_lower1, subset_refl] MRS Sigma_mono] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   208
qed "QPair_Int_Vfrom_succ_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   210
(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   212
(*Rule for level i -- preserving the level, not decreasing it*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
goalw QUniv.thy [QPair_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   215
 "!!X. Transset(X) ==>          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
\      <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   217
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   218
qed "QPair_Int_Vfrom_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   220
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   221
bind_thm ("QPair_Int_Vset_subset_trans", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   222
          [Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   224
goal QUniv.thy 
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   225
 "!!i. [| Ord(i) \
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   226
\      |] ==> <a;b> Int Vset(i)  <=  (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   227
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   228
(*0 case*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
by (rtac (Vfrom_0 RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (fast_tac ZF_cs 1);
170
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   231
(*succ(j) case*)
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   232
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1);
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   233
by (rtac (succI1 RS UN_upper) 1);
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   234
(*Limit(i) case*)
590c9d1e0d73 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents: 129
diff changeset
   235
by (asm_simp_tac (ZF_ss addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 838
diff changeset
   236
                                  UN_mono, QPair_Int_Vset_subset_trans]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 170
diff changeset
   237
qed "QPair_Int_Vset_subset_UN";