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