src/ZF/Fixedpt.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 14 1c0926788772 permissions -rw-r--r--
Initial revision
```     1 (*  Title: 	ZF/fixedpt.ML
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1992  University of Cambridge
```
```     5
```
```     6 For fixedpt.thy.  Least and greatest fixed points; the Knaster-Tarski Theorem
```
```     7
```
```     8 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
```
```     9 *)
```
```    10
```
```    11 open Fixedpt;
```
```    12
```
```    13 (*** Monotone operators ***)
```
```    14
```
```    15 val prems = goalw Fixedpt.thy [bnd_mono_def]
```
```    16     "[| h(D)<=D;  \
```
```    17 \       !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)  \
```
```    18 \    |] ==> bnd_mono(D,h)";
```
```    19 by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1
```
```    20      ORELSE etac subset_trans 1));
```
```    21 val bnd_monoI = result();
```
```    22
```
```    23 val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
```
```    24 by (rtac (major RS conjunct1) 1);
```
```    25 val bnd_monoD1 = result();
```
```    26
```
```    27 val major::prems = goalw Fixedpt.thy [bnd_mono_def]
```
```    28     "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
```
```    29 by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
```
```    30 by (REPEAT (resolve_tac prems 1));
```
```    31 val bnd_monoD2 = result();
```
```    32
```
```    33 val [major,minor] = goal Fixedpt.thy
```
```    34     "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D";
```
```    35 by (rtac (major RS bnd_monoD2 RS subset_trans) 1);
```
```    36 by (rtac (major RS bnd_monoD1) 3);
```
```    37 by (rtac minor 1);
```
```    38 by (rtac subset_refl 1);
```
```    39 val bnd_mono_subset = result();
```
```    40
```
```    41 goal Fixedpt.thy "!!A B. [| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
```
```    42 \                         h(A) Un h(B) <= h(A Un B)";
```
```    43 by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1
```
```    44      ORELSE etac bnd_monoD2 1));
```
```    45 val bnd_mono_Un = result();
```
```    46
```
```    47 (*Useful??*)
```
```    48 goal Fixedpt.thy "!!A B. [| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
```
```    49 \                        h(A Int B) <= h(A) Int h(B)";
```
```    50 by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1
```
```    51      ORELSE etac bnd_monoD2 1));
```
```    52 val bnd_mono_Int = result();
```
```    53
```
```    54 (**** Proof of Knaster-Tarski Theorem for the lfp ****)
```
```    55
```
```    56 (*lfp is contained in each pre-fixedpoint*)
```
```    57 val prems = goalw Fixedpt.thy [lfp_def]
```
```    58     "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
```
```    59 by (rtac (PowI RS CollectI RS Inter_lower) 1);
```
```    60 by (REPEAT (resolve_tac prems 1));
```
```    61 val lfp_lowerbound = result();
```
```    62
```
```    63 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
```
```    64 goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D";
```
```    65 by (fast_tac ZF_cs 1);
```
```    66 val lfp_subset = result();
```
```    67
```
```    68 (*Used in datatype package*)
```
```    69 val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D";
```
```    70 by (rewtac rew);
```
```    71 by (rtac lfp_subset 1);
```
```    72 val def_lfp_subset = result();
```
```    73
```
```    74 val subset0_cs = FOL_cs
```
```    75   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
```
```    76   addIs [bexI, UnionI, ReplaceI, RepFunI]
```
```    77   addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,
```
```    78 	  CollectE, emptyE]
```
```    79   addEs [rev_ballE, InterD, make_elim InterD, subsetD];
```
```    80
```
```    81 val subset_cs = subset0_cs
```
```    82   addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
```
```    83 	  Inter_greatest,Int_greatest,RepFun_subset]
```
```    84   addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
```
```    85   addIs  [Union_upper,Inter_lower]
```
```    86   addSEs [cons_subsetE];
```
```    87
```
```    88 val prems = goalw Fixedpt.thy [lfp_def]
```
```    89     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
```
```    90 \    A <= lfp(D,h)";
```
```    91 br (Pow_top RS CollectI RS Inter_greatest) 1;
```
```    92 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
```
```    93 val lfp_greatest = result();
```
```    94
```
```    95 val hmono::prems = goal Fixedpt.thy
```
```    96     "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A";
```
```    97 by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1);
```
```    98 by (rtac lfp_lowerbound 1);
```
```    99 by (REPEAT (resolve_tac prems 1));
```
```   100 val lfp_lemma1 = result();
```
```   101
```
```   102 val [hmono] = goal Fixedpt.thy
```
```   103     "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
```
```   104 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
```
```   105 by (rtac lfp_lemma1 2);
```
```   106 by (REPEAT (ares_tac [hmono] 1));
```
```   107 val lfp_lemma2 = result();
```
```   108
```
```   109 val [hmono] = goal Fixedpt.thy
```
```   110     "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))";
```
```   111 by (rtac lfp_lowerbound 1);
```
```   112 by (rtac (hmono RS bnd_monoD2) 1);
```
```   113 by (rtac (hmono RS lfp_lemma2) 1);
```
```   114 by (rtac (hmono RS bnd_mono_subset) 2);
```
```   115 by (REPEAT (rtac lfp_subset 1));
```
```   116 val lfp_lemma3 = result();
```
```   117
```
```   118 val prems = goal Fixedpt.thy
```
```   119     "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
```
```   120 by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
```
```   121 val lfp_Tarski = result();
```
```   122
```
```   123 (*Definition form, to control unfolding*)
```
```   124 val [rew,mono] = goal Fixedpt.thy
```
```   125     "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
```
```   126 by (rewtac rew);
```
```   127 by (rtac (mono RS lfp_Tarski) 1);
```
```   128 val def_lfp_Tarski = result();
```
```   129
```
```   130 (*** General induction rule for least fixedpoints ***)
```
```   131
```
```   132 val [hmono,indstep] = goal Fixedpt.thy
```
```   133     "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
```
```   134 \    |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
```
```   135 by (rtac subsetI 1);
```
```   136 by (rtac CollectI 1);
```
```   137 by (etac indstep 2);
```
```   138 by (rtac (hmono RS lfp_lemma2 RS subsetD) 1);
```
```   139 by (rtac (hmono RS bnd_monoD2 RS subsetD) 1);
```
```   140 by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1));
```
```   141 val Collect_is_pre_fixedpt = result();
```
```   142
```
```   143 (*This rule yields an induction hypothesis in which the components of a
```
```   144   data structure may be assumed to be elements of lfp(D,h)*)
```
```   145 val prems = goal Fixedpt.thy
```
```   146     "[| bnd_mono(D,h);  a : lfp(D,h);   		\
```
```   147 \       !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) 	\
```
```   148 \    |] ==> P(a)";
```
```   149 by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1);
```
```   150 by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3);
```
```   151 by (REPEAT (ares_tac prems 1));
```
```   152 val induct = result();
```
```   153
```
```   154 (*Definition form, to control unfolding*)
```
```   155 val rew::prems = goal Fixedpt.thy
```
```   156     "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;   \
```
```   157 \       !!x. x : h(Collect(A,P)) ==> P(x) \
```
```   158 \    |] ==> P(a)";
```
```   159 by (rtac induct 1);
```
```   160 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
```
```   161 val def_induct = result();
```
```   162
```
```   163 (*This version is useful when "A" is not a subset of D;
```
```   164   second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
```
```   165 val [hsub,hmono] = goal Fixedpt.thy
```
```   166     "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A";
```
```   167 by (rtac (lfp_lowerbound RS subset_trans) 1);
```
```   168 by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1);
```
```   169 by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1));
```
```   170 val lfp_Int_lowerbound = result();
```
```   171
```
```   172 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
```
```   173   monotonicity of h is not strictly necessary; h must be bounded by D*)
```
```   174 val [hmono,imono,subhi] = goal Fixedpt.thy
```
```   175     "[| bnd_mono(D,h);  bnd_mono(E,i); 		\
```
```   176 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
```
```   177 br (bnd_monoD1 RS lfp_greatest) 1;
```
```   178 br imono 1;
```
```   179 by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
```
```   180 by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
```
```   181 by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
```
```   182 by (REPEAT (ares_tac [Int_lower2] 1));
```
```   183 val lfp_mono = result();
```
```   184
```
```   185 (*This (unused) version illustrates that monotonicity is not really needed,
```
```   186   but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
```
```   187 val [isubD,subhi] = goal Fixedpt.thy
```
```   188     "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
```
```   189 br lfp_greatest 1;
```
```   190 br isubD 1;
```
```   191 by (rtac lfp_lowerbound 1);
```
```   192 be (subhi RS subset_trans) 1;
```
```   193 by (REPEAT (assume_tac 1));
```
```   194 val lfp_mono2 = result();
```
```   195
```
```   196
```
```   197 (**** Proof of Knaster-Tarski Theorem for the gfp ****)
```
```   198
```
```   199 (*gfp contains each post-fixedpoint that is contained in D*)
```
```   200 val prems = goalw Fixedpt.thy [gfp_def]
```
```   201     "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
```
```   202 by (rtac (PowI RS CollectI RS Union_upper) 1);
```
```   203 by (REPEAT (resolve_tac prems 1));
```
```   204 val gfp_upperbound = result();
```
```   205
```
```   206 goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
```
```   207 by (fast_tac ZF_cs 1);
```
```   208 val gfp_subset = result();
```
```   209
```
```   210 (*Used in datatype package*)
```
```   211 val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D";
```
```   212 by (rewtac rew);
```
```   213 by (rtac gfp_subset 1);
```
```   214 val def_gfp_subset = result();
```
```   215
```
```   216 val hmono::prems = goalw Fixedpt.thy [gfp_def]
```
```   217     "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==> \
```
```   218 \    gfp(D,h) <= A";
```
```   219 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
```
```   220 val gfp_least = result();
```
```   221
```
```   222 val hmono::prems = goal Fixedpt.thy
```
```   223     "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))";
```
```   224 by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1);
```
```   225 by (rtac gfp_subset 3);
```
```   226 by (rtac gfp_upperbound 2);
```
```   227 by (REPEAT (resolve_tac prems 1));
```
```   228 val gfp_lemma1 = result();
```
```   229
```
```   230 val [hmono] = goal Fixedpt.thy
```
```   231     "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
```
```   232 by (rtac gfp_least 1);
```
```   233 by (rtac gfp_lemma1 2);
```
```   234 by (REPEAT (ares_tac [hmono] 1));
```
```   235 val gfp_lemma2 = result();
```
```   236
```
```   237 val [hmono] = goal Fixedpt.thy
```
```   238     "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)";
```
```   239 by (rtac gfp_upperbound 1);
```
```   240 by (rtac (hmono RS bnd_monoD2) 1);
```
```   241 by (rtac (hmono RS gfp_lemma2) 1);
```
```   242 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
```
```   243 val gfp_lemma3 = result();
```
```   244
```
```   245 val prems = goal Fixedpt.thy
```
```   246     "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
```
```   247 by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
```
```   248 val gfp_Tarski = result();
```
```   249
```
```   250 (*Definition form, to control unfolding*)
```
```   251 val [rew,mono] = goal Fixedpt.thy
```
```   252     "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
```
```   253 by (rewtac rew);
```
```   254 by (rtac (mono RS gfp_Tarski) 1);
```
```   255 val def_gfp_Tarski = result();
```
```   256
```
```   257
```
```   258 (*** Coinduction rules for greatest fixed points ***)
```
```   259
```
```   260 (*weak version*)
```
```   261 goal Fixedpt.thy "!!X h. [| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)";
```
```   262 by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1));
```
```   263 val weak_coinduct = result();
```
```   264
```
```   265 val [subs_h,subs_D,mono] = goal Fixedpt.thy
```
```   266     "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>  \
```
```   267 \    X Un gfp(D,h) <= h(X Un gfp(D,h))";
```
```   268 by (rtac (subs_h RS Un_least) 1);
```
```   269 by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
```
```   270 by (rtac (Un_upper2 RS subset_trans) 1);
```
```   271 by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1);
```
```   272 val coinduct_lemma = result();
```
```   273
```
```   274 (*strong version*)
```
```   275 goal Fixedpt.thy
```
```   276     "!!X D. [| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |] ==> \
```
```   277 \           a : gfp(D,h)";
```
```   278 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
```
```   279 by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1));
```
```   280 val coinduct = result();
```
```   281
```
```   282 (*Definition form, to control unfolding*)
```
```   283 val rew::prems = goal Fixedpt.thy
```
```   284     "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==> \
```
```   285 \    a : A";
```
```   286 by (rewtac rew);
```
```   287 by (rtac coinduct 1);
```
```   288 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
```
```   289 val def_coinduct = result();
```
```   290
```
```   291 (*Lemma used immediately below!*)
```
```   292 val [subsA,XimpP] = goal ZF.thy
```
```   293     "[| X <= A;  !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
```
```   294 by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
```
```   295 by (assume_tac 1);
```
```   296 by (etac XimpP 1);
```
```   297 val subset_Collect = result();
```
```   298
```
```   299 (*The version used in the induction/coinduction package*)
```
```   300 val prems = goal Fixedpt.thy
```
```   301     "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));  \
```
```   302 \       a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==> \
```
```   303 \    a : A";
```
```   304 by (rtac def_coinduct 1);
```
```   305 by (REPEAT (ares_tac (subset_Collect::prems) 1));
```
```   306 val def_Collect_coinduct = result();
```
```   307
```
```   308 (*Monotonicity of gfp!*)
```
```   309 val [hmono,subde,subhi] = goal Fixedpt.thy
```
```   310     "[| bnd_mono(D,h);  D <= E; 		\
```
```   311 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)";
```
```   312 by (rtac gfp_upperbound 1);
```
```   313 by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1);
```
```   314 by (rtac (gfp_subset RS subhi) 1);
```
```   315 by (rtac ([gfp_subset, subde] MRS subset_trans) 1);
```
```   316 val gfp_mono = result();
```
```   317
```