src/HOLCF/Cont.thy
changeset 18088 e5b23b85e932
parent 17831 4a8c3f8b0a92
child 18092 2c5d5da79a1e
equal deleted inserted replaced
18087:577d57e51f89 18088:e5b23b85e932
    90 text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
    90 text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
    91 
    91 
    92 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
    92 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
    93 apply (rule contI)
    93 apply (rule contI)
    94 apply (rule thelubE)
    94 apply (rule thelubE)
    95 apply (erule ch2ch_monofun)
    95 apply (erule (1) ch2ch_monofun)
    96 apply assumption
    96 apply (erule (1) contlubE [symmetric])
    97 apply (erule contlubE [symmetric])
       
    98 apply assumption
       
    99 done
    97 done
   100 
    98 
   101 text {* first a lemma about binary chains *}
    99 text {* first a lemma about binary chains *}
   102 
   100 
   103 lemma binchain_cont:
   101 lemma binchain_cont:
   113 text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
   111 text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
   114 text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
   112 text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
   115 
   113 
   116 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
   114 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
   117 apply (rule monofunI)
   115 apply (rule monofunI)
   118 apply (drule binchain_cont, assumption)
   116 apply (drule (1) binchain_cont)
   119 apply (drule_tac i=0 in is_ub_lub)
   117 apply (drule_tac i=0 in is_ub_lub)
   120 apply simp
   118 apply simp
   121 done
   119 done
   122 
   120 
   123 lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
   121 lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
   126 text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
   124 text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
   127 
   125 
   128 lemma cont2contlub: "cont f \<Longrightarrow> contlub f"
   126 lemma cont2contlub: "cont f \<Longrightarrow> contlub f"
   129 apply (rule contlubI)
   127 apply (rule contlubI)
   130 apply (rule thelubI [symmetric])
   128 apply (rule thelubI [symmetric])
   131 apply (erule contE)
   129 apply (erule (1) contE)
   132 apply assumption
       
   133 done
   130 done
   134 
   131 
   135 lemmas cont2contlubE = cont2contlub [THEN contlubE]
   132 lemmas cont2contlubE = cont2contlub [THEN contlubE]
   136 
   133 
   137 subsection {* Continuity of basic functions *}
   134 subsection {* Continuity of basic functions *}
   188 lemma cont_lub_fun:
   185 lemma cont_lub_fun:
   189   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   186   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   190 apply (rule monocontlub2cont)
   187 apply (rule monocontlub2cont)
   191 apply (erule monofun_lub_fun)
   188 apply (erule monofun_lub_fun)
   192 apply (simp add: cont2mono)
   189 apply (simp add: cont2mono)
   193 apply (erule contlub_lub_fun)
   190 apply (erule (1) contlub_lub_fun)
   194 apply assumption
       
   195 done
   191 done
   196 
   192 
   197 lemma cont2cont_lub:
   193 lemma cont2cont_lub:
   198   "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
   194   "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
   199 by (simp add: thelub_fun [symmetric] cont_lub_fun)
   195 by (simp add: thelub_fun [symmetric] cont_lub_fun)
   229 apply (blast dest: cont2contlubE)
   225 apply (blast dest: cont2contlubE)
   230 apply (simp add: mono2mono_MF1L_rev cont2mono)
   226 apply (simp add: mono2mono_MF1L_rev cont2mono)
   231 done
   227 done
   232 
   228 
   233 lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. (\<lambda>y. f x y))"
   229 lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. (\<lambda>y. f x y))"
   234 apply (rule cont2cont_CF1L_rev)
   230 by (rule cont2cont_CF1L_rev, simp)
   235 apply simp
       
   236 done
       
   237 
   231 
   238 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   232 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   239 
   233 
   240 lemma contlub_abstraction:
   234 lemma contlub_abstraction:
   241   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
   235   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
   242     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
   236     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
       
   237 apply (drule cont2cont_CF1L_rev)
   243 apply (rule thelub_fun [symmetric])
   238 apply (rule thelub_fun [symmetric])
   244 apply (rule ch2ch_cont)
   239 apply (erule (1) ch2ch_cont)
   245 apply (erule (1) cont2cont_CF1L_rev)
       
   246 done
   240 done
   247 
   241 
   248 lemma mono2mono_app:
   242 lemma mono2mono_app:
   249   "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
   243   "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
   250 apply (rule monofunI)
   244 apply (rule monofunI)