--- a/src/HOL/Gfp.ML Tue Dec 07 16:15:05 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-(* Title: HOL/Gfp.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-The Knaster-Tarski Theorem for greatest fixed points.
-*)
-
-(*** Proof of Knaster-Tarski Theorem using gfp ***)
-
-val gfp_def = thm "gfp_def";
-
-(* gfp(f) is the least upper bound of {u. u <= f(u)} *)
-
-Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
-by (etac (CollectI RS Union_upper) 1);
-qed "gfp_upperbound";
-
-val prems = Goalw [gfp_def]
- "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
-by (REPEAT (ares_tac ([Union_least]@prems) 1));
-by (etac CollectD 1);
-qed "gfp_least";
-
-Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
-by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
- etac monoD, rtac gfp_upperbound, atac]);
-qed "gfp_lemma2";
-
-Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
-by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
- etac gfp_lemma2]);
-qed "gfp_lemma3";
-
-Goal "mono(f) ==> gfp(f) = f(gfp(f))";
-by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
-qed "gfp_unfold";
-
-(*** Coinduction rules for greatest fixed points ***)
-
-(*weak version*)
-Goal "[| a: X; X <= f(X) |] ==> a : gfp(f)";
-by (rtac (gfp_upperbound RS subsetD) 1);
-by Auto_tac;
-qed "weak_coinduct";
-
-Goal "!!X. [| a : X; g`X <= f (g`X) |] ==> g a : gfp f";
-by (etac (gfp_upperbound RS subsetD) 1);
-by (etac imageI 1);
-qed "weak_coinduct_image";
-
-Goal "[| X <= f(X Un gfp(f)); mono(f) |] ==> \
-\ X Un gfp(f) <= f(X Un gfp(f))";
-by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1);
-qed "coinduct_lemma";
-
-(*strong version, thanks to Coen & Frost*)
-Goal "[| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
-by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
-by (REPEAT (ares_tac [UnI1, Un_least] 1));
-qed "coinduct";
-
-Goal "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))";
-by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1);
-qed "gfp_fun_UnI2";
-
-(*** Even Stronger version of coinduct [by Martin Coen]
- - instead of the condition X <= f(X)
- consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
-
-Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
-by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
-qed "coinduct3_mono_lemma";
-
-Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \
-\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
-by (rtac subset_trans 1);
-by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1);
-by (rtac (Un_least RS Un_least) 1);
-by (rtac subset_refl 1);
-by (assume_tac 1);
-by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1);
-by (assume_tac 1);
-by (rtac monoD 1 THEN assume_tac 1);
-by (stac (coinduct3_mono_lemma RS lfp_unfold) 1);
-by Auto_tac;
-qed "coinduct3_lemma";
-
-Goal
- "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
-by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
-by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1);
-by Auto_tac;
-qed "coinduct3";
-
-
-(** Definition forms of gfp_unfold and coinduct, to control unfolding **)
-
-Goal "[| A==gfp(f); mono(f) |] ==> A = f(A)";
-by (auto_tac (claset() addSIs [gfp_unfold], simpset()));
-qed "def_gfp_unfold";
-
-Goal "[| A==gfp(f); mono(f); a:X; X <= f(X Un A) |] ==> a: A";
-by (auto_tac (claset() addSIs [coinduct], simpset()));
-qed "def_coinduct";
-
-(*The version used in the induction/coinduction package*)
-val prems = Goal
- "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \
-\ a: X; !!z. z: X ==> P (X Un A) z |] ==> \
-\ a : A";
-by (rtac def_coinduct 1);
-by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
-qed "def_Collect_coinduct";
-
-Goal "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] \
-\ ==> a: A";
-by (auto_tac (claset() addSIs [coinduct3], simpset()));
-qed "def_coinduct3";
-
-(*Monotonicity of gfp!*)
-val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
-by (rtac (gfp_upperbound RS gfp_least) 1);
-by (etac (prem RSN (2,subset_trans)) 1);
-qed "gfp_mono";
--- a/src/HOL/Gfp.thy Tue Dec 07 16:15:05 2004 +0100
+++ b/src/HOL/Gfp.thy Tue Dec 07 16:15:44 2004 +0100
@@ -1,17 +1,140 @@
-(* Title: HOL/gfp.thy
- ID: $Id$
+(* ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Greatest fixed points (requires Lfp too!)
*)
-theory Gfp
+header {*Greatest Fixed Points*}
+
+theory Gfp
imports Lfp
begin
constdefs
gfp :: "['a set=>'a set] => 'a set"
- "gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*)
+ "gfp(f) == Union({u. u \<subseteq> f(u)})"
+
+
+
+subsection{*Proof of Knaster-Tarski Theorem using gfp*}
+
+
+text{*@{term "gfp f"} is the least upper bound of
+ the set @{term "{u. u \<subseteq> f(u)}"} *}
+
+lemma gfp_upperbound: "[| X \<subseteq> f(X) |] ==> X \<subseteq> gfp(f)"
+by (auto simp add: gfp_def)
+
+lemma gfp_least: "[| !!u. u \<subseteq> f(u) ==> u\<subseteq>X |] ==> gfp(f) \<subseteq> X"
+by (auto simp add: gfp_def)
+
+lemma gfp_lemma2: "mono(f) ==> gfp(f) \<subseteq> f(gfp(f))"
+by (rules intro: gfp_least subset_trans monoD gfp_upperbound)
+
+lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \<subseteq> gfp(f)"
+by (rules intro: gfp_lemma2 monoD gfp_upperbound)
+
+lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))"
+by (rules intro: equalityI gfp_lemma2 gfp_lemma3)
+
+subsection{*Coinduction rules for greatest fixed points*}
+
+text{*weak version*}
+lemma weak_coinduct: "[| a: X; X \<subseteq> f(X) |] ==> a : gfp(f)"
+by (rule gfp_upperbound [THEN subsetD], auto)
+
+lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
+apply (erule gfp_upperbound [THEN subsetD])
+apply (erule imageI)
+done
+
+lemma coinduct_lemma:
+ "[| X \<subseteq> f(X Un gfp(f)); mono(f) |] ==> X Un gfp(f) \<subseteq> f(X Un gfp(f))"
+by (blast dest: gfp_lemma2 mono_Un)
+
+text{*strong version, thanks to Coen and Frost*}
+lemma coinduct: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
+by (blast intro: weak_coinduct [OF _ coinduct_lemma])
+
+lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"
+by (blast dest: gfp_lemma2 mono_Un)
+
+subsection{*Even Stronger Coinduction Rule, by Martin Coen*}
+
+text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
+ @{term lfp} and @{term gfp}*}
+
+lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
+by (rules intro: subset_refl monoI Un_mono monoD)
+
+lemma coinduct3_lemma:
+ "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |]
+ ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
+apply (rule subset_trans)
+apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
+apply (rule Un_least [THEN Un_least])
+apply (rule subset_refl, assumption)
+apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
+apply (rule monoD, assumption)
+apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
+done
+
+lemma coinduct3:
+ "[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
+apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
+apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto)
+done
+
+
+text{*Definition forms of @{text gfp_unfold} and @{text coinduct},
+ to control unfolding*}
+
+lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)"
+by (auto intro!: gfp_unfold)
+
+lemma def_coinduct:
+ "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) |] ==> a: A"
+by (auto intro!: coinduct)
+
+(*The version used in the induction/coinduction package*)
+lemma def_Collect_coinduct:
+ "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w)));
+ a: X; !!z. z: X ==> P (X Un A) z |] ==>
+ a : A"
+apply (erule def_coinduct, auto)
+done
+
+lemma def_coinduct3:
+ "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
+by (auto intro!: coinduct3)
+
+text{*Monotonicity of @{term gfp}!*}
+lemma gfp_mono: "[| !!Z. f(Z)\<subseteq>g(Z) |] ==> gfp(f) \<subseteq> gfp(g)"
+by (rule gfp_upperbound [THEN gfp_least], blast)
+
+
+ML
+{*
+val gfp_def = thm "gfp_def";
+val gfp_upperbound = thm "gfp_upperbound";
+val gfp_least = thm "gfp_least";
+val gfp_lemma2 = thm "gfp_lemma2";
+val gfp_lemma3 = thm "gfp_lemma3";
+val gfp_unfold = thm "gfp_unfold";
+val weak_coinduct = thm "weak_coinduct";
+val weak_coinduct_image = thm "weak_coinduct_image";
+val coinduct_lemma = thm "coinduct_lemma";
+val coinduct = thm "coinduct";
+val gfp_fun_UnI2 = thm "gfp_fun_UnI2";
+val coinduct3_mono_lemma = thm "coinduct3_mono_lemma";
+val coinduct3_lemma = thm "coinduct3_lemma";
+val coinduct3 = thm "coinduct3";
+val def_gfp_unfold = thm "def_gfp_unfold";
+val def_coinduct = thm "def_coinduct";
+val def_Collect_coinduct = thm "def_Collect_coinduct";
+val def_coinduct3 = thm "def_coinduct3";
+val gfp_mono = thm "gfp_mono";
+*}
+
end
--- a/src/HOL/IsaMakefile Tue Dec 07 16:15:05 2004 +0100
+++ b/src/HOL/IsaMakefile Tue Dec 07 16:15:44 2004 +0100
@@ -83,7 +83,7 @@
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
- Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \
+ Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/IntArith.thy Integ/IntDef.thy \