src/ZF/Fixedpt.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (21 months ago)
changeset 67006 b1278ed3cd46
parent 60770 240563fbf41d
child 69593 3dda49e08b9d
permissions -rw-r--r--
prefer main entry points of HOL;
     1 (*  Title:      ZF/Fixedpt.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 section\<open>Least and Greatest Fixed Points; the Knaster-Tarski Theorem\<close>
     7 
     8 theory Fixedpt imports equalities begin
     9 
    10 definition 
    11   (*monotone operator from Pow(D) to itself*)
    12   bnd_mono :: "[i,i=>i]=>o"  where
    13      "bnd_mono(D,h) == h(D)<=D & (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))"
    14 
    15 definition 
    16   lfp      :: "[i,i=>i]=>i"  where
    17      "lfp(D,h) == \<Inter>({X: Pow(D). h(X) \<subseteq> X})"
    18 
    19 definition 
    20   gfp      :: "[i,i=>i]=>i"  where
    21      "gfp(D,h) == \<Union>({X: Pow(D). X \<subseteq> h(X)})"
    22 
    23 text\<open>The theorem is proved in the lattice of subsets of @{term D}, 
    24       namely @{term "Pow(D)"}, with Inter as the greatest lower bound.\<close>
    25 
    26 subsection\<open>Monotone Operators\<close>
    27 
    28 lemma bnd_monoI:
    29     "[| h(D)<=D;   
    30         !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) \<subseteq> 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) \<subseteq> 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) \<subseteq> h(X)"
    40 by (unfold bnd_mono_def, blast)
    41 
    42 lemma bnd_mono_subset:
    43     "[| bnd_mono(D,h);  X<=D |] ==> h(X) \<subseteq> D"
    44 by (unfold bnd_mono_def, clarify, blast) 
    45 
    46 lemma bnd_mono_Un:
    47      "[| bnd_mono(D,h);  A \<subseteq> D;  B \<subseteq> D |] ==> h(A) \<union> h(B) \<subseteq> h(A \<union> 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) \<subseteq> D |] 
    55       ==> (\<Union>i\<in>I. h(A(i))) \<subseteq> 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 \<subseteq> D;  B \<subseteq> D |] ==> h(A \<inter> B) \<subseteq> h(A) \<inter> 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\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    73 
    74 (*lfp is contained in each pre-fixedpoint*)
    75 lemma lfp_lowerbound: 
    76     "[| h(A) \<subseteq> A;  A<=D |] ==> lfp(D,h) \<subseteq> 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) \<subseteq> 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 \<subseteq> D"
    85 apply simp
    86 apply (rule lfp_subset)
    87 done
    88 
    89 lemma lfp_greatest:  
    90     "[| h(D) \<subseteq> D;  !!X. [| h(X) \<subseteq> X;  X<=D |] ==> A<=X |] ==> A \<subseteq> 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)) \<subseteq> 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)) \<subseteq> 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) \<subseteq> 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\<open>General Induction Rule for Least Fixedpoints\<close>
   128 
   129 lemma Collect_is_pre_fixedpt:
   130     "[| bnd_mono(D,h);  !!x. x \<in> h(Collect(lfp(D,h),P)) ==> P(x) |]
   131      ==> h(Collect(lfp(D,h),P)) \<subseteq> 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 \<in> lfp(D,h);                    
   139         !!x. x \<in> 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 \<in> 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 \<inter> A) \<subseteq> D or !!X. X<=D ==> h(X)<=D *)
   156 lemma lfp_Int_lowerbound:
   157     "[| h(D \<inter> A) \<subseteq> A;  bnd_mono(D,h) |] ==> lfp(D,h) \<subseteq> 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) \<subseteq> i(X)"
   168     shows "lfp(D,h) \<subseteq> 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) \<subseteq> D;  !!X. X<=D ==> h(X) \<subseteq> i(X)  |] ==> lfp(D,h) \<subseteq> 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 \<subseteq> 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\<open>Proof of Knaster-Tarski Theorem using @{term gfp}\<close>
   193 
   194 (*gfp contains each post-fixedpoint that is contained in D*)
   195 lemma gfp_upperbound: "[| A \<subseteq> h(A);  A<=D |] ==> A \<subseteq> 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) \<subseteq> D"
   202 by (unfold gfp_def, blast)
   203 
   204 (*Used in datatype package*)
   205 lemma def_gfp_subset: "A==gfp(D,h) ==> A \<subseteq> D"
   206 apply simp
   207 apply (rule gfp_subset)
   208 done
   209 
   210 lemma gfp_least: 
   211     "[| bnd_mono(D,h);  !!X. [| X \<subseteq> h(X);  X<=D |] ==> X<=A |] ==>  
   212      gfp(D,h) \<subseteq> 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 \<subseteq> 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) \<subseteq> 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)) \<subseteq> 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\<open>Coinduction Rules for Greatest Fixed Points\<close>
   254 
   255 (*weak version*)
   256 lemma weak_coinduct: "[| a: X;  X \<subseteq> h(X);  X \<subseteq> D |] ==> a \<in> gfp(D,h)"
   257 by (blast intro: gfp_upperbound [THEN subsetD])
   258 
   259 lemma coinduct_lemma:
   260     "[| X \<subseteq> h(X \<union> gfp(D,h));  X \<subseteq> D;  bnd_mono(D,h) |] ==>   
   261      X \<union> gfp(D,h) \<subseteq> h(X \<union> 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 \<subseteq> h(X \<union> gfp(D,h));  X \<subseteq> D |]
   272       ==> a \<in> 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 \<subseteq> h(X \<union> A);  X \<subseteq> D |] ==>  
   281      a \<in> 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 \<subseteq> D;  !!z. z: X ==> P(X \<union> A, z) |] ==>  
   290      a \<in> 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 \<subseteq> E;                  
   297         !!X. X<=D ==> h(X) \<subseteq> i(X)  |] ==> gfp(D,h) \<subseteq> 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 end