src/HOLCF/Ffun.thy
changeset 25786 6b3c79acac1f
parent 25758 89c7c22e64b4
child 25827 c2adeb1bae5c
equal deleted inserted replaced
25785:dbe118fe3180 25786:6b3c79acac1f
     8 *)
     8 *)
     9 
     9 
    10 header {* Class instances for the full function space *}
    10 header {* Class instances for the full function space *}
    11 
    11 
    12 theory Ffun
    12 theory Ffun
    13 imports Pcpo
    13 imports Cont
    14 begin
    14 begin
    15 
    15 
    16 subsection {* Full function space is a partial order *}
    16 subsection {* Full function space is a partial order *}
    17 
    17 
    18 instantiation "fun"  :: (type, sq_ord) sq_ord
    18 instantiation "fun"  :: (type, sq_ord) sq_ord
    47 lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    47 lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    48 by (simp add: less_fun_def)
    48 by (simp add: less_fun_def)
    49 
    49 
    50 subsection {* Full function space is chain complete *}
    50 subsection {* Full function space is chain complete *}
    51 
    51 
       
    52 text {* function application is monotone *}
       
    53 
       
    54 lemma monofun_app: "monofun (\<lambda>f. f x)"
       
    55 by (rule monofunI, simp add: less_fun_def)
       
    56 
    52 text {* chains of functions yield chains in the po range *}
    57 text {* chains of functions yield chains in the po range *}
    53 
    58 
    54 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    59 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    55 by (simp add: chain_def less_fun_def)
    60 by (simp add: chain_def less_fun_def)
    56 
    61 
    59 
    64 
    60 
    65 
    61 text {* upper bounds of function chains yield upper bound in the po range *}
    66 text {* upper bounds of function chains yield upper bound in the po range *}
    62 
    67 
    63 lemma ub2ub_fun:
    68 lemma ub2ub_fun:
    64   "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    69   "range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    65 by (auto simp add: is_ub_def less_fun_def)
    70 by (auto simp add: is_ub_def less_fun_def)
    66 
    71 
    67 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    72 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    68 
    73 
    69 lemma lub_fun:
    74 lemma lub_fun:
    78 apply (rule is_lub_thelub)
    83 apply (rule is_lub_thelub)
    79 apply (erule ch2ch_fun)
    84 apply (erule ch2ch_fun)
    80 apply (erule ub2ub_fun)
    85 apply (erule ub2ub_fun)
    81 done
    86 done
    82 
    87 
       
    88 lemma lub_fun':
       
    89   fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set"
       
    90   assumes S: "directed S"
       
    91   shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)"
       
    92 apply (rule is_lubI)
       
    93 apply (rule is_ubI)
       
    94 apply (rule less_fun_ext)
       
    95 apply (rule is_ub_thelub')
       
    96 apply (rule dir2dir_monofun [OF monofun_app S])
       
    97 apply (erule imageI)
       
    98 apply (rule less_fun_ext)
       
    99 apply (rule is_lub_thelub')
       
   100 apply (rule dir2dir_monofun [OF monofun_app S])
       
   101 apply (erule ub2ub_monofun' [OF monofun_app])
       
   102 done
       
   103 
    83 lemma thelub_fun:
   104 lemma thelub_fun:
    84   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
   105   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    85     \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
   106     \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
    86 by (rule lub_fun [THEN thelubI])
   107 by (rule lub_fun [THEN thelubI])
    87 
   108 
       
   109 lemma thelub_fun':
       
   110   "directed (S::('a::type \<Rightarrow> 'b::dcpo) set)
       
   111     \<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)"
       
   112 by (rule lub_fun' [THEN thelubI])
       
   113 
    88 lemma cpo_fun:
   114 lemma cpo_fun:
    89   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
   115   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
    90 by (rule exI, erule lub_fun)
   116 by (rule exI, erule lub_fun)
    91 
   117 
    92 instance "fun"  :: (type, cpo) cpo
   118 instance "fun"  :: (type, cpo) cpo
    93 by intro_classes (rule cpo_fun)
   119 by intro_classes (rule cpo_fun)
    94 
   120 
       
   121 lemma dcpo_fun:
       
   122   "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x"
       
   123 by (rule exI, erule lub_fun')
       
   124 
       
   125 instance "fun" :: (type, dcpo) dcpo
       
   126 by intro_classes (rule dcpo_fun)
       
   127 
    95 subsection {* Full function space is pointed *}
   128 subsection {* Full function space is pointed *}
    96 
   129 
    97 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   130 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
    98 by (simp add: less_fun_def)
   131 by (simp add: less_fun_def)
    99 
   132 
   100 lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
   133 lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
   101 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
   134 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
   102 apply (rule minimal_fun [THEN allI])
   135 apply (rule minimal_fun [THEN allI])
   103 done
   136 done
   104 
   137 
   105 instance "fun"  :: (type, pcpo) pcpo
   138 instance "fun"  :: (type, pcpo) pcpo
   111 
   144 
   112 text {* function application is strict in the left argument *}
   145 text {* function application is strict in the left argument *}
   113 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   146 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   114 by (simp add: inst_fun_pcpo)
   147 by (simp add: inst_fun_pcpo)
   115 
   148 
       
   149 text {*
       
   150   The following results are about application for functions in @{typ "'a=>'b"}
       
   151 *}
       
   152 
       
   153 lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
       
   154 by (simp add: less_fun_def)
       
   155 
       
   156 lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
       
   157 by (rule monofunE)
       
   158 
       
   159 lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
       
   160 by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
       
   161 
       
   162 subsection {* Propagation of monotonicity and continuity *}
       
   163 
       
   164 text {* the lub of a chain of monotone functions is monotone *}
       
   165 
       
   166 lemma monofun_lub_fun:
       
   167   "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
       
   168     \<Longrightarrow> monofun (\<Squnion>i. F i)"
       
   169 apply (rule monofunI)
       
   170 apply (simp add: thelub_fun)
       
   171 apply (rule lub_mono [rule_format])
       
   172 apply (erule ch2ch_fun)
       
   173 apply (erule ch2ch_fun)
       
   174 apply (simp add: monofunE)
       
   175 done
       
   176 
       
   177 text {* the lub of a chain of continuous functions is continuous *}
       
   178 
       
   179 declare range_composition [simp del]
       
   180 
       
   181 lemma contlub_lub_fun:
       
   182   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
       
   183 apply (rule contlubI)
       
   184 apply (simp add: thelub_fun)
       
   185 apply (simp add: cont2contlubE)
       
   186 apply (rule ex_lub)
       
   187 apply (erule ch2ch_fun)
       
   188 apply (simp add: ch2ch_cont)
       
   189 done
       
   190 
       
   191 lemma cont_lub_fun:
       
   192   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
       
   193 apply (rule monocontlub2cont)
       
   194 apply (erule monofun_lub_fun)
       
   195 apply (simp add: cont2mono)
       
   196 apply (erule (1) contlub_lub_fun)
       
   197 done
       
   198 
       
   199 lemma cont2cont_lub:
       
   200   "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
       
   201 by (simp add: thelub_fun [symmetric] cont_lub_fun)
       
   202 
       
   203 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
       
   204 apply (rule monofunI)
       
   205 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
       
   206 done
       
   207 
       
   208 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
       
   209 apply (rule monocontlub2cont)
       
   210 apply (erule cont2mono [THEN mono2mono_fun])
       
   211 apply (rule contlubI)
       
   212 apply (simp add: cont2contlubE)
       
   213 apply (simp add: thelub_fun ch2ch_cont)
       
   214 done
       
   215 
       
   216 text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
       
   217 
       
   218 lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
       
   219 apply (rule monofunI)
       
   220 apply (rule less_fun_ext)
       
   221 apply (blast dest: monofunE)
       
   222 done
       
   223 
       
   224 lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
       
   225 apply (subgoal_tac "monofun f")
       
   226 apply (rule monocontlub2cont)
       
   227 apply assumption
       
   228 apply (rule contlubI)
       
   229 apply (rule ext)
       
   230 apply (simp add: thelub_fun ch2ch_monofun)
       
   231 apply (blast dest: cont2contlubE)
       
   232 apply (simp add: mono2mono_lambda cont2mono)
       
   233 done
       
   234 
       
   235 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
       
   236 
       
   237 lemma contlub_lambda:
       
   238   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
       
   239     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
       
   240 by (simp add: thelub_fun ch2ch_lambda)
       
   241 
       
   242 lemma contlub_abstraction:
       
   243   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
       
   244     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
       
   245 apply (rule thelub_fun [symmetric])
       
   246 apply (rule ch2ch_cont)
       
   247 apply (simp add: cont2cont_lambda)
       
   248 apply assumption
       
   249 done
       
   250 
       
   251 lemma mono2mono_app:
       
   252   "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
       
   253 apply (rule monofunI)
       
   254 apply (simp add: monofun_fun monofunE)
       
   255 done
       
   256 
       
   257 lemma cont2contlub_app:
       
   258   "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
       
   259 apply (rule contlubI)
       
   260 apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
       
   261 apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
       
   262 apply (simp add: cont2contlubE thelub_fun)
       
   263 apply (rule diag_lub)
       
   264 apply (erule ch2ch_fun)
       
   265 apply (drule spec)
       
   266 apply (erule (1) ch2ch_cont)
       
   267 apply (erule (1) ch2ch_cont)
       
   268 apply (erule (1) ch2ch_cont)
       
   269 done
       
   270 
       
   271 lemma cont2cont_app:
       
   272   "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
       
   273 by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
       
   274 
       
   275 lemmas cont2cont_app2 = cont2cont_app [rule_format]
       
   276 
       
   277 lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
       
   278 by (rule cont2cont_app2 [OF cont_const])
       
   279 
   116 end
   280 end
   117 
   281