isar-style proof for lemma contI2
Fri, 26 Nov 2010 14:13:34 -0800
changeset 40736 72857de90621
parent 40735 6f65843e78f3
child 40737 2037021f034f
isar-style proof for lemma contI2
--- a/src/HOLCF/Cont.thy	Fri Nov 26 15:11:08 2010 -0800
+++ b/src/HOLCF/Cont.thy	Fri Nov 26 14:13:34 2010 -0800
@@ -97,22 +97,26 @@
 lemma contI2:
+  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
   assumes mono: "monofun f"
   assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
      \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   shows "cont f"
-apply (rule contI)
-apply (rule thelubE)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule below_antisym)
-apply (rule is_lub_thelub)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule ub2ub_monofun [OF mono])
-apply (rule is_lubD1)
-apply (erule cpo_lubI)
-apply (rule below, assumption)
-apply (erule ch2ch_monofun [OF mono])
+proof (rule contI)
+  fix Y :: "nat \<Rightarrow> 'a"
+  assume Y: "chain Y"
+  with mono have fY: "chain (\<lambda>i. f (Y i))"
+    by (rule ch2ch_monofun)
+  have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
+    apply (rule below_antisym)
+    apply (rule lub_below [OF fY])
+    apply (rule monofunE [OF mono])
+    apply (rule is_ub_thelub [OF Y])
+    apply (rule below [OF Y fY])
+    done
+  with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+    by (rule thelubE)
 subsection {* Collection of continuity rules *}