conversion of Fixedpt to Isar script
authorpaulson
Tue Jun 18 10:52:08 2002 +0200 (2002-06-18)
changeset 132183732064ccbd1
parent 13217 bc5dc2392578
child 13219 7e44aa8a276e
conversion of Fixedpt to Isar script
src/ZF/Fixedpt.ML
src/ZF/Fixedpt.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Fixedpt.ML	Tue Jun 18 10:51:04 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,294 +0,0 @@
     1.4 -(*  Title:      ZF/fixedpt.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8 -
     1.9 -Least and greatest fixed points; the Knaster-Tarski Theorem
    1.10 -
    1.11 -Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
    1.12 -*)
    1.13 -
    1.14 -(*** Monotone operators ***)
    1.15 -
    1.16 -val prems = Goalw [bnd_mono_def]
    1.17 -    "[| h(D)<=D;  \
    1.18 -\       !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)  \
    1.19 -\    |] ==> bnd_mono(D,h)";  
    1.20 -by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1
    1.21 -     ORELSE etac subset_trans 1));
    1.22 -qed "bnd_monoI";
    1.23 -
    1.24 -Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
    1.25 -by (etac conjunct1 1);
    1.26 -qed "bnd_monoD1";
    1.27 -
    1.28 -Goalw [bnd_mono_def] "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
    1.29 -by (Blast_tac 1);
    1.30 -qed "bnd_monoD2";
    1.31 -
    1.32 -val [major,minor] = goal (the_context ())
    1.33 -    "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D";
    1.34 -by (rtac (major RS bnd_monoD2 RS subset_trans) 1);
    1.35 -by (rtac (major RS bnd_monoD1) 3);
    1.36 -by (rtac minor 1);
    1.37 -by (rtac subset_refl 1);
    1.38 -qed "bnd_mono_subset";
    1.39 -
    1.40 -Goal "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
    1.41 -\                         h(A) Un h(B) <= h(A Un B)";
    1.42 -by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1
    1.43 -     ORELSE etac bnd_monoD2 1));
    1.44 -qed "bnd_mono_Un";
    1.45 -
    1.46 -(*Useful??*)
    1.47 -Goal "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
    1.48 -\                        h(A Int B) <= h(A) Int h(B)";
    1.49 -by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1
    1.50 -     ORELSE etac bnd_monoD2 1));
    1.51 -qed "bnd_mono_Int";
    1.52 -
    1.53 -(**** Proof of Knaster-Tarski Theorem for the lfp ****)
    1.54 -
    1.55 -(*lfp is contained in each pre-fixedpoint*)
    1.56 -Goalw [lfp_def]
    1.57 -    "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
    1.58 -by (Blast_tac 1);
    1.59 -(*or  by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
    1.60 -qed "lfp_lowerbound";
    1.61 -
    1.62 -(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
    1.63 -Goalw [lfp_def,Inter_def] "lfp(D,h) <= D";
    1.64 -by (Blast_tac 1);
    1.65 -qed "lfp_subset";
    1.66 -
    1.67 -(*Used in datatype package*)
    1.68 -val [rew] = goal (the_context ()) "A==lfp(D,h) ==> A <= D";
    1.69 -by (rewtac rew);
    1.70 -by (rtac lfp_subset 1);
    1.71 -qed "def_lfp_subset";
    1.72 -
    1.73 -val prems = Goalw [lfp_def]
    1.74 -    "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
    1.75 -\    A <= lfp(D,h)";
    1.76 -by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
    1.77 -by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
    1.78 -qed "lfp_greatest";
    1.79 -
    1.80 -val hmono::prems = goal (the_context ())
    1.81 -    "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A";
    1.82 -by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1);
    1.83 -by (rtac lfp_lowerbound 1);
    1.84 -by (REPEAT (resolve_tac prems 1));
    1.85 -qed "lfp_lemma1";
    1.86 -
    1.87 -Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
    1.88 -by (rtac (bnd_monoD1 RS lfp_greatest) 1);
    1.89 -by (rtac lfp_lemma1 2);
    1.90 -by (REPEAT (assume_tac 1));
    1.91 -qed "lfp_lemma2";
    1.92 -
    1.93 -val [hmono] = goal (the_context ())
    1.94 -    "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))";
    1.95 -by (rtac lfp_lowerbound 1);
    1.96 -by (rtac (hmono RS bnd_monoD2) 1);
    1.97 -by (rtac (hmono RS lfp_lemma2) 1);
    1.98 -by (rtac (hmono RS bnd_mono_subset) 2);
    1.99 -by (REPEAT (rtac lfp_subset 1));
   1.100 -qed "lfp_lemma3";
   1.101 -
   1.102 -Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
   1.103 -by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
   1.104 -qed "lfp_unfold";
   1.105 -
   1.106 -(*Definition form, to control unfolding*)
   1.107 -val [rew,mono] = goal (the_context ())
   1.108 -    "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
   1.109 -by (rewtac rew);
   1.110 -by (rtac (mono RS lfp_unfold) 1);
   1.111 -qed "def_lfp_unfold";
   1.112 -
   1.113 -(*** General induction rule for least fixedpoints ***)
   1.114 -
   1.115 -val [hmono,indstep] = Goal
   1.116 -    "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
   1.117 -\    |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
   1.118 -by (rtac subsetI 1);
   1.119 -by (rtac CollectI 1);
   1.120 -by (etac indstep 2);
   1.121 -by (rtac (hmono RS lfp_lemma2 RS subsetD) 1);
   1.122 -by (rtac (hmono RS bnd_monoD2 RS subsetD) 1);
   1.123 -by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1));
   1.124 -qed "Collect_is_pre_fixedpt";
   1.125 -
   1.126 -(*This rule yields an induction hypothesis in which the components of a
   1.127 -  data structure may be assumed to be elements of lfp(D,h)*)
   1.128 -val prems = Goal
   1.129 -    "[| bnd_mono(D,h);  a : lfp(D,h);                   \
   1.130 -\       !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)        \
   1.131 -\    |] ==> P(a)";
   1.132 -by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1);
   1.133 -by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3);
   1.134 -by (REPEAT (ares_tac prems 1));
   1.135 -qed "induct";
   1.136 -
   1.137 -(*Definition form, to control unfolding*)
   1.138 -val rew::prems = Goal
   1.139 -    "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;   \
   1.140 -\       !!x. x : h(Collect(A,P)) ==> P(x) \
   1.141 -\    |] ==> P(a)";
   1.142 -by (rtac induct 1);
   1.143 -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
   1.144 -qed "def_induct";
   1.145 -
   1.146 -(*This version is useful when "A" is not a subset of D;
   1.147 -  second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
   1.148 -val [hsub,hmono] = goal (the_context ())
   1.149 -    "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A";
   1.150 -by (rtac (lfp_lowerbound RS subset_trans) 1);
   1.151 -by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1);
   1.152 -by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1));
   1.153 -qed "lfp_Int_lowerbound";
   1.154 -
   1.155 -(*Monotonicity of lfp, where h precedes i under a domain-like partial order
   1.156 -  monotonicity of h is not strictly necessary; h must be bounded by D*)
   1.157 -val [hmono,imono,subhi] = Goal
   1.158 -    "[| bnd_mono(D,h);  bnd_mono(E,i);          \
   1.159 -\       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
   1.160 -by (rtac (bnd_monoD1 RS lfp_greatest) 1);
   1.161 -by (rtac imono 1);
   1.162 -by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
   1.163 -by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
   1.164 -by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
   1.165 -by (REPEAT (ares_tac [Int_lower2] 1));
   1.166 -qed "lfp_mono";
   1.167 -
   1.168 -(*This (unused) version illustrates that monotonicity is not really needed,
   1.169 -  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
   1.170 -val [isubD,subhi] = Goal
   1.171 -    "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
   1.172 -by (rtac lfp_greatest 1);
   1.173 -by (rtac isubD 1);
   1.174 -by (rtac lfp_lowerbound 1);
   1.175 -by (etac (subhi RS subset_trans) 1);
   1.176 -by (REPEAT (assume_tac 1));
   1.177 -qed "lfp_mono2";
   1.178 -
   1.179 -
   1.180 -(**** Proof of Knaster-Tarski Theorem for the gfp ****)
   1.181 -
   1.182 -(*gfp contains each post-fixedpoint that is contained in D*)
   1.183 -Goalw [gfp_def] "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
   1.184 -by (rtac (PowI RS CollectI RS Union_upper) 1);
   1.185 -by (REPEAT (assume_tac 1));
   1.186 -qed "gfp_upperbound";
   1.187 -
   1.188 -Goalw [gfp_def] "gfp(D,h) <= D";
   1.189 -by (Blast_tac 1);
   1.190 -qed "gfp_subset";
   1.191 -
   1.192 -(*Used in datatype package*)
   1.193 -val [rew] = goal (the_context ()) "A==gfp(D,h) ==> A <= D";
   1.194 -by (rewtac rew);
   1.195 -by (rtac gfp_subset 1);
   1.196 -qed "def_gfp_subset";
   1.197 -
   1.198 -val hmono::prems = Goalw [gfp_def]
   1.199 -    "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==> \
   1.200 -\    gfp(D,h) <= A";
   1.201 -by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
   1.202 -qed "gfp_least";
   1.203 -
   1.204 -val hmono::prems = goal (the_context ())
   1.205 -    "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))";
   1.206 -by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1);
   1.207 -by (rtac gfp_subset 3);
   1.208 -by (rtac gfp_upperbound 2);
   1.209 -by (REPEAT (resolve_tac prems 1));
   1.210 -qed "gfp_lemma1";
   1.211 -
   1.212 -Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
   1.213 -by (rtac gfp_least 1);
   1.214 -by (rtac gfp_lemma1 2);
   1.215 -by (REPEAT (assume_tac 1));
   1.216 -qed "gfp_lemma2";
   1.217 -
   1.218 -val [hmono] = goal (the_context ())
   1.219 -    "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)";
   1.220 -by (rtac gfp_upperbound 1);
   1.221 -by (rtac (hmono RS bnd_monoD2) 1);
   1.222 -by (rtac (hmono RS gfp_lemma2) 1);
   1.223 -by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
   1.224 -qed "gfp_lemma3";
   1.225 -
   1.226 -Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
   1.227 -by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
   1.228 -qed "gfp_unfold";
   1.229 -
   1.230 -(*Definition form, to control unfolding*)
   1.231 -val [rew,mono] = goal (the_context ())
   1.232 -    "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
   1.233 -by (rewtac rew);
   1.234 -by (rtac (mono RS gfp_unfold) 1);
   1.235 -qed "def_gfp_unfold";
   1.236 -
   1.237 -
   1.238 -(*** Coinduction rules for greatest fixed points ***)
   1.239 -
   1.240 -(*weak version*)
   1.241 -Goal "[| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)";
   1.242 -by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1));
   1.243 -qed "weak_coinduct";
   1.244 -
   1.245 -val [subs_h,subs_D,mono] = goal (the_context ())
   1.246 -    "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>  \
   1.247 -\    X Un gfp(D,h) <= h(X Un gfp(D,h))";
   1.248 -by (rtac (subs_h RS Un_least) 1);
   1.249 -by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
   1.250 -by (rtac (Un_upper2 RS subset_trans) 1);
   1.251 -by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1);
   1.252 -qed "coinduct_lemma";
   1.253 -
   1.254 -(*strong version*)
   1.255 -Goal "[| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |] ==> \
   1.256 -\           a : gfp(D,h)";
   1.257 -by (rtac weak_coinduct 1);
   1.258 -by (etac coinduct_lemma 2);
   1.259 -by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1));
   1.260 -qed "coinduct";
   1.261 -
   1.262 -(*Definition form, to control unfolding*)
   1.263 -val rew::prems = goal (the_context ())
   1.264 -    "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==> \
   1.265 -\    a : A";
   1.266 -by (rewtac rew);
   1.267 -by (rtac coinduct 1);
   1.268 -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
   1.269 -qed "def_coinduct";
   1.270 -
   1.271 -(*Lemma used immediately below!*)
   1.272 -val [subsA,XimpP] = Goal
   1.273 -    "[| X <= A;  !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
   1.274 -by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
   1.275 -by (assume_tac 1);
   1.276 -by (etac XimpP 1);
   1.277 -qed "subset_Collect";
   1.278 -
   1.279 -(*The version used in the induction/coinduction package*)
   1.280 -val prems = Goal
   1.281 -    "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));  \
   1.282 -\       a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==> \
   1.283 -\    a : A";
   1.284 -by (rtac def_coinduct 1);
   1.285 -by (REPEAT (ares_tac (subset_Collect::prems) 1));
   1.286 -qed "def_Collect_coinduct";
   1.287 -
   1.288 -(*Monotonicity of gfp!*)
   1.289 -val [hmono,subde,subhi] = Goal
   1.290 -    "[| bnd_mono(D,h);  D <= E;                 \
   1.291 -\       !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)";
   1.292 -by (rtac gfp_upperbound 1);
   1.293 -by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1);
   1.294 -by (rtac (gfp_subset RS subhi) 1);
   1.295 -by (rtac ([gfp_subset, subde] MRS subset_trans) 1);
   1.296 -qed "gfp_mono";
   1.297 -
     2.1 --- a/src/ZF/Fixedpt.thy	Tue Jun 18 10:51:04 2002 +0200
     2.2 +++ b/src/ZF/Fixedpt.thy	Tue Jun 18 10:52:08 2002 +0200
     2.3 @@ -3,22 +3,321 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1992  University of Cambridge
     2.6  
     2.7 -Least and greatest fixed points
     2.8 +Least and greatest fixed points; the Knaster-Tarski Theorem
     2.9 +
    2.10 +Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
    2.11  *)
    2.12  
    2.13 -Fixedpt = equalities +
    2.14 +theory Fixedpt = equalities:
    2.15 +
    2.16 +constdefs
    2.17 +  
    2.18 +  (*monotone operator from Pow(D) to itself*)
    2.19 +  bnd_mono :: "[i,i=>i]=>o"
    2.20 +     "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
    2.21 +
    2.22 +  lfp      :: "[i,i=>i]=>i"
    2.23 +     "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
    2.24 +
    2.25 +  gfp      :: "[i,i=>i]=>i"
    2.26 +     "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
    2.27 +
    2.28 +
    2.29 +(*** Monotone operators ***)
    2.30 +
    2.31 +lemma bnd_monoI:
    2.32 +    "[| h(D)<=D;   
    2.33 +        !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)   
    2.34 +     |] ==> bnd_mono(D,h)"
    2.35 +by (unfold bnd_mono_def, clarify, blast)  
    2.36 +
    2.37 +lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) <= D"
    2.38 +apply (unfold bnd_mono_def)
    2.39 +apply (erule conjunct1)
    2.40 +done
    2.41 +
    2.42 +lemma bnd_monoD2: "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)"
    2.43 +by (unfold bnd_mono_def, blast)
    2.44 +
    2.45 +lemma bnd_mono_subset:
    2.46 +    "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D"
    2.47 +by (unfold bnd_mono_def, clarify, blast) 
    2.48 +
    2.49 +lemma bnd_mono_Un:
    2.50 +     "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A) Un h(B) <= h(A Un B)"
    2.51 +apply (unfold bnd_mono_def)
    2.52 +apply (rule Un_least, blast+)
    2.53 +done
    2.54 +
    2.55 +(*Useful??*)
    2.56 +lemma bnd_mono_Int:
    2.57 +     "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A Int B) <= h(A) Int h(B)"
    2.58 +apply (rule Int_greatest) 
    2.59 +apply (erule bnd_monoD2, rule Int_lower1, assumption) 
    2.60 +apply (erule bnd_monoD2, rule Int_lower2, assumption) 
    2.61 +done
    2.62 +
    2.63 +(**** Proof of Knaster-Tarski Theorem for the lfp ****)
    2.64 +
    2.65 +(*lfp is contained in each pre-fixedpoint*)
    2.66 +lemma lfp_lowerbound: 
    2.67 +    "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A"
    2.68 +by (unfold lfp_def, blast)
    2.69 +
    2.70 +(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
    2.71 +lemma lfp_subset: "lfp(D,h) <= D"
    2.72 +by (unfold lfp_def Inter_def, blast)
    2.73 +
    2.74 +(*Used in datatype package*)
    2.75 +lemma def_lfp_subset:  "A == lfp(D,h) ==> A <= D"
    2.76 +apply simp
    2.77 +apply (rule lfp_subset)
    2.78 +done
    2.79 +
    2.80 +lemma lfp_greatest:  
    2.81 +    "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> A <= lfp(D,h)"
    2.82 +by (unfold lfp_def, blast) 
    2.83 +
    2.84 +lemma lfp_lemma1:  
    2.85 +    "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A"
    2.86 +apply (erule bnd_monoD2 [THEN subset_trans])
    2.87 +apply (rule lfp_lowerbound, assumption+)
    2.88 +done
    2.89  
    2.90 -consts
    2.91 -  bnd_mono    :: [i,i=>i]=>o
    2.92 -  lfp, gfp    :: [i,i=>i]=>i
    2.93 +lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"
    2.94 +apply (rule bnd_monoD1 [THEN lfp_greatest])
    2.95 +apply (rule_tac [2] lfp_lemma1)
    2.96 +apply (assumption+)
    2.97 +done
    2.98 +
    2.99 +lemma lfp_lemma3: 
   2.100 +    "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"
   2.101 +apply (rule lfp_lowerbound)
   2.102 +apply (rule bnd_monoD2, assumption)
   2.103 +apply (rule lfp_lemma2, assumption)
   2.104 +apply (erule_tac [2] bnd_mono_subset)
   2.105 +apply (rule lfp_subset)+
   2.106 +done
   2.107 +
   2.108 +lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"
   2.109 +apply (rule equalityI) 
   2.110 +apply (erule lfp_lemma3) 
   2.111 +apply (erule lfp_lemma2) 
   2.112 +done
   2.113 +
   2.114 +(*Definition form, to control unfolding*)
   2.115 +lemma def_lfp_unfold:
   2.116 +    "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
   2.117 +apply simp
   2.118 +apply (erule lfp_unfold)
   2.119 +done
   2.120 +
   2.121 +(*** General induction rule for least fixedpoints ***)
   2.122 +
   2.123 +lemma Collect_is_pre_fixedpt:
   2.124 +    "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |]
   2.125 +     ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"
   2.126 +by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] 
   2.127 +                 lfp_subset [THEN subsetD]) 
   2.128 +
   2.129 +(*This rule yields an induction hypothesis in which the components of a
   2.130 +  data structure may be assumed to be elements of lfp(D,h)*)
   2.131 +lemma induct:
   2.132 +    "[| bnd_mono(D,h);  a : lfp(D,h);                    
   2.133 +        !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)         
   2.134 +     |] ==> P(a)"
   2.135 +apply (rule Collect_is_pre_fixedpt
   2.136 +              [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])
   2.137 +apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], 
   2.138 +       blast+)
   2.139 +done
   2.140 +
   2.141 +(*Definition form, to control unfolding*)
   2.142 +lemma def_induct:
   2.143 +    "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;    
   2.144 +        !!x. x : h(Collect(A,P)) ==> P(x)  
   2.145 +     |] ==> P(a)"
   2.146 +by (rule induct, blast+)
   2.147 +
   2.148 +(*This version is useful when "A" is not a subset of D
   2.149 +  second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
   2.150 +lemma lfp_Int_lowerbound:
   2.151 +    "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A" 
   2.152 +apply (rule lfp_lowerbound [THEN subset_trans])
   2.153 +apply (erule bnd_mono_subset [THEN Int_greatest], blast+)
   2.154 +done
   2.155 +
   2.156 +(*Monotonicity of lfp, where h precedes i under a domain-like partial order
   2.157 +  monotonicity of h is not strictly necessary; h must be bounded by D*)
   2.158 +lemma lfp_mono:
   2.159 +  assumes hmono: "bnd_mono(D,h)"
   2.160 +      and imono: "bnd_mono(E,i)"
   2.161 +      and subhi: "!!X. X<=D ==> h(X) <= i(X)"
   2.162 +    shows "lfp(D,h) <= lfp(E,i)"
   2.163 +apply (rule bnd_monoD1 [THEN lfp_greatest])
   2.164 +apply (rule imono)
   2.165 +apply (rule hmono [THEN [2] lfp_Int_lowerbound])
   2.166 +apply (rule Int_lower1 [THEN subhi, THEN subset_trans])
   2.167 +apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) 
   2.168 +done
   2.169  
   2.170 -defs
   2.171 -  (*monotone operator from Pow(D) to itself*)
   2.172 -  bnd_mono_def 
   2.173 -      "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
   2.174 +(*This (unused) version illustrates that monotonicity is not really needed,
   2.175 +  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
   2.176 +lemma lfp_mono2:
   2.177 +    "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)"
   2.178 +apply (rule lfp_greatest, assumption)
   2.179 +apply (rule lfp_lowerbound, blast, assumption)
   2.180 +done
   2.181 +
   2.182 +
   2.183 +(**** Proof of Knaster-Tarski Theorem for the gfp ****)
   2.184 +
   2.185 +(*gfp contains each post-fixedpoint that is contained in D*)
   2.186 +lemma gfp_upperbound: "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)"
   2.187 +apply (unfold gfp_def)
   2.188 +apply (rule PowI [THEN CollectI, THEN Union_upper])
   2.189 +apply (assumption+)
   2.190 +done
   2.191 +
   2.192 +lemma gfp_subset: "gfp(D,h) <= D"
   2.193 +by (unfold gfp_def, blast)
   2.194 +
   2.195 +(*Used in datatype package*)
   2.196 +lemma def_gfp_subset: "A==gfp(D,h) ==> A <= D"
   2.197 +apply simp
   2.198 +apply (rule gfp_subset)
   2.199 +done
   2.200 +
   2.201 +lemma gfp_least: 
   2.202 +    "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==>  
   2.203 +     gfp(D,h) <= A"
   2.204 +apply (unfold gfp_def)
   2.205 +apply (blast dest: bnd_monoD1) 
   2.206 +done
   2.207 +
   2.208 +lemma gfp_lemma1: 
   2.209 +    "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))"
   2.210 +apply (rule subset_trans, assumption)
   2.211 +apply (erule bnd_monoD2)
   2.212 +apply (rule_tac [2] gfp_subset)
   2.213 +apply (simp add: gfp_upperbound)
   2.214 +done
   2.215 +
   2.216 +lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"
   2.217 +apply (rule gfp_least)
   2.218 +apply (rule_tac [2] gfp_lemma1)
   2.219 +apply (assumption+)
   2.220 +done
   2.221 +
   2.222 +lemma gfp_lemma3: 
   2.223 +    "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"
   2.224 +apply (rule gfp_upperbound)
   2.225 +apply (rule bnd_monoD2, assumption)
   2.226 +apply (rule gfp_lemma2, assumption)
   2.227 +apply (erule bnd_mono_subset, rule gfp_subset)+
   2.228 +done
   2.229 +
   2.230 +lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"
   2.231 +apply (rule equalityI) 
   2.232 +apply (erule gfp_lemma2) 
   2.233 +apply (erule gfp_lemma3) 
   2.234 +done
   2.235 +
   2.236 +(*Definition form, to control unfolding*)
   2.237 +lemma def_gfp_unfold:
   2.238 +    "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
   2.239 +apply simp
   2.240 +apply (erule gfp_unfold)
   2.241 +done
   2.242 +
   2.243 +
   2.244 +(*** Coinduction rules for greatest fixed points ***)
   2.245 +
   2.246 +(*weak version*)
   2.247 +lemma weak_coinduct: "[| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)"
   2.248 +by (blast intro: gfp_upperbound [THEN subsetD])
   2.249  
   2.250 -  lfp_def     "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
   2.251 +lemma coinduct_lemma:
   2.252 +    "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>   
   2.253 +     X Un gfp(D,h) <= h(X Un gfp(D,h))"
   2.254 +apply (erule Un_least)
   2.255 +apply (rule gfp_lemma2 [THEN subset_trans], assumption)
   2.256 +apply (rule Un_upper2 [THEN subset_trans])
   2.257 +apply (rule bnd_mono_Un, assumption+) 
   2.258 +apply (rule gfp_subset)
   2.259 +done
   2.260 +
   2.261 +(*strong version*)
   2.262 +lemma coinduct:
   2.263 +     "[| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |]
   2.264 +      ==> a : gfp(D,h)"
   2.265 +apply (rule weak_coinduct)
   2.266 +apply (erule_tac [2] coinduct_lemma)
   2.267 +apply (simp_all add: gfp_subset Un_subset_iff) 
   2.268 +done
   2.269 +
   2.270 +(*Definition form, to control unfolding*)
   2.271 +lemma def_coinduct:
   2.272 +    "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==>  
   2.273 +     a : A"
   2.274 +apply simp
   2.275 +apply (rule coinduct, assumption+)
   2.276 +done
   2.277 +
   2.278 +(*The version used in the induction/coinduction package*)
   2.279 +lemma def_Collect_coinduct:
   2.280 +    "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));   
   2.281 +        a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==>  
   2.282 +     a : A"
   2.283 +apply (rule def_coinduct, assumption+, blast+)
   2.284 +done
   2.285  
   2.286 -  gfp_def     "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
   2.287 +(*Monotonicity of gfp!*)
   2.288 +lemma gfp_mono:
   2.289 +    "[| bnd_mono(D,h);  D <= E;                  
   2.290 +        !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)"
   2.291 +apply (rule gfp_upperbound)
   2.292 +apply (rule gfp_lemma2 [THEN subset_trans], assumption)
   2.293 +apply (blast del: subsetI intro: gfp_subset) 
   2.294 +apply (blast del: subsetI intro: subset_trans gfp_subset) 
   2.295 +done
   2.296 +
   2.297 +ML
   2.298 +{*
   2.299 +val bnd_mono_def = thm "bnd_mono_def";
   2.300 +val lfp_def = thm "lfp_def";
   2.301 +val gfp_def = thm "gfp_def";
   2.302 +
   2.303 +val bnd_monoI = thm "bnd_monoI";
   2.304 +val bnd_monoD1 = thm "bnd_monoD1";
   2.305 +val bnd_monoD2 = thm "bnd_monoD2";
   2.306 +val bnd_mono_subset = thm "bnd_mono_subset";
   2.307 +val bnd_mono_Un = thm "bnd_mono_Un";
   2.308 +val bnd_mono_Int = thm "bnd_mono_Int";
   2.309 +val lfp_lowerbound = thm "lfp_lowerbound";
   2.310 +val lfp_subset = thm "lfp_subset";
   2.311 +val def_lfp_subset = thm "def_lfp_subset";
   2.312 +val lfp_greatest = thm "lfp_greatest";
   2.313 +val lfp_unfold = thm "lfp_unfold";
   2.314 +val def_lfp_unfold = thm "def_lfp_unfold";
   2.315 +val Collect_is_pre_fixedpt = thm "Collect_is_pre_fixedpt";
   2.316 +val induct = thm "induct";
   2.317 +val def_induct = thm "def_induct";
   2.318 +val lfp_Int_lowerbound = thm "lfp_Int_lowerbound";
   2.319 +val lfp_mono = thm "lfp_mono";
   2.320 +val lfp_mono2 = thm "lfp_mono2";
   2.321 +val gfp_upperbound = thm "gfp_upperbound";
   2.322 +val gfp_subset = thm "gfp_subset";
   2.323 +val def_gfp_subset = thm "def_gfp_subset";
   2.324 +val gfp_least = thm "gfp_least";
   2.325 +val gfp_unfold = thm "gfp_unfold";
   2.326 +val def_gfp_unfold = thm "def_gfp_unfold";
   2.327 +val weak_coinduct = thm "weak_coinduct";
   2.328 +val coinduct = thm "coinduct";
   2.329 +val def_coinduct = thm "def_coinduct";
   2.330 +val def_Collect_coinduct = thm "def_Collect_coinduct";
   2.331 +val gfp_mono = thm "gfp_mono";
   2.332 +*}
   2.333 +
   2.334  
   2.335  end
     3.1 --- a/src/ZF/IsaMakefile	Tue Jun 18 10:51:04 2002 +0200
     3.2 +++ b/src/ZF/IsaMakefile	Tue Jun 18 10:52:08 2002 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4    ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
     3.5    CardinalArith.thy Cardinal_AC.thy \
     3.6    Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
     3.7 -  Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy 	\
     3.8 +  Fixedpt.thy Inductive.ML Inductive.thy 	\
     3.9    InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
    3.10    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
    3.11    Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\