Theory Cfun

(*  Title:      HOL/HOLCF/Cfun.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman

section ‹The type of continuous functions›

theory Cfun
  imports Cpodef Fun_Cpo Product_Cpo

default_sort cpo

subsection ‹Definition of continuous function type›

definition "cfun = {f::'a  'b. cont f}"

cpodef ('a, 'b) cfun ("(_ / _)" [1, 0] 0) = "cfun :: ('a  'b) set"
  by (auto simp: cfun_def intro: cont_const adm_cont)

type_notation (ASCII)
  cfun  (infixr "->" 0)

notation (ASCII)
  Rep_cfun  ("(_$/_)" [999,1000] 999)

  Rep_cfun  ("(_/_)" [999,1000] 999)

subsection ‹Syntax for continuous lambda abstraction›

syntax "_cabs" :: "[logic, logic]  logic"

parse_translation (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
  [Syntax_Trans.mk_binder_tr (syntax_const‹_cabs›, const_syntaxAbs_cfun)]

print_translation [(const_syntaxAbs_cfun, fn _ => fn [Abs abs] =>
      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
      in Syntax.const syntax_const‹_cabs› $ x $ t end)]  ― ‹To avoid eta-contraction of body›

text ‹Syntax for nested abstractions›

syntax (ASCII)
  "_Lambda" :: "[cargs, logic]  logic"  ("(3LAM _./ _)" [1000, 10] 10)

  "_Lambda" :: "[cargs, logic]  logic" ("(3Λ _./ _)" [1000, 10] 10)

parse_ast_translation (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
    fun Lambda_ast_tr [pats, body] =
          Ast.fold_ast_p syntax_const‹_cabs›
            (Ast.unfold_ast syntax_const‹_cargs› (Ast.strip_positions pats), body)
      | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
  in [(syntax_const‹_Lambda›, K Lambda_ast_tr)] end

print_ast_translation (* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
    fun cabs_ast_tr' asts =
      (case Ast.unfold_ast_p syntax_const‹_cabs›
          (Ast.Appl (Ast.Constant syntax_const‹_cabs› :: asts)) of
        ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
      | (xs, body) => Ast.Appl
          [Ast.Constant syntax_const‹_Lambda›,
           Ast.fold_ast syntax_const‹_cargs› xs, body]);
  in [(syntax_const‹_cabs›, K cabs_ast_tr')] end

text ‹Dummy patterns for continuous abstraction›
  "Λ _. t"  "CONST Abs_cfun (λ_. t)"

subsection ‹Continuous function space is pointed›

lemma bottom_cfun: "  cfun"
  by (simp add: cfun_def inst_fun_pcpo)

instance cfun :: (cpo, discrete_cpo) discrete_cpo
  by intro_classes (simp add: below_cfun_def Rep_cfun_inject)

instance cfun :: (cpo, pcpo) pcpo
  by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])

lemmas Rep_cfun_strict =
  typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]

lemmas Abs_cfun_strict =
  typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]

text ‹function application is strict in its first argument›

lemma Rep_cfun_strict1 [simp]: "x = "
  by (simp add: Rep_cfun_strict)

lemma LAM_strict [simp]: "(Λ x. ) = "
  by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)

text ‹for compatibility with old HOLCF-Version›
lemma inst_cfun_pcpo: " = (Λ x. )"
  by simp

subsection ‹Basic properties of continuous functions›

text ‹Beta-equality for continuous functions›

lemma Abs_cfun_inverse2: "cont f  Rep_cfun (Abs_cfun f) = f"
  by (simp add: Abs_cfun_inverse cfun_def)

lemma beta_cfun: "cont f  (Λ x. f x)u = f u"
  by (simp add: Abs_cfun_inverse2)

subsubsection ‹Beta-reduction simproc›

text ‹
  Given the term term(Λ x. f x)y, the procedure tries to
  construct the theorem term(Λ x. f x)y  f y.  If this
  theorem cannot be completely solved by the cont2cont rules, then
  the procedure returns the ordinary conditional beta_cfun›

  The simproc does not solve any more goals that would be solved by
  using beta_cfun› as a simp rule.  The advantage of the
  simproc is that it can avoid deeply-nested calls to the simplifier
  that would otherwise be caused by large continuity side conditions.

  Update: The simproc now uses rule Abs_cfun_inverse2› instead
  of beta_cfun›, to avoid problems with eta-contraction.

simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = K (fn ctxt => fn ct =>
      val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
      val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
      val rules = Named_Theorems.get ctxt named_theorems‹cont2cont›;
      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
    in SOME (perhaps (SINGLE (tac 1)) tr) end)

text ‹Eta-equality for continuous functions›

lemma eta_cfun: "(Λ x. fx) = f"
  by (rule Rep_cfun_inverse)

text ‹Extensionality for continuous functions›

lemma cfun_eq_iff: "f = g  (x. fx = gx)"
  by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)

lemma cfun_eqI: "(x. fx = gx)  f = g"
  by (simp add: cfun_eq_iff)

text ‹Extensionality wrt. ordering for continuous functions›

lemma cfun_below_iff: "f  g  (x. fx  gx)"
  by (simp add: below_cfun_def fun_below_iff)

lemma cfun_belowI: "(x. fx  gx)  f  g"
  by (simp add: cfun_below_iff)

text ‹Congruence for continuous function application›

lemma cfun_cong: "f = g  x = y  fx = gy"
  by simp

lemma cfun_fun_cong: "f = g  fx = gx"
  by simp

lemma cfun_arg_cong: "x = y  fx = fy"
  by simp

subsection ‹Continuity of application›

lemma cont_Rep_cfun1: "cont (λf. fx)"
  by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])

lemma cont_Rep_cfun2: "cont (λx. fx)"
  using Rep_cfun [where x = f] by (simp add: cfun_def)

lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]

lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono]
lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono]

text ‹contlub, cont properties of termRep_cfun in each argument›

lemma contlub_cfun_arg: "chain Y  f(i. Y i) = (i. f(Y i))"
  by (rule cont_Rep_cfun2 [THEN cont2contlubE])

lemma contlub_cfun_fun: "chain F  (i. F i)x = (i. F ix)"
  by (rule cont_Rep_cfun1 [THEN cont2contlubE])

text ‹monotonicity of application›

lemma monofun_cfun_fun: "f  g  fx  gx"
  by (simp add: cfun_below_iff)

lemma monofun_cfun_arg: "x  y  fx  fy"
  by (rule monofun_Rep_cfun2 [THEN monofunE])

lemma monofun_cfun: "f  g  x  y  fx  gy"
  by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])

text ‹ch2ch - rules for the type typ'a  'b

lemma chain_monofun: "chain Y  chain (λi. f(Y i))"
  by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])

lemma ch2ch_Rep_cfunR: "chain Y  chain (λi. f(Y i))"
  by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])

lemma ch2ch_Rep_cfunL: "chain F  chain (λi. (F i)x)"
  by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])

lemma ch2ch_Rep_cfun [simp]: "chain F  chain Y  chain (λi. (F i)(Y i))"
  by (simp add: chain_def monofun_cfun)

lemma ch2ch_LAM [simp]:
  "(x. chain (λi. S i x))  (i. cont (λx. S i x))  chain (λi. Λ x. S i x)"
  by (simp add: chain_def cfun_below_iff)

text ‹contlub, cont properties of termRep_cfun in both arguments›

lemma lub_APP: "chain F  chain Y  (i. F i(Y i)) = (i. F i)(i. Y i)"
  by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)

lemma lub_LAM:
  assumes "x. chain (λi. F i x)"
    and "i. cont (λx. F i x)"
  shows "(i. Λ x. F i x) = (Λ x. i. F i x)"
  using assms by (simp add: lub_cfun lub_fun ch2ch_lambda)

lemmas lub_distribs = lub_APP lub_LAM

text ‹strictness›

lemma strictI: "fx =   f = "
  apply (rule bottomI)
  apply (erule subst)
  apply (rule minimal [THEN monofun_cfun_arg])

text ‹type typ'a  'b is chain complete›

lemma lub_cfun: "chain F  (i. F i) = (Λ x. i. F ix)"
  by (simp add: lub_cfun lub_fun ch2ch_lambda)

subsection ‹Continuity simplification procedure›

text ‹cont2cont lemma for termRep_cfun

lemma cont2cont_APP [simp, cont2cont]:
  assumes f: "cont (λx. f x)"
  assumes t: "cont (λx. t x)"
  shows "cont (λx. (f x)(t x))"
proof -
  from cont_Rep_cfun1 f have "cont (λx. (f x)y)" for y
    by (rule cont_compose)
  with t cont_Rep_cfun2 show "cont (λx. (f x)(t x))"
    by (rule cont_apply)

text ‹
  Two specific lemmas for the combination of LCF and HOL terms.
  These lemmas are needed in theories that use types like typ'a  'b  'c.

lemma cont_APP_app [simp]: "cont f  cont g  cont (λx. ((f x)(g x)) s)"
  by (rule cont2cont_APP [THEN cont2cont_fun])

lemma cont_APP_app_app [simp]: "cont f  cont g  cont (λx. ((f x)(g x)) s t)"
  by (rule cont_APP_app [THEN cont2cont_fun])

text ‹cont2mono Lemma for termλx. LAM y. c1(x)(y)

lemma cont2mono_LAM:
  "x. cont (λy. f x y); y. monofun (λx. f x y)
     monofun (λx. Λ y. f x y)"
  by (simp add: monofun_def cfun_below_iff)

text ‹cont2cont Lemma for termλx. LAM y. f x y

text ‹
  Not suitable as a cont2cont rule, because on nested lambdas
  it causes exponential blow-up in the number of subgoals.

lemma cont2cont_LAM:
  assumes f1: "x. cont (λy. f x y)"
  assumes f2: "y. cont (λx. f x y)"
  shows "cont (λx. Λ y. f x y)"
proof (rule cont_Abs_cfun)
  from f1 show "f x  cfun" for x
    by (simp add: cfun_def)
  from f2 show "cont f"
    by (rule cont2cont_lambda)

text ‹
  This version does work as a cont2cont rule, since it
  has only a single subgoal.

lemma cont2cont_LAM' [simp, cont2cont]:
  fixes f :: "'a::cpo  'b::cpo  'c::cpo"
  assumes f: "cont (λp. f (fst p) (snd p))"
  shows "cont (λx. Λ y. f x y)"
  using assms by (simp add: cont2cont_LAM prod_cont_iff)

lemma cont2cont_LAM_discrete [simp, cont2cont]:
  "(y::'a::discrete_cpo. cont (λx. f x y))  cont (λx. Λ y. f x y)"
  by (simp add: cont2cont_LAM)

subsection ‹Miscellaneous›

text ‹Monotonicity of termAbs_cfun

lemma monofun_LAM: "cont f  cont g  (x. f x  g x)  (Λ x. f x)  (Λ x. g x)"
  by (simp add: cfun_below_iff)

text ‹some lemmata for functions with flat/chfin domain/range types›

lemma chfin_Rep_cfunR: "chain Y  s. n. (LUB i. Y i)s = Y ns"
  for Y :: "nat  'a::cpo  'b::chfin"
  apply (rule allI)
  apply (subst contlub_cfun_fun)
   apply assumption
  apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)

lemma adm_chfindom: "adm (λ(u::'a::cpo  'b::chfin). P(us))"
  by (rule adm_subst, simp, rule adm_chfin)

subsection ‹Continuous injection-retraction pairs›

text ‹Continuous retractions are strict.›

lemma retraction_strict: "x. f(gx) = x  f = "
  apply (rule bottomI)
  apply (drule_tac x="" in spec)
  apply (erule subst)
  apply (rule monofun_cfun_arg)
  apply (rule minimal)

lemma injection_eq: "x. f(gx) = x  (gx = gy) = (x = y)"
  apply (rule iffI)
   apply (drule_tac f=f in cfun_arg_cong)
   apply simp
  apply simp

lemma injection_below: "x. f(gx) = x  (gx  gy) = (x  y)"
  apply (rule iffI)
   apply (drule_tac f=f in monofun_cfun_arg)
   apply simp
  apply (erule monofun_cfun_arg)

lemma injection_defined_rev: "x. f(gx) = x  gz =   z = "
  apply (drule_tac f=f in cfun_arg_cong)
  apply (simp add: retraction_strict)

lemma injection_defined: "x. f(gx) = x  z    gz  "
  by (erule contrapos_nn, rule injection_defined_rev)

text ‹a result about functions with flat codomain›

lemma flat_eqI: "x  y  x    x = y"
  for x y :: "'a::flat"
  by (drule ax_flat) simp

lemma flat_codom: "fx = c  f =   (z. fz = c)"
  for c :: "'b::flat"
  apply (cases "fx = ")
   apply (rule disjI1)
   apply (rule bottomI)
   apply (erule_tac t="" in subst)
   apply (rule minimal [THEN monofun_cfun_arg])
  apply clarify
  apply (rule_tac a = "f" in refl [THEN box_equals])
   apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
  apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])

subsection ‹Identity and composition›

definition ID :: "'a  'a"
  where "ID = (Λ x. x)"

definition cfcomp  :: "('b  'c)  ('a  'b)  'a  'c"
  where oo_def: "cfcomp = (Λ f g x. f(gx))"

abbreviation cfcomp_syn :: "['b  'c, 'a  'b]  'a  'c"  (infixr "oo" 100)
  where "f oo g == cfcompfg"

lemma ID1 [simp]: "IDx = x"
  by (simp add: ID_def)

lemma cfcomp1: "(f oo g) = (Λ x. f(gx))"
  by (simp add: oo_def)

lemma cfcomp2 [simp]: "(f oo g)x = f(gx)"
  by (simp add: cfcomp1)

lemma cfcomp_LAM: "cont g  f oo (Λ x. g x) = (Λ x. f(g x))"
  by (simp add: cfcomp1)

lemma cfcomp_strict [simp]: " oo f = "
  by (simp add: cfun_eq_iff)

text ‹
  Show that interpretation of (pcpo, _→_›) is a category.
   The class of objects is interpretation of syntactical class pcpo.
   The class of arrows  between objects typ'a and typ'b is interpret. of typ'a  'b.
   The identity arrow is interpretation of termID.
   The composition of f and g is interpretation of oo›.

lemma ID2 [simp]: "f oo ID = f"
  by (rule cfun_eqI, simp)

lemma ID3 [simp]: "ID oo f = f"
  by (rule cfun_eqI) simp

lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
  by (rule cfun_eqI) simp

subsection ‹Strictified functions›

default_sort pcpo

definition seq :: "'a  'b  'b"
  where "seq = (Λ x. if x =  then  else ID)"

lemma cont2cont_if_bottom [cont2cont, simp]:
  assumes f: "cont (λx. f x)"
    and g: "cont (λx. g x)"
  shows "cont (λx. if f x =  then  else g x)"
proof (rule cont_apply [OF f])
  show "cont (λy. if y =  then  else g x)" for x
    unfolding cont_def is_lub_def is_ub_def ball_simps
    by (simp add: lub_eq_bottom_iff)
  show "cont (λx. if y =  then  else g x)" for y
    by (simp add: g)

lemma seq_conv_if: "seqx = (if x =  then  else ID)"
  by (simp add: seq_def)

lemma seq_simps [simp]:
  "seq = "
  "seqx = "
  "x    seqx = ID"
  by (simp_all add: seq_conv_if)

definition strictify  :: "('a  'b)  'a  'b"
  where "strictify = (Λ f x. seqx(fx))"

lemma strictify_conv_if: "strictifyfx = (if x =  then  else fx)"
  by (simp add: strictify_def)

lemma strictify1 [simp]: "strictifyf = "
  by (simp add: strictify_conv_if)

lemma strictify2 [simp]: "x    strictifyfx = fx"
  by (simp add: strictify_conv_if)

subsection ‹Continuity of let-bindings›

lemma cont2cont_Let:
  assumes f: "cont (λx. f x)"
  assumes g1: "y. cont (λx. g x y)"
  assumes g2: "x. cont (λy. g x y)"
  shows "cont (λx. let y = f x in g x y)"
  unfolding Let_def using f g2 g1 by (rule cont_apply)

lemma cont2cont_Let' [simp, cont2cont]:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λp. g (fst p) (snd p))"
  shows "cont (λx. let y = f x in g x y)"
  using f
proof (rule cont2cont_Let)
  from g show "cont (λy. g x y)" for x
    by (simp add: prod_cont_iff)
  from g show "cont (λx. g x y)" for y
    by (simp add: prod_cont_iff)

text ‹The simple version (suggested by Joachim Breitner) is needed if
  the type of the defined term is not a cpo.›

lemma cont2cont_Let_simple [simp, cont2cont]:
  assumes "y. cont (λx. g x y)"
  shows "cont (λx. let y = t in g x y)"
  unfolding Let_def using assms .