# HG changeset patch # User paulson # Date 1024390328 -7200 # Node ID 3732064ccbd1f22e1c391c82dfefde53d0ad3954 # Parent bc5dc23925785a66313b2f01954ea0df7ae5db3e conversion of Fixedpt to Isar script diff -r bc5dc2392578 -r 3732064ccbd1 src/ZF/Fixedpt.ML --- a/src/ZF/Fixedpt.ML Tue Jun 18 10:51:04 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,294 +0,0 @@ -(* Title: ZF/fixedpt.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Least and greatest fixed points; the Knaster-Tarski Theorem - -Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb -*) - -(*** Monotone operators ***) - -val prems = Goalw [bnd_mono_def] - "[| h(D)<=D; \ -\ !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) <= h(X) \ -\ |] ==> bnd_mono(D,h)"; -by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1 - ORELSE etac subset_trans 1)); -qed "bnd_monoI"; - -Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D"; -by (etac conjunct1 1); -qed "bnd_monoD1"; - -Goalw [bnd_mono_def] "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)"; -by (Blast_tac 1); -qed "bnd_monoD2"; - -val [major,minor] = goal (the_context ()) - "[| bnd_mono(D,h); X<=D |] ==> h(X) <= D"; -by (rtac (major RS bnd_monoD2 RS subset_trans) 1); -by (rtac (major RS bnd_monoD1) 3); -by (rtac minor 1); -by (rtac subset_refl 1); -qed "bnd_mono_subset"; - -Goal "[| bnd_mono(D,h); A <= D; B <= D |] ==> \ -\ h(A) Un h(B) <= h(A Un B)"; -by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1 - ORELSE etac bnd_monoD2 1)); -qed "bnd_mono_Un"; - -(*Useful??*) -Goal "[| bnd_mono(D,h); A <= D; B <= D |] ==> \ -\ h(A Int B) <= h(A) Int h(B)"; -by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1 - ORELSE etac bnd_monoD2 1)); -qed "bnd_mono_Int"; - -(**** Proof of Knaster-Tarski Theorem for the lfp ****) - -(*lfp is contained in each pre-fixedpoint*) -Goalw [lfp_def] - "[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; -by (Blast_tac 1); -(*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) -qed "lfp_lowerbound"; - -(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) -Goalw [lfp_def,Inter_def] "lfp(D,h) <= D"; -by (Blast_tac 1); -qed "lfp_subset"; - -(*Used in datatype package*) -val [rew] = goal (the_context ()) "A==lfp(D,h) ==> A <= D"; -by (rewtac rew); -by (rtac lfp_subset 1); -qed "def_lfp_subset"; - -val prems = Goalw [lfp_def] - "[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \ -\ A <= lfp(D,h)"; -by (rtac (Pow_top RS CollectI RS Inter_greatest) 1); -by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1)); -qed "lfp_greatest"; - -val hmono::prems = goal (the_context ()) - "[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) <= A"; -by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1); -by (rtac lfp_lowerbound 1); -by (REPEAT (resolve_tac prems 1)); -qed "lfp_lemma1"; - -Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"; -by (rtac (bnd_monoD1 RS lfp_greatest) 1); -by (rtac lfp_lemma1 2); -by (REPEAT (assume_tac 1)); -qed "lfp_lemma2"; - -val [hmono] = goal (the_context ()) - "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"; -by (rtac lfp_lowerbound 1); -by (rtac (hmono RS bnd_monoD2) 1); -by (rtac (hmono RS lfp_lemma2) 1); -by (rtac (hmono RS bnd_mono_subset) 2); -by (REPEAT (rtac lfp_subset 1)); -qed "lfp_lemma3"; - -Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; -by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1)); -qed "lfp_unfold"; - -(*Definition form, to control unfolding*) -val [rew,mono] = goal (the_context ()) - "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; -by (rewtac rew); -by (rtac (mono RS lfp_unfold) 1); -qed "def_lfp_unfold"; - -(*** General induction rule for least fixedpoints ***) - -val [hmono,indstep] = Goal - "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ -\ |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"; -by (rtac subsetI 1); -by (rtac CollectI 1); -by (etac indstep 2); -by (rtac (hmono RS lfp_lemma2 RS subsetD) 1); -by (rtac (hmono RS bnd_monoD2 RS subsetD) 1); -by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1)); -qed "Collect_is_pre_fixedpt"; - -(*This rule yields an induction hypothesis in which the components of a - data structure may be assumed to be elements of lfp(D,h)*) -val prems = Goal - "[| bnd_mono(D,h); a : lfp(D,h); \ -\ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ -\ |] ==> P(a)"; -by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1); -by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3); -by (REPEAT (ares_tac prems 1)); -qed "induct"; - -(*Definition form, to control unfolding*) -val rew::prems = Goal - "[| A == lfp(D,h); bnd_mono(D,h); a:A; \ -\ !!x. x : h(Collect(A,P)) ==> P(x) \ -\ |] ==> P(a)"; -by (rtac induct 1); -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); -qed "def_induct"; - -(*This version is useful when "A" is not a subset of D; - second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *) -val [hsub,hmono] = goal (the_context ()) - "[| h(D Int A) <= A; bnd_mono(D,h) |] ==> lfp(D,h) <= A"; -by (rtac (lfp_lowerbound RS subset_trans) 1); -by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1); -by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1)); -qed "lfp_Int_lowerbound"; - -(*Monotonicity of lfp, where h precedes i under a domain-like partial order - monotonicity of h is not strictly necessary; h must be bounded by D*) -val [hmono,imono,subhi] = Goal - "[| bnd_mono(D,h); bnd_mono(E,i); \ -\ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)"; -by (rtac (bnd_monoD1 RS lfp_greatest) 1); -by (rtac imono 1); -by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1); -by (rtac (Int_lower1 RS subhi RS subset_trans) 1); -by (rtac (imono RS bnd_monoD2 RS subset_trans) 1); -by (REPEAT (ares_tac [Int_lower2] 1)); -qed "lfp_mono"; - -(*This (unused) version illustrates that monotonicity is not really needed, - but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) -val [isubD,subhi] = Goal - "[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)"; -by (rtac lfp_greatest 1); -by (rtac isubD 1); -by (rtac lfp_lowerbound 1); -by (etac (subhi RS subset_trans) 1); -by (REPEAT (assume_tac 1)); -qed "lfp_mono2"; - - -(**** Proof of Knaster-Tarski Theorem for the gfp ****) - -(*gfp contains each post-fixedpoint that is contained in D*) -Goalw [gfp_def] "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)"; -by (rtac (PowI RS CollectI RS Union_upper) 1); -by (REPEAT (assume_tac 1)); -qed "gfp_upperbound"; - -Goalw [gfp_def] "gfp(D,h) <= D"; -by (Blast_tac 1); -qed "gfp_subset"; - -(*Used in datatype package*) -val [rew] = goal (the_context ()) "A==gfp(D,h) ==> A <= D"; -by (rewtac rew); -by (rtac gfp_subset 1); -qed "def_gfp_subset"; - -val hmono::prems = Goalw [gfp_def] - "[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> \ -\ gfp(D,h) <= A"; -by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1); -qed "gfp_least"; - -val hmono::prems = goal (the_context ()) - "[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A <= h(gfp(D,h))"; -by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1); -by (rtac gfp_subset 3); -by (rtac gfp_upperbound 2); -by (REPEAT (resolve_tac prems 1)); -qed "gfp_lemma1"; - -Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"; -by (rtac gfp_least 1); -by (rtac gfp_lemma1 2); -by (REPEAT (assume_tac 1)); -qed "gfp_lemma2"; - -val [hmono] = goal (the_context ()) - "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"; -by (rtac gfp_upperbound 1); -by (rtac (hmono RS bnd_monoD2) 1); -by (rtac (hmono RS gfp_lemma2) 1); -by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); -qed "gfp_lemma3"; - -Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; -by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); -qed "gfp_unfold"; - -(*Definition form, to control unfolding*) -val [rew,mono] = goal (the_context ()) - "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; -by (rewtac rew); -by (rtac (mono RS gfp_unfold) 1); -qed "def_gfp_unfold"; - - -(*** Coinduction rules for greatest fixed points ***) - -(*weak version*) -Goal "[| a: X; X <= h(X); X <= D |] ==> a : gfp(D,h)"; -by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1)); -qed "weak_coinduct"; - -val [subs_h,subs_D,mono] = goal (the_context ()) - "[| X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> \ -\ X Un gfp(D,h) <= h(X Un gfp(D,h))"; -by (rtac (subs_h RS Un_least) 1); -by (rtac (mono RS gfp_lemma2 RS subset_trans) 1); -by (rtac (Un_upper2 RS subset_trans) 1); -by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); -qed "coinduct_lemma"; - -(*strong version*) -Goal "[| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ -\ a : gfp(D,h)"; -by (rtac weak_coinduct 1); -by (etac coinduct_lemma 2); -by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); -qed "coinduct"; - -(*Definition form, to control unfolding*) -val rew::prems = goal (the_context ()) - "[| A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D |] ==> \ -\ a : A"; -by (rewtac rew); -by (rtac coinduct 1); -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); -qed "def_coinduct"; - -(*Lemma used immediately below!*) -val [subsA,XimpP] = Goal - "[| X <= A; !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)"; -by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1); -by (assume_tac 1); -by (etac XimpP 1); -qed "subset_Collect"; - -(*The version used in the induction/coinduction package*) -val prems = Goal - "[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \ -\ a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> \ -\ a : A"; -by (rtac def_coinduct 1); -by (REPEAT (ares_tac (subset_Collect::prems) 1)); -qed "def_Collect_coinduct"; - -(*Monotonicity of gfp!*) -val [hmono,subde,subhi] = Goal - "[| bnd_mono(D,h); D <= E; \ -\ !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)"; -by (rtac gfp_upperbound 1); -by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1); -by (rtac (gfp_subset RS subhi) 1); -by (rtac ([gfp_subset, subde] MRS subset_trans) 1); -qed "gfp_mono"; - diff -r bc5dc2392578 -r 3732064ccbd1 src/ZF/Fixedpt.thy --- a/src/ZF/Fixedpt.thy Tue Jun 18 10:51:04 2002 +0200 +++ b/src/ZF/Fixedpt.thy Tue Jun 18 10:52:08 2002 +0200 @@ -3,22 +3,321 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Least and greatest fixed points +Least and greatest fixed points; the Knaster-Tarski Theorem + +Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb *) -Fixedpt = equalities + +theory Fixedpt = equalities: + +constdefs + + (*monotone operator from Pow(D) to itself*) + bnd_mono :: "[i,i=>i]=>o" + "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))" + + lfp :: "[i,i=>i]=>i" + "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})" + + gfp :: "[i,i=>i]=>i" + "gfp(D,h) == Union({X: Pow(D). X <= h(X)})" + + +(*** Monotone operators ***) + +lemma bnd_monoI: + "[| h(D)<=D; + !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) <= h(X) + |] ==> bnd_mono(D,h)" +by (unfold bnd_mono_def, clarify, blast) + +lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) <= D" +apply (unfold bnd_mono_def) +apply (erule conjunct1) +done + +lemma bnd_monoD2: "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)" +by (unfold bnd_mono_def, blast) + +lemma bnd_mono_subset: + "[| bnd_mono(D,h); X<=D |] ==> h(X) <= D" +by (unfold bnd_mono_def, clarify, blast) + +lemma bnd_mono_Un: + "[| bnd_mono(D,h); A <= D; B <= D |] ==> h(A) Un h(B) <= h(A Un B)" +apply (unfold bnd_mono_def) +apply (rule Un_least, blast+) +done + +(*Useful??*) +lemma bnd_mono_Int: + "[| bnd_mono(D,h); A <= D; B <= D |] ==> h(A Int B) <= h(A) Int h(B)" +apply (rule Int_greatest) +apply (erule bnd_monoD2, rule Int_lower1, assumption) +apply (erule bnd_monoD2, rule Int_lower2, assumption) +done + +(**** Proof of Knaster-Tarski Theorem for the lfp ****) + +(*lfp is contained in each pre-fixedpoint*) +lemma lfp_lowerbound: + "[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A" +by (unfold lfp_def, blast) + +(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) +lemma lfp_subset: "lfp(D,h) <= D" +by (unfold lfp_def Inter_def, blast) + +(*Used in datatype package*) +lemma def_lfp_subset: "A == lfp(D,h) ==> A <= D" +apply simp +apply (rule lfp_subset) +done + +lemma lfp_greatest: + "[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> A <= lfp(D,h)" +by (unfold lfp_def, blast) + +lemma lfp_lemma1: + "[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) <= A" +apply (erule bnd_monoD2 [THEN subset_trans]) +apply (rule lfp_lowerbound, assumption+) +done -consts - bnd_mono :: [i,i=>i]=>o - lfp, gfp :: [i,i=>i]=>i +lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)" +apply (rule bnd_monoD1 [THEN lfp_greatest]) +apply (rule_tac [2] lfp_lemma1) +apply (assumption+) +done + +lemma lfp_lemma3: + "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))" +apply (rule lfp_lowerbound) +apply (rule bnd_monoD2, assumption) +apply (rule lfp_lemma2, assumption) +apply (erule_tac [2] bnd_mono_subset) +apply (rule lfp_subset)+ +done + +lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))" +apply (rule equalityI) +apply (erule lfp_lemma3) +apply (erule lfp_lemma2) +done + +(*Definition form, to control unfolding*) +lemma def_lfp_unfold: + "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)" +apply simp +apply (erule lfp_unfold) +done + +(*** General induction rule for least fixedpoints ***) + +lemma Collect_is_pre_fixedpt: + "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |] + ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)" +by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] + lfp_subset [THEN subsetD]) + +(*This rule yields an induction hypothesis in which the components of a + data structure may be assumed to be elements of lfp(D,h)*) +lemma induct: + "[| bnd_mono(D,h); a : lfp(D,h); + !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) + |] ==> P(a)" +apply (rule Collect_is_pre_fixedpt + [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2]) +apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], + blast+) +done + +(*Definition form, to control unfolding*) +lemma def_induct: + "[| A == lfp(D,h); bnd_mono(D,h); a:A; + !!x. x : h(Collect(A,P)) ==> P(x) + |] ==> P(a)" +by (rule induct, blast+) + +(*This version is useful when "A" is not a subset of D + second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *) +lemma lfp_Int_lowerbound: + "[| h(D Int A) <= A; bnd_mono(D,h) |] ==> lfp(D,h) <= A" +apply (rule lfp_lowerbound [THEN subset_trans]) +apply (erule bnd_mono_subset [THEN Int_greatest], blast+) +done + +(*Monotonicity of lfp, where h precedes i under a domain-like partial order + monotonicity of h is not strictly necessary; h must be bounded by D*) +lemma lfp_mono: + assumes hmono: "bnd_mono(D,h)" + and imono: "bnd_mono(E,i)" + and subhi: "!!X. X<=D ==> h(X) <= i(X)" + shows "lfp(D,h) <= lfp(E,i)" +apply (rule bnd_monoD1 [THEN lfp_greatest]) +apply (rule imono) +apply (rule hmono [THEN [2] lfp_Int_lowerbound]) +apply (rule Int_lower1 [THEN subhi, THEN subset_trans]) +apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) +done -defs - (*monotone operator from Pow(D) to itself*) - bnd_mono_def - "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))" +(*This (unused) version illustrates that monotonicity is not really needed, + but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) +lemma lfp_mono2: + "[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)" +apply (rule lfp_greatest, assumption) +apply (rule lfp_lowerbound, blast, assumption) +done + + +(**** Proof of Knaster-Tarski Theorem for the gfp ****) + +(*gfp contains each post-fixedpoint that is contained in D*) +lemma gfp_upperbound: "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)" +apply (unfold gfp_def) +apply (rule PowI [THEN CollectI, THEN Union_upper]) +apply (assumption+) +done + +lemma gfp_subset: "gfp(D,h) <= D" +by (unfold gfp_def, blast) + +(*Used in datatype package*) +lemma def_gfp_subset: "A==gfp(D,h) ==> A <= D" +apply simp +apply (rule gfp_subset) +done + +lemma gfp_least: + "[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> + gfp(D,h) <= A" +apply (unfold gfp_def) +apply (blast dest: bnd_monoD1) +done + +lemma gfp_lemma1: + "[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A <= h(gfp(D,h))" +apply (rule subset_trans, assumption) +apply (erule bnd_monoD2) +apply (rule_tac [2] gfp_subset) +apply (simp add: gfp_upperbound) +done + +lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))" +apply (rule gfp_least) +apply (rule_tac [2] gfp_lemma1) +apply (assumption+) +done + +lemma gfp_lemma3: + "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)" +apply (rule gfp_upperbound) +apply (rule bnd_monoD2, assumption) +apply (rule gfp_lemma2, assumption) +apply (erule bnd_mono_subset, rule gfp_subset)+ +done + +lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))" +apply (rule equalityI) +apply (erule gfp_lemma2) +apply (erule gfp_lemma3) +done + +(*Definition form, to control unfolding*) +lemma def_gfp_unfold: + "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)" +apply simp +apply (erule gfp_unfold) +done + + +(*** Coinduction rules for greatest fixed points ***) + +(*weak version*) +lemma weak_coinduct: "[| a: X; X <= h(X); X <= D |] ==> a : gfp(D,h)" +by (blast intro: gfp_upperbound [THEN subsetD]) - lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})" +lemma coinduct_lemma: + "[| X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> + X Un gfp(D,h) <= h(X Un gfp(D,h))" +apply (erule Un_least) +apply (rule gfp_lemma2 [THEN subset_trans], assumption) +apply (rule Un_upper2 [THEN subset_trans]) +apply (rule bnd_mono_Un, assumption+) +apply (rule gfp_subset) +done + +(*strong version*) +lemma coinduct: + "[| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] + ==> a : gfp(D,h)" +apply (rule weak_coinduct) +apply (erule_tac [2] coinduct_lemma) +apply (simp_all add: gfp_subset Un_subset_iff) +done + +(*Definition form, to control unfolding*) +lemma def_coinduct: + "[| A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D |] ==> + a : A" +apply simp +apply (rule coinduct, assumption+) +done + +(*The version used in the induction/coinduction package*) +lemma def_Collect_coinduct: + "[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); + a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> + a : A" +apply (rule def_coinduct, assumption+, blast+) +done - gfp_def "gfp(D,h) == Union({X: Pow(D). X <= h(X)})" +(*Monotonicity of gfp!*) +lemma gfp_mono: + "[| bnd_mono(D,h); D <= E; + !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)" +apply (rule gfp_upperbound) +apply (rule gfp_lemma2 [THEN subset_trans], assumption) +apply (blast del: subsetI intro: gfp_subset) +apply (blast del: subsetI intro: subset_trans gfp_subset) +done + +ML +{* +val bnd_mono_def = thm "bnd_mono_def"; +val lfp_def = thm "lfp_def"; +val gfp_def = thm "gfp_def"; + +val bnd_monoI = thm "bnd_monoI"; +val bnd_monoD1 = thm "bnd_monoD1"; +val bnd_monoD2 = thm "bnd_monoD2"; +val bnd_mono_subset = thm "bnd_mono_subset"; +val bnd_mono_Un = thm "bnd_mono_Un"; +val bnd_mono_Int = thm "bnd_mono_Int"; +val lfp_lowerbound = thm "lfp_lowerbound"; +val lfp_subset = thm "lfp_subset"; +val def_lfp_subset = thm "def_lfp_subset"; +val lfp_greatest = thm "lfp_greatest"; +val lfp_unfold = thm "lfp_unfold"; +val def_lfp_unfold = thm "def_lfp_unfold"; +val Collect_is_pre_fixedpt = thm "Collect_is_pre_fixedpt"; +val induct = thm "induct"; +val def_induct = thm "def_induct"; +val lfp_Int_lowerbound = thm "lfp_Int_lowerbound"; +val lfp_mono = thm "lfp_mono"; +val lfp_mono2 = thm "lfp_mono2"; +val gfp_upperbound = thm "gfp_upperbound"; +val gfp_subset = thm "gfp_subset"; +val def_gfp_subset = thm "def_gfp_subset"; +val gfp_least = thm "gfp_least"; +val gfp_unfold = thm "gfp_unfold"; +val def_gfp_unfold = thm "def_gfp_unfold"; +val weak_coinduct = thm "weak_coinduct"; +val coinduct = thm "coinduct"; +val def_coinduct = thm "def_coinduct"; +val def_Collect_coinduct = thm "def_Collect_coinduct"; +val gfp_mono = thm "gfp_mono"; +*} + end diff -r bc5dc2392578 -r 3732064ccbd1 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Jun 18 10:51:04 2002 +0200 +++ b/src/ZF/IsaMakefile Tue Jun 18 10:52:08 2002 +0200 @@ -32,7 +32,7 @@ ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ CardinalArith.thy Cardinal_AC.thy \ Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ - Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy \ + Fixedpt.thy Inductive.ML Inductive.thy \ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \