# Theory Pcpo

Up to index of Isabelle/HOLCF

theory Pcpo
imports Porder
uses [Pcpo.ML]
begin

    (*  Title:      HOLCF/Pcpo.thy
        ID:         $Id: Pcpo.thy,v 1.29 2005/07/07 16:22:01 huffman Exp $
        Author:     Franz Regensburger

    Introduction of the classes cpo and pcpo.
    *)

    header {* Classes cpo and pcpo *}

    theory Pcpo
    imports Porder
    begin

    subsection {* Complete partial orders *}

    text {* The class cpo of chain complete partial orders *}

    axclass cpo < po
            -- {* class axiom: *}
      cpo:   "chain S ==> ∃x. range S <<| x"

    text {* in cpo's everthing equal to THE lub has lub properties for every chain *}

    lemma thelubE: "[|chain S; (\<Squnion>i. S i) = (l::'a::cpo)|] ==> range S <<| l"
    by (blast dest: cpo intro: lubI)

    text {* Properties of the lub *}

    lemma is_ub_thelub: "chain (S::nat => 'a::cpo) ==> S x \<sqsubseteq> (\<Squnion>i. S i)"
    by (blast dest: cpo intro: lubI [THEN is_ub_lub])

    lemma is_lub_thelub:
      "[|chain (S::nat => 'a::cpo); range S <| x|] ==> (\<Squnion>i. S i) \<sqsubseteq> x"
    by (blast dest: cpo intro: lubI [THEN is_lub_lub])

    lemma lub_range_mono:
      "[|range X ⊆ range Y; chain Y; chain (X::nat => 'a::cpo)|]
        ==> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    apply (erule is_lub_thelub)
    apply (rule ub_rangeI)
    apply (subgoal_tac "∃j. X i = Y j")
    apply  clarsimp
    apply  (erule is_ub_thelub)
    apply auto
    done

    lemma lub_range_shift:
      "chain (Y::nat => 'a::cpo) ==> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
    apply (rule antisym_less)
    apply (rule lub_range_mono)
    apply    fast
    apply   assumption
    apply (erule chain_shift)
    apply (rule is_lub_thelub)
    apply assumption
    apply (rule ub_rangeI)
    apply (rule trans_less)
    apply (rule_tac [2] is_ub_thelub)
    apply (erule_tac [2] chain_shift)
    apply (erule chain_mono3)
    apply (rule le_add1)
    done

    lemma maxinch_is_thelub:
      "chain Y ==> max_in_chain i Y = ((\<Squnion>i. Y i) = ((Y i)::'a::cpo))"
    apply (rule iffI)
    apply (fast intro!: thelubI lub_finch1)
    apply (unfold max_in_chain_def)
    apply (safe intro!: antisym_less)
    apply (fast elim!: chain_mono3)
    apply (drule sym)
    apply (force elim!: is_ub_thelub)
    done

    text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}

    lemma lub_mono:
      "[|chain (X::nat => 'a::cpo); chain Y; ∀k. X k \<sqsubseteq> Y k|]
        ==> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    apply (erule is_lub_thelub)
    apply (rule ub_rangeI)
    apply (rule trans_less)
    apply (erule spec)
    apply (erule is_ub_thelub)
    done

    text {* the = relation between two chains is preserved by their lubs *}

    lemma lub_equal:
      "[|chain (X::nat => 'a::cpo); chain Y; ∀k. X k = Y k|]
        ==> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    by (simp only: expand_fun_eq [symmetric])

    text {* more results about mono and = of lubs of chains *}

    lemma lub_mono2:
      "[|∃j::nat. ∀i>j. X i = Y i; chain (X::nat=>'a::cpo); chain Y|]
        ==> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    apply (erule exE)
    apply (rule is_lub_thelub)
    apply assumption
    apply (rule ub_rangeI)
    apply (case_tac "j < i")
    apply (rule_tac s="Y i" and t="X i" in subst)
    apply simp
    apply (erule is_ub_thelub)
    apply (rule_tac y = "X (Suc j)" in trans_less)
    apply (erule chain_mono)
    apply (erule not_less_eq [THEN iffD1])
    apply (rule_tac s="Y (Suc j)" and t="X (Suc j)" in subst)
    apply simp
    apply (erule is_ub_thelub)
    done

    lemma lub_equal2:
      "[|∃j. ∀i>j. X i = Y i; chain (X::nat => 'a::cpo); chain Y|]
        ==> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    by (blast intro: antisym_less lub_mono2 sym)

    lemma lub_mono3:
      "[|chain (Y::nat => 'a::cpo); chain X; ∀i. ∃j. Y i \<sqsubseteq> X j|]
        ==> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
    apply (rule is_lub_thelub)
    apply assumption
    apply (rule ub_rangeI)
    apply (erule allE)
    apply (erule exE)
    apply (erule trans_less)
    apply (erule is_ub_thelub)
    done

    lemma ch2ch_lub:
      fixes Y :: "nat => nat => 'a::cpo"
      assumes 1: "!!j. chain (λi. Y i j)"
      assumes 2: "!!i. chain (λj. Y i j)"
      shows "chain (λi. \<Squnion>j. Y i j)"
    apply (rule chainI)
    apply (rule lub_mono [rule_format, OF 2 2])
    apply (rule chainE [OF 1])
    done

    lemma diag_lub:
      fixes Y :: "nat => nat => 'a::cpo"
      assumes 1: "!!j. chain (λi. Y i j)"
      assumes 2: "!!i. chain (λj. Y i j)"
      shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
    proof (rule antisym_less)
      have 3: "chain (λi. Y i i)"
        apply (rule chainI)
        apply (rule trans_less)
        apply (rule chainE [OF 1])
        apply (rule chainE [OF 2])
        done
      have 4: "chain (λi. \<Squnion>j. Y i j)"
        by (rule ch2ch_lub [OF 1 2])
      show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
        apply (rule is_lub_thelub [OF 4])
        apply (rule ub_rangeI)
        apply (rule lub_mono3 [rule_format, OF 2 3])
        apply (rule exI)
        apply (rule trans_less)
        apply (rule chain_mono3 [OF 1 le_maxI1])
        apply (rule chain_mono3 [OF 2 le_maxI2])
        done
      show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
        apply (rule lub_mono [rule_format, OF 3 4])
        apply (rule is_ub_thelub [OF 2])
        done
    qed

    lemma ex_lub:
      fixes Y :: "nat => nat => 'a::cpo"
      assumes 1: "!!j. chain (λi. Y i j)"
      assumes 2: "!!i. chain (λj. Y i j)"
      shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
    by (simp add: diag_lub 1 2)

    subsection {* Pointed cpos *}

    text {* The class pcpo of pointed cpos *}

    axclass pcpo < cpo
      least: "∃x. ∀y. x \<sqsubseteq> y"

    constdefs
      UU :: "'a::pcpo"
      "UU ≡ THE x. ALL y. x \<sqsubseteq> y"

    syntax (xsymbols)
      UU :: "'a::pcpo" ("⊥")

    text {* derive the old rule minimal *}

    lemma UU_least: "∀z. ⊥ \<sqsubseteq> z"
    apply (unfold UU_def)
    apply (rule theI')
    apply (rule ex_ex1I)
    apply (rule least)
    apply (blast intro: antisym_less)
    done

    lemma minimal [iff]: "⊥ \<sqsubseteq> x"
    by (rule UU_least [THEN spec])

    lemma UU_reorient: "(⊥ = x) = (x = ⊥)"
    by auto

    ML_setup {*
    local
      val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
      fun is_UU (Const ("Pcpo.UU",_)) = true
        | is_UU _ = false;
      fun reorient_proc sg _ (_ $ t $ u) =
        if is_UU u then NONE else SOME meta_UU_reorient;
    in
      val UU_reorient_simproc =
        Simplifier.simproc (the_context ())
          "UU_reorient_simproc" ["UU=x"] reorient_proc
    end;

    Addsimprocs [UU_reorient_simproc];
    *}

    text {* useful lemmas about @{term ⊥} *}

    lemma eq_UU_iff: "(x = ⊥) = (x \<sqsubseteq> ⊥)"
    apply (rule iffI)
    apply (erule ssubst)
    apply (rule refl_less)
    apply (rule antisym_less)
    apply assumption
    apply (rule minimal)
    done

    lemma UU_I: "x \<sqsubseteq> ⊥ ==> x = ⊥"
    by (subst eq_UU_iff)

    lemma not_less2not_eq: "¬ (x::'a::po) \<sqsubseteq> y ==> x ≠ y"
    by auto

    lemma chain_UU_I: "[|chain Y; (\<Squnion>i. Y i) = ⊥|] ==> ∀i. Y i = ⊥"
    apply (rule allI)
    apply (rule UU_I)
    apply (erule subst)
    apply (erule is_ub_thelub)
    done

    lemma chain_UU_I_inverse: "∀i::nat. Y i = ⊥ ==> (\<Squnion>i. Y i) = ⊥"
    apply (rule lub_chain_maxelem)
    apply (erule spec)
    apply simp
    done

    lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) ≠ ⊥ ==> ∃i::nat. Y i ≠ ⊥"
    by (blast intro: chain_UU_I_inverse)

    lemma notUU_I: "[|x \<sqsubseteq> y; x ≠ ⊥|] ==> y ≠ ⊥"
    by (blast intro: UU_I)

    lemma chain_mono2: "[|∃j. Y j ≠ ⊥; chain Y|] ==> ∃j. ∀i>j. Y i ≠ ⊥"
    by (blast dest: notUU_I chain_mono)

    subsection {* Chain-finite and flat cpos *}

    text {* further useful classes for HOLCF domains *}

    axclass chfin < po
      chfin: "∀Y. chain Y --> (∃n. max_in_chain n Y)"

    axclass flat < pcpo
      ax_flat: "∀x y. x \<sqsubseteq> y --> (x = ⊥) ∨ (x = y)"

    text {* some properties for chfin and flat *}

    text {* chfin types are cpo *}

    lemma chfin_imp_cpo:
      "chain (S::nat => 'a::chfin) ==> ∃x. range S <<| x"
    apply (frule chfin [rule_format])
    apply (blast intro: lub_finch1)
    done

    instance chfin < cpo
    by intro_classes (rule chfin_imp_cpo)

    text {* flat types are chfin *}

    lemma flat_imp_chfin:
         "∀Y::nat => 'a::flat. chain Y --> (∃n. max_in_chain n Y)"
    apply (unfold max_in_chain_def)
    apply clarify
    apply (case_tac "∀i. Y i = ⊥")
    apply simp
    apply simp
    apply (erule exE)
    apply (rule_tac x="i" in exI)
    apply clarify
    apply (erule le_imp_less_or_eq [THEN disjE])
    apply safe
    apply (blast dest: chain_mono ax_flat [rule_format])
    done

    instance flat < chfin
    by intro_classes (rule flat_imp_chfin)

    text {* flat subclass of chfin; @{text adm_flat} not needed *}

    lemma flat_eq: "(a::'a::flat) ≠ ⊥ ==> a \<sqsubseteq> b = (a = b)"
    by (safe dest!: ax_flat [rule_format])

    lemma chfin2finch: "chain (Y::nat => 'a::chfin) ==> finite_chain Y"
    by (simp add: chfin finite_chain_def)

    text {* lemmata for improved admissibility introdution rule *}

    lemma infinite_chain_adm_lemma:
      "[|chain Y; ∀i. P (Y i);
        !!Y. [|chain Y; ∀i. P (Y i); ¬ finite_chain Y|] ==> P (\<Squnion>i. Y i)|]
          ==> P (\<Squnion>i. Y i)"
    apply (case_tac "finite_chain Y")
    prefer 2 apply fast
    apply (unfold finite_chain_def)
    apply safe
    apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
    apply assumption
    apply (erule spec)
    done

    lemma increasing_chain_adm_lemma:
      "[|chain Y;  ∀i. P (Y i); !!Y. [|chain Y; ∀i. P (Y i);
        ∀i. ∃j>i. Y i ≠ Y j ∧ Y i \<sqsubseteq> Y j|] ==> P (\<Squnion>i. Y i)|]
          ==> P (\<Squnion>i. Y i)"
    apply (erule infinite_chain_adm_lemma)
    apply assumption
    apply (erule thin_rl)
    apply (unfold finite_chain_def)
    apply (unfold max_in_chain_def)
    apply (fast dest: le_imp_less_or_eq elim: chain_mono)
    done

    end

### Complete partial orders

lemma thelubE:

      [| chain S; lub (range S) = l |] ==> range S <<| l

lemma is_ub_thelub:

      chain S ==> S x << lub (range S)

lemma is_lub_thelub:

      [| chain S; range S <| x |] ==> lub (range S) << x

lemma lub_range_mono:

      [| range X ⊆ range Y; chain Y; chain X |] ==> lub (range X) << lub (range Y)

lemma lub_range_shift:

      chain Y ==> (LUB i. Y (i + j)) = lub (range Y)

lemma maxinch_is_thelub:

      chain Y ==> max_in_chain i Y = (lub (range Y) = Y i)

lemma lub_mono:

      [| chain X; chain Y; ∀k. X k << Y k |] ==> lub (range X) << lub (range Y)

lemma lub_equal:

      [| chain X; chain Y; ∀k. X k = Y k |] ==> lub (range X) = lub (range Y)

lemma lub_mono2:

      [| ∃j. ∀i. j < i --> X i = Y i; chain X; chain Y |]
      ==> lub (range X) << lub (range Y)

lemma lub_equal2:

      [| ∃j. ∀i. j < i --> X i = Y i; chain X; chain Y |]
      ==> lub (range X) = lub (range Y)

lemma lub_mono3:

      [| chain Y; chain X; ∀i. ∃j. Y i << X j |] ==> lub (range Y) << lub (range X)

lemma ch2ch_lub:

      [| !!j. chain (%i. Y i j); !!i. chain (Y i) |] ==> chain (%i. lub (range (Y i)))

lemma diag_lub:

      [| !!j. chain (%i. Y i j); !!i. chain (Y i) |]
      ==> (LUB i. lub (range (Y i))) = (LUB i. Y i i)

lemma ex_lub:

      [| !!j. chain (%i. Y i j); !!i. chain (Y i) |]
      ==> (LUB i. lub (range (Y i))) = (LUB j. LUB i. Y i j)

### Pointed cpos

lemma UU_least:

      ∀z. UU << z

lemma minimal:

      UU << x

lemma UU_reorient:

      (UU = x) = (x = UU)

lemma eq_UU_iff:

      (x = UU) = x << UU

lemma UU_I:

      x << UU ==> x = UU

lemma not_less2not_eq:

      ¬ x << y ==> x ≠ y

lemma chain_UU_I:

      [| chain Y; lub (range Y) = UU |] ==> ∀i. Y i = UU

lemma chain_UU_I_inverse:

      ∀i. Y i = UU ==> lub (range Y) = UU

lemma chain_UU_I_inverse2:

      lub (range Y) ≠ UU ==> ∃i. Y i ≠ UU

lemma notUU_I:

      [| x << y; x ≠ UU |] ==> y ≠ UU

lemma chain_mono2:

      [| ∃j. Y j ≠ UU; chain Y |] ==> ∃j. ∀i. j < i --> Y i ≠ UU

### Chain-finite and flat cpos

lemma chfin_imp_cpo:

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

lemma flat_imp_chfin:

      ∀Y. chain Y --> (∃n. max_in_chain n Y)

lemma flat_eq:

      a ≠ UU ==> a << b = (a = b)

lemma chfin2finch:

      chain Y ==> finite_chain Y

lemma infinite_chain_adm_lemma:

      [| chain Y; ∀i. P (Y i);
         !!Y. [| chain Y; ∀i. P (Y i); ¬ finite_chain Y |] ==> P (lub (range Y)) |]
      ==> P (lub (range Y))

lemma increasing_chain_adm_lemma:

      [| chain Y; ∀i. P (Y i);
         !!Y. [| chain Y; ∀i. P (Y i); ∀i. ∃j. i < j ∧ Y i ≠ Y j ∧ Y i << Y j |]
              ==> P (lub (range Y)) |]
      ==> P (lub (range Y))