--- 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