# Theory Cont

Up to index of Isabelle/HOLCF

theory Cont
imports Ffun
uses [Cont.ML]
begin

    (*  Title:      HOLCF/Cont.thy
        ID:         $Id: Cont.thy,v 1.25 2005/07/07 16:19:20 huffman Exp $
        Author:     Franz Regensburger

    Results about continuity and monotonicity.
    *)

    header {* Continuity and monotonicity *}

    theory Cont
    imports Ffun
    begin

    text {*
       Now we change the default class! Form now on all untyped type variables are
       of default class po
    *}

    defaultsort po

    subsection {* Definitions *}

    constdefs
      monofun :: "('a => 'b) => bool"  -- "monotonicity"
      "monofun f ≡ ∀x y. x \<sqsubseteq> y --> f x \<sqsubseteq> f y"

      contlub :: "('a::cpo => 'b::cpo) => bool"  -- "first cont. def"
      "contlub f ≡ ∀Y. chain Y --> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"

      cont    :: "('a::cpo => 'b::cpo) => bool"  -- "secnd cont. def"
      "cont f    ≡ ∀Y. chain Y --> range (λi. f (Y i)) <<| f (\<Squnion>i. Y i)"

    lemma contlubI:
      "[|!!Y. chain Y ==> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))|] ==> contlub f"
    by (simp add: contlub_def)

    lemma contlubE:
      "[|contlub f; chain Y|] ==> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
    by (simp add: contlub_def)

    lemma contI:
      "[|!!Y. chain Y ==> range (λi. f (Y i)) <<| f (\<Squnion>i. Y i)|] ==> cont f"
    by (simp add: cont_def)

    lemma contE:
      "[|cont f; chain Y|] ==> range (λi. f (Y i)) <<| f (\<Squnion>i. Y i)"
    by (simp add: cont_def)

    lemma monofunI:
      "[|!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y|] ==> monofun f"
    by (simp add: monofun_def)

    lemma monofunE:
      "[|monofun f; x \<sqsubseteq> y|] ==> f x \<sqsubseteq> f y"
    by (simp add: monofun_def)

    text {*
      The following results are about application for functions in @{typ "'a=>'b"}
    *}

    lemma monofun_fun_fun: "f \<sqsubseteq> g ==> f x \<sqsubseteq> g x"
    by (simp add: less_fun_def)

    lemma monofun_fun_arg: "[|monofun f; x \<sqsubseteq> y|] ==> f x \<sqsubseteq> f y"
    by (rule monofunE)

    lemma monofun_fun: "[|monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y|] ==> f x \<sqsubseteq> g y"
    by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])

    subsection {* @{prop "monofun f ∧ contlub f ≡ cont f"} *}

    text {* monotone functions map chains to chains *}

    lemma ch2ch_monofun: "[|monofun f; chain Y|] ==> chain (λi. f (Y i))"
    apply (rule chainI)
    apply (erule monofunE)
    apply (erule chainE)
    done

    text {* monotone functions map upper bound to upper bounds *}

    lemma ub2ub_monofun:
      "[|monofun f; range Y <| u|] ==> range (λi. f (Y i)) <| f u"
    apply (rule ub_rangeI)
    apply (erule monofunE)
    apply (erule ub_rangeD)
    done

    text {* left to right: @{prop "monofun f ∧ contlub f ==> cont f"} *}

    lemma monocontlub2cont: "[|monofun f; contlub f|] ==> cont f"
    apply (rule contI)
    apply (rule thelubE)
    apply (erule ch2ch_monofun)
    apply assumption
    apply (erule contlubE [symmetric])
    apply assumption
    done

    text {* first a lemma about binary chains *}

    lemma binchain_cont:
      "[|cont f; x \<sqsubseteq> y|] ==> range (λi::nat. f (if i = 0 then x else y)) <<| f y"
    apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y")
    apply (erule subst)
    apply (erule contE)
    apply (erule bin_chain)
    apply (rule_tac f=f in arg_cong)
    apply (erule lub_bin_chain [THEN thelubI])
    done

    text {* right to left: @{prop "cont f ==> monofun f ∧ contlub f"} *}
    text {* part1: @{prop "cont f ==> monofun f"} *}

    lemma cont2mono: "cont f ==> monofun f"
    apply (rule monofunI)
    apply (drule binchain_cont, assumption)
    apply (drule_tac i=0 in is_ub_lub)
    apply simp
    done

    lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]

    text {* right to left: @{prop "cont f ==> monofun f ∧ contlub f"} *}
    text {* part2: @{prop "cont f ==> contlub f"} *}

    lemma cont2contlub: "cont f ==> contlub f"
    apply (rule contlubI)
    apply (rule thelubI [symmetric])
    apply (erule contE)
    apply assumption
    done

    lemmas cont2contlubE = cont2contlub [THEN contlubE]

    subsection {* Continuity of basic functions *}

    text {* The identity function is continuous *}

    lemma cont_id: "cont (λx. x)"
    apply (rule contI)
    apply (erule thelubE)
    apply (rule refl)
    done

    text {* constant functions are continuous *}

    lemma cont_const: "cont (λx. c)"
    apply (rule contI)
    apply (rule lub_const)
    done

    text {* if-then-else is continuous *}

    lemma cont_if: "[|cont f; cont g|] ==> cont (λx. if b then f x else g x)"
    by (induct b) simp_all

    subsection {* Propagation of monotonicity and continuity *}

    text {* the lub of a chain of monotone functions is monotone *}

    lemma monofun_lub_fun:
      "[|chain (F::nat => 'a => 'b::cpo); ∀i. monofun (F i)|]
        ==> monofun (\<Squnion>i. F i)"
    apply (rule monofunI)
    apply (simp add: thelub_fun)
    apply (rule lub_mono [rule_format])
    apply (erule ch2ch_fun)
    apply (erule ch2ch_fun)
    apply (simp add: monofunE)
    done

    text {* the lub of a chain of continuous functions is continuous *}

    declare range_composition [simp del]

    lemma contlub_lub_fun:
      "[|chain F; ∀i. cont (F i)|] ==> contlub (\<Squnion>i. F i)"
    apply (rule contlubI)
    apply (simp add: thelub_fun)
    apply (simp add: cont2contlubE)
    apply (rule ex_lub)
    apply (erule ch2ch_fun)
    apply (simp add: ch2ch_cont)
    done

    lemma cont_lub_fun:
      "[|chain F; ∀i. cont (F i)|] ==> cont (\<Squnion>i. F i)"
    apply (rule monocontlub2cont)
    apply (erule monofun_lub_fun)
    apply (simp add: cont2mono)
    apply (erule contlub_lub_fun)
    apply assumption
    done

    lemma cont2cont_lub:
      "[|chain F; !!i. cont (F i)|] ==> cont (λx. \<Squnion>i. F i x)"
    by (simp add: thelub_fun [symmetric] cont_lub_fun)

    lemma mono2mono_MF1L: "monofun f ==> monofun (λx. f x y)"
    apply (rule monofunI)
    apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
    done

    lemma cont2cont_CF1L: "cont f ==> cont (λx. f x y)"
    apply (rule monocontlub2cont)
    apply (erule cont2mono [THEN mono2mono_MF1L])
    apply (rule contlubI)
    apply (simp add: cont2contlubE)
    apply (simp add: thelub_fun ch2ch_cont)
    done

    text {* Note @{text "(λx. λy. f x y) = f"} *}

    lemma mono2mono_MF1L_rev: "∀y. monofun (λx. f x y) ==> monofun f"
    apply (rule monofunI)
    apply (rule less_fun [THEN iffD2])
    apply (blast dest: monofunE)
    done

    lemma cont2cont_CF1L_rev: "∀y. cont (λx. f x y) ==> cont f"
    apply (subgoal_tac "monofun f")
    apply (rule monocontlub2cont)
    apply assumption
    apply (rule contlubI)
    apply (rule ext)
    apply (simp add: thelub_fun ch2ch_monofun)
    apply (blast dest: cont2contlubE)
    apply (simp add: mono2mono_MF1L_rev cont2mono)
    done

    lemma cont2cont_lambda: "(!!y. cont (λx. f x y)) ==> cont (λx. (λy. f x y))"
    apply (rule cont2cont_CF1L_rev)
    apply simp
    done

    text {* What D.A.Schmidt calls continuity of abstraction; never used here *}

    lemma contlub_abstraction:
      "[|chain Y; ∀y. cont (λx.(c::'a::cpo=>'b::type=>'c::cpo) x y)|] ==>
        (λy. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (λy. c (Y i) y))"
    apply (rule thelub_fun [symmetric])
    apply (rule ch2ch_cont)
    apply (erule (1) cont2cont_CF1L_rev)
    done

    lemma mono2mono_app:
      "[|monofun f; ∀x. monofun (f x); monofun t|] ==> monofun (λx. (f x) (t x))"
    apply (rule monofunI)
    apply (simp add: monofun_fun monofunE)
    done

    lemma cont2contlub_app:
      "[|cont f; ∀x. cont (f x); cont t|] ==> contlub (λx. (f x) (t x))"
    apply (rule contlubI)
    apply (subgoal_tac "chain (λi. f (Y i))")
    apply (subgoal_tac "chain (λi. t (Y i))")
    apply (simp add: cont2contlubE thelub_fun)
    apply (rule diag_lub)
    apply (erule ch2ch_fun)
    apply (drule spec)
    apply (erule (1) ch2ch_cont)
    apply (erule (1) ch2ch_cont)
    apply (erule (1) ch2ch_cont)
    done

    lemma cont2cont_app:
      "[|cont f; ∀x. cont (f x); cont t|] ==> cont (λx. (f x) (t x))"
    by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)

    lemmas cont2cont_app2 = cont2cont_app [rule_format]

    lemma cont2cont_app3: "[|cont f; cont t|] ==> cont (λx. f (t x))"
    by (rule cont2cont_app2 [OF cont_const])

    subsection {* Finite chains and flat pcpos *}

    text {* monotone functions map finite chains to finite chains *}

    lemma monofun_finch2finch:
      "[|monofun f; finite_chain Y|] ==> finite_chain (λn. f (Y n))"
    apply (unfold finite_chain_def)
    apply (simp add: ch2ch_monofun)
    apply (force simp add: max_in_chain_def)
    done

    text {* The same holds for continuous functions *}

    lemma cont_finch2finch:
      "[|cont f; finite_chain Y|] ==> finite_chain (λn. f (Y n))"
    by (rule cont2mono [THEN monofun_finch2finch])

    lemma chfindom_monofun2cont: "monofun f ==> cont (f::'a::chfin => 'b::pcpo)"
    apply (rule monocontlub2cont)
    apply assumption
    apply (rule contlubI)
    apply (frule chfin2finch)
    apply (clarsimp simp add: finite_chain_def)
    apply (subgoal_tac "max_in_chain i (λi. f (Y i))")
    apply (simp add: maxinch_is_thelub ch2ch_monofun)
    apply (force simp add: max_in_chain_def)
    done

    text {* some properties of flat *}

    lemma flatdom_strict2mono: "f ⊥ = ⊥ ==> monofun (f::'a::flat => 'b::pcpo)"
    apply (rule monofunI)
    apply (drule ax_flat [rule_format])
    apply auto
    done

    lemma flatdom_strict2cont: "f ⊥ = ⊥ ==> cont (f::'a::flat => 'b::pcpo)"
    by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])

    end

### Definitions

lemma contlubI:

      (!!Y. chain Y ==> f (lub (range Y)) = (LUB i. f (Y i))) ==> contlub f

lemma contlubE:

      [| contlub f; chain Y |] ==> f (lub (range Y)) = (LUB i. f (Y i))

lemma contI:

      (!!Y. chain Y ==> range (%i. f (Y i)) <<| f (lub (range Y))) ==> cont f

lemma contE:

      [| cont f; chain Y |] ==> range (%i. f (Y i)) <<| f (lub (range Y))

lemma monofunI:

      (!!x y. x << y ==> f x << f y) ==> monofun f

lemma monofunE:

      [| monofun f; x << y |] ==> f x << f y

lemma monofun_fun_fun:

      f << g ==> f x << g x

lemma monofun_fun_arg:

      [| monofun f; x << y |] ==> f x << f y

lemma monofun_fun:

      [| monofun f; monofun g; f << g; x << y |] ==> f x << g y

### @{prop "monofun f ∧ contlub f ≡ cont f"}

lemma ch2ch_monofun:

      [| monofun f; chain Y |] ==> chain (%i. f (Y i))

lemma ub2ub_monofun:

      [| monofun f; range Y <| u |] ==> range (%i. f (Y i)) <| f u

lemma monocontlub2cont:

      [| monofun f; contlub f |] ==> cont f

lemma binchain_cont:

      [| cont f; x << y |] ==> range (%i. f (if i = 0 then x else y)) <<| f y

lemma cont2mono:

      cont f ==> monofun f

lemmas ch2ch_cont:

      [| cont f; chain Y |] ==> chain (%i. f (Y i))

lemmas ch2ch_cont:

      [| cont f; chain Y |] ==> chain (%i. f (Y i))

lemma cont2contlub:

      cont f ==> contlub f

lemmas cont2contlubE:

      [| cont f; chain Y |] ==> f (lub (range Y)) = (LUB i. f (Y i))

lemmas cont2contlubE:

      [| cont f; chain Y |] ==> f (lub (range Y)) = (LUB i. f (Y i))

### Continuity of basic functions

lemma cont_id:

      cont (%x. x)

lemma cont_const:

      cont (%x. c)

lemma cont_if:

      [| cont f; cont g |] ==> cont (%x. if b then f x else g x)

### Propagation of monotonicity and continuity

lemma monofun_lub_fun:

      [| chain F; ∀i. monofun (F i) |] ==> monofun (lub (range F))

lemma contlub_lub_fun:

      [| chain F; ∀i. cont (F i) |] ==> contlub (lub (range F))

lemma cont_lub_fun:

      [| chain F; ∀i. cont (F i) |] ==> cont (lub (range F))

lemma cont2cont_lub:

      [| chain F; !!i. cont (F i) |] ==> cont (%x. LUB i. F i x)

lemma mono2mono_MF1L:

      monofun f ==> monofun (%x. f x y)

lemma cont2cont_CF1L:

      cont f ==> cont (%x. f x y)

lemma mono2mono_MF1L_rev:

      ∀y. monofun (%x. f x y) ==> monofun f

lemma cont2cont_CF1L_rev:

      ∀y. cont (%x. f x y) ==> cont f

lemma cont2cont_lambda:

      (!!y. cont (%x. f x y)) ==> cont f

lemma contlub_abstraction:

      [| chain Y; ∀y. cont (%x. c x y) |]
      ==> (%y. LUB i. c (Y i) y) = (LUB i. c (Y i))

lemma mono2mono_app:

      [| monofun f; ∀x. monofun (f x); monofun t |] ==> monofun (%x. f x (t x))

lemma cont2contlub_app:

      [| cont f; ∀x. cont (f x); cont t |] ==> contlub (%x. f x (t x))

lemma cont2cont_app:

      [| cont f; ∀x. cont (f x); cont t |] ==> cont (%x. f x (t x))

lemmas cont2cont_app2:

      [| cont f; !!x. cont (f x); cont t |] ==> cont (%x. f x (t x))

lemmas cont2cont_app2:

      [| cont f; !!x. cont (f x); cont t |] ==> cont (%x. f x (t x))

lemma cont2cont_app3:

      [| cont f; cont t |] ==> cont (%x. f (t x))

### Finite chains and flat pcpos

lemma monofun_finch2finch:

      [| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))

lemma cont_finch2finch:

      [| cont f; finite_chain Y |] ==> finite_chain (%n. f (Y n))

lemma chfindom_monofun2cont:

      monofun f ==> cont f

lemma flatdom_strict2mono:

      f UU = UU ==> monofun f

lemma flatdom_strict2cont:

      f UU = UU ==> cont f