# HG changeset patch
# User huffman
# Date 1269316492 25200
# Node ID 91a7311177c437f31b6bf3e015ecde7c5269fcda
# Parent  6943a36453e8337dbd961d7b22b9edebf03b26dd
remove contlub predicate

diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -185,23 +185,20 @@
 done
 
 lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
-lemmas contlub_Rep_CFun = cont_Rep_CFun [THEN cont2contlub]
 
 lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard]
-lemmas contlub_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2contlub, standard]
 lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard]
-lemmas contlub_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2contlub, standard]
 
 text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
 
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
-by (rule contlub_Rep_CFun2 [THEN contlubE])
+by (rule cont_Rep_CFun2 [THEN cont2contlubE])
 
 lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
 by (rule cont_Rep_CFun2 [THEN contE])
 
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
-by (rule contlub_Rep_CFun1 [THEN contlubE])
+by (rule cont_Rep_CFun1 [THEN cont2contlubE])
 
 lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
 by (rule cont_Rep_CFun1 [THEN contE])
@@ -530,26 +527,16 @@
 apply (auto simp add: monofun_cfun_arg)
 done
 
-(*FIXME: long proof*)
-lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-apply (rule contlubI)
-apply (case_tac "(\<Squnion>i. Y i) = \<bottom>")
-apply (drule (1) chain_UU_I)
-apply simp
-apply (simp del: if_image_distrib)
-apply (simp only: contlub_cfun_arg)
-apply (rule lub_equal2)
-apply (rule chain_mono2 [THEN exE])
-apply (erule chain_UU_I_inverse2)
-apply (assumption)
-apply (rule_tac x=x in exI, clarsimp)
-apply (erule chain_monofun)
-apply (erule monofun_strictify2 [THEN ch2ch_monofun])
+lemma cont_strictify2: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+apply (rule contI2)
+apply (rule monofun_strictify2)
+apply (case_tac "(\<Squnion>i. Y i) = \<bottom>", simp)
+apply (simp add: contlub_cfun_arg del: if_image_distrib)
+apply (drule chain_UU_I_inverse2, clarify, rename_tac j)
+apply (rule lub_mono2, rule_tac x=j in exI, simp_all)
+apply (auto dest!: chain_mono_less)
 done
 
-lemmas cont_strictify2 =
-  monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
-
 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
   unfolding strictify_def
   by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Cont.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -22,22 +22,17 @@
   monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
   "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
+(*
 definition
   contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
   "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
+*)
 
 definition
-  cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def" where
+  cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
+where
   "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
 
-lemma contlubI:
-  "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
-by (simp add: contlub_def)
-
-lemma contlubE: 
-  "\<lbrakk>contlub f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))" 
-by (simp add: contlub_def)
-
 lemma contI:
   "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f"
 by (simp add: cont_def)
@@ -74,16 +69,7 @@
 apply (erule ub_rangeD)
 done
 
-text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
-
-lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
-apply (rule contI)
-apply (rule thelubE)
-apply (erule (1) ch2ch_monofun)
-apply (erule (1) contlubE [symmetric])
-done
-
-text {* first a lemma about binary chains *}
+text {* a lemma about binary chains *}
 
 lemma binchain_cont:
   "\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
@@ -95,8 +81,7 @@
 apply (erule lub_bin_chain [THEN thelubI])
 done
 
-text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
-text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
+text {* continuity implies monotonicity *}
 
 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
 apply (rule monofunI)
@@ -109,33 +94,30 @@
 
 lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
 
-text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
-text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
+text {* continuity implies preservation of lubs *}
 
-lemma cont2contlub: "cont f \<Longrightarrow> contlub f"
-apply (rule contlubI)
+lemma cont2contlubE:
+  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
 apply (rule thelubI [symmetric])
 apply (erule (1) contE)
 done
 
-lemmas cont2contlubE = cont2contlub [THEN contlubE]
-
 lemma contI2:
   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 monocontlub2cont)
-apply (rule mono)
-apply (rule contlubI)
+apply (rule contI)
+apply (rule thelubE)
+apply (erule ch2ch_monofun [OF mono])
 apply (rule below_antisym)
-apply (rule below, assumption)
-apply (erule ch2ch_monofun [OF mono])
 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])
 done
 
 subsection {* Continuity simproc *}
@@ -190,7 +172,7 @@
   assumes 2: "\<And>x. cont (\<lambda>y. f x y)"
   assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
   shows "cont (\<lambda>x. (f x) (t x))"
-proof (rule monocontlub2cont [OF monofunI contlubI])
+proof (rule contI2 [OF monofunI])
   fix x y :: "'a" assume "x \<sqsubseteq> y"
   then show "f x (t x) \<sqsubseteq> f y (t y)"
     by (auto intro: cont2monofunE [OF 1]
@@ -199,11 +181,11 @@
                     below_trans)
 next
   fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
-  then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
+  then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))"
     by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
                    cont2contlubE [OF 2] ch2ch_cont [OF 2]
                    cont2contlubE [OF 3] ch2ch_cont [OF 3]
-                   diag_lub)
+                   diag_lub below_refl)
 qed
 
 lemma cont_compose:
@@ -234,9 +216,7 @@
 by (rule cont2mono [THEN monofun_finch2finch])
 
 lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
-apply (rule monocontlub2cont)
-apply assumption
-apply (rule contlubI)
+apply (erule contI2)
 apply (frule chfin2finch)
 apply (clarsimp simp add: finite_chain_def)
 apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))")
diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -324,15 +324,6 @@
 
 lemma cpo_cont_lemma:
   "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
-apply (rule monocontlub2cont, auto)
-apply (simp add: contlub_def, auto)
-apply (erule_tac x="Y" in allE, auto)
-apply (simp add: po_eq_conv)
-apply (frule cpo,auto)
-apply (frule is_lubD1)
-apply (frule ub2ub_monofun, auto)
-apply (drule thelubI, auto)
-apply (rule is_lub_thelub, auto)
-by (erule ch2ch_monofun, simp)
+by (erule contI2, simp)
 
 end
diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Ffun.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -196,22 +196,13 @@
 
 text {* the lub of a chain of continuous functions is continuous *}
 
-lemma contlub_lub_fun:
-  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
-apply (rule contlubI)
-apply (simp add: thelub_fun)
-apply (simp add: cont2contlubE)
-apply (rule ex_lub)
-apply (erule ch2ch_fun)
-apply (simp add: ch2ch_cont)
-done
-
 lemma cont_lub_fun:
   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
-apply (rule monocontlub2cont)
+apply (rule contI2)
 apply (erule monofun_lub_fun)
 apply (simp add: cont2mono)
-apply (erule (1) contlub_lub_fun)
+apply (simp add: thelub_fun cont2contlubE)
+apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
 done
 
 lemma cont2cont_lub:
@@ -224,9 +215,8 @@
 done
 
 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
-apply (rule monocontlub2cont)
+apply (rule contI2)
 apply (erule cont2mono [THEN mono2mono_fun])
-apply (rule contlubI)
 apply (simp add: cont2contlubE)
 apply (simp add: thelub_fun ch2ch_cont)
 done
@@ -242,14 +232,10 @@
 
 lemma cont2cont_lambda [simp]:
   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
-apply (subgoal_tac "monofun f")
-apply (rule monocontlub2cont)
-apply assumption
-apply (rule contlubI)
-apply (rule ext)
-apply (simp add: thelub_fun ch2ch_monofun)
-apply (erule cont2contlubE [OF f])
+apply (rule contI2)
 apply (simp add: mono2mono_lambda cont2mono f)
+apply (rule below_fun_ext)
+apply (simp add: thelub_fun cont2contlubE [OF f])
 done
 
 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
@@ -272,23 +258,12 @@
 apply (simp add: monofun_fun monofunE)
 done
 
-lemma cont2contlub_app:
-  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
-apply (rule contlubI)
-apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
-apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
-apply (simp add: cont2contlubE thelub_fun)
-apply (rule diag_lub)
-apply (erule ch2ch_fun)
-apply (drule spec)
-apply (erule (1) ch2ch_cont)
-apply (erule (1) ch2ch_cont)
-apply (erule (1) ch2ch_cont)
-done
-
 lemma cont2cont_app:
   "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
-by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
+apply (erule cont_apply [where t=t])
+apply (erule spec)
+apply (erule cont2cont_fun)
+done
 
 lemmas cont2cont_app2 = cont2cont_app [rule_format]
 
diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -203,26 +203,16 @@
 apply (erule cpo_lubI)
 done
 
-lemma contlub_fst: "contlub fst"
-apply (rule contlubI)
+lemma cont_fst: "cont fst"
+apply (rule contI)
 apply (simp add: thelub_cprod)
-done
-
-lemma contlub_snd: "contlub snd"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma cont_fst: "cont fst"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
+apply (erule cpo_lubI [OF ch2ch_fst])
 done
 
 lemma cont_snd: "cont snd"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
+apply (rule contI)
+apply (simp add: thelub_cprod)
+apply (erule cpo_lubI [OF ch2ch_snd])
 done
 
 lemma cont2cont_Pair [cont2cont]:
diff -r 6943a36453e8 -r 91a7311177c4 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/ex/Stream.thy	Mon Mar 22 20:54:52 2010 -0700
@@ -920,11 +920,8 @@
 apply (simp add: chain_def,auto)
 by (rule monofun_cfun_arg,simp)
 
-lemma contlub_scons: "contlub (%x. a && x)"
-by (simp add: contlub_Rep_CFun2)
-
 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-by (rule contlubE [OF contlub_Rep_CFun2, symmetric])
+by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric])
 
 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
                         (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
@@ -940,9 +937,6 @@
 apply (drule finite_lub_sconc,auto simp add: slen_infinite)
 done
 
-lemma contlub_sconc: "contlub (%y. x ooo y)"
-by (rule cont_sconc [THEN cont2contlub])
-
 lemma monofun_sconc: "monofun (%y. x ooo y)"
 by (simp add: monofun_def sconc_mono)