--- a/src/HOL/ex/Refute_Examples.thy Mon May 23 16:57:02 2005 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Mon May 23 17:17:06 2005 +0200
@@ -901,8 +901,6 @@
subsection {* Inductively defined sets *}
-(*TODO: can we implement lfp/gfp more efficiently? *)
-
consts
arbitrarySet :: "'a set"
inductive arbitrarySet
@@ -910,7 +908,7 @@
"arbitrary : arbitrarySet"
lemma "x : arbitrarySet"
- (*TODO refute*) -- {* unfortunately, this little example already takes too long *}
+ refute
oops
consts
@@ -921,7 +919,7 @@
"\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
lemma "S : evenCard"
- (*TODO refute*) -- {* unfortunately, this little example already takes too long *}
+ refute
oops
consts
@@ -934,7 +932,7 @@
"n : odd \<Longrightarrow> Suc n : even"
lemma "n : odd"
- (*TODO refute*) -- {* unfortunately, this little example already takes too long *}
+ (*refute*) -- {* unfortunately, this little example already takes too long *}
oops
(******************************************************************************)
@@ -977,6 +975,18 @@
refute
oops
+lemma "f (lfp f) = lfp f"
+ refute
+oops
+
+lemma "f (gfp f) = gfp f"
+ refute
+oops
+
+lemma "lfp f = gfp f"
+ refute
+oops
+
(******************************************************************************)
subsection {* Axiomatic type classes and overloading *}