src/HOL/HOLCF/Cfun.thy
changeset 40774 0437dbc127b3
parent 40772 c8b52f9e1680
child 40794 d28d41ee4cef
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,543 @@
     1.4 +(*  Title:      HOLCF/Cfun.thy
     1.5 +    Author:     Franz Regensburger
     1.6 +    Author:     Brian Huffman
     1.7 +*)
     1.8 +
     1.9 +header {* The type of continuous functions *}
    1.10 +
    1.11 +theory Cfun
    1.12 +imports Cpodef Fun_Cpo Product_Cpo
    1.13 +begin
    1.14 +
    1.15 +default_sort cpo
    1.16 +
    1.17 +subsection {* Definition of continuous function type *}
    1.18 +
    1.19 +cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
    1.20 +by (auto intro: cont_const adm_cont)
    1.21 +
    1.22 +type_notation (xsymbols)
    1.23 +  cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
    1.24 +
    1.25 +notation
    1.26 +  Rep_cfun  ("(_$/_)" [999,1000] 999)
    1.27 +
    1.28 +notation (xsymbols)
    1.29 +  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
    1.30 +
    1.31 +notation (HTML output)
    1.32 +  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
    1.33 +
    1.34 +subsection {* Syntax for continuous lambda abstraction *}
    1.35 +
    1.36 +syntax "_cabs" :: "'a"
    1.37 +
    1.38 +parse_translation {*
    1.39 +(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
    1.40 +  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
    1.41 +*}
    1.42 +
    1.43 +text {* To avoid eta-contraction of body: *}
    1.44 +typed_print_translation {*
    1.45 +  let
    1.46 +    fun cabs_tr' _ _ [Abs abs] = let
    1.47 +          val (x,t) = atomic_abs_tr' abs
    1.48 +        in Syntax.const @{syntax_const "_cabs"} $ x $ t end
    1.49 +
    1.50 +      | cabs_tr' _ T [t] = let
    1.51 +          val xT = domain_type (domain_type T);
    1.52 +          val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
    1.53 +          val (x,t') = atomic_abs_tr' abs';
    1.54 +        in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
    1.55 +
    1.56 +  in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
    1.57 +*}
    1.58 +
    1.59 +text {* Syntax for nested abstractions *}
    1.60 +
    1.61 +syntax
    1.62 +  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
    1.63 +
    1.64 +syntax (xsymbols)
    1.65 +  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
    1.66 +
    1.67 +parse_ast_translation {*
    1.68 +(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
    1.69 +(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
    1.70 +  let
    1.71 +    fun Lambda_ast_tr [pats, body] =
    1.72 +          Syntax.fold_ast_p @{syntax_const "_cabs"}
    1.73 +            (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
    1.74 +      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    1.75 +  in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
    1.76 +*}
    1.77 +
    1.78 +print_ast_translation {*
    1.79 +(* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
    1.80 +(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
    1.81 +  let
    1.82 +    fun cabs_ast_tr' asts =
    1.83 +      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
    1.84 +          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
    1.85 +        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
    1.86 +      | (xs, body) => Syntax.Appl
    1.87 +          [Syntax.Constant @{syntax_const "_Lambda"},
    1.88 +           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
    1.89 +  in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
    1.90 +*}
    1.91 +
    1.92 +text {* Dummy patterns for continuous abstraction *}
    1.93 +translations
    1.94 +  "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
    1.95 +
    1.96 +subsection {* Continuous function space is pointed *}
    1.97 +
    1.98 +lemma UU_cfun: "\<bottom> \<in> cfun"
    1.99 +by (simp add: cfun_def inst_fun_pcpo)
   1.100 +
   1.101 +instance cfun :: (cpo, discrete_cpo) discrete_cpo
   1.102 +by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
   1.103 +
   1.104 +instance cfun :: (cpo, pcpo) pcpo
   1.105 +by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
   1.106 +
   1.107 +lemmas Rep_cfun_strict =
   1.108 +  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
   1.109 +
   1.110 +lemmas Abs_cfun_strict =
   1.111 +  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
   1.112 +
   1.113 +text {* function application is strict in its first argument *}
   1.114 +
   1.115 +lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
   1.116 +by (simp add: Rep_cfun_strict)
   1.117 +
   1.118 +lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
   1.119 +by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
   1.120 +
   1.121 +text {* for compatibility with old HOLCF-Version *}
   1.122 +lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
   1.123 +by simp
   1.124 +
   1.125 +subsection {* Basic properties of continuous functions *}
   1.126 +
   1.127 +text {* Beta-equality for continuous functions *}
   1.128 +
   1.129 +lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
   1.130 +by (simp add: Abs_cfun_inverse cfun_def)
   1.131 +
   1.132 +lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
   1.133 +by (simp add: Abs_cfun_inverse2)
   1.134 +
   1.135 +text {* Beta-reduction simproc *}
   1.136 +
   1.137 +text {*
   1.138 +  Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to
   1.139 +  construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y == f y"}.  If this
   1.140 +  theorem cannot be completely solved by the cont2cont rules, then
   1.141 +  the procedure returns the ordinary conditional @{text beta_cfun}
   1.142 +  rule.
   1.143 +
   1.144 +  The simproc does not solve any more goals that would be solved by
   1.145 +  using @{text beta_cfun} as a simp rule.  The advantage of the
   1.146 +  simproc is that it can avoid deeply-nested calls to the simplifier
   1.147 +  that would otherwise be caused by large continuity side conditions.
   1.148 +*}
   1.149 +
   1.150 +simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
   1.151 +  fn phi => fn ss => fn ct =>
   1.152 +    let
   1.153 +      val dest = Thm.dest_comb;
   1.154 +      val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct;
   1.155 +      val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
   1.156 +      val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x]
   1.157 +          (mk_meta_eq @{thm beta_cfun});
   1.158 +      val rules = Cont2ContData.get (Simplifier.the_context ss);
   1.159 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
   1.160 +    in SOME (perhaps (SINGLE (tac 1)) tr) end
   1.161 +*}
   1.162 +
   1.163 +text {* Eta-equality for continuous functions *}
   1.164 +
   1.165 +lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
   1.166 +by (rule Rep_cfun_inverse)
   1.167 +
   1.168 +text {* Extensionality for continuous functions *}
   1.169 +
   1.170 +lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
   1.171 +by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
   1.172 +
   1.173 +lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
   1.174 +by (simp add: cfun_eq_iff)
   1.175 +
   1.176 +text {* Extensionality wrt. ordering for continuous functions *}
   1.177 +
   1.178 +lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
   1.179 +by (simp add: below_cfun_def fun_below_iff)
   1.180 +
   1.181 +lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
   1.182 +by (simp add: cfun_below_iff)
   1.183 +
   1.184 +text {* Congruence for continuous function application *}
   1.185 +
   1.186 +lemma cfun_cong: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f\<cdot>x = g\<cdot>y"
   1.187 +by simp
   1.188 +
   1.189 +lemma cfun_fun_cong: "f = g \<Longrightarrow> f\<cdot>x = g\<cdot>x"
   1.190 +by simp
   1.191 +
   1.192 +lemma cfun_arg_cong: "x = y \<Longrightarrow> f\<cdot>x = f\<cdot>y"
   1.193 +by simp
   1.194 +
   1.195 +subsection {* Continuity of application *}
   1.196 +
   1.197 +lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
   1.198 +by (rule cont_Rep_cfun [THEN cont2cont_fun])
   1.199 +
   1.200 +lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
   1.201 +apply (cut_tac x=f in Rep_cfun)
   1.202 +apply (simp add: cfun_def)
   1.203 +done
   1.204 +
   1.205 +lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
   1.206 +
   1.207 +lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
   1.208 +lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
   1.209 +
   1.210 +text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
   1.211 +
   1.212 +lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
   1.213 +by (rule cont_Rep_cfun2 [THEN cont2contlubE])
   1.214 +
   1.215 +lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
   1.216 +by (rule cont_Rep_cfun1 [THEN cont2contlubE])
   1.217 +
   1.218 +text {* monotonicity of application *}
   1.219 +
   1.220 +lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
   1.221 +by (simp add: cfun_below_iff)
   1.222 +
   1.223 +lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
   1.224 +by (rule monofun_Rep_cfun2 [THEN monofunE])
   1.225 +
   1.226 +lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
   1.227 +by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
   1.228 +
   1.229 +text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
   1.230 +
   1.231 +lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
   1.232 +by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
   1.233 +
   1.234 +lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
   1.235 +by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
   1.236 +
   1.237 +lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
   1.238 +by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
   1.239 +
   1.240 +lemma ch2ch_Rep_cfun [simp]:
   1.241 +  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
   1.242 +by (simp add: chain_def monofun_cfun)
   1.243 +
   1.244 +lemma ch2ch_LAM [simp]:
   1.245 +  "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
   1.246 +by (simp add: chain_def cfun_below_iff)
   1.247 +
   1.248 +text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
   1.249 +
   1.250 +lemma contlub_cfun: 
   1.251 +  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
   1.252 +by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
   1.253 +
   1.254 +lemma cont_cfun: 
   1.255 +  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
   1.256 +apply (rule thelubE)
   1.257 +apply (simp only: ch2ch_Rep_cfun)
   1.258 +apply (simp only: contlub_cfun)
   1.259 +done
   1.260 +
   1.261 +lemma contlub_LAM:
   1.262 +  "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
   1.263 +    \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
   1.264 +apply (simp add: lub_cfun)
   1.265 +apply (simp add: Abs_cfun_inverse2)
   1.266 +apply (simp add: thelub_fun ch2ch_lambda)
   1.267 +done
   1.268 +
   1.269 +lemmas lub_distribs = 
   1.270 +  contlub_cfun [symmetric]
   1.271 +  contlub_LAM [symmetric]
   1.272 +
   1.273 +text {* strictness *}
   1.274 +
   1.275 +lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   1.276 +apply (rule UU_I)
   1.277 +apply (erule subst)
   1.278 +apply (rule minimal [THEN monofun_cfun_arg])
   1.279 +done
   1.280 +
   1.281 +text {* type @{typ "'a -> 'b"} is chain complete *}
   1.282 +
   1.283 +lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
   1.284 +by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
   1.285 +
   1.286 +lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
   1.287 +by (rule lub_cfun [THEN lub_eqI])
   1.288 +
   1.289 +subsection {* Continuity simplification procedure *}
   1.290 +
   1.291 +text {* cont2cont lemma for @{term Rep_cfun} *}
   1.292 +
   1.293 +lemma cont2cont_APP [simp, cont2cont]:
   1.294 +  assumes f: "cont (\<lambda>x. f x)"
   1.295 +  assumes t: "cont (\<lambda>x. t x)"
   1.296 +  shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
   1.297 +proof -
   1.298 +  have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
   1.299 +    using cont_Rep_cfun1 f by (rule cont_compose)
   1.300 +  show "cont (\<lambda>x. (f x)\<cdot>(t x))"
   1.301 +    using t cont_Rep_cfun2 1 by (rule cont_apply)
   1.302 +qed
   1.303 +
   1.304 +text {*
   1.305 +  Two specific lemmas for the combination of LCF and HOL terms.
   1.306 +  These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
   1.307 +*}
   1.308 +
   1.309 +lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
   1.310 +by (rule cont2cont_APP [THEN cont2cont_fun])
   1.311 +
   1.312 +lemma cont_APP_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
   1.313 +by (rule cont_APP_app [THEN cont2cont_fun])
   1.314 +
   1.315 +
   1.316 +text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
   1.317 +
   1.318 +lemma cont2mono_LAM:
   1.319 +  "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
   1.320 +    \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
   1.321 +  unfolding monofun_def cfun_below_iff by simp
   1.322 +
   1.323 +text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
   1.324 +
   1.325 +text {*
   1.326 +  Not suitable as a cont2cont rule, because on nested lambdas
   1.327 +  it causes exponential blow-up in the number of subgoals.
   1.328 +*}
   1.329 +
   1.330 +lemma cont2cont_LAM:
   1.331 +  assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
   1.332 +  assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
   1.333 +  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
   1.334 +proof (rule cont_Abs_cfun)
   1.335 +  fix x
   1.336 +  from f1 show "f x \<in> cfun" by (simp add: cfun_def)
   1.337 +  from f2 show "cont f" by (rule cont2cont_lambda)
   1.338 +qed
   1.339 +
   1.340 +text {*
   1.341 +  This version does work as a cont2cont rule, since it
   1.342 +  has only a single subgoal.
   1.343 +*}
   1.344 +
   1.345 +lemma cont2cont_LAM' [simp, cont2cont]:
   1.346 +  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
   1.347 +  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
   1.348 +  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
   1.349 +using assms by (simp add: cont2cont_LAM prod_cont_iff)
   1.350 +
   1.351 +lemma cont2cont_LAM_discrete [simp, cont2cont]:
   1.352 +  "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
   1.353 +by (simp add: cont2cont_LAM)
   1.354 +
   1.355 +subsection {* Miscellaneous *}
   1.356 +
   1.357 +text {* Monotonicity of @{term Abs_cfun} *}
   1.358 +
   1.359 +lemma monofun_LAM:
   1.360 +  "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
   1.361 +by (simp add: cfun_below_iff)
   1.362 +
   1.363 +text {* some lemmata for functions with flat/chfin domain/range types *}
   1.364 +
   1.365 +lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
   1.366 +      ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
   1.367 +apply (rule allI)
   1.368 +apply (subst contlub_cfun_fun)
   1.369 +apply assumption
   1.370 +apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
   1.371 +done
   1.372 +
   1.373 +lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
   1.374 +by (rule adm_subst, simp, rule adm_chfin)
   1.375 +
   1.376 +subsection {* Continuous injection-retraction pairs *}
   1.377 +
   1.378 +text {* Continuous retractions are strict. *}
   1.379 +
   1.380 +lemma retraction_strict:
   1.381 +  "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   1.382 +apply (rule UU_I)
   1.383 +apply (drule_tac x="\<bottom>" in spec)
   1.384 +apply (erule subst)
   1.385 +apply (rule monofun_cfun_arg)
   1.386 +apply (rule minimal)
   1.387 +done
   1.388 +
   1.389 +lemma injection_eq:
   1.390 +  "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x = g\<cdot>y) = (x = y)"
   1.391 +apply (rule iffI)
   1.392 +apply (drule_tac f=f in cfun_arg_cong)
   1.393 +apply simp
   1.394 +apply simp
   1.395 +done
   1.396 +
   1.397 +lemma injection_below:
   1.398 +  "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
   1.399 +apply (rule iffI)
   1.400 +apply (drule_tac f=f in monofun_cfun_arg)
   1.401 +apply simp
   1.402 +apply (erule monofun_cfun_arg)
   1.403 +done
   1.404 +
   1.405 +lemma injection_defined_rev:
   1.406 +  "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; g\<cdot>z = \<bottom>\<rbrakk> \<Longrightarrow> z = \<bottom>"
   1.407 +apply (drule_tac f=f in cfun_arg_cong)
   1.408 +apply (simp add: retraction_strict)
   1.409 +done
   1.410 +
   1.411 +lemma injection_defined:
   1.412 +  "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; z \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
   1.413 +by (erule contrapos_nn, rule injection_defined_rev)
   1.414 +
   1.415 +text {* a result about functions with flat codomain *}
   1.416 +
   1.417 +lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
   1.418 +by (drule ax_flat, simp)
   1.419 +
   1.420 +lemma flat_codom:
   1.421 +  "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
   1.422 +apply (case_tac "f\<cdot>x = \<bottom>")
   1.423 +apply (rule disjI1)
   1.424 +apply (rule UU_I)
   1.425 +apply (erule_tac t="\<bottom>" in subst)
   1.426 +apply (rule minimal [THEN monofun_cfun_arg])
   1.427 +apply clarify
   1.428 +apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals])
   1.429 +apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
   1.430 +apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
   1.431 +done
   1.432 +
   1.433 +subsection {* Identity and composition *}
   1.434 +
   1.435 +definition
   1.436 +  ID :: "'a \<rightarrow> 'a" where
   1.437 +  "ID = (\<Lambda> x. x)"
   1.438 +
   1.439 +definition
   1.440 +  cfcomp  :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" where
   1.441 +  oo_def: "cfcomp = (\<Lambda> f g x. f\<cdot>(g\<cdot>x))"
   1.442 +
   1.443 +abbreviation
   1.444 +  cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c"  (infixr "oo" 100)  where
   1.445 +  "f oo g == cfcomp\<cdot>f\<cdot>g"
   1.446 +
   1.447 +lemma ID1 [simp]: "ID\<cdot>x = x"
   1.448 +by (simp add: ID_def)
   1.449 +
   1.450 +lemma cfcomp1: "(f oo g) = (\<Lambda> x. f\<cdot>(g\<cdot>x))"
   1.451 +by (simp add: oo_def)
   1.452 +
   1.453 +lemma cfcomp2 [simp]: "(f oo g)\<cdot>x = f\<cdot>(g\<cdot>x)"
   1.454 +by (simp add: cfcomp1)
   1.455 +
   1.456 +lemma cfcomp_LAM: "cont g \<Longrightarrow> f oo (\<Lambda> x. g x) = (\<Lambda> x. f\<cdot>(g x))"
   1.457 +by (simp add: cfcomp1)
   1.458 +
   1.459 +lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
   1.460 +by (simp add: cfun_eq_iff)
   1.461 +
   1.462 +text {*
   1.463 +  Show that interpretation of (pcpo,@{text "_->_"}) is a category.
   1.464 +  The class of objects is interpretation of syntactical class pcpo.
   1.465 +  The class of arrows  between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a -> 'b"}.
   1.466 +  The identity arrow is interpretation of @{term ID}.
   1.467 +  The composition of f and g is interpretation of @{text "oo"}.
   1.468 +*}
   1.469 +
   1.470 +lemma ID2 [simp]: "f oo ID = f"
   1.471 +by (rule cfun_eqI, simp)
   1.472 +
   1.473 +lemma ID3 [simp]: "ID oo f = f"
   1.474 +by (rule cfun_eqI, simp)
   1.475 +
   1.476 +lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
   1.477 +by (rule cfun_eqI, simp)
   1.478 +
   1.479 +subsection {* Strictified functions *}
   1.480 +
   1.481 +default_sort pcpo
   1.482 +
   1.483 +definition
   1.484 +  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
   1.485 +  "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
   1.486 +
   1.487 +lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
   1.488 +unfolding cont_def is_lub_def is_ub_def ball_simps
   1.489 +by (simp add: lub_eq_bottom_iff)
   1.490 +
   1.491 +lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
   1.492 +unfolding seq_def by (simp add: cont_seq)
   1.493 +
   1.494 +lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
   1.495 +by (simp add: seq_conv_if)
   1.496 +
   1.497 +lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
   1.498 +by (simp add: seq_conv_if)
   1.499 +
   1.500 +lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
   1.501 +by (simp add: seq_conv_if)
   1.502 +
   1.503 +definition
   1.504 +  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
   1.505 +  "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
   1.506 +
   1.507 +lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
   1.508 +unfolding strictify_def by simp
   1.509 +
   1.510 +lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
   1.511 +by (simp add: strictify_conv_if)
   1.512 +
   1.513 +lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
   1.514 +by (simp add: strictify_conv_if)
   1.515 +
   1.516 +subsection {* Continuity of let-bindings *}
   1.517 +
   1.518 +lemma cont2cont_Let:
   1.519 +  assumes f: "cont (\<lambda>x. f x)"
   1.520 +  assumes g1: "\<And>y. cont (\<lambda>x. g x y)"
   1.521 +  assumes g2: "\<And>x. cont (\<lambda>y. g x y)"
   1.522 +  shows "cont (\<lambda>x. let y = f x in g x y)"
   1.523 +unfolding Let_def using f g2 g1 by (rule cont_apply)
   1.524 +
   1.525 +lemma cont2cont_Let' [simp, cont2cont]:
   1.526 +  assumes f: "cont (\<lambda>x. f x)"
   1.527 +  assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
   1.528 +  shows "cont (\<lambda>x. let y = f x in g x y)"
   1.529 +using f
   1.530 +proof (rule cont2cont_Let)
   1.531 +  fix x show "cont (\<lambda>y. g x y)"
   1.532 +    using g by (simp add: prod_cont_iff)
   1.533 +next
   1.534 +  fix y show "cont (\<lambda>x. g x y)"
   1.535 +    using g by (simp add: prod_cont_iff)
   1.536 +qed
   1.537 +
   1.538 +text {* The simple version (suggested by Joachim Breitner) is needed if
   1.539 +  the type of the defined term is not a cpo. *}
   1.540 +
   1.541 +lemma cont2cont_Let_simple [simp, cont2cont]:
   1.542 +  assumes "\<And>y. cont (\<lambda>x. g x y)"
   1.543 +  shows "cont (\<lambda>x. let y = t in g x y)"
   1.544 +unfolding Let_def using assms .
   1.545 +
   1.546 +end