--- a/TODO Wed Dec 08 07:50:27 2004 +0100
+++ b/TODO Wed Dec 08 10:28:05 2004 +0100
@@ -15,11 +15,11 @@
- eliminate the last remaining old-style theories (Larry):
Datatype_Universe.ML
- Gfp.ML
HOL_lemmas.ML
- Lfp.ML
NatArith.ML
Relation_Power.ML
Sum_Type.ML
+
+- update or remove ex/MT (Larry? Tobias?)
- remove this file (Tobias)
--- a/src/HOL/Gfp.thy Wed Dec 08 07:50:27 2004 +0100
+++ b/src/HOL/Gfp.thy Wed Dec 08 10:28:05 2004 +0100
@@ -4,7 +4,7 @@
*)
-header {*Greatest Fixed Points*}
+header{*Greatest Fixed Points and the Knaster-Tarski Theorem*}
theory Gfp
imports Lfp
@@ -16,10 +16,10 @@
-subsection{*Proof of Knaster-Tarski Theorem using gfp*}
+subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}
-text{*@{term "gfp f"} is the least upper bound of
+text{*@{term "gfp f"} is the greatest lower bound of
the set @{term "{u. u \<subseteq> f(u)}"} *}
lemma gfp_upperbound: "[| X \<subseteq> f(X) |] ==> X \<subseteq> gfp(f)"
@@ -118,16 +118,11 @@
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";
--- a/src/HOL/IsaMakefile Wed Dec 08 07:50:27 2004 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 08 10:28:05 2004 +0100
@@ -90,7 +90,7 @@
Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
- Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
+ Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
Nat.thy NatArith.ML NatArith.thy \
Power.thy PreList.thy Product_Type.ML Product_Type.thy \
Refute.thy ROOT.ML \
--- a/src/HOL/Lfp.ML Wed Dec 08 07:50:27 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: HOL/Lfp.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-The Knaster-Tarski Theorem.
-*)
-
-(*** Proof of Knaster-Tarski Theorem ***)
-
-val lfp_def = thm "lfp_def";
-
-(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
-
-Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
-by (rtac (CollectI RS Inter_lower) 1);
-by (assume_tac 1);
-qed "lfp_lowerbound";
-
-val prems = Goalw [lfp_def]
- "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
-by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
-by (etac CollectD 1);
-qed "lfp_greatest";
-
-Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
-by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
- etac monoD, rtac lfp_lowerbound, atac, atac]);
-qed "lfp_lemma2";
-
-Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
-by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
- etac lfp_lemma2]);
-qed "lfp_lemma3";
-
-Goal "mono(f) ==> lfp(f) = f(lfp(f))";
-by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
-qed "lfp_unfold";
-
-(*** General induction rule for least fixed points ***)
-
-val [lfp,mono,indhyp] = Goal
- "[| a: lfp(f); mono(f); \
-\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \
-\ |] ==> P(a)";
-by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
-by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
-by (EVERY1 [rtac Int_greatest, rtac subset_trans,
- rtac (Int_lower1 RS (mono RS monoD)),
- rtac (mono RS lfp_lemma2),
- rtac (CollectI RS subsetI), rtac indhyp, atac]);
-qed "lfp_induct";
-
-bind_thm ("lfp_induct2",
- split_rule (read_instantiate [("a","(a,b)")] lfp_induct));
-
-
-val major::prems = Goal
- "[| mono f; !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |] ==> \
-\ P(lfp f)";
-by(subgoal_tac "lfp f = Union{S. S <= lfp f & P S}" 1);
- by(etac ssubst 1);
- by(simp_tac (simpset() addsimps prems) 1);
-by(subgoal_tac "Union{S. S <= lfp f & P S} <= lfp f" 1);
- by(Blast_tac 2);
-by(rtac equalityI 1);
- by(atac 2);
-by(dtac (major RS monoD) 1);
-by(cut_facts_tac [major RS lfp_unfold] 1);
-by(Asm_full_simp_tac 1);
-by(rtac lfp_lowerbound 1);
-by(blast_tac (claset() addSIs prems) 1);
-qed "lfp_ordinal_induct";
-
-
-(** Definition forms of lfp_unfold and lfp_induct, to control unfolding **)
-
-Goal "[| h==lfp(f); mono(f) |] ==> h = f(h)";
-by (auto_tac (claset() addSIs [lfp_unfold], simpset()));
-qed "def_lfp_unfold";
-
-val rew::prems = Goal
- "[| A == lfp(f); mono(f); a:A; \
-\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \
-\ |] ==> P(a)";
-by (EVERY1 [rtac lfp_induct, (*backtracking to force correct induction*)
- REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
-qed "def_lfp_induct";
-
-(*Monotonicity of lfp!*)
-val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
-by (rtac (lfp_lowerbound RS lfp_greatest) 1);
-by (etac (prem RS subset_trans) 1);
-qed "lfp_mono";
--- a/src/HOL/Lfp.thy Wed Dec 08 07:50:27 2004 +0100
+++ b/src/HOL/Lfp.thy Wed Dec 08 10:28:05 2004 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
+*)
-The Knaster-Tarski Theorem
-*)
+header{*Least Fixed Points and the Knaster-Tarski Theorem*}
theory Lfp
imports Product_Type
@@ -12,6 +12,96 @@
constdefs
lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
- "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*)
+ "lfp(f) == Inter({u. f(u) \<subseteq> u})" --{*least fixed point*}
+
+
+
+subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
+
+
+text{*@{term "lfp f"} is the least upper bound of
+ the set @{term "{u. f(u) \<subseteq> u}"} *}
+
+lemma lfp_lowerbound: "f(A) \<subseteq> A ==> lfp(f) \<subseteq> A"
+by (auto simp add: lfp_def)
+
+lemma lfp_greatest: "[| !!u. f(u) \<subseteq> u ==> A\<subseteq>u |] ==> A \<subseteq> lfp(f)"
+by (auto simp add: lfp_def)
+
+lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"
+by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)
+
+lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"
+by (rules intro: lfp_lemma2 monoD lfp_lowerbound)
+
+lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"
+by (rules intro: equalityI lfp_lemma2 lfp_lemma3)
+
+subsection{*General induction rules for greatest fixed points*}
+
+lemma lfp_induct:
+ assumes lfp: "a: lfp(f)"
+ and mono: "mono(f)"
+ and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
+ shows "P(a)"
+apply (rule_tac a=a in Int_lower2 [THEN subsetD, THEN CollectD])
+apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]])
+apply (rule Int_greatest)
+ apply (rule subset_trans [OF Int_lower1 [THEN mono [THEN monoD]]
+ mono [THEN lfp_lemma2]])
+apply (blast intro: indhyp)
+done
+
+
+text{*Version of induction for binary relations*}
+lemmas lfp_induct2 = lfp_induct [of "(a,b)", split_format (complete)]
+
+
+lemma lfp_ordinal_induct:
+ assumes mono: "mono f"
+ shows "[| !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |]
+ ==> P(lfp f)"
+apply(subgoal_tac "lfp f = Union{S. S \<subseteq> lfp f & P S}")
+ apply (erule ssubst, simp)
+apply(subgoal_tac "Union{S. S \<subseteq> lfp f & P S} \<subseteq> lfp f")
+ prefer 2 apply blast
+apply(rule equalityI)
+ prefer 2 apply assumption
+apply(drule mono [THEN monoD])
+apply (cut_tac mono [THEN lfp_unfold], simp)
+apply (rule lfp_lowerbound, auto)
+done
+
+
+text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
+ to control unfolding*}
+
+lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)"
+by (auto intro!: lfp_unfold)
+
+lemma def_lfp_induct:
+ "[| A == lfp(f); mono(f); a:A;
+ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)
+ |] ==> P(a)"
+by (blast intro: lfp_induct)
+
+(*Monotonicity of lfp!*)
+lemma lfp_mono: "[| !!Z. f(Z)\<subseteq>g(Z) |] ==> lfp(f) \<subseteq> lfp(g)"
+by (rule lfp_lowerbound [THEN lfp_greatest], blast)
+
+
+ML
+{*
+val lfp_def = thm "lfp_def";
+val lfp_lowerbound = thm "lfp_lowerbound";
+val lfp_greatest = thm "lfp_greatest";
+val lfp_unfold = thm "lfp_unfold";
+val lfp_induct = thm "lfp_induct";
+val lfp_induct2 = thm "lfp_induct2";
+val lfp_ordinal_induct = thm "lfp_ordinal_induct";
+val def_lfp_unfold = thm "def_lfp_unfold";
+val def_lfp_induct = thm "def_lfp_induct";
+val lfp_mono = thm "lfp_mono";
+*}
end
--- a/src/HOL/ex/MT.ML Wed Dec 08 07:50:27 2004 +0100
+++ b/src/HOL/ex/MT.ML Wed Dec 08 10:28:05 2004 +0100
@@ -19,6 +19,11 @@
(* Inference systems *)
(* ############################################################ *)
+val lfp_lemma2 = thm "lfp_lemma2";
+val lfp_lemma3 = thm "lfp_lemma3";
+val gfp_lemma2 = thm "gfp_lemma2";
+val gfp_lemma3 = thm "gfp_lemma3";
+
val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";