--- a/src/HOL/Inductive.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Inductive.thy Fri Jul 03 08:26:34 2015 +0200
@@ -230,7 +230,6 @@
apply (simp_all)
done
-
text{*Definition forms of @{text gfp_unfold} and @{text coinduct},
to control unfolding*}
@@ -283,15 +282,6 @@
qed
qed
-lemma lfp_square:
- assumes "mono f" shows "lfp f = lfp (\<lambda>x. f (f x))"
-proof (rule antisym)
- show "lfp f \<le> lfp (\<lambda>x. f (f x))"
- by (intro lfp_lowerbound) (simp add: assms lfp_rolling)
- show "lfp (\<lambda>x. f (f x)) \<le> lfp f"
- by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric])
-qed
-
lemma lfp_lfp:
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
@@ -330,15 +320,6 @@
qed
qed
-lemma gfp_square:
- assumes "mono f" shows "gfp f = gfp (\<lambda>x. f (f x))"
-proof (rule antisym)
- show "gfp (\<lambda>x. f (f x)) \<le> gfp f"
- by (intro gfp_upperbound) (simp add: assms gfp_rolling)
- show "gfp f \<le> gfp (\<lambda>x. f (f x))"
- by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric])
-qed
-
lemma gfp_gfp:
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"