replace lub (range Y) with (LUB i. Y i)
authorhuffman
Tue Jul 01 02:19:53 2008 +0200 (2008-07-01)
changeset 274133154f3765cc7
parent 27412 e93b937ca933
child 27414 95ec4bda5bb9
replace lub (range Y) with (LUB i. Y i)
src/HOLCF/Adm.thy
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/FOCUS/Stream_adm.thy
src/HOLCF/Ffun.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Adm.thy	Tue Jul 01 01:28:44 2008 +0200
     1.2 +++ b/src/HOLCF/Adm.thy	Tue Jul 01 02:19:53 2008 +0200
     1.3 @@ -167,11 +167,11 @@
     1.4  unfolding compact_def .
     1.5  
     1.6  lemma compactI2:
     1.7 -  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
     1.8 +  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
     1.9  unfolding compact_def adm_def by fast
    1.10  
    1.11  lemma compactD2:
    1.12 -  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
    1.13 +  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
    1.14  unfolding compact_def adm_def by fast
    1.15  
    1.16  lemma compact_chfin [simp]: "compact (x::'a::chfin)"
     2.1 --- a/src/HOLCF/Cfun.thy	Tue Jul 01 01:28:44 2008 +0200
     2.2 +++ b/src/HOLCF/Cfun.thy	Tue Jul 01 02:19:53 2008 +0200
     2.3 @@ -192,16 +192,16 @@
     2.4  
     2.5  text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
     2.6  
     2.7 -lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(lub (range Y)) = (\<Squnion>i. f\<cdot>(Y i))"
     2.8 +lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
     2.9  by (rule contlub_Rep_CFun2 [THEN contlubE])
    2.10  
    2.11 -lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(lub (range Y))"
    2.12 +lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
    2.13  by (rule cont_Rep_CFun2 [THEN contE])
    2.14  
    2.15 -lemma contlub_cfun_fun: "chain F \<Longrightarrow> lub (range F)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
    2.16 +lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
    2.17  by (rule contlub_Rep_CFun1 [THEN contlubE])
    2.18  
    2.19 -lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| lub (range F)\<cdot>x"
    2.20 +lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
    2.21  by (rule cont_Rep_CFun1 [THEN contE])
    2.22  
    2.23  text {* monotonicity of application *}
    2.24 @@ -295,7 +295,7 @@
    2.25  lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.26  by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
    2.27  
    2.28 -lemma thelub_cfun: "chain F \<Longrightarrow> lub (range F) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.29 +lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.30  by (rule lub_cfun [THEN thelubI])
    2.31  
    2.32  subsection {* Continuity simplification procedure *}
    2.33 @@ -351,7 +351,7 @@
    2.34  text {* some lemmata for functions with flat/chfin domain/range types *}
    2.35  
    2.36  lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
    2.37 -      ==> !s. ? n. lub(range(Y))$s = Y n$s"
    2.38 +      ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
    2.39  apply (rule allI)
    2.40  apply (subst contlub_cfun_fun)
    2.41  apply assumption
    2.42 @@ -510,7 +510,7 @@
    2.43  (*FIXME: long proof*)
    2.44  lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    2.45  apply (rule contlubI)
    2.46 -apply (case_tac "lub (range Y) = \<bottom>")
    2.47 +apply (case_tac "(\<Squnion>i. Y i) = \<bottom>")
    2.48  apply (drule (1) chain_UU_I)
    2.49  apply simp
    2.50  apply (simp del: if_image_distrib)
     3.1 --- a/src/HOLCF/Cont.thy	Tue Jul 01 01:28:44 2008 +0200
     3.2 +++ b/src/HOLCF/Cont.thy	Tue Jul 01 02:19:53 2008 +0200
     3.3 @@ -153,7 +153,7 @@
     3.4  lemma contI2:
     3.5    assumes mono: "monofun f"
     3.6    assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
     3.7 -     \<Longrightarrow> f (lub (range Y)) \<sqsubseteq> (\<Squnion>i. f (Y i))"
     3.8 +     \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
     3.9    shows "cont f"
    3.10  apply (rule monocontlub2cont)
    3.11  apply (rule mono)
     4.1 --- a/src/HOLCF/Cprod.thy	Tue Jul 01 01:28:44 2008 +0200
     4.2 +++ b/src/HOLCF/Cprod.thy	Tue Jul 01 02:19:53 2008 +0200
     4.3 @@ -129,7 +129,7 @@
     4.4  
     4.5  lemma thelub_cprod:
     4.6    "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
     4.7 -    \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
     4.8 +    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
     4.9  by (rule lub_cprod [THEN thelubI])
    4.10  
    4.11  instance "*" :: (cpo, cpo) cpo
    4.12 @@ -326,7 +326,7 @@
    4.13  done
    4.14  
    4.15  lemma thelub_cprod2:
    4.16 -  "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    4.17 +  "chain S \<Longrightarrow> (\<Squnion>i. S i) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    4.18  by (rule lub_cprod2 [THEN thelubI])
    4.19  
    4.20  lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
     5.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 01 01:28:44 2008 +0200
     5.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 01 02:19:53 2008 +0200
     5.3 @@ -230,7 +230,7 @@
     5.4  by (simp add: fsfilter_fscons)
     5.5  
     5.6  lemma fstream_lub_lemma1:
     5.7 -    "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
     5.8 +    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
     5.9  apply (case_tac "max_in_chain i Y")
    5.10  apply  (drule (1) lub_finch1 [THEN thelubI, THEN sym])
    5.11  apply  (force)
    5.12 @@ -244,7 +244,7 @@
    5.13  done
    5.14  
    5.15  lemma fstream_lub_lemma:
    5.16 -      "\<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)"
    5.17 +      "\<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)"
    5.18  apply (frule (1) fstream_lub_lemma1)
    5.19  apply (clarsimp)
    5.20  apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
     6.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 01 01:28:44 2008 +0200
     6.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 01 02:19:53 2008 +0200
     6.3 @@ -236,15 +236,15 @@
     6.4  apply (simp add: flat_less_iff)
     6.5  by (simp add: flat_less_iff)
     6.6  
     6.7 -lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
     6.8 -apply (subgoal_tac "lub(range Y) ~= UU")
     6.9 +lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
    6.10 +apply (subgoal_tac "(LUB i. Y i) ~= UU")
    6.11  apply (drule chain_UU_I_inverse2, auto)
    6.12  apply (drule_tac x="i" in is_ub_thelub, auto)
    6.13  by (drule fstreams_prefix' [THEN iffD1], auto)
    6.14  
    6.15  lemma fstreams_lub1: 
    6.16 - "[| chain Y; lub (range Y) = <a> ooo s |]
    6.17 -     ==> (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)"
    6.18 + "[| chain Y; (LUB i. Y i) = <a> ooo s |]
    6.19 +     ==> (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)"
    6.20  apply (auto simp add: fstreams_lub_lemma1)
    6.21  apply (rule_tac x="%n. stream_take n$s" in exI, auto)
    6.22  apply (simp add: chain_stream_take)
    6.23 @@ -270,7 +270,7 @@
    6.24  
    6.25  
    6.26  lemma lub_Pair_not_UU_lemma: 
    6.27 -  "[| chain Y; lub (range Y) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
    6.28 +  "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
    6.29        ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
    6.30  apply (frule thelub_cprod, clarsimp)
    6.31  apply (drule chain_UU_I_inverse2, clarsimp)
    6.32 @@ -289,15 +289,15 @@
    6.33  by (drule chain_mono, auto)
    6.34  
    6.35  lemma fstreams_lub_lemma2: 
    6.36 -  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
    6.37 +  "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
    6.38  apply (frule lub_Pair_not_UU_lemma, auto)
    6.39  apply (drule_tac x="j" in is_ub_thelub, auto)
    6.40  apply (drule ax_flat, clarsimp)
    6.41  by (drule fstreams_prefix' [THEN iffD1], auto)
    6.42  
    6.43  lemma fstreams_lub2:
    6.44 -  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
    6.45 -      ==> (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)"
    6.46 +  "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
    6.47 +      ==> (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)"
    6.48  apply (auto simp add: fstreams_lub_lemma2)
    6.49  apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
    6.50  apply (simp add: chain_stream_take)
     7.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 01 01:28:44 2008 +0200
     7.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 01 02:19:53 2008 +0200
     7.3 @@ -34,8 +34,8 @@
     7.4    assumes 1: "Porder.chain Y"
     7.5    assumes 2: "!i. P (Y i)"
     7.6    assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
     7.7 -  ==> P(lub (range Y)))"
     7.8 -  shows "P(lub (range Y))"
     7.9 +  ==> P(LUB i. Y i))"
    7.10 +  shows "P(LUB i. Y i)"
    7.11  apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
    7.12  apply (erule 3, assumption)
    7.13  apply (erule thin_rl)
    7.14 @@ -59,7 +59,7 @@
    7.15  
    7.16  (* should be without reference to stream length? *)
    7.17  lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
    7.18 - !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
    7.19 + !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
    7.20  apply (unfold adm_def)
    7.21  apply (intro strip)
    7.22  apply (erule (1) flatstream_adm_lemma)
    7.23 @@ -190,13 +190,13 @@
    7.24  done
    7.25  
    7.26  lemma adm_set:
    7.27 -"{lub (range Y) |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
    7.28 +"{\<Squnion>i. Y i |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
    7.29  apply (unfold adm_def)
    7.30  apply (fast)
    7.31  done
    7.32  
    7.33 -lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {lub (range Y) |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
    7.34 -  F {lub (range Y) |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
    7.35 +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> 
    7.36 +  F {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
    7.37  apply (simp)
    7.38  apply (rule adm_set)
    7.39  apply (erule gfp_upperbound)
     8.1 --- a/src/HOLCF/Ffun.thy	Tue Jul 01 01:28:44 2008 +0200
     8.2 +++ b/src/HOLCF/Ffun.thy	Tue Jul 01 02:19:53 2008 +0200
     8.3 @@ -92,7 +92,7 @@
     8.4  
     8.5  lemma thelub_fun:
     8.6    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     8.7 -    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
     8.8 +    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
     8.9  by (rule lub_fun [THEN thelubI])
    8.10  
    8.11  lemma cpo_fun:
     9.1 --- a/src/HOLCF/Pcpo.thy	Tue Jul 01 01:28:44 2008 +0200
     9.2 +++ b/src/HOLCF/Pcpo.thy	Tue Jul 01 02:19:53 2008 +0200
     9.3 @@ -15,11 +15,11 @@
     9.4  
     9.5  axclass cpo < po
     9.6          -- {* class axiom: *}
     9.7 -  cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x" 
     9.8 +  cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
     9.9  
    9.10  text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
    9.11  
    9.12 -lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| lub (range S)"
    9.13 +lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
    9.14  by (fast dest: cpo elim: lubI)
    9.15  
    9.16  lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
    10.1 --- a/src/HOLCF/Up.thy	Tue Jul 01 01:28:44 2008 +0200
    10.2 +++ b/src/HOLCF/Up.thy	Tue Jul 01 02:19:53 2008 +0200
    10.3 @@ -154,7 +154,7 @@
    10.4  
    10.5  lemma up_chain_lemma:
    10.6    "chain Y \<Longrightarrow>
    10.7 -   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
    10.8 +   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
    10.9     (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
   10.10  apply (rule disjCI)
   10.11  apply (simp add: expand_fun_eq)
   10.12 @@ -168,7 +168,7 @@
   10.13  
   10.14  lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
   10.15  apply (frule up_chain_lemma, safe)
   10.16 -apply (rule_tac x="Iup (lub (range A))" in exI)
   10.17 +apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
   10.18  apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
   10.19  apply (simp add: is_lub_Iup cpo_lubI)
   10.20  apply (rule exI, rule lub_const)