# HG changeset patch
# User huffman
# Date 1214871593 -7200
# Node ID 3154f3765cc74f3ef93cfafe803f93b54b0b92c7
# Parent  e93b937ca933d5261efdb5181831f20d775f41af
replace lub (range Y) with (LUB i. Y i)

diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Adm.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -167,11 +167,11 @@
 unfolding compact_def .
 
 lemma compactI2:
-  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
+  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
 unfolding compact_def adm_def by fast
 
 lemma compactD2:
-  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
+  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
 unfolding compact_def adm_def by fast
 
 lemma compact_chfin [simp]: "compact (x::'a::chfin)"
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Cfun.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -192,16 +192,16 @@
 
 text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
 
-lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(lub (range Y)) = (\<Squnion>i. f\<cdot>(Y i))"
+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])
 
-lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(lub (range Y))"
+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> lub (range F)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
+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])
 
-lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| lub (range F)\<cdot>x"
+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])
 
 text {* monotonicity of application *}
@@ -295,7 +295,7 @@
 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
 by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
 
-lemma thelub_cfun: "chain F \<Longrightarrow> lub (range F) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
+lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
 by (rule lub_cfun [THEN thelubI])
 
 subsection {* Continuity simplification procedure *}
@@ -351,7 +351,7 @@
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
 lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
-      ==> !s. ? n. lub(range(Y))$s = Y n$s"
+      ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption
@@ -510,7 +510,7 @@
 (*FIXME: long proof*)
 lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 apply (rule contlubI)
-apply (case_tac "lub (range Y) = \<bottom>")
+apply (case_tac "(\<Squnion>i. Y i) = \<bottom>")
 apply (drule (1) chain_UU_I)
 apply simp
 apply (simp del: if_image_distrib)
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Cont.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -153,7 +153,7 @@
 lemma contI2:
   assumes mono: "monofun f"
   assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
-     \<Longrightarrow> f (lub (range Y)) \<sqsubseteq> (\<Squnion>i. f (Y i))"
+     \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   shows "cont f"
 apply (rule monocontlub2cont)
 apply (rule mono)
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Cprod.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -129,7 +129,7 @@
 
 lemma thelub_cprod:
   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
-    \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
 by (rule lub_cprod [THEN thelubI])
 
 instance "*" :: (cpo, cpo) cpo
@@ -326,7 +326,7 @@
 done
 
 lemma thelub_cprod2:
-  "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
+  "chain S \<Longrightarrow> (\<Squnion>i. S i) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
 by (rule lub_cprod2 [THEN thelubI])
 
 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -230,7 +230,7 @@
 by (simp add: fsfilter_fscons)
 
 lemma fstream_lub_lemma1:
-    "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
+    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
 apply (case_tac "max_in_chain i Y")
 apply  (drule (1) lub_finch1 [THEN thelubI, THEN sym])
 apply  (force)
@@ -244,7 +244,7 @@
 done
 
 lemma fstream_lub_lemma:
-      "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & lub (range X) = s)"
+      "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & (\<Squnion>i. X i) = s)"
 apply (frule (1) fstream_lub_lemma1)
 apply (clarsimp)
 apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -236,15 +236,15 @@
 apply (simp add: flat_less_iff)
 by (simp add: flat_less_iff)
 
-lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
-apply (subgoal_tac "lub(range Y) ~= UU")
+lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
+apply (subgoal_tac "(LUB i. Y i) ~= UU")
 apply (drule chain_UU_I_inverse2, auto)
 apply (drule_tac x="i" in is_ub_thelub, auto)
 by (drule fstreams_prefix' [THEN iffD1], auto)
 
 lemma fstreams_lub1: 
- "[| chain Y; lub (range Y) = <a> ooo s |]
-     ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & lub (range X) = s)"
+ "[| chain Y; (LUB i. Y i) = <a> ooo s |]
+     ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & (LUB i. X i) = s)"
 apply (auto simp add: fstreams_lub_lemma1)
 apply (rule_tac x="%n. stream_take n$s" in exI, auto)
 apply (simp add: chain_stream_take)
@@ -270,7 +270,7 @@
 
 
 lemma lub_Pair_not_UU_lemma: 
-  "[| chain Y; lub (range Y) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
+  "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
       ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
 apply (frule thelub_cprod, clarsimp)
 apply (drule chain_UU_I_inverse2, clarsimp)
@@ -289,15 +289,15 @@
 by (drule chain_mono, auto)
 
 lemma fstreams_lub_lemma2: 
-  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
+  "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
 apply (frule lub_Pair_not_UU_lemma, auto)
 apply (drule_tac x="j" in is_ub_thelub, auto)
 apply (drule ax_flat, clarsimp)
 by (drule fstreams_prefix' [THEN iffD1], auto)
 
 lemma fstreams_lub2:
-  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
-      ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & lub (range X) = ms)"
+  "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
+      ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & (LUB i. X i) = ms)"
 apply (auto simp add: fstreams_lub_lemma2)
 apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
 apply (simp add: chain_stream_take)
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -34,8 +34,8 @@
   assumes 1: "Porder.chain Y"
   assumes 2: "!i. P (Y i)"
   assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
-  ==> P(lub (range Y)))"
-  shows "P(lub (range Y))"
+  ==> P(LUB i. Y i))"
+  shows "P(LUB i. Y i)"
 apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
 apply (erule 3, assumption)
 apply (erule thin_rl)
@@ -59,7 +59,7 @@
 
 (* should be without reference to stream length? *)
 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
- !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
+ !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
 apply (unfold adm_def)
 apply (intro strip)
 apply (erule (1) flatstream_adm_lemma)
@@ -190,13 +190,13 @@
 done
 
 lemma adm_set:
-"{lub (range Y) |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
+"{\<Squnion>i. Y i |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
 apply (unfold adm_def)
 apply (fast)
 done
 
-lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {lub (range Y) |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
-  F {lub (range Y) |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
+lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
+  F {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
 apply (simp)
 apply (rule adm_set)
 apply (erule gfp_upperbound)
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Ffun.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -92,7 +92,7 @@
 
 lemma thelub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
-    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
+    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
 by (rule lub_fun [THEN thelubI])
 
 lemma cpo_fun:
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Pcpo.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -15,11 +15,11 @@
 
 axclass cpo < po
         -- {* class axiom: *}
-  cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x" 
+  cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
-lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| lub (range S)"
+lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
 by (fast dest: cpo elim: lubI)
 
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
diff -r e93b937ca933 -r 3154f3765cc7 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Up.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -154,7 +154,7 @@
 
 lemma up_chain_lemma:
   "chain Y \<Longrightarrow>
-   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
+   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
    (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
 apply (rule disjCI)
 apply (simp add: expand_fun_eq)
@@ -168,7 +168,7 @@
 
 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
 apply (frule up_chain_lemma, safe)
-apply (rule_tac x="Iup (lub (range A))" in exI)
+apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
 apply (simp add: is_lub_Iup cpo_lubI)
 apply (rule exI, rule lub_const)