# Theory Limit

Up to index of Isabelle/ZF/ex

theory Limit
imports Main
begin

    (*  Title:      ZF/ex/Limit
        ID:         $Id: Limit.thy,v 1.18 2005/06/17 14:15:11 haftmann Exp $
        Author:     Sten Agerholm

        A formalization of the inverse limit construction of domain theory.

        The following paper comments on the formalization:

        "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
        In Proceedings of the First Isabelle Users Workshop, Technical
        Report No. 379, University of Cambridge Computer Laboratory, 1995.

        This is a condensed version of:

        "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
        Technical Report No. 369, University of Cambridge Computer
        Laboratory, 1995.

    (Proofs converted to Isar and tidied up considerably by lcp)
    *)

    theory Limit  imports  Main begin

    constdefs

      rel :: "[i,i,i]=>o"
        "rel(D,x,y) == <x,y>:snd(D)"

      set :: "i=>i"
        "set(D) == fst(D)"

      po  :: "i=>o"
        "po(D) ==
         (∀x ∈ set(D). rel(D,x,x)) &
         (∀x ∈ set(D). ∀y ∈ set(D). ∀z ∈ set(D).
           rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) &
         (∀x ∈ set(D). ∀y ∈ set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"

      chain :: "[i,i]=>o"
        (* Chains are object level functions nat->set(D) *)
        "chain(D,X) == X ∈ nat->set(D) & (∀n ∈ nat. rel(D,X`n,X`(succ(n))))"

      isub :: "[i,i,i]=>o"
        "isub(D,X,x) == x ∈ set(D) & (∀n ∈ nat. rel(D,X`n,x))"

      islub :: "[i,i,i]=>o"
        "islub(D,X,x) == isub(D,X,x) & (∀y. isub(D,X,y) --> rel(D,x,y))"

      lub :: "[i,i]=>i"
        "lub(D,X) == THE x. islub(D,X,x)"

      cpo :: "i=>o"
        "cpo(D) == po(D) & (∀X. chain(D,X) --> (∃x. islub(D,X,x)))"

      pcpo :: "i=>o"
        "pcpo(D) == cpo(D) & (∃x ∈ set(D). ∀y ∈ set(D). rel(D,x,y))"

      bot :: "i=>i"
        "bot(D) == THE x. x ∈ set(D) & (∀y ∈ set(D). rel(D,x,y))"

      mono :: "[i,i]=>i"
        "mono(D,E) ==
         {f ∈ set(D)->set(E).
          ∀x ∈ set(D). ∀y ∈ set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"

      cont :: "[i,i]=>i"
        "cont(D,E) ==
         {f ∈ mono(D,E).
          ∀X. chain(D,X) --> f`(lub(D,X)) = lub(E,λn ∈ nat. f`(X`n))}"

      cf :: "[i,i]=>i"
        "cf(D,E) ==
         <cont(D,E),
          {y ∈ cont(D,E)*cont(D,E). ∀x ∈ set(D). rel(E,(fst(y))`x,(snd(y))`x)}>"

      suffix :: "[i,i]=>i"
        "suffix(X,n) == λm ∈ nat. X`(n #+ m)"

      subchain :: "[i,i]=>o"
        "subchain(X,Y) == ∀m ∈ nat. ∃n ∈ nat. X`m = Y`(m #+ n)"

      dominate :: "[i,i,i]=>o"
        "dominate(D,X,Y) == ∀m ∈ nat. ∃n ∈ nat. rel(D,X`m,Y`n)"

      matrix :: "[i,i]=>o"
        "matrix(D,M) ==
         M ∈ nat -> (nat -> set(D)) &
         (∀n ∈ nat. ∀m ∈ nat. rel(D,M`n`m,M`succ(n)`m)) &
         (∀n ∈ nat. ∀m ∈ nat. rel(D,M`n`m,M`n`succ(m))) &
         (∀n ∈ nat. ∀m ∈ nat. rel(D,M`n`m,M`succ(n)`succ(m)))"

      projpair  :: "[i,i,i,i]=>o"
        "projpair(D,E,e,p) ==
         e ∈ cont(D,E) & p ∈ cont(E,D) &
         p O e = id(set(D)) & rel(cf(E,E),e O p,id(set(E)))"

      emb       :: "[i,i,i]=>o"
        "emb(D,E,e) == ∃p. projpair(D,E,e,p)"

      Rp        :: "[i,i,i]=>i"
        "Rp(D,E,e) == THE p. projpair(D,E,e,p)"

      (* Twice, constructions on cpos are more difficult. *)
      iprod     :: "i=>i"
        "iprod(DD) ==
         <(Π n ∈ nat. set(DD`n)),
          {x:(Π n ∈ nat. set(DD`n))*(Π n ∈ nat. set(DD`n)).
           ∀n ∈ nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"

      mkcpo     :: "[i,i=>o]=>i"
        (* Cannot use rel(D), is meta fun, need two more args *)
        "mkcpo(D,P) ==
         <{x ∈ set(D). P(x)},{x ∈ set(D)*set(D). rel(D,fst(x),snd(x))}>"

      subcpo    :: "[i,i]=>o"
        "subcpo(D,E) ==
         set(D) ⊆ set(E) &
         (∀x ∈ set(D). ∀y ∈ set(D). rel(D,x,y) <-> rel(E,x,y)) &
         (∀X. chain(D,X) --> lub(E,X):set(D))"

      subpcpo   :: "[i,i]=>o"
        "subpcpo(D,E) == subcpo(D,E) & bot(E):set(D)"

      emb_chain :: "[i,i]=>o"
        "emb_chain(DD,ee) ==
         (∀n ∈ nat. cpo(DD`n)) & (∀n ∈ nat. emb(DD`n,DD`succ(n),ee`n))"

      Dinf      :: "[i,i]=>i"
        "Dinf(DD,ee) ==
         mkcpo(iprod(DD))
         (%x. ∀n ∈ nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)"

    consts
      e_less    :: "[i,i,i,i]=>i"
      e_gr      :: "[i,i,i,i]=>i"

    defs  (*???NEEDS PRIMREC*)

      e_less_def: (* Valid for m le n only. *)
        "e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)"

      e_gr_def: (* Valid for n le m only. *)
        "e_gr(DD,ee,m,n) ==
         rec(m#-n,id(set(DD`n)),
             %x y. y O Rp(DD`(n#+x),DD`(succ(n#+x)),ee`(n#+x)))"

    constdefs
      eps       :: "[i,i,i,i]=>i"
        "eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"

      rho_emb   :: "[i,i,i]=>i"
        "rho_emb(DD,ee,n) == λx ∈ set(DD`n). λm ∈ nat. eps(DD,ee,n,m)`x"

      rho_proj  :: "[i,i,i]=>i"
        "rho_proj(DD,ee,n) == λx ∈ set(Dinf(DD,ee)). x`n"

      commute   :: "[i,i,i,i=>i]=>o"
        "commute(DD,ee,E,r) ==
         (∀n ∈ nat. emb(DD`n,E,r(n))) &
         (∀m ∈ nat. ∀n ∈ nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"

      mediating :: "[i,i,i=>i,i=>i,i]=>o"
        "mediating(E,G,r,f,t) == emb(E,G,t) & (∀n ∈ nat. f(n) = t O r(n))"

    lemmas nat_linear_le = Ord_linear_le [OF nat_into_Ord nat_into_Ord]

    (*----------------------------------------------------------------------*)
    (* Basic results.                                                       *)
    (*----------------------------------------------------------------------*)

    lemma set_I: "x ∈ fst(D) ==> x ∈ set(D)"
    by (simp add: set_def)

    lemma rel_I: "<x,y>:snd(D) ==> rel(D,x,y)"
    by (simp add: rel_def)

    lemma rel_E: "rel(D,x,y) ==> <x,y>:snd(D)"
    by (simp add: rel_def)

    (*----------------------------------------------------------------------*)
    (* I/E/D rules for po and cpo.                                          *)
    (*----------------------------------------------------------------------*)

    lemma po_refl: "[|po(D); x ∈ set(D)|] ==> rel(D,x,x)"
    by (unfold po_def, blast)

    lemma po_trans: "[|po(D); rel(D,x,y); rel(D,y,z); x ∈ set(D);
                      y ∈ set(D); z ∈ set(D)|] ==> rel(D,x,z)"
    by (unfold po_def, blast)

    lemma po_antisym:
        "[|po(D); rel(D,x,y); rel(D,y,x); x ∈ set(D); y ∈ set(D)|] ==> x = y"
    by (unfold po_def, blast)

    lemma poI:
      "[| !!x. x ∈ set(D) ==> rel(D,x,x);
          !!x y z. [| rel(D,x,y); rel(D,y,z); x ∈ set(D); y ∈ set(D); z ∈ set(D)|]
                   ==> rel(D,x,z);
          !!x y. [| rel(D,x,y); rel(D,y,x); x ∈ set(D); y ∈ set(D)|] ==> x=y |]
       ==> po(D)"
    by (unfold po_def, blast)

    lemma cpoI: "[| po(D); !!X. chain(D,X) ==> islub(D,X,x(D,X))|] ==> cpo(D)"
    by (simp add: cpo_def, blast)

    lemma cpo_po: "cpo(D) ==> po(D)"
    by (simp add: cpo_def)

    lemma cpo_refl [simp,intro!,TC]: "[|cpo(D); x ∈ set(D)|] ==> rel(D,x,x)"
    by (blast intro: po_refl cpo_po)

    lemma cpo_trans:
         "[|cpo(D); rel(D,x,y); rel(D,y,z); x ∈ set(D);
            y ∈ set(D); z ∈ set(D)|] ==> rel(D,x,z)"
    by (blast intro: cpo_po po_trans)

    lemma cpo_antisym:
         "[|cpo(D); rel(D,x,y); rel(D,y,x); x ∈ set(D); y ∈ set(D)|] ==> x = y"
    by (blast intro: cpo_po po_antisym)

    lemma cpo_islub: "[|cpo(D); chain(D,X);  !!x. islub(D,X,x) ==> R|] ==> R"
    by (simp add: cpo_def, blast)

    (*----------------------------------------------------------------------*)
    (* Theorems about isub and islub.                                       *)
    (*----------------------------------------------------------------------*)

    lemma islub_isub: "islub(D,X,x) ==> isub(D,X,x)"
    by (simp add: islub_def)

    lemma islub_in: "islub(D,X,x) ==> x ∈ set(D)"
    by (simp add: islub_def isub_def)

    lemma islub_ub: "[|islub(D,X,x); n ∈ nat|] ==> rel(D,X`n,x)"
    by (simp add: islub_def isub_def)

    lemma islub_least: "[|islub(D,X,x); isub(D,X,y)|] ==> rel(D,x,y)"
    by (simp add: islub_def)

    lemma islubI:
        "[|isub(D,X,x); !!y. isub(D,X,y) ==> rel(D,x,y)|] ==> islub(D,X,x)"
    by (simp add: islub_def)

    lemma isubI:
        "[|x ∈ set(D);  !!n. n ∈ nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)"
    by (simp add: isub_def)

    lemma isubE:
        "[|isub(D,X,x); [|x ∈ set(D);  !!n. n ∈ nat==>rel(D,X`n,x)|] ==> P
         |] ==> P"
    by (simp add: isub_def)

    lemma isubD1: "isub(D,X,x) ==> x ∈ set(D)"
    by (simp add: isub_def)

    lemma isubD2: "[|isub(D,X,x); n ∈ nat|]==>rel(D,X`n,x)"
    by (simp add: isub_def)

    lemma islub_unique: "[|islub(D,X,x); islub(D,X,y); cpo(D)|] ==> x = y"
    by (blast intro: cpo_antisym islub_least islub_isub islub_in)

    (*----------------------------------------------------------------------*)
    (* lub gives the least upper bound of chains.                           *)
    (*----------------------------------------------------------------------*)

    lemma cpo_lub: "[|chain(D,X); cpo(D)|] ==> islub(D,X,lub(D,X))"
    apply (simp add: lub_def)
    apply (best elim: cpo_islub intro: theI islub_unique)
    done

    (*----------------------------------------------------------------------*)
    (* Theorems about chains.                                               *)
    (*----------------------------------------------------------------------*)

    lemma chainI:
      "[|X ∈ nat->set(D);  !!n. n ∈ nat ==> rel(D,X`n,X`succ(n))|] ==> chain(D,X)"
    by (simp add: chain_def)

    lemma chain_fun: "chain(D,X) ==> X ∈ nat -> set(D)"
    by (simp add: chain_def)

    lemma chain_in [simp,TC]: "[|chain(D,X); n ∈ nat|] ==> X`n ∈ set(D)"
    apply (simp add: chain_def)
    apply (blast dest: apply_type)
    done

    lemma chain_rel [simp,TC]:
         "[|chain(D,X); n ∈ nat|] ==> rel(D, X ` n, X ` succ(n))"
    by (simp add: chain_def)

    lemma chain_rel_gen_add:
         "[|chain(D,X); cpo(D); n ∈ nat; m ∈ nat|] ==> rel(D,X`n,(X`(m #+ n)))"
    apply (induct_tac m)
    apply (auto intro: cpo_trans)
    done

    lemma chain_rel_gen:
        "[|n le m; chain(D,X); cpo(D); m ∈ nat|] ==> rel(D,X`n,X`m)"
    apply (frule lt_nat_in_nat, erule nat_succI)
    apply (erule rev_mp) (*prepare the induction*)
    apply (induct_tac m)
    apply (auto intro: cpo_trans simp add: le_iff)
    done

    (*----------------------------------------------------------------------*)
    (* Theorems about pcpos and bottom.                                     *)
    (*----------------------------------------------------------------------*)

    lemma pcpoI:
        "[|!!y. y ∈ set(D)==>rel(D,x,y); x ∈ set(D); cpo(D)|]==>pcpo(D)"
    by (simp add: pcpo_def, auto)

    lemma pcpo_cpo [TC]: "pcpo(D) ==> cpo(D)"
    by (simp add: pcpo_def)

    lemma pcpo_bot_ex1:
        "pcpo(D) ==> ∃! x. x ∈ set(D) & (∀y ∈ set(D). rel(D,x,y))"
    apply (simp add: pcpo_def)
    apply (blast intro: cpo_antisym)
    done

    lemma bot_least [TC]:
        "[| pcpo(D); y ∈ set(D)|] ==> rel(D,bot(D),y)"
    apply (simp add: bot_def)
    apply (best intro: pcpo_bot_ex1 [THEN theI2])
    done

    lemma bot_in [TC]:
        "pcpo(D) ==> bot(D):set(D)"
    apply (simp add: bot_def)
    apply (best intro: pcpo_bot_ex1 [THEN theI2])
    done

    lemma bot_unique:
        "[| pcpo(D); x ∈ set(D); !!y. y ∈ set(D) ==> rel(D,x,y)|] ==> x = bot(D)"
    by (blast intro: cpo_antisym pcpo_cpo bot_in bot_least)

    (*----------------------------------------------------------------------*)
    (* Constant chains and lubs and cpos.                                   *)
    (*----------------------------------------------------------------------*)

    lemma chain_const: "[|x ∈ set(D); cpo(D)|] ==> chain(D,(λn ∈ nat. x))"
    by (simp add: chain_def)

    lemma islub_const:
       "[|x ∈ set(D); cpo(D)|] ==> islub(D,(λn ∈ nat. x),x)"
    by (simp add: islub_def isub_def, blast)

    lemma lub_const: "[|x ∈ set(D); cpo(D)|] ==> lub(D,λn ∈ nat. x) = x"
    by (blast intro: islub_unique cpo_lub chain_const islub_const)

    (*----------------------------------------------------------------------*)
    (* Taking the suffix of chains has no effect on ub's.                   *)
    (*----------------------------------------------------------------------*)

    lemma isub_suffix:
        "[| chain(D,X); cpo(D) |] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)"
    apply (simp add: isub_def suffix_def, safe)
    apply (drule_tac x = na in bspec)
    apply (auto intro: cpo_trans chain_rel_gen_add)
    done

    lemma islub_suffix:
      "[|chain(D,X); cpo(D)|] ==> islub(D,suffix(X,n),x) <-> islub(D,X,x)"
    by (simp add: islub_def isub_suffix)

    lemma lub_suffix:
        "[|chain(D,X); cpo(D)|] ==> lub(D,suffix(X,n)) = lub(D,X)"
    by (simp add: lub_def islub_suffix)

    (*----------------------------------------------------------------------*)
    (* Dominate and subchain.                                               *)
    (*----------------------------------------------------------------------*)

    lemma dominateI:
      "[| !!m. m ∈ nat ==> n(m):nat; !!m. m ∈ nat ==> rel(D,X`m,Y`n(m))|]
       ==> dominate(D,X,Y)"
    by (simp add: dominate_def, blast)

    lemma dominate_isub:
      "[|dominate(D,X,Y); isub(D,Y,x); cpo(D);
         X ∈ nat->set(D); Y ∈ nat->set(D)|] ==> isub(D,X,x)"
    apply (simp add: isub_def dominate_def)
    apply (blast intro: cpo_trans intro!: apply_funtype)
    done

    lemma dominate_islub:
      "[|dominate(D,X,Y); islub(D,X,x); islub(D,Y,y); cpo(D);
         X ∈ nat->set(D); Y ∈ nat->set(D)|] ==> rel(D,x,y)"
    apply (simp add: islub_def)
    apply (blast intro: dominate_isub)
    done

    lemma subchain_isub:
         "[|subchain(Y,X); isub(D,X,x)|] ==> isub(D,Y,x)"
    by (simp add: isub_def subchain_def, force)

    lemma dominate_islub_eq:
         "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);
            X ∈ nat->set(D); Y ∈ nat->set(D)|] ==> x = y"
    by (blast intro: cpo_antisym dominate_islub islub_least subchain_isub
                     islub_isub islub_in)

    (*----------------------------------------------------------------------*)
    (* Matrix.                                                              *)
    (*----------------------------------------------------------------------*)

    lemma matrix_fun: "matrix(D,M) ==> M ∈ nat -> (nat -> set(D))"
    by (simp add: matrix_def)

    lemma matrix_in_fun: "[|matrix(D,M); n ∈ nat|] ==> M`n ∈ nat -> set(D)"
    by (blast intro: apply_funtype matrix_fun)

    lemma matrix_in: "[|matrix(D,M); n ∈ nat; m ∈ nat|] ==> M`n`m ∈ set(D)"
    by (blast intro: apply_funtype matrix_in_fun)

    lemma matrix_rel_1_0:
        "[|matrix(D,M); n ∈ nat; m ∈ nat|] ==> rel(D,M`n`m,M`succ(n)`m)"
    by (simp add: matrix_def)

    lemma matrix_rel_0_1:
        "[|matrix(D,M); n ∈ nat; m ∈ nat|] ==> rel(D,M`n`m,M`n`succ(m))"
    by (simp add: matrix_def)

    lemma matrix_rel_1_1:
        "[|matrix(D,M); n ∈ nat; m ∈ nat|] ==> rel(D,M`n`m,M`succ(n)`succ(m))"
    by (simp add: matrix_def)

    lemma fun_swap: "f ∈ X->Y->Z ==> (λy ∈ Y. λx ∈ X. f`x`y):Y->X->Z"
    by (blast intro: lam_type apply_funtype)

    lemma matrix_sym_axis:
        "matrix(D,M) ==> matrix(D,λm ∈ nat. λn ∈ nat. M`n`m)"
    by (simp add: matrix_def fun_swap)

    lemma matrix_chain_diag:
        "matrix(D,M) ==> chain(D,λn ∈ nat. M`n`n)"
    apply (simp add: chain_def)
    apply (auto intro: lam_type matrix_in matrix_rel_1_1)
    done

    lemma matrix_chain_left:
        "[|matrix(D,M); n ∈ nat|] ==> chain(D,M`n)"
    apply (unfold chain_def)
    apply (auto intro: matrix_fun [THEN apply_type] matrix_in matrix_rel_0_1)
    done

    lemma matrix_chain_right:
        "[|matrix(D,M); m ∈ nat|] ==> chain(D,λn ∈ nat. M`n`m)"
    apply (simp add: chain_def)
    apply (auto intro: lam_type matrix_in matrix_rel_1_0)
    done

    lemma matrix_chainI:
      assumes xprem: "!!x. x ∈ nat==>chain(D,M`x)"
          and yprem: "!!y. y ∈ nat==>chain(D,λx ∈ nat. M`x`y)"
          and Mfun:  "M ∈ nat->nat->set(D)"
          and cpoD:  "cpo(D)"
      shows "matrix(D,M)"
    apply (simp add: matrix_def, safe)
    apply (rule Mfun)
    apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
    apply (simp add: chain_rel xprem)
    apply (rule cpo_trans [OF cpoD])
    apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
    apply (simp_all add: chain_fun [THEN apply_type] xprem)
    done

    lemma lemma_rel_rel:
         "[|m ∈ nat; rel(D, (λn ∈ nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)"
    by simp

    lemma lemma2:
         "[|x ∈ nat; m ∈ nat; rel(D,(λn ∈ nat. M`n`m1)`x,(λn ∈ nat. M`n`m1)`m)|]
          ==> rel(D,M`x`m1,M`m`m1)"
    by simp

    lemma isub_lemma:
        "[|isub(D, λn ∈ nat. M`n`n, y); matrix(D,M); cpo(D)|]
         ==> isub(D, λn ∈ nat. lub(D,λm ∈ nat. M`n`m), y)"
    apply (unfold isub_def, safe)
    apply (simp (no_asm_simp))
    apply (frule matrix_fun [THEN apply_type], assumption)
    apply (simp (no_asm_simp))
    apply (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], assumption+)
    apply (unfold isub_def, safe)
    (*???VERY indirect proof: beta-redexes could be simplified now!*)
    apply (rename_tac k n)
    apply (case_tac "k le n")
    apply (rule cpo_trans, assumption)
    apply (rule lemma2)
    apply (rule_tac [4] lemma_rel_rel)
    prefer 5 apply blast
    apply (assumption | rule chain_rel_gen matrix_chain_right matrix_in isubD1)+
    txt{*opposite case*}
    apply (rule cpo_trans, assumption)
    apply (rule not_le_iff_lt [THEN iffD1, THEN leI, THEN chain_rel_gen])
    prefer 3 apply assumption
    apply (assumption | rule nat_into_Ord matrix_chain_left)+
    apply (rule lemma_rel_rel)
    apply (simp_all add: matrix_in)
    done

    lemma matrix_chain_lub:
        "[|matrix(D,M); cpo(D)|] ==> chain(D,λn ∈ nat. lub(D,λm ∈ nat. M`n`m))"
    apply (simp add: chain_def, safe)
    apply (rule lam_type)
    apply (rule islub_in)
    apply (rule cpo_lub)
    prefer 2 apply assumption
    apply (rule chainI)
    apply (rule lam_type)
    apply (simp_all add: matrix_in)
    apply (rule matrix_rel_0_1, assumption+)
    apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
    apply (rule dominate_islub)
    apply (rule_tac [3] cpo_lub)
    apply (rule_tac [2] cpo_lub)
    apply (simp add: dominate_def)
    apply (blast intro: matrix_rel_1_0)
    apply (simp_all add: matrix_chain_left nat_succI chain_fun)
    done

    lemma isub_eq:
        "[|matrix(D,M); cpo(D)|]
         ==> isub(D,(λn ∈ nat. lub(D,λm ∈ nat. M`n`m)),y) <->
             isub(D,(λn ∈ nat. M`n`n),y)"
    apply (rule iffI)
    apply (rule dominate_isub)
    prefer 2 apply assumption
    apply (simp add: dominate_def)
    apply (rule ballI)
    apply (rule bexI, auto)
    apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
    apply (rule islub_ub)
    apply (rule cpo_lub)
    apply (simp_all add: matrix_chain_left matrix_chain_diag chain_fun
                         matrix_chain_lub isub_lemma)
    done

    lemma lub_matrix_diag_aux1:
        "lub(D,(λn ∈ nat. lub(D,λm ∈ nat. M`n`m))) =
         (THE x. islub(D, (λn ∈ nat. lub(D,λm ∈ nat. M`n`m)), x))"
    by (simp add: lub_def)

    lemma lub_matrix_diag_aux2:
        "lub(D,(λn ∈ nat. M`n`n)) =
         (THE x. islub(D, (λn ∈ nat. M`n`n), x))"
    by (simp add: lub_def)

    lemma lub_matrix_diag:
        "[|matrix(D,M); cpo(D)|]
         ==> lub(D,(λn ∈ nat. lub(D,λm ∈ nat. M`n`m))) =
             lub(D,(λn ∈ nat. M`n`n))"
    apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2)
    apply (simp add: islub_def isub_eq)
    done

    lemma lub_matrix_diag_sym:
        "[|matrix(D,M); cpo(D)|]
         ==> lub(D,(λm ∈ nat. lub(D,λn ∈ nat. M`n`m))) =
             lub(D,(λn ∈ nat. M`n`n))"
    by (drule matrix_sym_axis [THEN lub_matrix_diag], auto)

    (*----------------------------------------------------------------------*)
    (* I/E/D rules for mono and cont.                                       *)
    (*----------------------------------------------------------------------*)

    lemma monoI:
        "[|f ∈ set(D)->set(E);
           !!x y. [|rel(D,x,y); x ∈ set(D); y ∈ set(D)|] ==> rel(E,f`x,f`y)|]
         ==> f ∈ mono(D,E)"
    by (simp add: mono_def)

    lemma mono_fun: "f ∈ mono(D,E) ==> f ∈ set(D)->set(E)"
    by (simp add: mono_def)

    lemma mono_map: "[|f ∈ mono(D,E); x ∈ set(D)|] ==> f`x ∈ set(E)"
    by (blast intro!: mono_fun [THEN apply_type])

    lemma mono_mono:
        "[|f ∈ mono(D,E); rel(D,x,y); x ∈ set(D); y ∈ set(D)|] ==> rel(E,f`x,f`y)"
    by (simp add: mono_def)

    lemma contI:
        "[|f ∈ set(D)->set(E);
           !!x y. [|rel(D,x,y); x ∈ set(D); y ∈ set(D)|] ==> rel(E,f`x,f`y);
           !!X. chain(D,X) ==> f`lub(D,X) = lub(E,λn ∈ nat. f`(X`n))|]
         ==> f ∈ cont(D,E)"
    by (simp add: cont_def mono_def)

    lemma cont2mono: "f ∈ cont(D,E) ==> f ∈ mono(D,E)"
    by (simp add: cont_def)

    lemma cont_fun [TC] : "f ∈ cont(D,E) ==> f ∈ set(D)->set(E)"
    apply (simp add: cont_def)
    apply (rule mono_fun, blast)
    done

    lemma cont_map [TC]: "[|f ∈ cont(D,E); x ∈ set(D)|] ==> f`x ∈ set(E)"
    by (blast intro!: cont_fun [THEN apply_type])

    declare comp_fun [TC]

    lemma cont_mono:
        "[|f ∈ cont(D,E); rel(D,x,y); x ∈ set(D); y ∈ set(D)|] ==> rel(E,f`x,f`y)"
    apply (simp add: cont_def)
    apply (blast intro!: mono_mono)
    done

    lemma cont_lub:
       "[|f ∈ cont(D,E); chain(D,X)|] ==> f`(lub(D,X)) = lub(E,λn ∈ nat. f`(X`n))"
    by (simp add: cont_def)

    (*----------------------------------------------------------------------*)
    (* Continuity and chains.                                               *)
    (*----------------------------------------------------------------------*)

    lemma mono_chain:
         "[|f ∈ mono(D,E); chain(D,X)|] ==> chain(E,λn ∈ nat. f`(X`n))"
    apply (simp (no_asm) add: chain_def)
    apply (blast intro: lam_type mono_map chain_in mono_mono chain_rel)
    done

    lemma cont_chain:
         "[|f ∈ cont(D,E); chain(D,X)|] ==> chain(E,λn ∈ nat. f`(X`n))"
    by (blast intro: mono_chain cont2mono)

    (*----------------------------------------------------------------------*)
    (* I/E/D rules about (set+rel) cf, the continuous function space.       *)
    (*----------------------------------------------------------------------*)

    (* The following development more difficult with cpo-as-relation approach. *)

    lemma cf_cont: "f ∈ set(cf(D,E)) ==> f ∈ cont(D,E)"
    by (simp add: set_def cf_def)

    lemma cont_cf: (* Non-trivial with relation *)
        "f ∈ cont(D,E) ==> f ∈ set(cf(D,E))"
    by (simp add: set_def cf_def)

    (* rel_cf originally an equality. Now stated as two rules. Seemed easiest. *)

    lemma rel_cfI:
        "[|!!x. x ∈ set(D) ==> rel(E,f`x,g`x); f ∈ cont(D,E); g ∈ cont(D,E)|]
         ==> rel(cf(D,E),f,g)"
    by (simp add: rel_I cf_def)

    lemma rel_cf: "[|rel(cf(D,E),f,g); x ∈ set(D)|] ==> rel(E,f`x,g`x)"
    by (simp add: rel_def cf_def)

    (*----------------------------------------------------------------------*)
    (* Theorems about the continuous function space.                        *)
    (*----------------------------------------------------------------------*)

    lemma chain_cf:
        "[| chain(cf(D,E),X); x ∈ set(D)|] ==> chain(E,λn ∈ nat. X`n`x)"
    apply (rule chainI)
    apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
    apply (blast intro: rel_cf chain_rel)
    done

    lemma matrix_lemma:
        "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |]
         ==> matrix(E,λx ∈ nat. λxa ∈ nat. X`x`(Xa`xa))"
    apply (rule matrix_chainI, auto)
    apply (rule chainI)
    apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
    apply (blast intro: cont_mono nat_succI chain_rel cf_cont chain_in)
    apply (rule chainI)
    apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
    apply (rule rel_cf)
    apply (simp_all add: chain_in chain_rel)
    apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in)
    done

    lemma chain_cf_lub_cont:
        "[|chain(cf(D,E),X); cpo(D); cpo(E) |]
         ==> (λx ∈ set(D). lub(E, λn ∈ nat. X ` n ` x)) ∈ cont(D, E)"
    apply (rule contI)
    apply (rule lam_type)
    apply (assumption | rule chain_cf [THEN cpo_lub, THEN islub_in])+
    apply simp
    apply (rule dominate_islub)
    apply (erule_tac [2] chain_cf [THEN cpo_lub], simp_all)+
    apply (rule dominateI, assumption, simp)
    apply (assumption | rule chain_in [THEN cf_cont, THEN cont_mono])+
    apply (assumption | rule chain_cf [THEN chain_fun])+
    apply (simp add: cpo_lub [THEN islub_in]
                     chain_in [THEN cf_cont, THEN cont_lub])
    apply (frule matrix_lemma [THEN lub_matrix_diag], assumption+)
    apply (simp add: chain_in [THEN beta])
    apply (drule matrix_lemma [THEN lub_matrix_diag_sym], auto)
    done

    lemma islub_cf:
        "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
         ==> islub(cf(D,E), X, λx ∈ set(D). lub(E,λn ∈ nat. X`n`x))"
    apply (rule islubI)
    apply (rule isubI)
    apply (rule chain_cf_lub_cont [THEN cont_cf], assumption+)
    apply (rule rel_cfI)
    apply (force dest!: chain_cf [THEN cpo_lub, THEN islub_ub])
    apply (blast intro: cf_cont chain_in)
    apply (blast intro: cont_cf chain_cf_lub_cont)
    apply (rule rel_cfI, simp)
    apply (force intro: chain_cf [THEN cpo_lub, THEN islub_least]
                       cf_cont [THEN cont_fun, THEN apply_type] isubI
                elim: isubD2 [THEN rel_cf] isubD1)
    apply (blast intro: chain_cf_lub_cont isubD1 cf_cont)+
    done

    lemma cpo_cf [TC]:
        "[| cpo(D); cpo(E)|] ==> cpo(cf(D,E))"
    apply (rule poI [THEN cpoI])
    apply (rule rel_cfI)
    apply (assumption | rule cpo_refl cf_cont [THEN cont_fun, THEN apply_type]
                             cf_cont)+
    apply (rule rel_cfI)
    apply (rule cpo_trans, assumption)
    apply (erule rel_cf, assumption)
    apply (rule rel_cf, assumption)
    apply (assumption | rule cf_cont [THEN cont_fun, THEN apply_type] cf_cont)+
    apply (rule fun_extension)
    apply (assumption | rule cf_cont [THEN cont_fun])+
    apply (blast intro: cpo_antisym rel_cf
                        cf_cont [THEN cont_fun, THEN apply_type])
    apply (fast intro: islub_cf)
    done

    lemma lub_cf:
         "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
          ==> lub(cf(D,E), X) = (λx ∈ set(D). lub(E,λn ∈ nat. X`n`x))"
    by (blast intro: islub_unique cpo_lub islub_cf cpo_cf)

    lemma const_cont [TC]:
         "[|y ∈ set(E); cpo(D); cpo(E)|] ==> (λx ∈ set(D).y) ∈ cont(D,E)"
    apply (rule contI)
    prefer 2 apply simp
    apply (blast intro: lam_type)
    apply (simp add: chain_in cpo_lub [THEN islub_in] lub_const)
    done

    lemma cf_least:
        "[|cpo(D); pcpo(E); y ∈ cont(D,E)|]==>rel(cf(D,E),(λx ∈ set(D).bot(E)),y)"
    apply (rule rel_cfI, simp, typecheck)
    done

    lemma pcpo_cf:
        "[|cpo(D); pcpo(E)|] ==> pcpo(cf(D,E))"
    apply (rule pcpoI)
    apply (assumption |
           rule cf_least bot_in const_cont [THEN cont_cf] cf_cont cpo_cf pcpo_cpo)+
    done

    lemma bot_cf:
        "[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (λx ∈ set(D).bot(E))"
    by (blast intro: bot_unique [symmetric] pcpo_cf cf_least
                     bot_in [THEN const_cont, THEN cont_cf] cf_cont pcpo_cpo)

    (*----------------------------------------------------------------------*)
    (* Identity and composition.                                            *)
    (*----------------------------------------------------------------------*)

    lemma id_cont [TC,intro!]:
        "cpo(D) ==> id(set(D)) ∈ cont(D,D)"
    by (simp add: id_type contI cpo_lub [THEN islub_in] chain_fun [THEN eta])

    lemmas comp_cont_apply =  cont_fun [THEN comp_fun_apply]

    lemma comp_pres_cont [TC]:
        "[| f ∈ cont(D',E); g ∈ cont(D,D'); cpo(D)|] ==> f O g ∈ cont(D,E)"
    apply (rule contI)
    apply (rule_tac [2] comp_cont_apply [THEN ssubst])
    apply (rule_tac [4] comp_cont_apply [THEN ssubst])
    apply (rule_tac [6] cont_mono)
    apply (rule_tac [7] cont_mono) (* 13 subgoals *)
    apply typecheck (* proves all but the lub case *)
    apply (subst comp_cont_apply)
    apply (rule_tac [3] cont_lub [THEN ssubst])
    apply (rule_tac [5] cont_lub [THEN ssubst])
    prefer 7 apply (simp add: comp_cont_apply chain_in)
    apply (auto intro: cpo_lub [THEN islub_in] cont_chain)
    done

    lemma comp_mono:
        "[| f ∈ cont(D',E); g ∈ cont(D,D'); f':cont(D',E); g':cont(D,D');
            rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |]
         ==> rel(cf(D,E),f O g,f' O g')"
    apply (rule rel_cfI)
    apply (subst comp_cont_apply)
    apply (rule_tac [3] comp_cont_apply [THEN ssubst])
    apply (rule_tac [5] cpo_trans)
    apply (assumption | rule rel_cf cont_mono cont_map comp_pres_cont)+
    done

    lemma chain_cf_comp:
        "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|]
         ==> chain(cf(D,E),λn ∈ nat. X`n O Y`n)"
    apply (rule chainI)
    defer 1
    apply simp
    apply (rule rel_cfI)
    apply (rule comp_cont_apply [THEN ssubst])
    apply (rule_tac [3] comp_cont_apply [THEN ssubst])
    apply (rule_tac [5] cpo_trans)
    apply (rule_tac [6] rel_cf)
    apply (rule_tac [8] cont_mono)
    apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont]
                        cont_map chain_rel rel_cf)+
    done

    lemma comp_lubs:
        "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|]
         ==> lub(cf(D',E),X) O lub(cf(D,D'),Y) = lub(cf(D,E),λn ∈ nat. X`n O Y`n)"
    apply (rule fun_extension)
    apply (rule_tac [3] lub_cf [THEN ssubst])
    apply (assumption |
           rule comp_fun cf_cont [THEN cont_fun]  cpo_lub [THEN islub_in]
                cpo_cf chain_cf_comp)+
    apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply])
    apply (subst comp_cont_apply)
    apply (assumption | rule cpo_lub [THEN islub_in, THEN cf_cont]  cpo_cf)+
    apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub]
                     chain_cf [THEN cpo_lub, THEN islub_in])
    apply (cut_tac M = "λxa ∈ nat. λxb ∈ nat. X`xa` (Y`xb`x)" in lub_matrix_diag)
    prefer 3 apply simp
    apply (rule matrix_chainI, simp_all)
    apply (drule chain_in [THEN cf_cont], assumption)
    apply (force dest: cont_chain [OF _ chain_cf])
    apply (rule chain_cf)
    apply (assumption |
           rule cont_fun [THEN apply_type] chain_in [THEN cf_cont] lam_type)+
    done

    (*----------------------------------------------------------------------*)
    (* Theorems about projpair.                                             *)
    (*----------------------------------------------------------------------*)

    lemma projpairI:
        "[| e ∈ cont(D,E); p ∈ cont(E,D); p O e = id(set(D));
            rel(cf(E,E))(e O p)(id(set(E)))|] ==> projpair(D,E,e,p)"
    by (simp add: projpair_def)

    lemma projpair_e_cont: "projpair(D,E,e,p) ==> e ∈ cont(D,E)"
    by (simp add: projpair_def)

    lemma projpair_p_cont: "projpair(D,E,e,p) ==> p ∈ cont(E,D)"
    by (simp add: projpair_def)

    lemma projpair_ep_cont: "projpair(D,E,e,p) ==> e ∈ cont(D,E) & p ∈ cont(E,D)"
    by (simp add: projpair_def)

    lemma projpair_eq: "projpair(D,E,e,p) ==> p O e = id(set(D))"
    by (simp add: projpair_def)

    lemma projpair_rel: "projpair(D,E,e,p) ==> rel(cf(E,E))(e O p)(id(set(E)))"
    by (simp add: projpair_def)

    (*----------------------------------------------------------------------*)
    (* NB! projpair_e_cont and projpair_p_cont cannot be used repeatedly    *)
    (*   at the same time since both match a goal of the form f ∈ cont(X,Y).*)
    (*----------------------------------------------------------------------*)

    (*----------------------------------------------------------------------*)
    (* Uniqueness of embedding projection pairs.                            *)
    (*----------------------------------------------------------------------*)

    lemmas id_comp = fun_is_rel [THEN left_comp_id]
    and    comp_id = fun_is_rel [THEN right_comp_id]

    lemma projpair_unique_aux1:
        "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
           rel(cf(D,E),e,e')|] ==> rel(cf(E,D),p',p)"
    apply (rule_tac b=p' in
           projpair_p_cont [THEN cont_fun, THEN id_comp, THEN subst], assumption)
    apply (rule projpair_eq [THEN subst], assumption)
    apply (rule cpo_trans)
    apply (assumption | rule cpo_cf)+
    (* The following corresponds to EXISTS_TAC, non-trivial instantiation. *)
    apply (rule_tac [4] f = "p O (e' O p')" in cont_cf)
    apply (subst comp_assoc)
    apply (blast intro:  cpo_cf cont_cf comp_mono comp_pres_cont
                 dest: projpair_ep_cont)
    apply (rule_tac P = "%x. rel (cf (E,D),p O e' O p',x)"
             in projpair_p_cont [THEN cont_fun, THEN comp_id, THEN subst],
           assumption)
    apply (rule comp_mono)
    apply (blast intro: cpo_cf cont_cf comp_pres_cont projpair_rel
                 dest: projpair_ep_cont)+
    done

    text{*Proof's very like the previous one.  Is there a pattern that
          could be exploited?*}
    lemma projpair_unique_aux2:
        "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
           rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')"
    apply (rule_tac b=e
             in projpair_e_cont [THEN cont_fun, THEN comp_id, THEN subst],
           assumption)
    apply (rule_tac e1=e' in projpair_eq [THEN subst], assumption)
    apply (rule cpo_trans)
    apply (assumption | rule cpo_cf)+
    apply (rule_tac [4] f = "(e O p) O e'" in cont_cf)
    apply (subst comp_assoc)
    apply (blast intro:  cpo_cf cont_cf comp_mono comp_pres_cont
                 dest: projpair_ep_cont)
    apply (rule_tac P = "%x. rel (cf (D,E), (e O p) O e',x)"
             in projpair_e_cont [THEN cont_fun, THEN id_comp, THEN subst],
           assumption)
    apply (blast intro: cpo_cf cont_cf comp_pres_cont projpair_rel comp_mono
                 dest: projpair_ep_cont)+
    done

    lemma projpair_unique:
        "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|]
         ==> (e=e')<->(p=p')"
    by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf
              dest: projpair_ep_cont)

    (* Slightly different, more asms, since THE chooses the unique element. *)

    lemma embRp:
        "[|emb(D,E,e); cpo(D); cpo(E)|] ==> projpair(D,E,e,Rp(D,E,e))"
    apply (simp add: emb_def Rp_def)
    apply (blast intro: theI2 projpair_unique [THEN iffD1])
    done

    lemma embI: "projpair(D,E,e,p) ==> emb(D,E,e)"
    by (simp add: emb_def, auto)

    lemma Rp_unique: "[|projpair(D,E,e,p); cpo(D); cpo(E)|] ==> Rp(D,E,e) = p"
    by (blast intro: embRp embI projpair_unique [THEN iffD1])

    lemma emb_cont [TC]: "emb(D,E,e) ==> e ∈ cont(D,E)"
    apply (simp add: emb_def)
    apply (blast intro: projpair_e_cont)
    done

    (* The following three theorems have cpo asms due to THE (uniqueness). *)

    lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont, standard]
    lemmas embRp_eq = embRp [THEN projpair_eq, standard]
    lemmas embRp_rel = embRp [THEN projpair_rel, standard]

    lemma embRp_eq_thm:
        "[|emb(D,E,e); x ∈ set(D); cpo(D); cpo(E)|] ==> Rp(D,E,e)`(e`x) = x"
    apply (rule comp_fun_apply [THEN subst])
    apply (assumption | rule Rp_cont emb_cont cont_fun)+
    apply (subst embRp_eq)
    apply (auto intro: id_conv)
    done

    (*----------------------------------------------------------------------*)
    (* The identity embedding.                                              *)
    (*----------------------------------------------------------------------*)

    lemma projpair_id:
        "cpo(D) ==> projpair(D,D,id(set(D)),id(set(D)))"
    apply (simp add: projpair_def)
    apply (blast intro: cpo_cf cont_cf)
    done

    lemma emb_id:
        "cpo(D) ==> emb(D,D,id(set(D)))"
    by (auto intro: embI projpair_id)

    lemma Rp_id:
        "cpo(D) ==> Rp(D,D,id(set(D))) = id(set(D))"
    by (auto intro: Rp_unique projpair_id)

    (*----------------------------------------------------------------------*)
    (* Composition preserves embeddings.                                    *)
    (*----------------------------------------------------------------------*)

    (* Considerably shorter, only partly due to a simpler comp_assoc. *)
    (* Proof in HOL-ST: 70 lines (minus 14 due to comp_assoc complication). *)
    (* Proof in Isa/ZF: 23 lines (compared to 56: 60% reduction). *)

    lemma comp_lemma:
        "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|]
         ==> projpair(D,E,e' O e,(Rp(D,D',e)) O (Rp(D',E,e')))"
    apply (simp add: projpair_def, safe)
    apply (assumption | rule comp_pres_cont Rp_cont emb_cont)+
    apply (rule comp_assoc [THEN subst])
    apply (rule_tac t1 = e' in comp_assoc [THEN ssubst])
    apply (subst embRp_eq) (* Matches everything due to subst/ssubst. *)
    apply assumption+
    apply (subst comp_id)
    apply (assumption | rule cont_fun Rp_cont embRp_eq)+
    apply (rule comp_assoc [THEN subst])
    apply (rule_tac t1 = "Rp (D,D',e)" in comp_assoc [THEN ssubst])
    apply (rule cpo_trans)
    apply (assumption | rule cpo_cf)+
    apply (rule comp_mono)
    apply (rule_tac [6] cpo_refl)
    apply (erule_tac [7] asm_rl | rule_tac [7] cont_cf Rp_cont)+
    prefer 6 apply (blast intro: cpo_cf)
    apply (rule_tac [5] comp_mono)
    apply (rule_tac [10] embRp_rel)
    apply (rule_tac [9] cpo_cf [THEN cpo_refl])
    apply (simp_all add: comp_id embRp_rel comp_pres_cont Rp_cont
                         id_cont emb_cont cont_fun cont_cf)
    done

    (* The use of THEN is great in places like the following, both ugly in HOL. *)

    lemmas emb_comp = comp_lemma [THEN embI]
    lemmas Rp_comp = comp_lemma [THEN Rp_unique]

    (*----------------------------------------------------------------------*)
    (* Infinite cartesian product.                                          *)
    (*----------------------------------------------------------------------*)

    lemma iprodI:
        "x:(Π n ∈ nat. set(DD`n)) ==> x ∈ set(iprod(DD))"
    by (simp add: set_def iprod_def)

    lemma iprodE:
        "x ∈ set(iprod(DD)) ==> x:(Π n ∈ nat. set(DD`n))"
    by (simp add: set_def iprod_def)

    (* Contains typing conditions in contrast to HOL-ST *)

    lemma rel_iprodI:
        "[|!!n. n ∈ nat ==> rel(DD`n,f`n,g`n); f:(Π n ∈ nat. set(DD`n));
           g:(Π n ∈ nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
    by (simp add: iprod_def rel_I)

    lemma rel_iprodE:
        "[|rel(iprod(DD),f,g); n ∈ nat|] ==> rel(DD`n,f`n,g`n)"
    by (simp add: iprod_def rel_def)

    lemma chain_iprod:
        "[|chain(iprod(DD),X);  !!n. n ∈ nat ==> cpo(DD`n); n ∈ nat|]
         ==> chain(DD`n,λm ∈ nat. X`m`n)"
    apply (unfold chain_def, safe)
    apply (rule lam_type)
    apply (rule apply_type)
    apply (rule iprodE)
    apply (blast intro: apply_funtype, assumption)
    apply (simp add: rel_iprodE)
    done

    lemma islub_iprod:
        "[|chain(iprod(DD),X);  !!n. n ∈ nat ==> cpo(DD`n)|]
         ==> islub(iprod(DD),X,λn ∈ nat. lub(DD`n,λm ∈ nat. X`m`n))"
    apply (simp add: islub_def isub_def, safe)
    apply (rule iprodI)
    apply (blast intro: lam_type chain_iprod [THEN cpo_lub, THEN islub_in])
    apply (rule rel_iprodI, simp)
    (*looks like something should be inserted into the assumptions!*)
    apply (rule_tac P = "%t. rel (DD`na,t,lub (DD`na,λx ∈ nat. X`x`na))"
                and b1 = "%n. X`n`na" in beta [THEN subst])
    apply (simp del: beta_if
                add: chain_iprod [THEN cpo_lub, THEN islub_ub] iprodE
                    chain_in)+
    apply (blast intro: iprodI lam_type chain_iprod [THEN cpo_lub, THEN islub_in])
    apply (rule rel_iprodI)
    apply (simp | rule islub_least chain_iprod [THEN cpo_lub])+
    apply (simp add: isub_def, safe)
    apply (erule iprodE [THEN apply_type])
    apply (simp_all add: rel_iprodE lam_type iprodE
                         chain_iprod [THEN cpo_lub, THEN islub_in])
    done

    lemma cpo_iprod [TC]:
        "(!!n. n ∈ nat ==> cpo(DD`n)) ==> cpo(iprod(DD))"
    apply (assumption | rule cpoI poI)+
    apply (rule rel_iprodI) (*not repeated: want to solve 1, leave 2 unchanged *)
    apply (simp | rule cpo_refl iprodE [THEN apply_type] iprodE)+
    apply (rule rel_iprodI)
    apply (drule rel_iprodE)
    apply (drule_tac [2] rel_iprodE)
    apply (simp | rule cpo_trans iprodE [THEN apply_type] iprodE)+
    apply (rule fun_extension)
    apply (blast intro: iprodE)
    apply (blast intro: iprodE)
    apply (blast intro: cpo_antisym rel_iprodE iprodE [THEN apply_type])+
    apply (auto intro: islub_iprod)
    done

    lemma lub_iprod:
        "[|chain(iprod(DD),X);  !!n. n ∈ nat ==> cpo(DD`n)|]
         ==> lub(iprod(DD),X) = (λn ∈ nat. lub(DD`n,λm ∈ nat. X`m`n))"
    by (blast intro: cpo_lub [THEN islub_unique] islub_iprod cpo_iprod)

    (*----------------------------------------------------------------------*)
    (* The notion of subcpo.                                                *)
    (*----------------------------------------------------------------------*)

    lemma subcpoI:
        "[|set(D)<=set(E);
           !!x y. [|x ∈ set(D); y ∈ set(D)|] ==> rel(D,x,y)<->rel(E,x,y);
           !!X. chain(D,X) ==> lub(E,X) ∈ set(D)|] ==> subcpo(D,E)"
    by (simp add: subcpo_def)

    lemma subcpo_subset: "subcpo(D,E) ==> set(D)<=set(E)"
    by (simp add: subcpo_def)

    lemma subcpo_rel_eq:
        "[|subcpo(D,E); x ∈ set(D); y ∈ set(D)|] ==> rel(D,x,y)<->rel(E,x,y)"
    by (simp add: subcpo_def)

    lemmas subcpo_relD1 = subcpo_rel_eq [THEN iffD1]
    lemmas subcpo_relD2 = subcpo_rel_eq [THEN iffD2]

    lemma subcpo_lub: "[|subcpo(D,E); chain(D,X)|] ==> lub(E,X) ∈ set(D)"
    by (simp add: subcpo_def)

    lemma chain_subcpo: "[|subcpo(D,E); chain(D,X)|] ==> chain(E,X)"
    by (blast intro: Pi_type [THEN chainI] chain_fun subcpo_relD1
                        subcpo_subset [THEN subsetD]
                        chain_in chain_rel)

    lemma ub_subcpo: "[|subcpo(D,E); chain(D,X); isub(D,X,x)|] ==> isub(E,X,x)"
    by (blast intro: isubI subcpo_relD1 subcpo_relD1 chain_in isubD1 isubD2
                        subcpo_subset [THEN subsetD] chain_in chain_rel)

    lemma islub_subcpo:
         "[|subcpo(D,E); cpo(E); chain(D,X)|] ==> islub(D,X,lub(E,X))"
    by (blast intro: islubI isubI subcpo_lub subcpo_relD2 chain_in islub_ub
                     islub_least cpo_lub chain_subcpo isubD1 ub_subcpo)

    lemma subcpo_cpo: "[|subcpo(D,E); cpo(E)|] ==> cpo(D)"
    apply (assumption | rule cpoI poI)+
    apply (simp add: subcpo_rel_eq)
    apply (assumption | rule cpo_refl subcpo_subset [THEN subsetD])+
    apply (simp add: subcpo_rel_eq)
    apply (blast intro: subcpo_subset [THEN subsetD] cpo_trans)
    apply (simp add: subcpo_rel_eq)
    apply (blast intro: cpo_antisym subcpo_subset [THEN subsetD])
    apply (fast intro: islub_subcpo)
    done

    lemma lub_subcpo: "[|subcpo(D,E); cpo(E); chain(D,X)|] ==> lub(D,X) = lub(E,X)"
    by (blast intro: cpo_lub [THEN islub_unique] islub_subcpo subcpo_cpo)

    (*----------------------------------------------------------------------*)
    (* Making subcpos using mkcpo.                                          *)
    (*----------------------------------------------------------------------*)

    lemma mkcpoI: "[|x ∈ set(D); P(x)|] ==> x ∈ set(mkcpo(D,P))"
    by (simp add: set_def mkcpo_def)

    lemma mkcpoD1: "x ∈ set(mkcpo(D,P))==> x ∈ set(D)"
    by (simp add: set_def mkcpo_def)

    lemma mkcpoD2: "x ∈ set(mkcpo(D,P))==> P(x)"
    by (simp add: set_def mkcpo_def)

    lemma rel_mkcpoE: "rel(mkcpo(D,P),x,y) ==> rel(D,x,y)"
    by (simp add: rel_def mkcpo_def)

    lemma rel_mkcpo:
        "[|x ∈ set(D); y ∈ set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)"
    by (simp add: mkcpo_def rel_def set_def)

    lemma chain_mkcpo:
        "chain(mkcpo(D,P),X) ==> chain(D,X)"
    apply (rule chainI)
    apply (blast intro: Pi_type chain_fun chain_in [THEN mkcpoD1])
    apply (blast intro: rel_mkcpo [THEN iffD1] chain_rel mkcpoD1 chain_in)
    done

    lemma subcpo_mkcpo:
         "[|!!X. chain(mkcpo(D,P),X) ==> P(lub(D,X)); cpo(D)|]
          ==> subcpo(mkcpo(D,P),D)"
    apply (intro subcpoI subsetI rel_mkcpo)
    apply (erule mkcpoD1)+
    apply (blast intro: mkcpoI cpo_lub [THEN islub_in] chain_mkcpo)
    done

    (*----------------------------------------------------------------------*)
    (* Embedding projection chains of cpos.                                 *)
    (*----------------------------------------------------------------------*)

    lemma emb_chainI:
        "[|!!n. n ∈ nat ==> cpo(DD`n);
           !!n. n ∈ nat ==> emb(DD`n,DD`succ(n),ee`n)|] ==> emb_chain(DD,ee)"
    by (simp add: emb_chain_def)

    lemma emb_chain_cpo [TC]: "[|emb_chain(DD,ee); n ∈ nat|] ==> cpo(DD`n)"
    by (simp add: emb_chain_def)

    lemma emb_chain_emb:
        "[|emb_chain(DD,ee); n ∈ nat|] ==> emb(DD`n,DD`succ(n),ee`n)"
    by (simp add: emb_chain_def)

    (*----------------------------------------------------------------------*)
    (* Dinf, the inverse Limit.                                             *)
    (*----------------------------------------------------------------------*)

    lemma DinfI:
        "[|x:(Π n ∈ nat. set(DD`n));
           !!n. n ∈ nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
         ==> x ∈ set(Dinf(DD,ee))"
    apply (simp add: Dinf_def)
    apply (blast intro: mkcpoI iprodI)
    done

    lemma Dinf_prod: "x ∈ set(Dinf(DD,ee)) ==> x:(Π n ∈ nat. set(DD`n))"
    apply (simp add: Dinf_def)
    apply (erule mkcpoD1 [THEN iprodE])
    done

    lemma Dinf_eq:
        "[|x ∈ set(Dinf(DD,ee)); n ∈ nat|]
         ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n"
    apply (simp add: Dinf_def)
    apply (blast dest: mkcpoD2)
    done

    lemma rel_DinfI:
        "[|!!n. n ∈ nat ==> rel(DD`n,x`n,y`n);
           x:(Π n ∈ nat. set(DD`n)); y:(Π n ∈ nat. set(DD`n))|]
         ==> rel(Dinf(DD,ee),x,y)"
    apply (simp add: Dinf_def)
    apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)
    done

    lemma rel_Dinf: "[|rel(Dinf(DD,ee),x,y); n ∈ nat|] ==> rel(DD`n,x`n,y`n)"
    apply (simp add: Dinf_def)
    apply (erule rel_mkcpoE [THEN rel_iprodE], assumption)
    done

    lemma chain_Dinf: "chain(Dinf(DD,ee),X) ==> chain(iprod(DD),X)"
    apply (simp add: Dinf_def)
    apply (erule chain_mkcpo)
    done

    lemma subcpo_Dinf: "emb_chain(DD,ee) ==> subcpo(Dinf(DD,ee),iprod(DD))"
    apply (simp add: Dinf_def)
    apply (rule subcpo_mkcpo)
    apply (simp add: Dinf_def [symmetric])
    apply (rule ballI)
    apply (simplesubst lub_iprod)
      --{*Subst would rewrite the lhs. We want to change the rhs.*}
    apply (assumption | rule chain_Dinf emb_chain_cpo)+
    apply simp
    apply (subst Rp_cont [THEN cont_lub])
    apply (assumption |
           rule emb_chain_cpo emb_chain_emb nat_succI chain_iprod chain_Dinf)+
    (* Useful simplification, ugly in HOL. *)
    apply (simp add: Dinf_eq chain_in)
    apply (auto intro: cpo_iprod emb_chain_cpo)
    done

    (* Simple example of existential reasoning in Isabelle versus HOL. *)

    lemma cpo_Dinf: "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))"
    apply (rule subcpo_cpo)
    apply (erule subcpo_Dinf)
    apply (auto intro: cpo_iprod emb_chain_cpo)
    done

    (* Again and again the proofs are much easier to WRITE in Isabelle, but
      the proof steps are essentially the same (I think). *)

    lemma lub_Dinf:
        "[|chain(Dinf(DD,ee),X); emb_chain(DD,ee)|]
         ==> lub(Dinf(DD,ee),X) = (λn ∈ nat. lub(DD`n,λm ∈ nat. X`m`n))"
    apply (subst subcpo_Dinf [THEN lub_subcpo])
    apply (auto intro: cpo_iprod emb_chain_cpo lub_iprod chain_Dinf)
    done

    (*----------------------------------------------------------------------*)
    (* Generalising embedddings D_m -> D_{m+1} to embeddings D_m -> D_n,    *)
    (* defined as eps(DD,ee,m,n), via e_less and e_gr.                      *)
    (*----------------------------------------------------------------------*)

    lemma e_less_eq:
        "m ∈ nat ==> e_less(DD,ee,m,m) = id(set(DD`m))"
    by (simp add: e_less_def)

    lemma lemma_succ_sub: "succ(m#+n)#-m = succ(natify(n))"
    by simp

    lemma e_less_add:
         "e_less(DD,ee,m,succ(m#+k)) = (ee`(m#+k))O(e_less(DD,ee,m,m#+k))"
    by (simp add: e_less_def)

    lemma le_exists:
        "[| m le n;  !!x. [|n=m#+x; x ∈ nat|] ==> Q;  n ∈ nat |] ==> Q"
    apply (drule less_imp_succ_add, auto)
    done

    lemma e_less_le: "[| m le n;  n ∈ nat |]
         ==> e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)"
    apply (rule le_exists, assumption)
    apply (simp add: e_less_add, assumption)
    done

    (* All theorems assume variables m and n are natural numbers. *)

    lemma e_less_succ:
         "m ∈ nat ==> e_less(DD,ee,m,succ(m)) = ee`m O id(set(DD`m))"
    by (simp add: e_less_le e_less_eq)

    lemma e_less_succ_emb:
        "[|!!n. n ∈ nat ==> emb(DD`n,DD`succ(n),ee`n); m ∈ nat|]
         ==> e_less(DD,ee,m,succ(m)) = ee`m"
    apply (simp add: e_less_succ)
    apply (blast intro: emb_cont cont_fun comp_id)
    done

    (* Compare this proof with the HOL one, here we do type checking. *)
    (* In any case the one below was very easy to write. *)

    lemma emb_e_less_add:
         "[| emb_chain(DD,ee); m ∈ nat |]
          ==> emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))"
    apply (subgoal_tac "emb (DD`m, DD` (m#+natify (k)),
                             e_less (DD,ee,m,m#+natify (k))) ")
    apply (rule_tac [2] n = "natify (k) " in nat_induct)
    apply (simp_all add: e_less_eq)
    apply (assumption | rule emb_id emb_chain_cpo)+
    apply (simp add: e_less_add)
    apply (auto intro: emb_comp emb_chain_emb emb_chain_cpo)
    done

    lemma emb_e_less:
         "[| m le n;  emb_chain(DD,ee);  n ∈ nat |]
          ==> emb(DD`m, DD`n, e_less(DD,ee,m,n))"
    apply (frule lt_nat_in_nat)
    apply (erule nat_succI)
    (* same proof as e_less_le *)
    apply (rule le_exists, assumption)
    apply (simp add: emb_e_less_add, assumption)
    done

    lemma comp_mono_eq: "[|f=f'; g=g'|] ==> f O g = f' O g'"
    by simp

    (* Note the object-level implication for induction on k. This
       must be removed later to allow the theorems to be used for simp.
       Therefore this theorem is only a lemma. *)

    lemma e_less_split_add_lemma [rule_format]:
        "[| emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> n le k -->
             e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
    apply (induct_tac k)
    apply (simp add: e_less_eq id_type [THEN id_comp])
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (erule impE, assumption)
    apply (simp add: e_less_add)
    apply (subst e_less_le)
    apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+
    apply (subst comp_assoc)
    apply (assumption | rule comp_mono_eq refl)+
    apply (simp del: add_succ_right add: add_succ_right [symmetric]
                add: e_less_eq add_type nat_succI)
    apply (subst id_comp) (* simp cannot unify/inst right, use brr below (?) . *)
    apply (assumption |
           rule emb_e_less_add [THEN emb_cont, THEN cont_fun] refl nat_succI)+
    done

    lemma e_less_split_add:
        "[| n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
    by (blast intro: e_less_split_add_lemma)

    lemma e_gr_eq:
        "m ∈ nat ==> e_gr(DD,ee,m,m) = id(set(DD`m))"
    by (simp add: e_gr_def)

    lemma e_gr_add:
        "[|n ∈ nat; k ∈ nat|]
         ==> e_gr(DD,ee,succ(n#+k),n) =
             e_gr(DD,ee,n#+k,n) O Rp(DD`(n#+k),DD`succ(n#+k),ee`(n#+k))"
    by (simp add: e_gr_def)

    lemma e_gr_le:
         "[|n le m; m ∈ nat; n ∈ nat|]
          ==> e_gr(DD,ee,succ(m),n) = e_gr(DD,ee,m,n) O Rp(DD`m,DD`succ(m),ee`m)"
    apply (erule le_exists)
    apply (simp add: e_gr_add, assumption+)
    done

    lemma e_gr_succ:
     "m ∈ nat ==> e_gr(DD,ee,succ(m),m) = id(set(DD`m)) O Rp(DD`m,DD`succ(m),ee`m)"
    by (simp add: e_gr_le e_gr_eq)

    (* Cpo asm's due to THE uniqueness. *)
    lemma e_gr_succ_emb: "[|emb_chain(DD,ee); m ∈ nat|]
         ==> e_gr(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)"
    apply (simp add: e_gr_succ)
    apply (blast intro: id_comp Rp_cont cont_fun emb_chain_cpo emb_chain_emb)
    done

    lemma e_gr_fun_add:
        "[|emb_chain(DD,ee); n ∈ nat; k ∈ nat|]
         ==> e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)"
    apply (induct_tac k)
    apply (simp add: e_gr_eq id_type)
    apply (simp add: e_gr_add)
    apply (blast intro: comp_fun Rp_cont cont_fun emb_chain_emb emb_chain_cpo)
    done

    lemma e_gr_fun:
        "[|n le m; emb_chain(DD,ee); m ∈ nat; n ∈ nat|]
         ==> e_gr(DD,ee,m,n): set(DD`m)->set(DD`n)"
    apply (rule le_exists, assumption)
    apply (simp add: e_gr_fun_add, assumption+)
    done

    lemma e_gr_split_add_lemma:
        "[| emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> m le k -->
             e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
    apply (induct_tac k)
    apply (rule impI)
    apply (simp add: le0_iff e_gr_eq id_type [THEN comp_id])
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (erule impE, assumption)
    apply (simp add: e_gr_add)
    apply (subst e_gr_le)
    apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+
    apply (subst comp_assoc)
    apply (assumption | rule comp_mono_eq refl)+
    (* New direct subgoal *)
    apply (simp del: add_succ_right add: add_succ_right [symmetric]
                add: e_gr_eq)
    apply (subst comp_id) (* simp cannot unify/inst right, use brr below (?) . *)
    apply (assumption | rule e_gr_fun add_type refl add_le_self nat_succI)+
    done

    lemma e_gr_split_add:
         "[| m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
          ==> e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
    apply (blast intro: e_gr_split_add_lemma [THEN mp])
    done

    lemma e_less_cont:
         "[|m le n; emb_chain(DD,ee); m ∈ nat; n ∈ nat|]
          ==> e_less(DD,ee,m,n):cont(DD`m,DD`n)"
    apply (blast intro: emb_cont emb_e_less)
    done

    lemma e_gr_cont:
        "[|n le m; emb_chain(DD,ee); m ∈ nat; n ∈ nat|]
         ==> e_gr(DD,ee,m,n):cont(DD`m,DD`n)"
    apply (erule rev_mp)
    apply (induct_tac m)
    apply (simp add: le0_iff e_gr_eq nat_0I)
    apply (assumption | rule impI id_cont emb_chain_cpo nat_0I)+
    apply (simp add: le_succ_iff)
    apply (erule disjE)
    apply (erule impE, assumption)
    apply (simp add: e_gr_le)
    apply (blast intro: comp_pres_cont Rp_cont emb_chain_cpo emb_chain_emb)
    apply (simp add: e_gr_eq)
    done

    (* Considerably shorter.... 57 against 26 *)

    lemma e_less_e_gr_split_add:
        "[|n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)"
    (* Use mp to prepare for induction. *)
    apply (erule rev_mp)
    apply (induct_tac k)
    apply (simp add: e_gr_eq e_less_eq id_type [THEN id_comp])
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (erule impE, assumption)
    apply (simp add: e_gr_le e_less_le add_le_mono)
    apply (subst comp_assoc)
    apply (rule_tac s1 = "ee` (m#+x)" in comp_assoc [THEN subst])
    apply (subst embRp_eq)
    apply (assumption | rule emb_chain_emb add_type emb_chain_cpo nat_succI)+
    apply (subst id_comp)
    apply (blast intro: e_less_cont [THEN cont_fun] add_le_self)
    apply (rule refl)
    apply (simp del: add_succ_right add: add_succ_right [symmetric]
                add: e_gr_eq)
    apply (blast intro: id_comp [symmetric] e_less_cont [THEN cont_fun]
                        add_le_self)
    done

    (* Again considerably shorter, and easy to obtain from the previous thm. *)

    lemma e_gr_e_less_split_add:
        "[|m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)"
    (* Use mp to prepare for induction. *)
    apply (erule rev_mp)
    apply (induct_tac k)
    apply (simp add: e_gr_eq e_less_eq id_type [THEN id_comp])
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (erule impE, assumption)
    apply (simp add: e_gr_le e_less_le add_le_self nat_le_refl add_le_mono)
    apply (subst comp_assoc)
    apply (rule_tac s1 = "ee` (n#+x)" in comp_assoc [THEN subst])
    apply (subst embRp_eq)
    apply (assumption | rule emb_chain_emb add_type emb_chain_cpo nat_succI)+
    apply (subst id_comp)
    apply (blast intro!: e_less_cont [THEN cont_fun] add_le_mono nat_le_refl)
    apply (rule refl)
    apply (simp del: add_succ_right add: add_succ_right [symmetric]
                add: e_less_eq)
    apply (blast intro: comp_id [symmetric] e_gr_cont [THEN cont_fun] add_le_self)
    done

    lemma emb_eps:
        "[|m le n; emb_chain(DD,ee); m ∈ nat; n ∈ nat|]
         ==> emb(DD`m,DD`n,eps(DD,ee,m,n))"
    apply (simp add: eps_def)
    apply (blast intro: emb_e_less)
    done

    lemma eps_fun:
        "[|emb_chain(DD,ee); m ∈ nat; n ∈ nat|]
         ==> eps(DD,ee,m,n): set(DD`m)->set(DD`n)"
    apply (simp add: eps_def)
    apply (auto intro: e_less_cont [THEN cont_fun]
                       not_le_iff_lt [THEN iffD1, THEN leI]
                       e_gr_fun nat_into_Ord)
    done

    lemma eps_id: "n ∈ nat ==> eps(DD,ee,n,n) = id(set(DD`n))"
    by (simp add: eps_def e_less_eq)

    lemma eps_e_less_add:
        "[|m ∈ nat; n ∈ nat|] ==> eps(DD,ee,m,m#+n) = e_less(DD,ee,m,m#+n)"
    by (simp add: eps_def add_le_self)

    lemma eps_e_less:
        "[|m le n; m ∈ nat; n ∈ nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)"
    by (simp add: eps_def)

    lemma eps_e_gr_add:
        "[|n ∈ nat; k ∈ nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)"
    by (simp add: eps_def e_less_eq e_gr_eq)

    lemma eps_e_gr:
        "[|n le m; m ∈ nat; n ∈ nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)"
    apply (erule le_exists)
    apply (simp_all add: eps_e_gr_add)
    done

    lemma eps_succ_ee:
        "[|!!n. n ∈ nat ==> emb(DD`n,DD`succ(n),ee`n); m ∈ nat|]
         ==> eps(DD,ee,m,succ(m)) = ee`m"
    by (simp add: eps_e_less le_succ_iff e_less_succ_emb)

    lemma eps_succ_Rp:
        "[|emb_chain(DD,ee); m ∈ nat|]
         ==> eps(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)"
    by (simp add: eps_e_gr le_succ_iff e_gr_succ_emb)

    lemma eps_cont:
      "[|emb_chain(DD,ee); m ∈ nat; n ∈ nat|] ==> eps(DD,ee,m,n): cont(DD`m,DD`n)"
    apply (rule_tac i = m and j = n in nat_linear_le)
    apply (simp_all add: eps_e_less e_less_cont eps_e_gr e_gr_cont)
    done

    (* Theorems about splitting. *)

    lemma eps_split_add_left:
        "[|n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,m#+k) = eps(DD,ee,m#+n,m#+k) O eps(DD,ee,m,m#+n)"
    apply (simp add: eps_e_less add_le_self add_le_mono)
    apply (auto intro: e_less_split_add)
    done

    lemma eps_split_add_left_rev:
        "[|n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,m#+n) = eps(DD,ee,m#+k,m#+n) O eps(DD,ee,m,m#+k)"
    apply (simp add: eps_e_less_add eps_e_gr add_le_self add_le_mono)
    apply (auto intro: e_less_e_gr_split_add)
    done

    lemma eps_split_add_right:
        "[|m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,n#+k,n) = eps(DD,ee,n#+m,n) O eps(DD,ee,n#+k,n#+m)"
    apply (simp add: eps_e_gr add_le_self add_le_mono)
    apply (auto intro: e_gr_split_add)
    done

    lemma eps_split_add_right_rev:
        "[|m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,n#+m,n) = eps(DD,ee,n#+k,n) O eps(DD,ee,n#+m,n#+k)"
    apply (simp add: eps_e_gr_add eps_e_less add_le_self add_le_mono)
    apply (auto intro: e_gr_e_less_split_add)
    done

    (* Arithmetic *)

    lemma le_exists_lemma:
        "[| n le k; k le m;
            !!p q. [|p le q; k=n#+p; m=n#+q; p ∈ nat; q ∈ nat|] ==> R;
            m ∈ nat |]==>R"
    apply (rule le_exists, assumption)
    prefer 2 apply (simp add: lt_nat_in_nat)
    apply (rule le_trans [THEN le_exists], assumption+, force+)
    done

    lemma eps_split_left_le:
        "[|m le k; k le n; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule le_exists_lemma, assumption+)
    apply (auto intro: eps_split_add_left)
    done

    lemma eps_split_left_le_rev:
        "[|m le n; n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule le_exists_lemma, assumption+)
    apply (auto intro: eps_split_add_left_rev)
    done

    lemma eps_split_right_le:
        "[|n le k; k le m; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule le_exists_lemma, assumption+)
    apply (auto intro: eps_split_add_right)
    done

    lemma eps_split_right_le_rev:
        "[|n le m; m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule le_exists_lemma, assumption+)
    apply (auto intro: eps_split_add_right_rev)
    done

    (* The desired two theorems about `splitting'. *)

    lemma eps_split_left:
        "[|m le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule nat_linear_le)
    apply (rule_tac [4] eps_split_right_le_rev)
    prefer 4 apply assumption
    apply (rule_tac [3] nat_linear_le)
    apply (rule_tac [5] eps_split_left_le)
    prefer 6 apply assumption
    apply (simp_all add: eps_split_left_le_rev)
    done

    lemma eps_split_right:
        "[|n le k; emb_chain(DD,ee); m ∈ nat; n ∈ nat; k ∈ nat|]
         ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
    apply (rule nat_linear_le)
    apply (rule_tac [3] eps_split_left_le_rev)
    prefer 3 apply assumption
    apply (rule_tac [8] nat_linear_le)
    apply (rule_tac [10] eps_split_right_le)
    prefer 11 apply assumption
    apply (simp_all add: eps_split_right_le_rev)
    done

    (*----------------------------------------------------------------------*)
    (* That was eps: D_m -> D_n, NEXT rho_emb: D_n -> Dinf.                 *)
    (*----------------------------------------------------------------------*)

    (* Considerably shorter. *)

    lemma rho_emb_fun:
        "[|emb_chain(DD,ee); n ∈ nat|]
         ==> rho_emb(DD,ee,n): set(DD`n) -> set(Dinf(DD,ee))"
    apply (simp add: rho_emb_def)
    apply (assumption |
           rule lam_type DinfI eps_cont [THEN cont_fun, THEN apply_type])+
    apply simp
    apply (rule_tac i = "succ (na) " and j = n in nat_linear_le)
       apply blast
      apply assumption
     apply (simplesubst eps_split_right_le)
        --{*Subst would rewrite the lhs. We want to change the rhs.*}
           prefer 2 apply assumption
          apply simp
         apply (assumption | rule add_le_self nat_0I nat_succI)+
     apply (simp add: eps_succ_Rp)
     apply (subst comp_fun_apply)
        apply (assumption |
               rule eps_fun nat_succI Rp_cont [THEN cont_fun]
                    emb_chain_emb emb_chain_cpo refl)+
    (* Now the second part of the proof. Slightly different than HOL. *)
    apply (simp add: eps_e_less nat_succI)
    apply (erule le_iff [THEN iffD1, THEN disjE])
    apply (simp add: e_less_le)
    apply (subst comp_fun_apply)
    apply (assumption | rule e_less_cont cont_fun emb_chain_emb emb_cont)+
    apply (subst embRp_eq_thm)
    apply (assumption |
           rule emb_chain_emb e_less_cont [THEN cont_fun, THEN apply_type]
                emb_chain_cpo nat_succI)+
     apply (simp add: eps_e_less)
    apply (simp add: eps_succ_Rp e_less_eq id_conv nat_succI)
    done

    lemma rho_emb_apply1:
        "x ∈ set(DD`n) ==> rho_emb(DD,ee,n)`x = (λm ∈ nat. eps(DD,ee,n,m)`x)"
    by (simp add: rho_emb_def)

    lemma rho_emb_apply2:
        "[|x ∈ set(DD`n); m ∈ nat|] ==> rho_emb(DD,ee,n)`x`m = eps(DD,ee,n,m)`x"
    by (simp add: rho_emb_def)

    lemma rho_emb_id: "[| x ∈ set(DD`n); n ∈ nat|] ==> rho_emb(DD,ee,n)`x`n = x"
    by (simp add: rho_emb_apply2 eps_id)

    (* Shorter proof, 23 against 62. *)

    lemma rho_emb_cont:
        "[|emb_chain(DD,ee); n ∈ nat|]
         ==> rho_emb(DD,ee,n): cont(DD`n,Dinf(DD,ee))"
    apply (rule contI)
    apply (assumption | rule rho_emb_fun)+
    apply (rule rel_DinfI)
    apply (simp add: rho_emb_def)
    apply (assumption |
           rule eps_cont [THEN cont_mono]  Dinf_prod apply_type rho_emb_fun)+
    (* Continuity, different order, slightly different proofs. *)
    apply (subst lub_Dinf)
    apply (rule chainI)
    apply (assumption | rule lam_type rho_emb_fun [THEN apply_type]  chain_in)+
    apply simp
    apply (rule rel_DinfI)
    apply (simp add: rho_emb_apply2 chain_in)
    apply (assumption |
           rule eps_cont [THEN cont_mono]  chain_rel Dinf_prod
                rho_emb_fun [THEN apply_type]  chain_in nat_succI)+
    (* Now, back to the result of applying lub_Dinf *)
    apply (simp add: rho_emb_apply2 chain_in)
    apply (subst rho_emb_apply1)
    apply (assumption | rule cpo_lub [THEN islub_in]  emb_chain_cpo)+
    apply (rule fun_extension)
    apply (assumption |
           rule lam_type eps_cont [THEN cont_fun, THEN apply_type]
                cpo_lub [THEN islub_in]  emb_chain_cpo)+
    apply (assumption | rule cont_chain eps_cont emb_chain_cpo)+
    apply simp
    apply (simp add: eps_cont [THEN cont_lub])
    done

    (* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)

    lemma eps1_aux1:
        "[|m le n; emb_chain(DD,ee); x ∈ set(Dinf(DD,ee)); m ∈ nat; n ∈ nat|]
         ==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)"
    apply (erule rev_mp) (* For induction proof *)
    apply (induct_tac n)
    apply (rule impI)
    apply (simp add: e_less_eq)
    apply (subst id_conv)
    apply (assumption | rule apply_type Dinf_prod cpo_refl emb_chain_cpo nat_0I)+
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (drule mp, assumption)
    apply (rule cpo_trans)
    apply (rule_tac [2] e_less_le [THEN ssubst])
    apply (assumption | rule emb_chain_cpo nat_succI)+
    apply (subst comp_fun_apply)
    apply (assumption |
           rule emb_chain_emb [THEN emb_cont]  e_less_cont cont_fun apply_type
                Dinf_prod)+
    apply (rule_tac y = "x`xa" in emb_chain_emb [THEN emb_cont, THEN cont_mono])
    apply (assumption | rule e_less_cont [THEN cont_fun]  apply_type Dinf_prod)+
    apply (rule_tac x1 = x and n1 = xa in Dinf_eq [THEN subst])
    apply (rule_tac [3] comp_fun_apply [THEN subst])
    apply (rename_tac [5] y)
    apply (rule_tac [5] P =
             "%z. rel(DD`succ(y),
                      (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
                      z)"
           in id_conv [THEN subst])
    apply (rule_tac [6] rel_cf)
    (* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
    (* solves 10 of 11 subgoals *)
    apply (assumption |
           rule Dinf_prod [THEN apply_type] cont_fun Rp_cont e_less_cont
                emb_cont emb_chain_emb emb_chain_cpo apply_type embRp_rel
                disjI1 [THEN le_succ_iff [THEN iffD2]]  nat_succI)+
    apply (simp add: e_less_eq)
    apply (subst id_conv)
    apply (auto intro: apply_type Dinf_prod emb_chain_cpo)
    done

    (* 18 vs 40 *)

    lemma eps1_aux2:
        "[|n le m; emb_chain(DD,ee); x ∈ set(Dinf(DD,ee)); m ∈ nat; n ∈ nat|]
         ==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)"
    apply (erule rev_mp) (* For induction proof *)
    apply (induct_tac m)
    apply (rule impI)
    apply (simp add: e_gr_eq)
    apply (subst id_conv)
    apply (assumption | rule apply_type Dinf_prod cpo_refl emb_chain_cpo nat_0I)+
    apply (simp add: le_succ_iff)
    apply (rule impI)
    apply (erule disjE)
    apply (drule mp, assumption)
    apply (subst e_gr_le)
    apply (rule_tac [4] comp_fun_apply [THEN ssubst])
    apply (rule_tac [6] Dinf_eq [THEN ssubst])
    apply (assumption |
           rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont
                apply_type Dinf_prod nat_succI)+
    apply (simp add: e_gr_eq)
    apply (subst id_conv)
    apply (auto intro: apply_type Dinf_prod emb_chain_cpo)
    done

    lemma eps1:
        "[|emb_chain(DD,ee); x ∈ set(Dinf(DD,ee)); m ∈ nat; n ∈ nat|]
         ==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)"
    apply (simp add: eps_def)
    apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2]
                        nat_into_Ord)
    done

    (* The following theorem is needed/useful due to type check for rel_cfI,
       but also elsewhere.
       Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)

    lemma lam_Dinf_cont:
      "[| emb_chain(DD,ee); n ∈ nat |]
         ==> (λx ∈ set(Dinf(DD,ee)). x`n) ∈ cont(Dinf(DD,ee),DD`n)"
    apply (rule contI)
    apply (assumption | rule lam_type apply_type Dinf_prod)+
    apply simp
    apply (assumption | rule rel_Dinf)+
    apply (subst beta)
    apply (auto intro: cpo_Dinf islub_in cpo_lub)
    apply (simp add: chain_in lub_Dinf)
    done

    lemma rho_projpair:
        "[| emb_chain(DD,ee); n ∈ nat |]
         ==> projpair(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n),rho_proj(DD,ee,n))"
    apply (simp add: rho_proj_def)
    apply (rule projpairI)
    apply (assumption | rule rho_emb_cont)+
    (* lemma used, introduced because same fact needed below due to rel_cfI. *)
    apply (assumption | rule lam_Dinf_cont)+
    (*-----------------------------------------------*)
    (* This part is 7 lines, but 30 in HOL (75% reduction!) *)
    apply (rule fun_extension)
    apply (rule_tac [3] id_conv [THEN ssubst])
    apply (rule_tac [4] comp_fun_apply [THEN ssubst])
    apply (rule_tac [6] beta [THEN ssubst])
    apply (rule_tac [7] rho_emb_id [THEN ssubst])
    apply (assumption |
           rule comp_fun id_type lam_type rho_emb_fun Dinf_prod [THEN apply_type]
                apply_type refl)+
    (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    apply (rule rel_cfI) (* ------------------>>>Yields type cond, not in HOL *)
    apply (subst id_conv)
    apply (rule_tac [2] comp_fun_apply [THEN ssubst])
    apply (rule_tac [4] beta [THEN ssubst])
    apply (rule_tac [5] rho_emb_apply1 [THEN ssubst])
    apply (rule_tac [6] rel_DinfI)
    apply (rule_tac [6] beta [THEN ssubst])
    (* Dinf_prod bad with lam_type *)
    apply (assumption |
           rule eps1 lam_type rho_emb_fun eps_fun
                Dinf_prod [THEN apply_type] refl)+
    apply (assumption |
           rule apply_type eps_fun Dinf_prod comp_pres_cont rho_emb_cont
                lam_Dinf_cont id_cont cpo_Dinf emb_chain_cpo)+
    done

    lemma emb_rho_emb:
      "[| emb_chain(DD,ee); n ∈ nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"
    by (auto simp add: emb_def intro: exI rho_projpair)

    lemma rho_proj_cont: "[| emb_chain(DD,ee); n ∈ nat |]
         ==> rho_proj(DD,ee,n) ∈ cont(Dinf(DD,ee),DD`n)"
    by (auto intro: rho_projpair projpair_p_cont)

    (*----------------------------------------------------------------------*)
    (* Commutivity and universality.                                        *)
    (*----------------------------------------------------------------------*)

    lemma commuteI:
      "[| !!n. n ∈ nat ==> emb(DD`n,E,r(n));
          !!m n. [|m le n; m ∈ nat; n ∈ nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |]
         ==> commute(DD,ee,E,r)"
    by (simp add: commute_def)

    lemma commute_emb [TC]:
      "[| commute(DD,ee,E,r); n ∈ nat |] ==> emb(DD`n,E,r(n))"
    by (simp add: commute_def)

    lemma commute_eq:
      "[| commute(DD,ee,E,r); m le n; m ∈ nat; n ∈ nat |]
         ==> r(n) O eps(DD,ee,m,n) = r(m) "
    by (simp add: commute_def)

    (* Shorter proof: 11 vs 46 lines. *)

    lemma rho_emb_commute:
      "emb_chain(DD,ee) ==> commute(DD,ee,Dinf(DD,ee),rho_emb(DD,ee))"
    apply (rule commuteI)
    apply (assumption | rule emb_rho_emb)+
    apply (rule fun_extension) (* Manual instantiation in HOL. *)
    apply (rule_tac [3] comp_fun_apply [THEN ssubst])
    apply (rule_tac [5] fun_extension) (*Next, clean up and instantiate unknowns *)
    apply (assumption | rule comp_fun rho_emb_fun eps_fun Dinf_prod apply_type)+
    apply (simp add: rho_emb_apply2 eps_fun [THEN apply_type])
    apply (rule comp_fun_apply [THEN subst])
    apply (rule_tac [3] eps_split_left [THEN subst])
    apply (auto intro: eps_fun)
    done

    lemma le_succ: "n ∈ nat ==> n le succ(n)"
    by (simp add: le_succ_iff)

    (* Shorter proof: 21 vs 83 (106 - 23, due to OAssoc complication) *)

    lemma commute_chain:
        "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |]
         ==> chain(cf(E,E),λn ∈ nat. r(n) O Rp(DD`n,E,r(n)))"
    apply (rule chainI)
    apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
                        emb_cont emb_chain_cpo,
           simp)
    apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
    apply (assumption | rule le_succ nat_succI)+
    apply (subst Rp_comp)
    apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+
    apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
    apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
    apply (rule comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                        emb_cont emb_chain_cpo le_succ)+
    apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
    apply (rule_tac [2] comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                        Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
    apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
    apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                        emb_chain_cpo embRp_rel emb_eps le_succ)+
    done

    lemma rho_emb_chain:
      "emb_chain(DD,ee) ==>
       chain(cf(Dinf(DD,ee),Dinf(DD,ee)),
             λn ∈ nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))"
    by (auto intro: commute_chain rho_emb_commute cpo_Dinf)

    lemma rho_emb_chain_apply1:
         "[| emb_chain(DD,ee); x ∈ set(Dinf(DD,ee)) |]
          ==> chain(Dinf(DD,ee),
                    λn ∈ nat.
                     (rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))`x)"
    by (drule rho_emb_chain [THEN chain_cf], assumption, simp)

    lemma chain_iprod_emb_chain:
         "[| chain(iprod(DD),X); emb_chain(DD,ee); n ∈ nat |]
          ==> chain(DD`n,λm ∈ nat. X `m `n)"
    by (auto intro: chain_iprod emb_chain_cpo)

    lemma rho_emb_chain_apply2:
      "[| emb_chain(DD,ee); x ∈ set(Dinf(DD,ee)); n ∈ nat |] ==>
       chain
        (DD`n,
         λxa ∈ nat.
          (rho_emb(DD, ee, xa) O Rp(DD ` xa, Dinf(DD, ee),rho_emb(DD, ee, xa))) `
           x ` n)"
    by (frule rho_emb_chain_apply1 [THEN chain_Dinf, THEN chain_iprod_emb_chain],
        auto)

    (* Shorter proof: 32 vs 72 (roughly), Isabelle proof has lemmas. *)

    lemma rho_emb_lub:
      "emb_chain(DD,ee) ==>
       lub(cf(Dinf(DD,ee),Dinf(DD,ee)),
           λn ∈ nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))) =
       id(set(Dinf(DD,ee)))"
    apply (rule cpo_antisym)
    apply (rule cpo_cf) (*Instantiate variable, continued below (loops otherwise)*)
    apply (assumption | rule cpo_Dinf)+
    apply (rule islub_least)
    apply (assumption |
           rule cpo_lub rho_emb_chain cpo_cf cpo_Dinf isubI cont_cf id_cont)+
    apply simp
    apply (assumption | rule embRp_rel emb_rho_emb emb_chain_cpo cpo_Dinf)+
    apply (rule rel_cfI)
    apply (simp add: lub_cf rho_emb_chain cpo_Dinf)
    apply (rule rel_DinfI) (* Additional assumptions *)
    apply (subst lub_Dinf)
    apply (assumption | rule rho_emb_chain_apply1)+
    defer 1
    apply (assumption |
           rule Dinf_prod cpo_lub [THEN islub_in]  id_cont cpo_Dinf cpo_cf cf_cont
                rho_emb_chain rho_emb_chain_apply1 id_cont [THEN cont_cf])+
    apply simp
    apply (rule dominate_islub)
    apply (rule_tac [3] cpo_lub)
    apply (rule_tac [6] x1 = "x`n" in chain_const [THEN chain_fun])
    defer 1
    apply (assumption |
           rule rho_emb_chain_apply2 emb_chain_cpo islub_const apply_type
                Dinf_prod emb_chain_cpo chain_fun rho_emb_chain_apply2)+
    apply (rule dominateI, assumption, simp)
    apply (subst comp_fun_apply)
    apply (assumption |
           rule cont_fun Rp_cont emb_cont emb_rho_emb cpo_Dinf emb_chain_cpo)+
    apply (subst rho_projpair [THEN Rp_unique])
    prefer 5
    apply (simp add: rho_proj_def)
    apply (rule rho_emb_id [THEN ssubst])
    apply (auto intro: cpo_Dinf apply_type Dinf_prod emb_chain_cpo)
    done

    lemma theta_chain: (* almost same proof as commute_chain *)
        "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
            emb_chain(DD,ee); cpo(E); cpo(G) |]
         ==> chain(cf(E,G),λn ∈ nat. f(n) O Rp(DD`n,E,r(n)))"
    apply (rule chainI)
    apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
                        emb_cont emb_chain_cpo,
           simp)
    apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
    apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
    apply (assumption | rule le_succ nat_succI)+
    apply (subst Rp_comp)
    apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+
    apply (rule comp_assoc [THEN subst])
    apply (rule_tac r1 = "f (succ (n))" in comp_assoc [THEN ssubst])
    apply (rule comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                         emb_cont emb_chain_cpo le_succ)+
    apply (rule_tac b="f(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
    apply (rule_tac [2] comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                        Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
    apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
    apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                        emb_chain_cpo embRp_rel emb_eps le_succ)+
    done

    lemma theta_proj_chain: (* similar proof to theta_chain *)
      "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
          emb_chain(DD,ee); cpo(E); cpo(G) |]
         ==> chain(cf(G,E),λn ∈ nat. r(n) O Rp(DD`n,G,f(n)))"
    apply (rule chainI)
    apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
                        emb_cont emb_chain_cpo, simp)
    apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
    apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
    apply (assumption | rule le_succ nat_succI)+
    apply (subst Rp_comp)
    apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+
    apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
    apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
    apply (rule comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                        emb_cont emb_chain_cpo le_succ)+
    apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
    apply (rule_tac [2] comp_mono)
    apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                        Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
    apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
    apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                        emb_chain_cpo embRp_rel emb_eps le_succ)+
    done

    (* Simplification with comp_assoc is possible inside a λ-abstraction,
       because it does not have assumptions. If it had, as the HOL-ST theorem
       too strongly has, we would be in deep trouble due to HOL's lack of proper
       conditional rewriting (a HOL contrib provides something that works). *)

    (* Controlled simplification inside lambda: introduce lemmas *)

    lemma commute_O_lemma:
         "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
             emb_chain(DD,ee); cpo(E); cpo(G); x ∈ nat |]
          ==> r(x) O Rp(DD ` x, G, f(x)) O f(x) O Rp(DD ` x, E, r(x)) =
              r(x) O Rp(DD ` x, E, r(x))"
    apply (rule_tac s1 = "f (x) " in comp_assoc [THEN subst])
    apply (subst embRp_eq)
    apply (rule_tac [4] id_comp [THEN ssubst])
    apply (auto intro: cont_fun Rp_cont commute_emb emb_chain_cpo)
    done

    (* Shorter proof (but lemmas): 19 vs 79 (103 - 24, due to OAssoc)  *)

    lemma theta_projpair:
      "[| lub(cf(E,E), λn ∈ nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
          commute(DD,ee,E,r); commute(DD,ee,G,f);
          emb_chain(DD,ee); cpo(E); cpo(G) |]
       ==> projpair
            (E,G,
             lub(cf(E,G), λn ∈ nat. f(n) O Rp(DD`n,E,r(n))),
             lub(cf(G,E), λn ∈ nat. r(n) O Rp(DD`n,G,f(n))))"
    apply (simp add: projpair_def rho_proj_def, safe)
    apply (rule_tac [3] comp_lubs [THEN ssubst])
    (* The following one line is 15 lines in HOL, and includes existentials. *)
    apply (assumption |
           rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
    apply (simp (no_asm) add: comp_assoc)
    apply (simp add: commute_O_lemma)
    apply (subst comp_lubs)
    apply (assumption |
           rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
    apply (simp (no_asm) add: comp_assoc)
    apply (simp add: commute_O_lemma)
    apply (rule dominate_islub)
    defer 1
    apply (rule cpo_lub)
    apply (assumption |
           rule commute_chain commute_emb islub_const cont_cf id_cont
        cpo_cf chain_fun chain_const)+
    apply (rule dominateI, assumption, simp)
    apply (blast intro: embRp_rel commute_emb emb_chain_cpo)
    done

    lemma emb_theta:
        "[| lub(cf(E,E), λn ∈ nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
            commute(DD,ee,E,r); commute(DD,ee,G,f);
            emb_chain(DD,ee); cpo(E); cpo(G) |]
         ==> emb(E,G,lub(cf(E,G), λn ∈ nat. f(n) O Rp(DD`n,E,r(n))))"
    apply (simp add: emb_def)
    apply (blast intro: theta_projpair)
    done

    lemma mono_lemma:
        "[| g ∈ cont(D,D'); cpo(D); cpo(D'); cpo(E) |]
         ==> (λf ∈ cont(D',E). f O g) ∈ mono(cf(D',E),cf(D,E))"
    apply (rule monoI)
    apply (simp add: set_def cf_def)
    apply (drule cf_cont)+
    apply simp
    apply (blast intro: comp_mono lam_type comp_pres_cont cpo_cf cont_cf)
    done

    lemma commute_lam_lemma:
         "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
             emb_chain(DD,ee); cpo(E); cpo(G); n ∈ nat |]
          ==> (λna ∈ nat. (λf ∈ cont(E, G). f O r(n)) `
               ((λn ∈ nat. f(n) O Rp(DD ` n, E, r(n))) ` na))  =
              (λna ∈ nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))"
    apply (rule fun_extension)
    (*something wrong here*)
    apply (auto simp del: beta_if simp add: beta intro: lam_type)
    done

    lemma chain_lemma:
         "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
             emb_chain(DD,ee); cpo(E); cpo(G); n ∈ nat |]
          ==> chain(cf(DD`n,G),λx ∈ nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))"
    apply (rule commute_lam_lemma [THEN subst])
    apply (blast intro: theta_chain emb_chain_cpo
                   commute_emb [THEN emb_cont, THEN mono_lemma, THEN mono_chain])+
    done

    lemma suffix_lemma:
        "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
            emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x ∈ nat |]
         ==> suffix(λn ∈ nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) =
             (λn ∈ nat. f(x))"
    apply (simp add: suffix_def)
    apply (rule lam_type [THEN fun_extension])
    apply (blast intro: lam_type comp_fun cont_fun Rp_cont emb_cont
                        commute_emb emb_chain_cpo)+
    apply simp
    apply (rename_tac y)
    apply (subgoal_tac
           "f(x#+y) O (Rp(DD`(x#+y), E, r(x#+y)) O r (x#+y)) O eps(DD, ee, x, x#+y)
            = f(x)")
    apply (simp add: comp_assoc commute_eq add_le_self)
    apply (simp add: embRp_eq eps_fun [THEN id_comp] commute_emb emb_chain_cpo)
    apply (blast intro: commute_eq add_le_self)
    done

    lemma mediatingI:
      "[|emb(E,G,t);  !!n. n ∈ nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
    by (simp add: mediating_def)

    lemma mediating_emb: "mediating(E,G,r,f,t) ==> emb(E,G,t)"
    by (simp add: mediating_def)

    lemma mediating_eq: "[| mediating(E,G,r,f,t); n ∈ nat |] ==> f(n) = t O r(n)"
    by (simp add: mediating_def)

    lemma lub_universal_mediating:
      "[| lub(cf(E,E), λn ∈ nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
          commute(DD,ee,E,r); commute(DD,ee,G,f);
          emb_chain(DD,ee); cpo(E); cpo(G) |]
         ==> mediating(E,G,r,f,lub(cf(E,G), λn ∈ nat. f(n) O Rp(DD`n,E,r(n))))"
    apply (assumption | rule mediatingI emb_theta)+
    apply (rule_tac b = "r (n) " in lub_const [THEN subst])
    apply (rule_tac [3] comp_lubs [THEN ssubst])
    apply (blast intro: cont_cf emb_cont commute_emb cpo_cf theta_chain
                        chain_const emb_chain_cpo)+
    apply (simp (no_asm))
    apply (rule_tac n1 = n in lub_suffix [THEN subst])
    apply (assumption | rule chain_lemma cpo_cf emb_chain_cpo)+
    apply (simp add: suffix_lemma lub_const cont_cf emb_cont commute_emb cpo_cf
                     emb_chain_cpo)
    done

    lemma lub_universal_unique:
        "[| mediating(E,G,r,f,t);
            lub(cf(E,E), λn ∈ nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
            commute(DD,ee,E,r); commute(DD,ee,G,f);
            emb_chain(DD,ee); cpo(E); cpo(G) |]
         ==> t = lub(cf(E,G), λn ∈ nat. f(n) O Rp(DD`n,E,r(n)))"
    apply (rule_tac b = t in comp_id [THEN subst])
    apply (erule_tac [2] subst)
    apply (rule_tac [2] b = t in lub_const [THEN subst])
    apply (rule_tac [4] comp_lubs [THEN ssubst])
    prefer 9 apply (simp add: comp_assoc mediating_eq)
    apply (assumption |
           rule cont_fun emb_cont mediating_emb cont_cf cpo_cf chain_const
                commute_chain emb_chain_cpo)+
    done

    (*---------------------------------------------------------------------*)
    (* Dinf yields the inverse_limit, stated as rho_emb_commute and        *)
    (* Dinf_universal.                                                     *)
    (*---------------------------------------------------------------------*)

    theorem Dinf_universal:
      "[| commute(DD,ee,G,f); emb_chain(DD,ee); cpo(G) |] ==>
       mediating
        (Dinf(DD,ee),G,rho_emb(DD,ee),f,
         lub(cf(Dinf(DD,ee),G),
             λn ∈ nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))) &
       (∀t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->
         t = lub(cf(Dinf(DD,ee),G),
             λn ∈ nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))"
    apply safe
    apply (assumption |
           rule lub_universal_mediating rho_emb_commute rho_emb_lub cpo_Dinf)+
    apply (auto intro: lub_universal_unique rho_emb_commute rho_emb_lub cpo_Dinf)
    done

    end

lemmas nat_linear_le:

      [| i ∈ nat; j ∈ nat; i ≤ j ==> P; j ≤ i ==> P |] ==> P

lemmas nat_linear_le:

      [| i ∈ nat; j ∈ nat; i ≤ j ==> P; j ≤ i ==> P |] ==> P

lemma set_I:

      x ∈ fst(D) ==> x ∈ set(D)

lemma rel_I:

      ⟨x, y⟩ ∈ snd(D) ==> rel(D, x, y)

lemma rel_E:

      rel(D, x, y) ==> ⟨x, y⟩ ∈ snd(D)

lemma po_refl:

      [| po(D); x ∈ set(D) |] ==> rel(D, x, x)

lemma po_trans:

      [| po(D); rel(D, x, y); rel(D, y, z); x ∈ set(D); y ∈ set(D); z ∈ set(D) |]
      ==> rel(D, x, z)

lemma po_antisym:

      [| po(D); rel(D, x, y); rel(D, y, x); x ∈ set(D); y ∈ set(D) |] ==> x = y

lemma poI:

      [| !!x. x ∈ set(D) ==> rel(D, x, x);
         !!x y z.
            [| rel(D, x, y); rel(D, y, z); x ∈ set(D); y ∈ set(D); z ∈ set(D) |]
            ==> rel(D, x, z);
         !!x y. [| rel(D, x, y); rel(D, y, x); x ∈ set(D); y ∈ set(D) |] ==> x = y |]
      ==> po(D)

lemma cpoI:

      [| po(D); !!X. chain(D, X) ==> islub(D, X, x(D, X)) |] ==> cpo(D)

lemma cpo_po:

      cpo(D) ==> po(D)

lemma cpo_refl:

      [| cpo(D); x ∈ set(D) |] ==> rel(D, x, x)

lemma cpo_trans:

      [| cpo(D); rel(D, x, y); rel(D, y, z); x ∈ set(D); y ∈ set(D); z ∈ set(D) |]
      ==> rel(D, x, z)

lemma cpo_antisym:

      [| cpo(D); rel(D, x, y); rel(D, y, x); x ∈ set(D); y ∈ set(D) |] ==> x = y

lemma cpo_islub:

      [| cpo(D); chain(D, X); !!x. islub(D, X, x) ==> R |] ==> R

lemma islub_isub:

      islub(D, X, x) ==> isub(D, X, x)

lemma islub_in:

      islub(D, X, x) ==> x ∈ set(D)

lemma islub_ub:

      [| islub(D, X, x); n ∈ nat |] ==> rel(D, X ` n, x)

lemma islub_least:

      [| islub(D, X, x); isub(D, X, y) |] ==> rel(D, x, y)

lemma islubI:

      [| isub(D, X, x); !!y. isub(D, X, y) ==> rel(D, x, y) |] ==> islub(D, X, x)

lemma isubI:

      [| x ∈ set(D); !!n. n ∈ nat ==> rel(D, X ` n, x) |] ==> isub(D, X, x)

lemma isubE:

      [| isub(D, X, x); [| x ∈ set(D); !!n. n ∈ nat ==> rel(D, X ` n, x) |] ==> P |]
      ==> P

lemma isubD1:

      isub(D, X, x) ==> x ∈ set(D)

lemma isubD2:

      [| isub(D, X, x); n ∈ nat |] ==> rel(D, X ` n, x)

lemma islub_unique:

      [| islub(D, X, x); islub(D, X, y); cpo(D) |] ==> x = y

lemma cpo_lub:

      [| chain(D, X); cpo(D) |] ==> islub(D, X, lub(D, X))

lemma chainI:

      [| X ∈ nat -> set(D); !!n. n ∈ nat ==> rel(D, X ` n, X ` succ(n)) |]
      ==> chain(D, X)

lemma chain_fun:

      chain(D, X) ==> X ∈ nat -> set(D)

lemma chain_in:

      [| chain(D, X); n ∈ nat |] ==> X ` n ∈ set(D)

lemma chain_rel:

      [| chain(D, X); n ∈ nat |] ==> rel(D, X ` n, X ` succ(n))

lemma chain_rel_gen_add:

      [| chain(D, X); cpo(D); n ∈ nat; m ∈ nat |] ==> rel(D, X ` n, X ` (m #+ n))

lemma chain_rel_gen:

      [| n ≤ m; chain(D, X); cpo(D); m ∈ nat |] ==> rel(D, X ` n, X ` m)

lemma pcpoI:

      [| !!y. y ∈ set(D) ==> rel(D, x, y); x ∈ set(D); cpo(D) |] ==> pcpo(D)

lemma pcpo_cpo:

      pcpo(D) ==> cpo(D)

lemma pcpo_bot_ex1:

      pcpo(D) ==> ∃!x. x ∈ set(D) ∧ (∀y∈set(D). rel(D, x, y))

lemma bot_least:

      [| pcpo(D); y ∈ set(D) |] ==> rel(D, bot(D), y)

lemma bot_in:

      pcpo(D) ==> bot(D) ∈ set(D)

lemma bot_unique:

      [| pcpo(D); x ∈ set(D); !!y. y ∈ set(D) ==> rel(D, x, y) |] ==> x = bot(D)

lemma chain_const:

      [| x ∈ set(D); cpo(D) |] ==> chain(D, λn∈nat. x)

lemma islub_const:

      [| x ∈ set(D); cpo(D) |] ==> islub(D, λn∈nat. x, x)

lemma lub_const:

      [| x ∈ set(D); cpo(D) |] ==> lub(D, λn∈nat. x) = x

lemma isub_suffix:

      [| chain(D, X); cpo(D) |] ==> isub(D, suffix(X, n), x) <-> isub(D, X, x)

lemma islub_suffix:

      [| chain(D, X); cpo(D) |] ==> islub(D, suffix(X, n), x) <-> islub(D, X, x)

lemma lub_suffix:

      [| chain(D, X); cpo(D) |] ==> lub(D, suffix(X, n)) = lub(D, X)

lemma dominateI:

      [| !!m. m ∈ nat ==> n(m) ∈ nat; !!m. m ∈ nat ==> rel(D, X ` m, Y ` n(m)) |]
      ==> dominate(D, X, Y)

lemma dominate_isub:

      [| dominate(D, X, Y); isub(D, Y, x); cpo(D); X ∈ nat -> set(D);
         Y ∈ nat -> set(D) |]
      ==> isub(D, X, x)

lemma dominate_islub:

      [| dominate(D, X, Y); islub(D, X, x); islub(D, Y, y); cpo(D); X ∈ nat -> set(D);
         Y ∈ nat -> set(D) |]
      ==> rel(D, x, y)

lemma subchain_isub:

      [| subchain(Y, X); isub(D, X, x) |] ==> isub(D, Y, x)

lemma dominate_islub_eq:

      [| dominate(D, X, Y); subchain(Y, X); islub(D, X, x); islub(D, Y, y); cpo(D);
         X ∈ nat -> set(D); Y ∈ nat -> set(D) |]
      ==> x = y

lemma matrix_fun:

      matrix(D, M) ==> M ∈ nat -> nat -> set(D)

lemma matrix_in_fun:

      [| matrix(D, M); n ∈ nat |] ==> M ` n ∈ nat -> set(D)

lemma matrix_in:

      [| matrix(D, M); n ∈ nat; m ∈ nat |] ==> M ` n ` m ∈ set(D)

lemma matrix_rel_1_0:

      [| matrix(D, M); n ∈ nat; m ∈ nat |] ==> rel(D, M ` n ` m, M ` succ(n) ` m)

lemma matrix_rel_0_1:

      [| matrix(D, M); n ∈ nat; m ∈ nat |] ==> rel(D, M ` n ` m, M ` n ` succ(m))

lemma matrix_rel_1_1:

      [| matrix(D, M); n ∈ nat; m ∈ nat |]
      ==> rel(D, M ` n ` m, M ` succ(n) ` succ(m))

lemma fun_swap:

      f ∈ X -> Y -> Z ==> (λy∈Y. λx∈X. f ` x ` y) ∈ Y -> X -> Z

lemma matrix_sym_axis:

      matrix(D, M) ==> matrix(D, λm∈nat. λn∈nat. M ` n ` m)

lemma matrix_chain_diag:

      matrix(D, M) ==> chain(D, λn∈nat. M ` n ` n)

lemma matrix_chain_left:

      [| matrix(D, M); n ∈ nat |] ==> chain(D, M ` n)

lemma matrix_chain_right:

      [| matrix(D, M); m ∈ nat |] ==> chain(D, λn∈nat. M ` n ` m)

lemma matrix_chainI:

      [| !!x. x ∈ nat ==> chain(D, M ` x);
         !!y. y ∈ nat ==> chain(D, λx∈nat. M ` x ` y); M ∈ nat -> nat -> set(D);
         cpo(D) |]
      ==> matrix(D, M)

lemma lemma_rel_rel:

      [| m ∈ nat; rel(D, (λn∈nat. M ` n ` n) ` m, y) |] ==> rel(D, M ` m ` m, y)

lemma lemma2:

      [| x ∈ nat; m ∈ nat;
         rel(D, (λn∈nat. M ` n ` m1.0) ` x, (λn∈nat. M ` n ` m1.0) ` m) |]
      ==> rel(D, M ` x ` m1.0, M ` m ` m1.0)

lemma isub_lemma:

      [| isub(D, λn∈nat. M ` n ` n, y); matrix(D, M); cpo(D) |]
      ==> isub(D, λn∈nat. lub(D, λm∈nat. M ` n ` m), y)

lemma matrix_chain_lub:

      [| matrix(D, M); cpo(D) |] ==> chain(D, λn∈nat. lub(D, λm∈nat. M ` n ` m))

lemma isub_eq:

      [| matrix(D, M); cpo(D) |]
      ==> isub(D, λn∈nat. lub(D, λm∈nat. M ` n ` m), y) <->
          isub(D, λn∈nat. M ` n ` n, y)

lemma lub_matrix_diag_aux1:

      lub(D, λn∈nat. lub(D, λm∈nat. M ` n ` m)) =
      (THE x. islub(D, λn∈nat. lub(D, λm∈nat. M ` n ` m), x))

lemma lub_matrix_diag_aux2:

      lub(D, λn∈nat. M ` n ` n) = (THE x. islub(D, λn∈nat. M ` n ` n, x))

lemma lub_matrix_diag:

      [| matrix(D, M); cpo(D) |]
      ==> lub(D, λn∈nat. lub(D, λm∈nat. M ` n ` m)) = lub(D, λn∈nat. M ` n ` n)

lemma lub_matrix_diag_sym:

      [| matrix(D, M); cpo(D) |]
      ==> lub(D, λm∈nat. lub(D, λn∈nat. M ` n ` m)) = lub(D, λn∈nat. M ` n ` n)

lemma monoI:

      [| f ∈ set(D) -> set(E);
         !!x y. [| rel(D, x, y); x ∈ set(D); y ∈ set(D) |] ==> rel(E, f ` x, f ` y) |]
      ==> f ∈ mono(D, E)

lemma mono_fun:

      f ∈ mono(D, E) ==> f ∈ set(D) -> set(E)

lemma mono_map:

      [| f ∈ mono(D, E); x ∈ set(D) |] ==> f ` x ∈ set(E)

lemma mono_mono:

      [| f ∈ mono(D, E); rel(D, x, y); x ∈ set(D); y ∈ set(D) |]
      ==> rel(E, f ` x, f ` y)

lemma contI:

      [| f ∈ set(D) -> set(E);
         !!x y. [| rel(D, x, y); x ∈ set(D); y ∈ set(D) |] ==> rel(E, f ` x, f ` y);
         !!X. chain(D, X) ==> f ` lub(D, X) = lub(E, λn∈nat. f ` (X ` n)) |]
      ==> f ∈ cont(D, E)

lemma cont2mono:

      f ∈ cont(D, E) ==> f ∈ mono(D, E)

lemma cont_fun:

      f ∈ cont(D, E) ==> f ∈ set(D) -> set(E)

lemma cont_map:

      [| f ∈ cont(D, E); x ∈ set(D) |] ==> f ` x ∈ set(E)

lemma cont_mono:

      [| f ∈ cont(D, E); rel(D, x, y); x ∈ set(D); y ∈ set(D) |]
      ==> rel(E, f ` x, f ` y)

lemma cont_lub:

      [| f ∈ cont(D, E); chain(D, X) |]
      ==> f ` lub(D, X) = lub(E, λn∈nat. f ` (X ` n))

lemma mono_chain:

      [| f ∈ mono(D, E); chain(D, X) |] ==> chain(E, λn∈nat. f ` (X ` n))

lemma cont_chain:

      [| f ∈ cont(D, E); chain(D, X) |] ==> chain(E, λn∈nat. f ` (X ` n))

lemma cf_cont:

      f ∈ set(cf(D, E)) ==> f ∈ cont(D, E)

lemma cont_cf:

      f ∈ cont(D, E) ==> f ∈ set(cf(D, E))

lemma rel_cfI:

      [| !!x. x ∈ set(D) ==> rel(E, f ` x, g ` x); f ∈ cont(D, E); g ∈ cont(D, E) |]
      ==> rel(cf(D, E), f, g)

lemma rel_cf:

      [| rel(cf(D, E), f, g); x ∈ set(D) |] ==> rel(E, f ` x, g ` x)

lemma chain_cf:

      [| chain(cf(D, E), X); x ∈ set(D) |] ==> chain(E, λn∈nat. X ` n ` x)

lemma matrix_lemma:

      [| chain(cf(D, E), X); chain(D, Xa); cpo(D); cpo(E) |]
      ==> matrix(E, λx∈nat. λxa∈nat. X ` x ` (Xa ` xa))

lemma chain_cf_lub_cont:

      [| chain(cf(D, E), X); cpo(D); cpo(E) |]
      ==> (λx∈set(D). lub(E, λn∈nat. X ` n ` x)) ∈ cont(D, E)

lemma islub_cf:

      [| chain(cf(D, E), X); cpo(D); cpo(E) |]
      ==> islub(cf(D, E), X, λx∈set(D). lub(E, λn∈nat. X ` n ` x))

lemma cpo_cf:

      [| cpo(D); cpo(E) |] ==> cpo(cf(D, E))

lemma lub_cf:

      [| chain(cf(D, E), X); cpo(D); cpo(E) |]
      ==> lub(cf(D, E), X) = (λx∈set(D). lub(E, λn∈nat. X ` n ` x))

lemma const_cont:

      [| y ∈ set(E); cpo(D); cpo(E) |] ==> (λx∈set(D). y) ∈ cont(D, E)

lemma cf_least:

      [| cpo(D); pcpo(E); y ∈ cont(D, E) |] ==> rel(cf(D, E), λx∈set(D). bot(E), y)

lemma pcpo_cf:

      [| cpo(D); pcpo(E) |] ==> pcpo(cf(D, E))

lemma bot_cf:

      [| cpo(D); pcpo(E) |] ==> bot(cf(D, E)) = (λx∈set(D). bot(E))

lemma id_cont:

      cpo(D) ==> id(set(D)) ∈ cont(D, D)

lemmas comp_cont_apply:

      [| g ∈ cont(D1, E2); a ∈ set(D1) |] ==> (f O g) ` a = f ` (g ` a)

lemmas comp_cont_apply:

      [| g ∈ cont(D1, E2); a ∈ set(D1) |] ==> (f O g) ` a = f ` (g ` a)

lemma comp_pres_cont:

      [| f ∈ cont(D', E); g ∈ cont(D, D'); cpo(D) |] ==> f O g ∈ cont(D, E)

lemma comp_mono:

      [| f ∈ cont(D', E); g ∈ cont(D, D'); f' ∈ cont(D', E); g' ∈ cont(D, D');
         rel(cf(D', E), f, f'); rel(cf(D, D'), g, g'); cpo(D); cpo(E) |]
      ==> rel(cf(D, E), f O g, f' O g')

lemma chain_cf_comp:

      [| chain(cf(D', E), X); chain(cf(D, D'), Y); cpo(D); cpo(E) |]
      ==> chain(cf(D, E), λn∈nat. X ` n O Y ` n)

lemma comp_lubs:

      [| chain(cf(D', E), X); chain(cf(D, D'), Y); cpo(D); cpo(D'); cpo(E) |]
      ==> lub(cf(D', E), X) O lub(cf(D, D'), Y) = lub(cf(D, E), λn∈nat. X ` n O Y ` n)

lemma projpairI:

      [| e ∈ cont(D, E); p ∈ cont(E, D); p O e = id(set(D));
         rel(cf(E, E), e O p, id(set(E))) |]
      ==> projpair(D, E, e, p)

lemma projpair_e_cont:

      projpair(D, E, e, p) ==> e ∈ cont(D, E)

lemma projpair_p_cont:

      projpair(D, E, e, p) ==> p ∈ cont(E, D)

lemma projpair_ep_cont:

      projpair(D, E, e, p) ==> e ∈ cont(D, E) ∧ p ∈ cont(E, D)

lemma projpair_eq:

      projpair(D, E, e, p) ==> p O e = id(set(D))

lemma projpair_rel:

      projpair(D, E, e, p) ==> rel(cf(E, E), e O p, id(set(E)))

lemmas id_comp:

      r ∈ A -> B ==> id(B) O r = r

and comp_id:

      r ∈ A -> B ==> r O id(A) = r

lemmas id_comp:

      r ∈ A -> B ==> id(B) O r = r

and comp_id:

      r ∈ A -> B ==> r O id(A) = r

lemma projpair_unique_aux1:

      [| cpo(D); cpo(E); projpair(D, E, e, p); projpair(D, E, e', p');
         rel(cf(D, E), e, e') |]
      ==> rel(cf(E, D), p', p)

lemma projpair_unique_aux2:

      [| cpo(D); cpo(E); projpair(D, E, e, p); projpair(D, E, e', p');
         rel(cf(E, D), p', p) |]
      ==> rel(cf(D, E), e, e')

lemma projpair_unique:

      [| cpo(D); cpo(E); projpair(D, E, e, p); projpair(D, E, e', p') |]
      ==> e = e' <-> p = p'

lemma embRp:

      [| emb(D, E, e); cpo(D); cpo(E) |] ==> projpair(D, E, e, Rp(D, E, e))

lemma embI:

      projpair(D, E, e, p) ==> emb(D, E, e)

lemma Rp_unique:

      [| projpair(D, E, e, p); cpo(D); cpo(E) |] ==> Rp(D, E, e) = p

lemma emb_cont:

      emb(D, E, e) ==> e ∈ cont(D, E)

lemmas Rp_cont:

      [| emb(D, E, e); cpo(D); cpo(E) |] ==> Rp(D, E, e) ∈ cont(E, D)

lemmas Rp_cont:

      [| emb(D, E, e); cpo(D); cpo(E) |] ==> Rp(D, E, e) ∈ cont(E, D)

lemmas embRp_eq:

      [| emb(D, E, e); cpo(D); cpo(E) |] ==> Rp(D, E, e) O e = id(set(D))

lemmas embRp_eq:

      [| emb(D, E, e); cpo(D); cpo(E) |] ==> Rp(D, E, e) O e = id(set(D))

lemmas embRp_rel:

      [| emb(D, E, e); cpo(D); cpo(E) |]
      ==> rel(cf(E, E), e O Rp(D, E, e), id(set(E)))

lemmas embRp_rel:

      [| emb(D, E, e); cpo(D); cpo(E) |]
      ==> rel(cf(E, E), e O Rp(D, E, e), id(set(E)))

lemma embRp_eq_thm:

      [| emb(D, E, e); x ∈ set(D); cpo(D); cpo(E) |] ==> Rp(D, E, e) ` (e ` x) = x

lemma projpair_id:

      cpo(D) ==> projpair(D, D, id(set(D)), id(set(D)))

lemma emb_id:

      cpo(D) ==> emb(D, D, id(set(D)))

lemma Rp_id:

      cpo(D) ==> Rp(D, D, id(set(D))) = id(set(D))

lemma comp_lemma:

      [| emb(D, D', e); emb(D', E, e'); cpo(D); cpo(D'); cpo(E) |]
      ==> projpair(D, E, e' O e, Rp(D, D', e) O Rp(D', E, e'))

lemmas emb_comp:

      [| emb(D, D'1, e1); emb(D'1, E, e'1); cpo(D); cpo(D'1); cpo(E) |]
      ==> emb(D, E, e'1 O e1)

lemmas emb_comp:

      [| emb(D, D'1, e1); emb(D'1, E, e'1); cpo(D); cpo(D'1); cpo(E) |]
      ==> emb(D, E, e'1 O e1)

lemmas Rp_comp:

      [| emb(D, D'1, e1); emb(D'1, E, e'1); cpo(D); cpo(D'1); cpo(E); cpo(D);
         cpo(E) |]
      ==> Rp(D, E, e'1 O e1) = Rp(D, D'1, e1) O Rp(D'1, E, e'1)

lemmas Rp_comp:

      [| emb(D, D'1, e1); emb(D'1, E, e'1); cpo(D); cpo(D'1); cpo(E); cpo(D);
         cpo(E) |]
      ==> Rp(D, E, e'1 O e1) = Rp(D, D'1, e1) O Rp(D'1, E, e'1)

lemma iprodI:

      x ∈ (Πn∈nat. set(DD ` n)) ==> x ∈ set(iprod(DD))

lemma iprodE:

      x ∈ set(iprod(DD)) ==> x ∈ (Πn∈nat. set(DD ` n))

lemma rel_iprodI:

      [| !!n. n ∈ nat ==> rel(DD ` n, f ` n, g ` n); f ∈ (Πn∈nat. set(DD ` n));
         g ∈ (Πn∈nat. set(DD ` n)) |]
      ==> rel(iprod(DD), f, g)

lemma rel_iprodE:

      [| rel(iprod(DD), f, g); n ∈ nat |] ==> rel(DD ` n, f ` n, g ` n)

lemma chain_iprod:

      [| chain(iprod(DD), X); !!n. n ∈ nat ==> cpo(DD ` n); n ∈ nat |]
      ==> chain(DD ` n, λm∈nat. X ` m ` n)

lemma islub_iprod:

      [| chain(iprod(DD), X); !!n. n ∈ nat ==> cpo(DD ` n) |]
      ==> islub(iprod(DD), X, λn∈nat. lub(DD ` n, λm∈nat. X ` m ` n))

lemma cpo_iprod:

      (!!n. n ∈ nat ==> cpo(DD ` n)) ==> cpo(iprod(DD))

lemma lub_iprod:

      [| chain(iprod(DD), X); !!n. n ∈ nat ==> cpo(DD ` n) |]
      ==> lub(iprod(DD), X) = (λn∈nat. lub(DD ` n, λm∈nat. X ` m ` n))

lemma subcpoI:

      [| set(D) ⊆ set(E);
         !!x y. [| x ∈ set(D); y ∈ set(D) |] ==> rel(D, x, y) <-> rel(E, x, y);
         !!X. chain(D, X) ==> lub(E, X) ∈ set(D) |]
      ==> subcpo(D, E)

lemma subcpo_subset:

      subcpo(D, E) ==> set(D) ⊆ set(E)

lemma subcpo_rel_eq:

      [| subcpo(D, E); x ∈ set(D); y ∈ set(D) |] ==> rel(D, x, y) <-> rel(E, x, y)

lemmas subcpo_relD1:

      [| subcpo(D1, E1); x1 ∈ set(D1); y1 ∈ set(D1); rel(D1, x1, y1) |]
      ==> rel(E1, x1, y1)

lemmas subcpo_relD1:

      [| subcpo(D1, E1); x1 ∈ set(D1); y1 ∈ set(D1); rel(D1, x1, y1) |]
      ==> rel(E1, x1, y1)

lemmas subcpo_relD2:

      [| subcpo(D1, E1); x1 ∈ set(D1); y1 ∈ set(D1); rel(E1, x1, y1) |]
      ==> rel(D1, x1, y1)

lemmas subcpo_relD2:

      [| subcpo(D1, E1); x1 ∈ set(D1); y1 ∈ set(D1); rel(E1, x1, y1) |]
      ==> rel(D1, x1, y1)

lemma subcpo_lub:

      [| subcpo(D, E); chain(D, X) |] ==> lub(E, X) ∈ set(D)

lemma chain_subcpo:

      [| subcpo(D, E); chain(D, X) |] ==> chain(E, X)

lemma ub_subcpo:

      [| subcpo(D, E); chain(D, X); isub(D, X, x) |] ==> isub(E, X, x)

lemma islub_subcpo:

      [| subcpo(D, E); cpo(E); chain(D, X) |] ==> islub(D, X, lub(E, X))

lemma subcpo_cpo:

      [| subcpo(D, E); cpo(E) |] ==> cpo(D)

lemma lub_subcpo:

      [| subcpo(D, E); cpo(E); chain(D, X) |] ==> lub(D, X) = lub(E, X)

lemma mkcpoI:

      [| x ∈ set(D); P(x) |] ==> x ∈ set(mkcpo(D, P))

lemma mkcpoD1:

      x ∈ set(mkcpo(D, P)) ==> x ∈ set(D)

lemma mkcpoD2:

      x ∈ set(mkcpo(D, P)) ==> P(x)

lemma rel_mkcpoE:

      rel(mkcpo(D, P), x, y) ==> rel(D, x, y)

lemma rel_mkcpo:

      [| x ∈ set(D); y ∈ set(D) |] ==> rel(mkcpo(D, P), x, y) <-> rel(D, x, y)

lemma chain_mkcpo:

      chain(mkcpo(D, P), X) ==> chain(D, X)

lemma subcpo_mkcpo:

      [| !!X. chain(mkcpo(D, P), X) ==> P(lub(D, X)); cpo(D) |]
      ==> subcpo(mkcpo(D, P), D)

lemma emb_chainI:

      [| !!n. n ∈ nat ==> cpo(DD ` n);
         !!n. n ∈ nat ==> emb(DD ` n, DD ` succ(n), ee ` n) |]
      ==> emb_chain(DD, ee)

lemma emb_chain_cpo:

      [| emb_chain(DD, ee); n ∈ nat |] ==> cpo(DD ` n)

lemma emb_chain_emb:

      [| emb_chain(DD, ee); n ∈ nat |] ==> emb(DD ` n, DD ` succ(n), ee ` n)

lemma DinfI:

      [| x ∈ (Πn∈nat. set(DD ` n));
         !!n. n ∈ nat ==> Rp(DD ` n, DD ` succ(n), ee ` n) ` (x ` succ(n)) = x ` n |]
      ==> x ∈ set(Dinf(DD, ee))

lemma Dinf_prod:

      x ∈ set(Dinf(DD, ee)) ==> x ∈ (Πn∈nat. set(DD ` n))

lemma Dinf_eq:

      [| x ∈ set(Dinf(DD, ee)); n ∈ nat |]
      ==> Rp(DD ` n, DD ` succ(n), ee ` n) ` (x ` succ(n)) = x ` n

lemma rel_DinfI:

      [| !!n. n ∈ nat ==> rel(DD ` n, x ` n, y ` n); x ∈ (Πn∈nat. set(DD ` n));
         y ∈ (Πn∈nat. set(DD ` n)) |]
      ==> rel(Dinf(DD, ee), x, y)

lemma rel_Dinf:

      [| rel(Dinf(DD, ee), x, y); n ∈ nat |] ==> rel(DD ` n, x ` n, y ` n)

lemma chain_Dinf:

      chain(Dinf(DD, ee), X) ==> chain(iprod(DD), X)

lemma subcpo_Dinf:

      emb_chain(DD, ee) ==> subcpo(Dinf(DD, ee), iprod(DD))

lemma cpo_Dinf:

      emb_chain(DD, ee) ==> cpo(Dinf(DD, ee))

lemma lub_Dinf:

      [| chain(Dinf(DD, ee), X); emb_chain(DD, ee) |]
      ==> lub(Dinf(DD, ee), X) = (λn∈nat. lub(DD ` n, λm∈nat. X ` m ` n))

lemma e_less_eq:

      m ∈ nat ==> e_less(DD, ee, m, m) = id(set(DD ` m))

lemma lemma_succ_sub:

      succ(m #+ n) #- m = succ(natify(n))

lemma e_less_add:

      e_less(DD, ee, m, succ(m #+ k)) = ee ` (m #+ k) O e_less(DD, ee, m, m #+ k)

lemma le_exists:

      [| m ≤ n; !!x. [| n = m #+ x; x ∈ nat |] ==> Q; n ∈ nat |] ==> Q

lemma e_less_le:

      [| m ≤ n; n ∈ nat |]
      ==> e_less(DD, ee, m, succ(n)) = ee ` n O e_less(DD, ee, m, n)

lemma e_less_succ:

      m ∈ nat ==> e_less(DD, ee, m, succ(m)) = ee ` m O id(set(DD ` m))

lemma e_less_succ_emb:

      [| !!n. n ∈ nat ==> emb(DD ` n, DD ` succ(n), ee ` n); m ∈ nat |]
      ==> e_less(DD, ee, m, succ(m)) = ee ` m

lemma emb_e_less_add:

      [| emb_chain(DD, ee); m ∈ nat |]
      ==> emb(DD ` m, DD ` (m #+ k), e_less(DD, ee, m, m #+ k))

lemma emb_e_less:

      [| m ≤ n; emb_chain(DD, ee); n ∈ nat |]
      ==> emb(DD ` m, DD ` n, e_less(DD, ee, m, n))

lemma comp_mono_eq:

      [| f = f'; g = g' |] ==> f O g = f' O g'

lemma e_less_split_add_lemma:

      [| emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat; n ≤ k |]
      ==> e_less(DD, ee, m, m #+ k) =
          e_less(DD, ee, m #+ n, m #+ k) O e_less(DD, ee, m, m #+ n)

lemma e_less_split_add:

      [| n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> e_less(DD, ee, m, m #+ k) =
          e_less(DD, ee, m #+ n, m #+ k) O e_less(DD, ee, m, m #+ n)

lemma e_gr_eq:

      m ∈ nat ==> e_gr(DD, ee, m, m) = id(set(DD ` m))

lemma e_gr_add:

      [| n ∈ nat; k ∈ nat |]
      ==> e_gr(DD, ee, succ(n #+ k), n) =
          e_gr(DD, ee, n #+ k, n) O
          Rp(DD ` (n #+ k), DD ` succ(n #+ k), ee ` (n #+ k))

lemma e_gr_le:

      [| n ≤ m; m ∈ nat; n ∈ nat |]
      ==> e_gr(DD, ee, succ(m), n) =
          e_gr(DD, ee, m, n) O Rp(DD ` m, DD ` succ(m), ee ` m)

lemma e_gr_succ:

      m ∈ nat
      ==> e_gr(DD, ee, succ(m), m) =
          id(set(DD ` m)) O Rp(DD ` m, DD ` succ(m), ee ` m)

lemma e_gr_succ_emb:

      [| emb_chain(DD, ee); m ∈ nat |]
      ==> e_gr(DD, ee, succ(m), m) = Rp(DD ` m, DD ` succ(m), ee ` m)

lemma e_gr_fun_add:

      [| emb_chain(DD, ee); n ∈ nat; k ∈ nat |]
      ==> e_gr(DD, ee, n #+ k, n) ∈ set(DD ` (n #+ k)) -> set(DD ` n)

lemma e_gr_fun:

      [| n ≤ m; emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> e_gr(DD, ee, m, n) ∈ set(DD ` m) -> set(DD ` n)

lemma e_gr_split_add_lemma:

      [| emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> m ≤ k -->
          e_gr(DD, ee, n #+ k, n) =
          e_gr(DD, ee, n #+ m, n) O e_gr(DD, ee, n #+ k, n #+ m)

lemma e_gr_split_add:

      [| m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> e_gr(DD, ee, n #+ k, n) =
          e_gr(DD, ee, n #+ m, n) O e_gr(DD, ee, n #+ k, n #+ m)

lemma e_less_cont:

      [| m ≤ n; emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> e_less(DD, ee, m, n) ∈ cont(DD ` m, DD ` n)

lemma e_gr_cont:

      [| n ≤ m; emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> e_gr(DD, ee, m, n) ∈ cont(DD ` m, DD ` n)

lemma e_less_e_gr_split_add:

      [| n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> e_less(DD, ee, m, m #+ n) =
          e_gr(DD, ee, m #+ k, m #+ n) O e_less(DD, ee, m, m #+ k)

lemma e_gr_e_less_split_add:

      [| m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> e_gr(DD, ee, n #+ m, n) =
          e_gr(DD, ee, n #+ k, n) O e_less(DD, ee, n #+ m, n #+ k)

lemma emb_eps:

      [| m ≤ n; emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> emb(DD ` m, DD ` n, eps(DD, ee, m, n))

lemma eps_fun:

      [| emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> eps(DD, ee, m, n) ∈ set(DD ` m) -> set(DD ` n)

lemma eps_id:

      n ∈ nat ==> eps(DD, ee, n, n) = id(set(DD ` n))

lemma eps_e_less_add:

      [| m ∈ nat; n ∈ nat |] ==> eps(DD, ee, m, m #+ n) = e_less(DD, ee, m, m #+ n)

lemma eps_e_less:

      [| m ≤ n; m ∈ nat; n ∈ nat |] ==> eps(DD, ee, m, n) = e_less(DD, ee, m, n)

lemma eps_e_gr_add:

      [| n ∈ nat; k ∈ nat |] ==> eps(DD, ee, n #+ k, n) = e_gr(DD, ee, n #+ k, n)

lemma eps_e_gr:

      [| n ≤ m; m ∈ nat; n ∈ nat |] ==> eps(DD, ee, m, n) = e_gr(DD, ee, m, n)

lemma eps_succ_ee:

      [| !!n. n ∈ nat ==> emb(DD ` n, DD ` succ(n), ee ` n); m ∈ nat |]
      ==> eps(DD, ee, m, succ(m)) = ee ` m

lemma eps_succ_Rp:

      [| emb_chain(DD, ee); m ∈ nat |]
      ==> eps(DD, ee, succ(m), m) = Rp(DD ` m, DD ` succ(m), ee ` m)

lemma eps_cont:

      [| emb_chain(DD, ee); m ∈ nat; n ∈ nat |]
      ==> eps(DD, ee, m, n) ∈ cont(DD ` m, DD ` n)

lemma eps_split_add_left:

      [| n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, m #+ k) =
          eps(DD, ee, m #+ n, m #+ k) O eps(DD, ee, m, m #+ n)

lemma eps_split_add_left_rev:

      [| n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, m #+ n) =
          eps(DD, ee, m #+ k, m #+ n) O eps(DD, ee, m, m #+ k)

lemma eps_split_add_right:

      [| m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, n #+ k, n) =
          eps(DD, ee, n #+ m, n) O eps(DD, ee, n #+ k, n #+ m)

lemma eps_split_add_right_rev:

      [| m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, n #+ m, n) =
          eps(DD, ee, n #+ k, n) O eps(DD, ee, n #+ m, n #+ k)

lemma le_exists_lemma:

      [| n ≤ k; k ≤ m;
         !!p q. [| p ≤ q; k = n #+ p; m = n #+ q; p ∈ nat; q ∈ nat |] ==> R;
         m ∈ nat |]
      ==> R

lemma eps_split_left_le:

      [| m ≤ k; k ≤ n; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma eps_split_left_le_rev:

      [| m ≤ n; n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma eps_split_right_le:

      [| n ≤ k; k ≤ m; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma eps_split_right_le_rev:

      [| n ≤ m; m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma eps_split_left:

      [| m ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma eps_split_right:

      [| n ≤ k; emb_chain(DD, ee); m ∈ nat; n ∈ nat; k ∈ nat |]
      ==> eps(DD, ee, m, n) = eps(DD, ee, k, n) O eps(DD, ee, m, k)

lemma rho_emb_fun:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> rho_emb(DD, ee, n) ∈ set(DD ` n) -> set(Dinf(DD, ee))

lemma rho_emb_apply1:

      x ∈ set(DD ` n) ==> rho_emb(DD, ee, n) ` x = (λm∈nat. eps(DD, ee, n, m) ` x)

lemma rho_emb_apply2:

      [| x ∈ set(DD ` n); m ∈ nat |]
      ==> rho_emb(DD, ee, n) ` x ` m = eps(DD, ee, n, m) ` x

lemma rho_emb_id:

      [| x ∈ set(DD ` n); n ∈ nat |] ==> rho_emb(DD, ee, n) ` x ` n = x

lemma rho_emb_cont:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> rho_emb(DD, ee, n) ∈ cont(DD ` n, Dinf(DD, ee))

lemma eps1_aux1:

      [| m ≤ n; emb_chain(DD, ee); x ∈ set(Dinf(DD, ee)); m ∈ nat; n ∈ nat |]
      ==> rel(DD ` n, e_less(DD, ee, m, n) ` (x ` m), x ` n)

lemma eps1_aux2:

      [| n ≤ m; emb_chain(DD, ee); x ∈ set(Dinf(DD, ee)); m ∈ nat; n ∈ nat |]
      ==> rel(DD ` n, e_gr(DD, ee, m, n) ` (x ` m), x ` n)

lemma eps1:

      [| emb_chain(DD, ee); x ∈ set(Dinf(DD, ee)); m ∈ nat; n ∈ nat |]
      ==> rel(DD ` n, eps(DD, ee, m, n) ` (x ` m), x ` n)

lemma lam_Dinf_cont:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> (λx∈set(Dinf(DD, ee)). x ` n) ∈ cont(Dinf(DD, ee), DD ` n)

lemma rho_projpair:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> projpair(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n), rho_proj(DD, ee, n))

lemma emb_rho_emb:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> emb(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n))

lemma rho_proj_cont:

      [| emb_chain(DD, ee); n ∈ nat |]
      ==> rho_proj(DD, ee, n) ∈ cont(Dinf(DD, ee), DD ` n)

lemma commuteI:

      [| !!n. n ∈ nat ==> emb(DD ` n, E, r(n));
         !!m n. [| m ≤ n; m ∈ nat; n ∈ nat |] ==> r(n) O eps(DD, ee, m, n) = r(m) |]
      ==> commute(DD, ee, E, r)

lemma commute_emb:

      [| commute(DD, ee, E, r); n ∈ nat |] ==> emb(DD ` n, E, r(n))

lemma commute_eq:

      [| commute(DD, ee, E, r); m ≤ n; m ∈ nat; n ∈ nat |]
      ==> r(n) O eps(DD, ee, m, n) = r(m)

lemma rho_emb_commute:

      emb_chain(DD, ee) ==> commute(DD, ee, Dinf(DD, ee), rho_emb(DD, ee))

lemma le_succ:

      n ∈ nat ==> n ≤ succ(n)

lemma commute_chain:

      [| commute(DD, ee, E, r); emb_chain(DD, ee); cpo(E) |]
      ==> chain(cf(E, E), λn∈nat. r(n) O Rp(DD ` n, E, r(n)))

lemma rho_emb_chain:

      emb_chain(DD, ee)
      ==> chain(cf(Dinf(DD, ee), Dinf(DD, ee)),
                λn∈nat.
                   rho_emb(DD, ee, n) O Rp(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n)))

lemma rho_emb_chain_apply1:

      [| emb_chain(DD, ee); x ∈ set(Dinf(DD, ee)) |]
      ==> chain(Dinf(DD, ee),
                λn∈nat.
                   (rho_emb(DD, ee, n) O
                    Rp(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n))) `
                   x)

lemma chain_iprod_emb_chain:

      [| chain(iprod(DD), X); emb_chain(DD, ee); n ∈ nat |]
      ==> chain(DD ` n, λm∈nat. X ` m ` n)

lemma rho_emb_chain_apply2:

      [| emb_chain(DD, ee); x ∈ set(Dinf(DD, ee)); n ∈ nat |]
      ==> chain(DD ` n,
                λxa∈nat.
                   (rho_emb(DD, ee, xa) O
                    Rp(DD ` xa, Dinf(DD, ee), rho_emb(DD, ee, xa))) `
                   x `
                   n)

lemma rho_emb_lub:

      emb_chain(DD, ee)
      ==> lub(cf(Dinf(DD, ee), Dinf(DD, ee)),
              λn∈nat.
                 rho_emb(DD, ee, n) O Rp(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n))) =
          id(set(Dinf(DD, ee)))

lemma theta_chain:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> chain(cf(E, G), λn∈nat. f(n) O Rp(DD ` n, E, r(n)))

lemma theta_proj_chain:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> chain(cf(G, E), λn∈nat. r(n) O Rp(DD ` n, G, f(n)))

lemma commute_O_lemma:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G); x ∈ nat |]
      ==> r(x) O Rp(DD ` x, G, f(x)) O f(x) O Rp(DD ` x, E, r(x)) =
          r(x) O Rp(DD ` x, E, r(x))

lemma theta_projpair:

      [| lub(cf(E, E), λn∈nat. r(n) O Rp(DD ` n, E, r(n))) = id(set(E));
         commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> projpair
           (E, G, lub(cf(E, G), λn∈nat. f(n) O Rp(DD ` n, E, r(n))),
            lub(cf(G, E), λn∈nat. r(n) O Rp(DD ` n, G, f(n))))

lemma emb_theta:

      [| lub(cf(E, E), λn∈nat. r(n) O Rp(DD ` n, E, r(n))) = id(set(E));
         commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> emb(E, G, lub(cf(E, G), λn∈nat. f(n) O Rp(DD ` n, E, r(n))))

lemma mono_lemma:

      [| g ∈ cont(D, D'); cpo(D); cpo(D'); cpo(E) |]
      ==> (λf∈cont(D', E). f O g) ∈ mono(cf(D', E), cf(D, E))

lemma commute_lam_lemma:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G); n ∈ nat |]
      ==> (λna∈nat.
              (λf∈cont(E, G). f O r(n)) `
              ((λn∈nat. f(n) O Rp(DD ` n, E, r(n))) ` na)) =
          (λna∈nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))

lemma chain_lemma:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G); n ∈ nat |]
      ==> chain(cf(DD ` n, G), λx∈nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))

lemma suffix_lemma:

      [| commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G); cpo(DD ` x); x ∈ nat |]
      ==> suffix(λn∈nat. (f(n) O Rp(DD ` n, E, r(n))) O r(x), x) = (λn∈nat. f(x))

lemma mediatingI:

      [| emb(E, G, t); !!n. n ∈ nat ==> f(n) = t O r(n) |]
      ==> mediating(E, G, r, f, t)

lemma mediating_emb:

      mediating(E, G, r, f, t) ==> emb(E, G, t)

lemma mediating_eq:

      [| mediating(E, G, r, f, t); n ∈ nat |] ==> f(n) = t O r(n)

lemma lub_universal_mediating:

      [| lub(cf(E, E), λn∈nat. r(n) O Rp(DD ` n, E, r(n))) = id(set(E));
         commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> mediating(E, G, r, f, lub(cf(E, G), λn∈nat. f(n) O Rp(DD ` n, E, r(n))))

lemma lub_universal_unique:

      [| mediating(E, G, r, f, t);
         lub(cf(E, E), λn∈nat. r(n) O Rp(DD ` n, E, r(n))) = id(set(E));
         commute(DD, ee, E, r); commute(DD, ee, G, f); emb_chain(DD, ee); cpo(E);
         cpo(G) |]
      ==> t = lub(cf(E, G), λn∈nat. f(n) O Rp(DD ` n, E, r(n)))

theorem Dinf_universal:

      [| commute(DD, ee, G, f); emb_chain(DD, ee); cpo(G) |]
      ==> mediating
           (Dinf(DD, ee), G, rho_emb(DD, ee), f,
            lub(cf(Dinf(DD, ee), G),
                λn∈nat. f(n) O Rp(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n)))) ∧
          (∀t. mediating(Dinf(DD, ee), G, rho_emb(DD, ee), f, t) -->
               t = lub(cf(Dinf(DD, ee), G),
                       λn∈nat. f(n) O Rp(DD ` n, Dinf(DD, ee), rho_emb(DD, ee, n))))