author skalberg Wed, 27 Aug 2003 18:13:59 +0200 changeset 14169 0590de71a016 parent 14168 ed81cd283816 child 14170 edd5a2ea3807
Converted to new style theories.
 src/HOL/Gfp.ML file | annotate | diff | comparison | revisions src/HOL/Gfp.thy file | annotate | diff | comparison | revisions src/HOL/Lfp.ML file | annotate | diff | comparison | revisions src/HOL/Lfp.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Gfp.ML	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Gfp.ML	Wed Aug 27 18:13:59 2003 +0200
@@ -8,6 +8,8 @@

(*** 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)";```
```--- a/src/HOL/Gfp.thy	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Gfp.thy	Wed Aug 27 18:13:59 2003 +0200
@@ -6,10 +6,10 @@
Greatest fixed points (requires Lfp too!)
*)

-Gfp = Lfp +
+theory Gfp = Lfp:

constdefs
-  gfp :: ['a set=>'a set] => 'a set
+  gfp :: "['a set=>'a set] => 'a set"
"gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)

end```
```--- a/src/HOL/Lfp.ML	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Lfp.ML	Wed Aug 27 18:13:59 2003 +0200
@@ -8,6 +8,8 @@

(*** 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";```
```--- a/src/HOL/Lfp.thy	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Lfp.thy	Wed Aug 27 18:13:59 2003 +0200
@@ -6,10 +6,10 @@
The Knaster-Tarski Theorem
*)

-Lfp = Product_Type +
+theory Lfp = Product_Type:

constdefs
-  lfp :: ['a set=>'a set] => 'a set
+  lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
"lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)

end```