# Theory Ffun

Up to index of Isabelle/HOLCF

theory Ffun
imports Pcpo
uses [Ffun.ML]
begin

    (*  Title:      HOLCF/FunCpo.thy
        ID:         $Id: Ffun.thy,v 1.1 2005/06/03 20:07:30 huffman Exp $
        Author:     Franz Regensburger

    Definition of the partial ordering for the type of all functions => (fun)

    Class instance of  => (fun) for class pcpo.
    *)

    header {* Class instances for the full function space *}

    theory Ffun
    imports Pcpo
    begin

    subsection {* Type @{typ "'a => 'b"} is a partial order *}

    instance fun  :: (type, sq_ord) sq_ord ..

    defs (overloaded)
      less_fun_def: "(op \<sqsubseteq>) ≡ (λf g. ∀x. f x \<sqsubseteq> g x)"

    lemma refl_less_fun: "(f::'a::type => 'b::po) \<sqsubseteq> f"
    by (simp add: less_fun_def)

    lemma antisym_less_fun:
      "[|(f1::'a::type => 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1|] ==> f1 = f2"
    by (simp add: less_fun_def expand_fun_eq antisym_less)

    lemma trans_less_fun:
      "[|(f1::'a::type => 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3|] ==> f1 \<sqsubseteq> f3"
    apply (unfold less_fun_def)
    apply clarify
    apply (rule trans_less)
    apply (erule spec)
    apply (erule spec)
    done

    instance fun  :: (type, po) po
    by intro_classes
      (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+

    text {* make the symbol @{text "<<"} accessible for type fun *}

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

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

    subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *}

    lemma minimal_fun: "(λx. ⊥) \<sqsubseteq> f"
    by (simp add: less_fun_def)

    lemma least_fun: "∃x::'a => 'b::pcpo. ∀y. x \<sqsubseteq> y"
    apply (rule_tac x = "λx. ⊥" in exI)
    apply (rule minimal_fun [THEN allI])
    done

    subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}

    text {* chains of functions yield chains in the po range *}

    lemma ch2ch_fun: "chain S ==> chain (λi. S i x)"
    by (simp add: chain_def less_fun_def)

    lemma ch2ch_fun_rev: "(!!x. chain (λi. S i x)) ==> chain S"
    by (simp add: chain_def less_fun_def)

    text {* upper bounds of function chains yield upper bound in the po range *}

    lemma ub2ub_fun:
      "range (S::nat => 'a => 'b::po) <| u ==> range (λi. S i x) <| u x"
    by (auto simp add: is_ub_def less_fun_def)

    text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}

    lemma lub_fun:
      "chain (S::nat => 'a::type => 'b::cpo)
        ==> range S <<| (λx. \<Squnion>i. S i x)"
    apply (rule is_lubI)
    apply (rule ub_rangeI)
    apply (rule less_fun_ext)
    apply (rule is_ub_thelub)
    apply (erule ch2ch_fun)
    apply (rule less_fun_ext)
    apply (rule is_lub_thelub)
    apply (erule ch2ch_fun)
    apply (erule ub2ub_fun)
    done

    lemma thelub_fun:
      "chain (S::nat => 'a::type => 'b::cpo)
        ==> lub (range S) = (λx. \<Squnion>i. S i x)"
    by (rule lub_fun [THEN thelubI])

    lemma cpo_fun:
      "chain (S::nat => 'a::type => 'b::cpo) ==> ∃x. range S <<| x"
    by (rule exI, erule lub_fun)

    instance fun  :: (type, cpo) cpo
    by intro_classes (rule cpo_fun)

    instance fun  :: (type, pcpo) pcpo
    by intro_classes (rule least_fun)

    text {* for compatibility with old HOLCF-Version *}
    lemma inst_fun_pcpo: "UU = (%x. UU)"
    by (rule minimal_fun [THEN UU_I, symmetric])

    text {* function application is strict in the left argument *}
    lemma app_strict [simp]: "⊥ x = ⊥"
    by (simp add: inst_fun_pcpo)

    end

### Type @{typ "'a => 'b"} is a partial order

lemma refl_less_fun:

      f << f

lemma antisym_less_fun:

      [| f1.0 << f2.0; f2.0 << f1.0 |] ==> f1.0 = f2.0

lemma trans_less_fun:

      [| f1.0 << f2.0; f2.0 << f3.0 |] ==> f1.0 << f3.0

lemma less_fun:

      f << g = (∀x. f x << g x)

lemma less_fun_ext:

      (!!x. f x << g x) ==> f << g

### Type @{typ "'a::type => 'b::pcpo"} is pointed

lemma minimal_fun:

      (%x. UU) << f

lemma least_fun:

      ∃x. ∀y. x << y

### Type @{typ "'a::type => 'b::cpo"} is chain complete

lemma ch2ch_fun:

      chain S ==> chain (%i. S i x)

lemma ch2ch_fun_rev:

      (!!x. chain (%i. S i x)) ==> chain S

lemma ub2ub_fun:

      range S <| u ==> range (%i. S i x) <| u x

lemma lub_fun:

      chain S ==> range S <<| (%x. LUB i. S i x)

lemma thelub_fun:

      chain S ==> lub (range S) = (%x. LUB i. S i x)

lemma cpo_fun:

      chain S ==> ∃x. range S <<| x

lemma inst_fun_pcpo:

      UU = (%x. UU)

lemma app_strict:

      UU x = UU