# HG changeset patch
# User hoelzl
# Date 1394533952 -3600
# Node ID 1ca060139a59c6917d440524a7f74d2083da2da1
# Parent  f78b4c3e8e843e61aaa947b2119a07c76398f56e
measurable_lfp/gfp: indirection not necessary

diff -r f78b4c3e8e84 -r 1ca060139a59 src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Mon Mar 10 23:03:51 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Tue Mar 11 11:32:32 2014 +0100
@@ -263,10 +263,9 @@
 subsection {* Measurability for (co)inductive predicates *}
 
 lemma measurable_lfp:
-  assumes "P = lfp F"
   assumes "Order_Continuity.continuous F"
   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M P"
+  shows "pred M (lfp F)"
 proof -
   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
       by (induct i) (auto intro!: *) }
@@ -274,16 +273,15 @@
     by measurable
   also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
     by (auto simp add: bot_fun_def)
-  also have "\<dots> = P"
-    unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
+  also have "\<dots> = lfp F"
+    by (rule continuous_lfp[symmetric]) fact
   finally show ?thesis .
 qed
 
 lemma measurable_gfp:
-  assumes "P = gfp F"
   assumes "Order_Continuity.down_continuous F"
   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M P"
+  shows "pred M (gfp F)"
 proof -
   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
       by (induct i) (auto intro!: *) }
@@ -291,8 +289,8 @@
     by measurable
   also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
     by (auto simp add: top_fun_def)
-  also have "\<dots> = P"
-    unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
+  also have "\<dots> = gfp F"
+    by (rule down_continuous_gfp[symmetric]) fact
   finally show ?thesis .
 qed