# HG changeset patch
# User paulson
# Date 1102498085 -3600
# Node ID 06757406d8cfd8a0c0b51bb7febb994d53eac981
# Parent  26b05d4bc21ac36e9599801d2e28841848541e3f
converted Lfp to new-style theory

diff -r 26b05d4bc21a -r 06757406d8cf TODO
--- 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)
diff -r 26b05d4bc21a -r 06757406d8cf src/HOL/Gfp.thy
--- 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";
diff -r 26b05d4bc21a -r 06757406d8cf src/HOL/IsaMakefile
--- 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 \
diff -r 26b05d4bc21a -r 06757406d8cf src/HOL/Lfp.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";
diff -r 26b05d4bc21a -r 06757406d8cf src/HOL/Lfp.thy
--- 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
diff -r 26b05d4bc21a -r 06757406d8cf src/HOL/ex/MT.ML
--- 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))";