src/ZF/Fixedpt.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/fixedpt.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 *)
     6 
     7 header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
     8 
     9 theory Fixedpt imports equalities begin
    10 
    11 constdefs
    12   
    13   (*monotone operator from Pow(D) to itself*)
    14   bnd_mono :: "[i,i=>i]=>o"
    15      "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
    16 
    17   lfp      :: "[i,i=>i]=>i"
    18      "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
    19 
    20   gfp      :: "[i,i=>i]=>i"
    21      "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
    22 
    23 text{*The theorem is proved in the lattice of subsets of @{term D}, 
    24       namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}
    25 
    26 subsection{*Monotone Operators*}
    27 
    28 lemma bnd_monoI:
    29     "[| h(D)<=D;   
    30         !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)   
    31      |] ==> bnd_mono(D,h)"
    32 by (unfold bnd_mono_def, clarify, blast)  
    33 
    34 lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) <= D"
    35 apply (unfold bnd_mono_def)
    36 apply (erule conjunct1)
    37 done
    38 
    39 lemma bnd_monoD2: "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)"
    40 by (unfold bnd_mono_def, blast)
    41 
    42 lemma bnd_mono_subset:
    43     "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D"
    44 by (unfold bnd_mono_def, clarify, blast) 
    45 
    46 lemma bnd_mono_Un:
    47      "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A) Un h(B) <= h(A Un B)"
    48 apply (unfold bnd_mono_def)
    49 apply (rule Un_least, blast+)
    50 done
    51 
    52 (*unused*)
    53 lemma bnd_mono_UN:
    54      "[| bnd_mono(D,h);  \<forall>i\<in>I. A(i) <= D |] 
    55       ==> (\<Union>i\<in>I. h(A(i))) <= h((\<Union>i\<in>I. A(i)))"
    56 apply (unfold bnd_mono_def) 
    57 apply (rule UN_least)
    58 apply (elim conjE) 
    59 apply (drule_tac x="A(i)" in spec)
    60 apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec) 
    61 apply blast 
    62 done
    63 
    64 (*Useful??*)
    65 lemma bnd_mono_Int:
    66      "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A Int B) <= h(A) Int h(B)"
    67 apply (rule Int_greatest) 
    68 apply (erule bnd_monoD2, rule Int_lower1, assumption) 
    69 apply (erule bnd_monoD2, rule Int_lower2, assumption) 
    70 done
    71 
    72 subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
    73 
    74 (*lfp is contained in each pre-fixedpoint*)
    75 lemma lfp_lowerbound: 
    76     "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A"
    77 by (unfold lfp_def, blast)
    78 
    79 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
    80 lemma lfp_subset: "lfp(D,h) <= D"
    81 by (unfold lfp_def Inter_def, blast)
    82 
    83 (*Used in datatype package*)
    84 lemma def_lfp_subset:  "A == lfp(D,h) ==> A <= D"
    85 apply simp
    86 apply (rule lfp_subset)
    87 done
    88 
    89 lemma lfp_greatest:  
    90     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> A <= lfp(D,h)"
    91 by (unfold lfp_def, blast) 
    92 
    93 lemma lfp_lemma1:  
    94     "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A"
    95 apply (erule bnd_monoD2 [THEN subset_trans])
    96 apply (rule lfp_lowerbound, assumption+)
    97 done
    98 
    99 lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"
   100 apply (rule bnd_monoD1 [THEN lfp_greatest])
   101 apply (rule_tac [2] lfp_lemma1)
   102 apply (assumption+)
   103 done
   104 
   105 lemma lfp_lemma3: 
   106     "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"
   107 apply (rule lfp_lowerbound)
   108 apply (rule bnd_monoD2, assumption)
   109 apply (rule lfp_lemma2, assumption)
   110 apply (erule_tac [2] bnd_mono_subset)
   111 apply (rule lfp_subset)+
   112 done
   113 
   114 lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"
   115 apply (rule equalityI) 
   116 apply (erule lfp_lemma3) 
   117 apply (erule lfp_lemma2) 
   118 done
   119 
   120 (*Definition form, to control unfolding*)
   121 lemma def_lfp_unfold:
   122     "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
   123 apply simp
   124 apply (erule lfp_unfold)
   125 done
   126 
   127 subsection{*General Induction Rule for Least Fixedpoints*}
   128 
   129 lemma Collect_is_pre_fixedpt:
   130     "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |]
   131      ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"
   132 by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] 
   133                  lfp_subset [THEN subsetD]) 
   134 
   135 (*This rule yields an induction hypothesis in which the components of a
   136   data structure may be assumed to be elements of lfp(D,h)*)
   137 lemma induct:
   138     "[| bnd_mono(D,h);  a : lfp(D,h);                    
   139         !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)         
   140      |] ==> P(a)"
   141 apply (rule Collect_is_pre_fixedpt
   142               [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])
   143 apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], 
   144        blast+)
   145 done
   146 
   147 (*Definition form, to control unfolding*)
   148 lemma def_induct:
   149     "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;    
   150         !!x. x : h(Collect(A,P)) ==> P(x)  
   151      |] ==> P(a)"
   152 by (rule induct, blast+)
   153 
   154 (*This version is useful when "A" is not a subset of D
   155   second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
   156 lemma lfp_Int_lowerbound:
   157     "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A" 
   158 apply (rule lfp_lowerbound [THEN subset_trans])
   159 apply (erule bnd_mono_subset [THEN Int_greatest], blast+)
   160 done
   161 
   162 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
   163   monotonicity of h is not strictly necessary; h must be bounded by D*)
   164 lemma lfp_mono:
   165   assumes hmono: "bnd_mono(D,h)"
   166       and imono: "bnd_mono(E,i)"
   167       and subhi: "!!X. X<=D ==> h(X) <= i(X)"
   168     shows "lfp(D,h) <= lfp(E,i)"
   169 apply (rule bnd_monoD1 [THEN lfp_greatest])
   170 apply (rule imono)
   171 apply (rule hmono [THEN [2] lfp_Int_lowerbound])
   172 apply (rule Int_lower1 [THEN subhi, THEN subset_trans])
   173 apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) 
   174 done
   175 
   176 (*This (unused) version illustrates that monotonicity is not really needed,
   177   but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
   178 lemma lfp_mono2:
   179     "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)"
   180 apply (rule lfp_greatest, assumption)
   181 apply (rule lfp_lowerbound, blast, assumption)
   182 done
   183 
   184 lemma lfp_cong:
   185      "[|D=D'; !!X. X <= D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')"
   186 apply (simp add: lfp_def)
   187 apply (rule_tac t=Inter in subst_context)
   188 apply (rule Collect_cong, simp_all) 
   189 done 
   190 
   191 
   192 subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}
   193 
   194 (*gfp contains each post-fixedpoint that is contained in D*)
   195 lemma gfp_upperbound: "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)"
   196 apply (unfold gfp_def)
   197 apply (rule PowI [THEN CollectI, THEN Union_upper])
   198 apply (assumption+)
   199 done
   200 
   201 lemma gfp_subset: "gfp(D,h) <= D"
   202 by (unfold gfp_def, blast)
   203 
   204 (*Used in datatype package*)
   205 lemma def_gfp_subset: "A==gfp(D,h) ==> A <= D"
   206 apply simp
   207 apply (rule gfp_subset)
   208 done
   209 
   210 lemma gfp_least: 
   211     "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==>  
   212      gfp(D,h) <= A"
   213 apply (unfold gfp_def)
   214 apply (blast dest: bnd_monoD1) 
   215 done
   216 
   217 lemma gfp_lemma1: 
   218     "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))"
   219 apply (rule subset_trans, assumption)
   220 apply (erule bnd_monoD2)
   221 apply (rule_tac [2] gfp_subset)
   222 apply (simp add: gfp_upperbound)
   223 done
   224 
   225 lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"
   226 apply (rule gfp_least)
   227 apply (rule_tac [2] gfp_lemma1)
   228 apply (assumption+)
   229 done
   230 
   231 lemma gfp_lemma3: 
   232     "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"
   233 apply (rule gfp_upperbound)
   234 apply (rule bnd_monoD2, assumption)
   235 apply (rule gfp_lemma2, assumption)
   236 apply (erule bnd_mono_subset, rule gfp_subset)+
   237 done
   238 
   239 lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"
   240 apply (rule equalityI) 
   241 apply (erule gfp_lemma2) 
   242 apply (erule gfp_lemma3) 
   243 done
   244 
   245 (*Definition form, to control unfolding*)
   246 lemma def_gfp_unfold:
   247     "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
   248 apply simp
   249 apply (erule gfp_unfold)
   250 done
   251 
   252 
   253 subsection{*Coinduction Rules for Greatest Fixed Points*}
   254 
   255 (*weak version*)
   256 lemma weak_coinduct: "[| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)"
   257 by (blast intro: gfp_upperbound [THEN subsetD])
   258 
   259 lemma coinduct_lemma:
   260     "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>   
   261      X Un gfp(D,h) <= h(X Un gfp(D,h))"
   262 apply (erule Un_least)
   263 apply (rule gfp_lemma2 [THEN subset_trans], assumption)
   264 apply (rule Un_upper2 [THEN subset_trans])
   265 apply (rule bnd_mono_Un, assumption+) 
   266 apply (rule gfp_subset)
   267 done
   268 
   269 (*strong version*)
   270 lemma coinduct:
   271      "[| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |]
   272       ==> a : gfp(D,h)"
   273 apply (rule weak_coinduct)
   274 apply (erule_tac [2] coinduct_lemma)
   275 apply (simp_all add: gfp_subset Un_subset_iff) 
   276 done
   277 
   278 (*Definition form, to control unfolding*)
   279 lemma def_coinduct:
   280     "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==>  
   281      a : A"
   282 apply simp
   283 apply (rule coinduct, assumption+)
   284 done
   285 
   286 (*The version used in the induction/coinduction package*)
   287 lemma def_Collect_coinduct:
   288     "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));   
   289         a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==>  
   290      a : A"
   291 apply (rule def_coinduct, assumption+, blast+)
   292 done
   293 
   294 (*Monotonicity of gfp!*)
   295 lemma gfp_mono:
   296     "[| bnd_mono(D,h);  D <= E;                  
   297         !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)"
   298 apply (rule gfp_upperbound)
   299 apply (rule gfp_lemma2 [THEN subset_trans], assumption)
   300 apply (blast del: subsetI intro: gfp_subset) 
   301 apply (blast del: subsetI intro: subset_trans gfp_subset) 
   302 done
   303 
   304 ML
   305 {*
   306 val bnd_mono_def = thm "bnd_mono_def";
   307 val lfp_def = thm "lfp_def";
   308 val gfp_def = thm "gfp_def";
   309 
   310 val bnd_monoI = thm "bnd_monoI";
   311 val bnd_monoD1 = thm "bnd_monoD1";
   312 val bnd_monoD2 = thm "bnd_monoD2";
   313 val bnd_mono_subset = thm "bnd_mono_subset";
   314 val bnd_mono_Un = thm "bnd_mono_Un";
   315 val bnd_mono_Int = thm "bnd_mono_Int";
   316 val lfp_lowerbound = thm "lfp_lowerbound";
   317 val lfp_subset = thm "lfp_subset";
   318 val def_lfp_subset = thm "def_lfp_subset";
   319 val lfp_greatest = thm "lfp_greatest";
   320 val lfp_unfold = thm "lfp_unfold";
   321 val def_lfp_unfold = thm "def_lfp_unfold";
   322 val Collect_is_pre_fixedpt = thm "Collect_is_pre_fixedpt";
   323 val induct = thm "induct";
   324 val def_induct = thm "def_induct";
   325 val lfp_Int_lowerbound = thm "lfp_Int_lowerbound";
   326 val lfp_mono = thm "lfp_mono";
   327 val lfp_mono2 = thm "lfp_mono2";
   328 val gfp_upperbound = thm "gfp_upperbound";
   329 val gfp_subset = thm "gfp_subset";
   330 val def_gfp_subset = thm "def_gfp_subset";
   331 val gfp_least = thm "gfp_least";
   332 val gfp_unfold = thm "gfp_unfold";
   333 val def_gfp_unfold = thm "def_gfp_unfold";
   334 val weak_coinduct = thm "weak_coinduct";
   335 val coinduct = thm "coinduct";
   336 val def_coinduct = thm "def_coinduct";
   337 val def_Collect_coinduct = thm "def_Collect_coinduct";
   338 val gfp_mono = thm "gfp_mono";
   339 *}
   340 
   341 
   342 end