1(* Title: HOL/HOLCF/Cfun.thy 2 Author: Franz Regensburger 3 Author: Brian Huffman 4*) 5 6section \<open>The type of continuous functions\<close> 7 8theory Cfun 9 imports Cpodef Fun_Cpo Product_Cpo 10begin 11 12default_sort cpo 13 14 15subsection \<open>Definition of continuous function type\<close> 16 17definition "cfun = {f::'a \<Rightarrow> 'b. cont f}" 18 19cpodef ('a, 'b) cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set" 20 by (auto simp: cfun_def intro: cont_const adm_cont) 21 22type_notation (ASCII) 23 cfun (infixr "->" 0) 24 25notation (ASCII) 26 Rep_cfun ("(_$/_)" [999,1000] 999) 27 28notation 29 Rep_cfun ("(_\<cdot>/_)" [999,1000] 999) 30 31 32subsection \<open>Syntax for continuous lambda abstraction\<close> 33 34syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic" 35 36parse_translation \<open> 37(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *) 38 [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})]; 39\<close> 40 41print_translation \<open> 42 [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] => 43 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 44 in Syntax.const @{syntax_const "_cabs"} $ x $ t end)] 45\<close> \<comment> \<open>To avoid eta-contraction of body\<close> 46 47text \<open>Syntax for nested abstractions\<close> 48 49syntax (ASCII) 50 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10) 51 52syntax 53 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10) 54 55parse_ast_translation \<open> 56(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *) 57(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *) 58 let 59 fun Lambda_ast_tr [pats, body] = 60 Ast.fold_ast_p @{syntax_const "_cabs"} 61 (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body) 62 | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts); 63 in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end; 64\<close> 65 66print_ast_translation \<open> 67(* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *) 68(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *) 69 let 70 fun cabs_ast_tr' asts = 71 (case Ast.unfold_ast_p @{syntax_const "_cabs"} 72 (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of 73 ([], _) => raise Ast.AST ("cabs_ast_tr'", asts) 74 | (xs, body) => Ast.Appl 75 [Ast.Constant @{syntax_const "_Lambda"}, 76 Ast.fold_ast @{syntax_const "_cargs"} xs, body]); 77 in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end 78\<close> 79 80text \<open>Dummy patterns for continuous abstraction\<close> 81translations 82 "\<Lambda> _. t" \<rightharpoonup> "CONST Abs_cfun (\<lambda>_. t)" 83 84 85subsection \<open>Continuous function space is pointed\<close> 86 87lemma bottom_cfun: "\<bottom> \<in> cfun" 88 by (simp add: cfun_def inst_fun_pcpo) 89 90instance cfun :: (cpo, discrete_cpo) discrete_cpo 91 by intro_classes (simp add: below_cfun_def Rep_cfun_inject) 92 93instance cfun :: (cpo, pcpo) pcpo 94 by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun]) 95 96lemmas Rep_cfun_strict = 97 typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun] 98 99lemmas Abs_cfun_strict = 100 typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun] 101 102text \<open>function application is strict in its first argument\<close> 103 104lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>" 105 by (simp add: Rep_cfun_strict) 106 107lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>" 108 by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict) 109 110text \<open>for compatibility with old HOLCF-Version\<close> 111lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)" 112 by simp 113 114 115subsection \<open>Basic properties of continuous functions\<close> 116 117text \<open>Beta-equality for continuous functions\<close> 118 119lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f" 120 by (simp add: Abs_cfun_inverse cfun_def) 121 122lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u" 123 by (simp add: Abs_cfun_inverse2) 124 125 126subsubsection \<open>Beta-reduction simproc\<close> 127 128text \<open> 129 Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to 130 construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y \<equiv> f y"}. If this 131 theorem cannot be completely solved by the cont2cont rules, then 132 the procedure returns the ordinary conditional \<open>beta_cfun\<close> 133 rule. 134 135 The simproc does not solve any more goals that would be solved by 136 using \<open>beta_cfun\<close> as a simp rule. The advantage of the 137 simproc is that it can avoid deeply-nested calls to the simplifier 138 that would otherwise be caused by large continuity side conditions. 139 140 Update: The simproc now uses rule \<open>Abs_cfun_inverse2\<close> instead 141 of \<open>beta_cfun\<close>, to avoid problems with eta-contraction. 142\<close> 143 144simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open> 145 fn phi => fn ctxt => fn ct => 146 let 147 val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct))); 148 val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f); 149 val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2}); 150 val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>; 151 val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules))); 152 in SOME (perhaps (SINGLE (tac 1)) tr) end 153\<close> 154 155text \<open>Eta-equality for continuous functions\<close> 156 157lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f" 158 by (rule Rep_cfun_inverse) 159 160text \<open>Extensionality for continuous functions\<close> 161 162lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)" 163 by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff) 164 165lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g" 166 by (simp add: cfun_eq_iff) 167 168text \<open>Extensionality wrt. ordering for continuous functions\<close> 169 170lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 171 by (simp add: below_cfun_def fun_below_iff) 172 173lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g" 174 by (simp add: cfun_below_iff) 175 176text \<open>Congruence for continuous function application\<close> 177 178lemma cfun_cong: "f = g \<Longrightarrow> x = y \<Longrightarrow> f\<cdot>x = g\<cdot>y" 179 by simp 180 181lemma cfun_fun_cong: "f = g \<Longrightarrow> f\<cdot>x = g\<cdot>x" 182 by simp 183 184lemma cfun_arg_cong: "x = y \<Longrightarrow> f\<cdot>x = f\<cdot>y" 185 by simp 186 187 188subsection \<open>Continuity of application\<close> 189 190lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)" 191 by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun]) 192 193lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)" 194 using Rep_cfun [where x = f] by (simp add: cfun_def) 195 196lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono] 197 198lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono] 199lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono] 200 201text \<open>contlub, cont properties of @{term Rep_cfun} in each argument\<close> 202 203lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))" 204 by (rule cont_Rep_cfun2 [THEN cont2contlubE]) 205 206lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)" 207 by (rule cont_Rep_cfun1 [THEN cont2contlubE]) 208 209text \<open>monotonicity of application\<close> 210 211lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x" 212 by (simp add: cfun_below_iff) 213 214lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y" 215 by (rule monofun_Rep_cfun2 [THEN monofunE]) 216 217lemma monofun_cfun: "f \<sqsubseteq> g \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y" 218 by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg]) 219 220text \<open>ch2ch - rules for the type @{typ "'a \<rightarrow> 'b"}\<close> 221 222lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))" 223 by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun]) 224 225lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))" 226 by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun]) 227 228lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)" 229 by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun]) 230 231lemma ch2ch_Rep_cfun [simp]: "chain F \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))" 232 by (simp add: chain_def monofun_cfun) 233 234lemma ch2ch_LAM [simp]: 235 "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> (\<And>i. cont (\<lambda>x. S i x)) \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)" 236 by (simp add: chain_def cfun_below_iff) 237 238text \<open>contlub, cont properties of @{term Rep_cfun} in both arguments\<close> 239 240lemma lub_APP: "chain F \<Longrightarrow> chain Y \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)" 241 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) 242 243lemma lub_LAM: 244 assumes "\<And>x. chain (\<lambda>i. F i x)" 245 and "\<And>i. cont (\<lambda>x. F i x)" 246 shows "(\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)" 247 using assms by (simp add: lub_cfun lub_fun ch2ch_lambda) 248 249lemmas lub_distribs = lub_APP lub_LAM 250 251text \<open>strictness\<close> 252 253lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>" 254 apply (rule bottomI) 255 apply (erule subst) 256 apply (rule minimal [THEN monofun_cfun_arg]) 257 done 258 259text \<open>type @{typ "'a \<rightarrow> 'b"} is chain complete\<close> 260 261lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)" 262 by (simp add: lub_cfun lub_fun ch2ch_lambda) 263 264 265subsection \<open>Continuity simplification procedure\<close> 266 267text \<open>cont2cont lemma for @{term Rep_cfun}\<close> 268 269lemma cont2cont_APP [simp, cont2cont]: 270 assumes f: "cont (\<lambda>x. f x)" 271 assumes t: "cont (\<lambda>x. t x)" 272 shows "cont (\<lambda>x. (f x)\<cdot>(t x))" 273proof - 274 from cont_Rep_cfun1 f have "cont (\<lambda>x. (f x)\<cdot>y)" for y 275 by (rule cont_compose) 276 with t cont_Rep_cfun2 show "cont (\<lambda>x. (f x)\<cdot>(t x))" 277 by (rule cont_apply) 278qed 279 280text \<open> 281 Two specific lemmas for the combination of LCF and HOL terms. 282 These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}. 283\<close> 284 285lemma cont_APP_app [simp]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)" 286 by (rule cont2cont_APP [THEN cont2cont_fun]) 287 288lemma cont_APP_app_app [simp]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)" 289 by (rule cont_APP_app [THEN cont2cont_fun]) 290 291 292text \<open>cont2mono Lemma for @{term "\<lambda>x. LAM y. c1(x)(y)"}\<close> 293 294lemma cont2mono_LAM: 295 "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk> 296 \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)" 297 by (simp add: monofun_def cfun_below_iff) 298 299text \<open>cont2cont Lemma for @{term "\<lambda>x. LAM y. f x y"}\<close> 300 301text \<open> 302 Not suitable as a cont2cont rule, because on nested lambdas 303 it causes exponential blow-up in the number of subgoals. 304\<close> 305 306lemma cont2cont_LAM: 307 assumes f1: "\<And>x. cont (\<lambda>y. f x y)" 308 assumes f2: "\<And>y. cont (\<lambda>x. f x y)" 309 shows "cont (\<lambda>x. \<Lambda> y. f x y)" 310proof (rule cont_Abs_cfun) 311 from f1 show "f x \<in> cfun" for x 312 by (simp add: cfun_def) 313 from f2 show "cont f" 314 by (rule cont2cont_lambda) 315qed 316 317text \<open> 318 This version does work as a cont2cont rule, since it 319 has only a single subgoal. 320\<close> 321 322lemma cont2cont_LAM' [simp, cont2cont]: 323 fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" 324 assumes f: "cont (\<lambda>p. f (fst p) (snd p))" 325 shows "cont (\<lambda>x. \<Lambda> y. f x y)" 326 using assms by (simp add: cont2cont_LAM prod_cont_iff) 327 328lemma cont2cont_LAM_discrete [simp, cont2cont]: 329 "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)" 330 by (simp add: cont2cont_LAM) 331 332 333subsection \<open>Miscellaneous\<close> 334 335text \<open>Monotonicity of @{term Abs_cfun}\<close> 336 337lemma monofun_LAM: "cont f \<Longrightarrow> cont g \<Longrightarrow> (\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)" 338 by (simp add: cfun_below_iff) 339 340text \<open>some lemmata for functions with flat/chfin domain/range types\<close> 341 342lemma chfin_Rep_cfunR: "chain Y \<Longrightarrow> \<forall>s. \<exists>n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s" 343 for Y :: "nat \<Rightarrow> 'a::cpo \<rightarrow> 'b::chfin" 344 apply (rule allI) 345 apply (subst contlub_cfun_fun) 346 apply assumption 347 apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL) 348 done 349 350lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))" 351 by (rule adm_subst, simp, rule adm_chfin) 352 353 354subsection \<open>Continuous injection-retraction pairs\<close> 355 356text \<open>Continuous retractions are strict.\<close> 357 358lemma retraction_strict: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>" 359 apply (rule bottomI) 360 apply (drule_tac x="\<bottom>" in spec) 361 apply (erule subst) 362 apply (rule monofun_cfun_arg) 363 apply (rule minimal) 364 done 365 366lemma injection_eq: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x = g\<cdot>y) = (x = y)" 367 apply (rule iffI) 368 apply (drule_tac f=f in cfun_arg_cong) 369 apply simp 370 apply simp 371 done 372 373lemma injection_below: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)" 374 apply (rule iffI) 375 apply (drule_tac f=f in monofun_cfun_arg) 376 apply simp 377 apply (erule monofun_cfun_arg) 378 done 379 380lemma injection_defined_rev: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> g\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" 381 apply (drule_tac f=f in cfun_arg_cong) 382 apply (simp add: retraction_strict) 383 done 384 385lemma injection_defined: "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> z \<noteq> \<bottom> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>" 386 by (erule contrapos_nn, rule injection_defined_rev) 387 388 389text \<open>a result about functions with flat codomain\<close> 390 391lemma flat_eqI: "x \<sqsubseteq> y \<Longrightarrow> x \<noteq> \<bottom> \<Longrightarrow> x = y" 392 for x y :: "'a::flat" 393 by (drule ax_flat) simp 394 395lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)" 396 for c :: "'b::flat" 397 apply (cases "f\<cdot>x = \<bottom>") 398 apply (rule disjI1) 399 apply (rule bottomI) 400 apply (erule_tac t="\<bottom>" in subst) 401 apply (rule minimal [THEN monofun_cfun_arg]) 402 apply clarify 403 apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals]) 404 apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) 405 apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) 406 done 407 408 409subsection \<open>Identity and composition\<close> 410 411definition ID :: "'a \<rightarrow> 'a" 412 where "ID = (\<Lambda> x. x)" 413 414definition cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" 415 where oo_def: "cfcomp = (\<Lambda> f g x. f\<cdot>(g\<cdot>x))" 416 417abbreviation cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100) 418 where "f oo g == cfcomp\<cdot>f\<cdot>g" 419 420lemma ID1 [simp]: "ID\<cdot>x = x" 421 by (simp add: ID_def) 422 423lemma cfcomp1: "(f oo g) = (\<Lambda> x. f\<cdot>(g\<cdot>x))" 424 by (simp add: oo_def) 425 426lemma cfcomp2 [simp]: "(f oo g)\<cdot>x = f\<cdot>(g\<cdot>x)" 427 by (simp add: cfcomp1) 428 429lemma cfcomp_LAM: "cont g \<Longrightarrow> f oo (\<Lambda> x. g x) = (\<Lambda> x. f\<cdot>(g x))" 430 by (simp add: cfcomp1) 431 432lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>" 433 by (simp add: cfun_eq_iff) 434 435text \<open> 436 Show that interpretation of (pcpo, \<open>_\<rightarrow>_\<close>) is a category. 437 \<^item> The class of objects is interpretation of syntactical class pcpo. 438 \<^item> The class of arrows between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a \<rightarrow> 'b"}. 439 \<^item> The identity arrow is interpretation of @{term ID}. 440 \<^item> The composition of f and g is interpretation of \<open>oo\<close>. 441\<close> 442 443lemma ID2 [simp]: "f oo ID = f" 444 by (rule cfun_eqI, simp) 445 446lemma ID3 [simp]: "ID oo f = f" 447 by (rule cfun_eqI) simp 448 449lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h" 450 by (rule cfun_eqI) simp 451 452 453subsection \<open>Strictified functions\<close> 454 455default_sort pcpo 456 457definition seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" 458 where "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)" 459 460lemma cont2cont_if_bottom [cont2cont, simp]: 461 assumes f: "cont (\<lambda>x. f x)" 462 and g: "cont (\<lambda>x. g x)" 463 shows "cont (\<lambda>x. if f x = \<bottom> then \<bottom> else g x)" 464proof (rule cont_apply [OF f]) 465 show "cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)" for x 466 unfolding cont_def is_lub_def is_ub_def ball_simps 467 by (simp add: lub_eq_bottom_iff) 468 show "cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)" for y 469 by (simp add: g) 470qed 471 472lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)" 473 by (simp add: seq_def) 474 475lemma seq_simps [simp]: 476 "seq\<cdot>\<bottom> = \<bottom>" 477 "seq\<cdot>x\<cdot>\<bottom> = \<bottom>" 478 "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID" 479 by (simp_all add: seq_conv_if) 480 481definition strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" 482 where "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))" 483 484lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" 485 by (simp add: strictify_def) 486 487lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>" 488 by (simp add: strictify_conv_if) 489 490lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x" 491 by (simp add: strictify_conv_if) 492 493 494subsection \<open>Continuity of let-bindings\<close> 495 496lemma cont2cont_Let: 497 assumes f: "cont (\<lambda>x. f x)" 498 assumes g1: "\<And>y. cont (\<lambda>x. g x y)" 499 assumes g2: "\<And>x. cont (\<lambda>y. g x y)" 500 shows "cont (\<lambda>x. let y = f x in g x y)" 501 unfolding Let_def using f g2 g1 by (rule cont_apply) 502 503lemma cont2cont_Let' [simp, cont2cont]: 504 assumes f: "cont (\<lambda>x. f x)" 505 assumes g: "cont (\<lambda>p. g (fst p) (snd p))" 506 shows "cont (\<lambda>x. let y = f x in g x y)" 507 using f 508proof (rule cont2cont_Let) 509 from g show "cont (\<lambda>y. g x y)" for x 510 by (simp add: prod_cont_iff) 511 from g show "cont (\<lambda>x. g x y)" for y 512 by (simp add: prod_cont_iff) 513qed 514 515text \<open>The simple version (suggested by Joachim Breitner) is needed if 516 the type of the defined term is not a cpo.\<close> 517 518lemma cont2cont_Let_simple [simp, cont2cont]: 519 assumes "\<And>y. cont (\<lambda>x. g x y)" 520 shows "cont (\<lambda>x. let y = t in g x y)" 521 unfolding Let_def using assms . 522 523end 524