project image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      ZF/ex/Limit.thy
    Author:     Sten Agerholm
    Author:     Lawrence C Paulson

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.
*)

theory Limit  imports  ZF begin

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

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

definition
  po  :: "i=>o"  where
    "po(D) ==
     (\<forall>x \<in> set(D). rel(D,x,x)) &
     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). \<forall>z \<in> set(D).
       rel(D,x,y) \<longrightarrow> rel(D,y,z) \<longrightarrow> rel(D,x,z)) &
     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(D,y,x) \<longrightarrow> x = y)"

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

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

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

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

definition
  cpo :: "i=>o"  where
    "cpo(D) == po(D) & (\X. chain(D,X) \ (\x. islub(D,X,x)))"

definition
  pcpo :: "i=>o"  where
    "pcpo(D) == cpo(D) & (\x \ set(D). \y \ set(D). rel(D,x,y))"

definition
  bot :: "i=>i"  where
    "bot(D) == THE x. x \ set(D) & (\y \ set(D). rel(D,x,y))"

definition
  mono :: "[i,i]=>i"  where
    "mono(D,E) ==
     {f \<in> set(D)->set(E).
      \<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(E,f`x,f`y)}"

definition
  cont :: "[i,i]=>i"  where
    "cont(D,E) ==
     {f \<in> mono(D,E).
      \<forall>X. chain(D,X) \<longrightarrow> f`(lub(D,X)) = lub(E,\<lambda>n \<in> nat. f`(X`n))}"

definition
  cf :: "[i,i]=>i"  where
    "cf(D,E) ==
     <cont(D,E),
      {y \<in> cont(D,E)*cont(D,E). \<forall>x \<in> set(D). rel(E,(fst(y))`x,(snd(y))`x)}>"

definition
  suffix :: "[i,i]=>i"  where
    "suffix(X,n) == \m \ nat. X`(n #+ m)"

definition
  subchain :: "[i,i]=>o"  where
    "subchain(X,Y) == \m \ nat. \n \ nat. X`m = Y`(m #+ n)"

definition
  dominate :: "[i,i,i]=>o"  where
    "dominate(D,X,Y) == \m \ nat. \n \ nat. rel(D,X`m,Y`n)"

definition
  matrix :: "[i,i]=>o"  where
    "matrix(D,M) ==
     M \<in> nat -> (nat -> set(D)) &
     (\<forall>n \<in> nat. \<forall>m \<in> nat. rel(D,M`n`m,M`succ(n)`m)) &
     (\<forall>n \<in> nat. \<forall>m \<in> nat. rel(D,M`n`m,M`n`succ(m))) &
     (\<forall>n \<in> nat. \<forall>m \<in> nat. rel(D,M`n`m,M`succ(n)`succ(m)))"

definition
  projpair  :: "[i,i,i,i]=>o"  where
    "projpair(D,E,e,p) ==
     e \<in> cont(D,E) & p \<in> cont(E,D) &
     p O e = id(set(D)) & rel(cf(E,E),e O p,id(set(E)))"

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

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

definition
  (* Twice, constructions on cpos are more difficult. *)
  iprod     :: "i=>i"  where
    "iprod(DD) ==
     <(\<Prod>n \<in> nat. set(DD`n)),
      {x:(\<Prod>n \<in> nat. set(DD`n))*(\<Prod>n \<in> nat. set(DD`n)).
       \<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"

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

definition
  subcpo    :: "[i,i]=>o"  where
    "subcpo(D,E) ==
     set(D) \<subseteq> set(E) &
     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longleftrightarrow> rel(E,x,y)) &an>
     (\<forall>X. chain(D,X) \<longrightarrow> lub(E,X):set(D))"

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

definition
  emb_chain :: "[i,i]=>o"  where
    "emb_chain(DD,ee) ==
     (\<forall>n \<in> nat. cpo(DD`n)) & (\<forall>n \<in> nat. emb(DD`n,DD`succ(n),ee`n))"

definition
  Dinf      :: "[i,i]=>i"  where
    "Dinf(DD,ee) ==
     mkcpo(iprod(DD))
     (%x. \<forall>n \<in> nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)"

definition
  e_less    :: "[i,i,i,i]=>i"  where
  (* 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)"


definition
  e_gr      :: "[i,i,i,i]=>i"  where
  (* 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)))"


definition
  eps       :: "[i,i,i,i]=>i"  where
    "eps(DD,ee,m,n) == if(m \ n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"

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

definition
  rho_proj  :: "[i,i,i]=>i"  where
    "rho_proj(DD,ee,n) == \x \ set(Dinf(DD,ee)). x`n"

definition
  commute   :: "[i,i,i,i=>i]=>o"  where
    "commute(DD,ee,E,r) ==
     (\<forall>n \<in> nat. emb(DD`n,E,r(n))) &
     (\<forall>m \<in> nat. \<forall>n \<in> nat. m \<le> n \<longrightarrow> r(n) O eps(DD,ee,m,n) = r(m))"

definition
  mediating :: "[i,i,i=>i,i=>i,i]=>o"  where
    "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: ":snd(D) ==> rel(D,x,y)"
by (simp add: rel_def)

lemma rel_E: "rel(D,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 \<in> set(D); z \<in> 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 \<in> set(D); y \<in> set(D); z \<in> set(D)|]
               ==> rel(D,x,z);
      !!x y. [| rel(D,x,y); rel(D,y,x); x \<in> set(D); y \<in> 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 \<in> set(D); z \<in> 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 \ 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 \<in> nat->set(D); Y \<in> 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 \<in> nat->set(D); Y \<in> 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 \<in> nat->set(D); Y \<in> 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)"
proof -
  {
    fix n m assume "n \ nat" "m \ nat"
    with chain_rel [OF yprem]
    have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp
  } note rel_succ = this
  show "matrix(D,M)"
  proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI)
    fix n m assume n: "n \ nat" and m: "m \ nat"
    thus "rel(D, M ` n ` m, M ` n ` succ(m))"
      by (simp add: chain_rel xprem)
  next
    fix n m assume n: "n \ nat" and m: "m \ nat"
    thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))"
      by (rule cpo_trans [OF cpoD rel_succ],
          simp_all add: chain_fun [THEN apply_type] xprem)
  qed
qed

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, \<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m), y)"
proof (simp add: isub_def, safe)
  fix n
  assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \ nat" and y: "y \ set(D)"
     and rel: "\n\nat. rel(D, M ` n ` n, y)"
  have "rel(D, lub(D, M ` n), y)"
  proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM)
    show "isub(D, M ` n, y)"
      proof (unfold isub_def, intro conjI ballI y)
        fix k assume k: "k \ nat"
        show "rel(D, M ` n ` k, y)"
          proof (cases "n \ k")
            case True
            hence yy: "rel(D, M`n`k, M`k`k)"
              by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right)
            show "?thesis"
              by (rule cpo_trans [OF D yy],
                  simp_all add: k rel n y DM matrix_in)
          next
            case False
            hence le: "k \ n"
              by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k)
            show "?thesis"
              by (rule cpo_trans [OF D chain_rel_gen [OF le]],
                  simp_all add: n y k rel DM D matrix_chain_left)
          qed
        qed
  qed
  moreover
  have "M ` n \ nat \ set(D)" by (blast intro: DM n matrix_fun [THEN apply_type])
  ultimately show "rel(D, lub(D, Lambda(nat, (`)(M ` n))), y)"  by simp
qed

lemma matrix_chain_lub:
    "[|matrix(D,M); cpo(D)|] ==> chain(D,\n \ nat. lub(D,\m \ nat. M`n`m))"
proof (simp add: chain_def, intro conjI ballI)
  assume "matrix(D, M)" "cpo(D)"
  thus "(\x\nat. lub(D, Lambda(nat, (`)(M ` x)))) \ nat \ set(D)"
    by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1)
next
  fix n
  assume DD: "matrix(D, M)" "cpo(D)" "n \ nat"
  hence "dominate(D, M ` n, M ` succ(n))"
    by (force simp add: dominate_def intro: matrix_rel_1_0)
  with DD show "rel(D, lub(D, Lambda(nat, (`)(M ` n))),
               lub(D, Lambda(nat, (`)(M ` succ(n)))))"
    by (simp add: matrix_chain_left [THEN chain_fun, THEN eta]
      dominate_islub cpo_lub matrix_chain_left chain_fun)
qed

lemma isub_eq:
  assumes DM: "matrix(D, M)" and D: "cpo(D)"
  shows "isub(D,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) \ isub(D,(\n \ nat. M`n`n),y)"
proof
  assume isub: "isub(D, \n\nat. lub(D, Lambda(nat, (`)(M ` n))), y)"
  hence dom: "dominate(D, \n\nat. M ` n ` n, \n\nat. lub(D, Lambda(nat, (`)(M ` n))))"
    using DM D
    by (simp add: dominate_def, intro ballI bexI,
        simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left)
  thus "isub(D, \n\nat. M ` n ` n, y)" using DM D
    by - (rule dominate_isub [OF dom isub],
          simp_all add: matrix_chain_diag chain_fun matrix_chain_lub)
next
  assume isub: "isub(D, \n\nat. M ` n ` n, y)"
  thus "isub(D, \n\nat. lub(D, Lambda(nat, (`)(M ` n))), y)" using DM D
    by (simp add: isub_lemma)
qed

lemma lub_matrix_diag_aux1:
    "lub(D,(\n \ nat. lub(D,\m \ nat. M`n`m))) =
     (THE x. islub(D, (\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> 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, (\<lambda>n \<in> nat. M`n`n), x))"
by (simp add: lub_def)

lemma lub_matrix_diag:
    "[|matrix(D,M); cpo(D)|]
     ==> lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
         lub(D,(\<lambda>n \<in> 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,(\<lambda>m \<in> nat. lub(D,\<lambda>n \<in> nat. M`n`m))) =
         lub(D,(\<lambda>n \<in> 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 \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y)|]
     ==> f \<in> 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 \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y);
       !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\<lambda>n \<in> nat. f`(X`n))|]
     ==> f \<in> 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,\<lambda>x \<in> nat. \<lambda>xa \<in> nat. X`x`(Xa`xa))"
apply (rule matrix_chainI, auto)
apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono)
apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont rel_cf)
apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in)
done

lemma chain_cf_lub_cont:
  assumes ch: "chain(cf(D,E),X)" and D: "cpo(D)" and E: "cpo(E)"
  shows   "(\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ cont(D, E)"
proof (rule contI)
  show "(\x\set(D). lub(E, \n\nat. X ` n ` x)) \ set(D) \ set(E)"
    by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E)
next
  fix x y
  assume xy: "rel(D, x, y)" "x \ set(D)" "y \ set(D)"
  hence dom: "dominate(E, \n\nat. X ` n ` x, \n\nat. X ` n ` y)"
    by (force intro: dominateI  chain_in [OF ch, THEN cf_cont, THEN cont_mono])
  note chE = chain_cf [OF ch]
  from xy show "rel(E, (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` x,
                       (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` y)"
    by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE])
next
  fix Y
  assume chDY: "chain(D,Y)"
  have "lub(E, \x\nat. lub(E, \y\nat. X ` x ` (Y ` y))) =
        lub(E, \<lambda>x\<in>nat. X ` x ` (Y ` x))"
    using matrix_lemma [THEN lub_matrix_diag, OF ch chDY]
    by (simp add: D E)
   also have "... = lub(E, \x\nat. lub(E, \n\nat. X ` n ` (Y ` x)))"
    using  matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY]
    by (simp add: D E)
  finally have "lub(E, \x\nat. lub(E, \n\nat. X ` x ` (Y ` n))) =
                lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))" .
  thus "(\x\set(D). lub(E, \n\nat. X ` n ` x)) ` lub(D, Y) =
        lub(E, \<lambda>n\<in>nat. (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` (Y ` n))"
    by (simp add: cpo_lub [THEN islub_in]  D chDY
                  chain_in [THEN cf_cont, THEN cont_lub, OF ch])
  qed

lemma islub_cf:
    "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
     ==> islub(cf(D,E), X, \<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> 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) = (\<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> 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),\<lambda>n \<in> 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),\<lambda>n \<in> 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 \<in> 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\<open>Proof's very like the previous one.  Is there a pattern that
      could be exploited?\<close>
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]
lemmas embRp_eq = embRp [THEN projpair_eq]
lemmas embRp_rel = embRp [THEN projpair_rel]


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:(\<Prod>n \<in> 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,\<lambda>m \<in> 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,\<lambda>n \<in> nat. lub(DD`n,\<lambda>m \<in> 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) = (\<lambda>n \<in> nat. lub(DD`n,\<lambda>m \<in> 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 \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)\<longleftrightarrow>rel(E,x,y);
       !!X. chain(D,X) ==> lub(E,X) \<in> 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 \<in> 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 \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
     ==> x \<in> 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:(\<Prod>n \<in> nat. set(DD`n)); y:(\<Prod>n \<in> 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)
  \<comment> \<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
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) = (\<lambda>n \<in> nat. lub(DD`n,\<lambda>m \<in> 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 \ n; !!x. [|n=m#+x; x \ nat|] ==> Q; n \ nat |] ==> Q"
apply (drule less_imp_succ_add, auto)
done

lemma e_less_le: "[| m \ 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 \ 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 \<longrightarrow>
         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 \ 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 \ 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 \ 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 \<longrightarrow>
         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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ k; k \ m;
        !!p q. [|p \<le> q; k=n#+p; m=n#+q; p \<in> nat; q \<in> nat|] ==> R;
        m \<in> 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 \ 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)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_left)
done

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)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_left_rev)
done

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)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_right)
done

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)"
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 \ 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 \ 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)
    \<comment> \<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
       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]
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.72Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff