src/ZF/ex/Limit.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 1281 68f6be60ab1c
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/ex/Limit
     2     ID:         $Id$
     3     Author: 	Sten Agerholm
     4 
     5     A formalization of the inverse limit construction of domain theory.
     6 
     7     The following paper comments on the formalization:
     8 
     9     "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
    10     In Proceedings of the First Isabelle Users Workshop, Technical 
    11     Report No. 379, University of Cambridge Computer Laboratory, 1995.
    12 
    13     This is a condensed version of:
    14 
    15     "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
    16     Technical Report No. 369, University of Cambridge Computer 
    17     Laboratory, 1995.
    18 *)
    19 
    20 Limit  =  ZF + Perm + Arith +
    21 
    22 consts
    23 
    24   "rel" :: [i,i,i]=>o                 (* rel(D,x,y) *)
    25   "set" :: i=>i                       (* set(D) *)
    26   "po"  :: i=>o                       (* po(D) *)
    27   "chain" :: [i,i]=>o                 (* chain(D,X) *)
    28   "isub" :: [i,i,i]=>o                (* isub(D,X,x) *)
    29   "islub" :: [i,i,i]=>o               (* islub(D,X,x) *)
    30   "lub" :: [i,i]=>i                   (* lub(D,X) *)
    31   "cpo" :: i=>o                       (* cpo(D) *)
    32   "pcpo" :: i=>o                      (* pcpo(D) *)
    33   "bot" :: i=>i                       (* bot(D) *)
    34   "mono" :: [i,i]=>i                  (* mono(D,E) *)
    35   "cont" :: [i,i]=>i                  (* cont(D,E) *)
    36   "cf" :: [i,i]=>i                    (* cf(D,E) *)
    37 
    38   "suffix" :: [i,i]=>i                (* suffix(X,n) *)
    39   "subchain" :: [i,i]=>o              (* subchain(X,Y) *)
    40   "dominate" :: [i,i,i]=>o            (* dominate(D,X,Y) *)
    41   "matrix" :: [i,i]=>o                (* matrix(D,M) *)
    42 
    43   "projpair"  :: [i,i,i,i]=>o         (* projpair(D,E,e,p) *)
    44   "emb"       :: [i,i,i]=>o           (* emb(D,E,e) *)
    45   "Rp"        :: [i,i,i]=>i           (* Rp(D,E,e) *)
    46   "iprod"     :: i=>i                 (* iprod(DD) *)
    47   "mkcpo"     :: [i,i=>o]=>i          (* mkcpo(D,P) *)
    48   "subcpo"    :: [i,i]=>o             (* subcpo(D,E) *)
    49   "subpcpo"   :: [i,i]=>o             (* subpcpo(D,E) *)
    50 
    51   "emb_chain" :: [i,i]=>o             (* emb_chain(DD,ee) *)
    52   "Dinf"      :: [i,i]=>i             (* Dinf(DD,ee) *)
    53 
    54   "e_less"    :: [i,i,i,i]=>i         (* e_less(DD,ee,m,n) *)
    55   "e_gr"      :: [i,i,i,i]=>i         (* e_gr(DD,ee,m,n) *)
    56   "eps"       :: [i,i,i,i]=>i         (* eps(DD,ee,m,n) *)
    57   "rho_emb"   :: [i,i,i]=>i           (* rho_emb(DD,ee,n) *)
    58   "rho_proj"  :: [i,i,i]=>i           (* rho_proj(DD,ee,n) *)
    59   "commute"   :: [i,i,i,i=>i]=>o      (* commute(DD,ee,E,r) *)
    60   "mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *)
    61 
    62 rules
    63 
    64   set_def
    65     "set(D) == fst(D)"
    66 
    67   rel_def
    68     "rel(D,x,y) == <x,y>:snd(D)" 
    69   
    70   po_def
    71     "po(D) ==   \
    72 \    (ALL x:set(D). rel(D,x,x)) &   \
    73 \    (ALL x:set(D). ALL y:set(D). ALL z:set(D).   \
    74 \      rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) &   \
    75 \    (ALL x:set(D). ALL y:set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"
    76 
    77     (* Chains are object level functions nat->set(D) *)
    78 
    79   chain_def
    80     "chain(D,X) == X:nat->set(D) & (ALL n:nat. rel(D,X`n,X`(succ(n))))"
    81 
    82   isub_def
    83     "isub(D,X,x) == x:set(D) & (ALL n:nat. rel(D,X`n,x))"
    84 
    85   islub_def
    86     "islub(D,X,x) == isub(D,X,x) & (ALL y. isub(D,X,y) --> rel(D,x,y))"
    87 
    88   lub_def
    89     "lub(D,X) == THE x. islub(D,X,x)"
    90 
    91   cpo_def
    92     "cpo(D) == po(D) & (ALL X. chain(D,X) --> (EX x. islub(D,X,x)))"
    93 
    94   pcpo_def
    95     "pcpo(D) == cpo(D) & (EX x:set(D). ALL y:set(D). rel(D,x,y))"
    96   
    97   bot_def
    98     "bot(D) == THE x. x:set(D) & (ALL y:set(D). rel(D,x,y))"
    99 
   100   
   101   mono_def
   102     "mono(D,E) ==   \
   103 \    {f:set(D)->set(E).   \
   104 \     ALL x:set(D). ALL y:set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"
   105 
   106   cont_def
   107     "cont(D,E) ==   \
   108 \    {f:mono(D,E).   \
   109 \     ALL X. chain(D,X) --> f`(lub(D,X)) = lub(E,lam n:nat. f`(X`n))}" 
   110   
   111   cf_def
   112     "cf(D,E) ==   \
   113 \    <cont(D,E),   \
   114 \     {y:cont(D,E)*cont(D,E). ALL x:set(D). rel(E,(fst(y))`x,(snd(y))`x)}>"
   115 
   116   suffix_def
   117     "suffix(X,n) == lam m:nat. X`(n #+ m)"
   118 
   119   subchain_def
   120     "subchain(X,Y) == ALL m:nat. EX n:nat. X`m = Y`(m #+ n)"
   121 
   122   dominate_def
   123     "dominate(D,X,Y) == ALL m:nat. EX n:nat. rel(D,X`m,Y`n)"
   124 
   125   matrix_def
   126     "matrix(D,M) ==   \
   127 \    M: nat -> (nat -> set(D)) &   \
   128 \    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`succ(n)`m)) &   \
   129 \    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`n`succ(m))) &   \
   130 \    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`succ(n)`succ(m)))"
   131 
   132   projpair_def
   133     "projpair(D,E,e,p) ==   \
   134 \    e:cont(D,E) & p:cont(E,D) &   \
   135 \    p O e = id(set(D)) & rel(cf(E,E),e O p,id(set(E)))"
   136 
   137   emb_def
   138     "emb(D,E,e) == EX p. projpair(D,E,e,p)"
   139 
   140   Rp_def
   141     "Rp(D,E,e) == THE p. projpair(D,E,e,p)"
   142 
   143 (* Twice, constructions on cpos are more difficult. *)
   144 
   145   iprod_def
   146     "iprod(DD) ==   \
   147 \    <(PROD n:nat. set(DD`n)),  \
   148 \     {x:(PROD n:nat. set(DD`n))*(PROD n:nat. set(DD`n)).   \
   149 \      ALL n:nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
   150 
   151   mkcpo_def   (* Cannot use rel(D), is meta fun, need two more args *)
   152     "mkcpo(D,P) ==   \
   153 \    <{x:set(D). P(x)},{x:set(D)*set(D). rel(D,fst(x),snd(x))}>"
   154 
   155 
   156   subcpo_def
   157     "subcpo(D,E) ==   \
   158 \    set(D) <= set(E) &   \
   159 \    (ALL x:set(D). ALL y:set(D). rel(D,x,y) <-> rel(E,x,y)) &   \
   160 \    (ALL X. chain(D,X) --> lub(E,X):set(D))"
   161 
   162   subpcpo_def
   163     "subpcpo(D,E) == subcpo(D,E) & bot(E):set(D)"
   164 
   165   emb_chain_def
   166     "emb_chain(DD,ee) ==   \
   167 \    (ALL n:nat. cpo(DD`n)) & (ALL n:nat. emb(DD`n,DD`succ(n),ee`n))"
   168 
   169   Dinf_def
   170     "Dinf(DD,ee) ==   \
   171 \    mkcpo(iprod(DD))   \
   172 \    (%x. ALL n:nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)"
   173 
   174   e_less_def (* Valid for m le n only. *)
   175     "e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)"
   176 
   177   e_gr_def (* Valid for n le m only. *)
   178     "e_gr(DD,ee,m,n) ==   \
   179 \    rec(m#-n,id(set(DD`n)),   \
   180 \        %x y. y O Rp(DD`(n#+x),DD`(succ(n#+x)),ee`(n#+x)))"
   181 
   182   eps_def
   183     "eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
   184 
   185   rho_emb_def
   186     "rho_emb(DD,ee,n) == lam x:set(DD`n). lam m:nat. eps(DD,ee,n,m)`x"
   187 
   188   rho_proj_def
   189     "rho_proj(DD,ee,n) == lam x:set(Dinf(DD,ee)). x`n"
   190   
   191   commute_def
   192     "commute(DD,ee,E,r) ==   \
   193 \    (ALL n:nat. emb(DD`n,E,r(n))) &   \
   194 \    (ALL m:nat. ALL n:nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"
   195 
   196   mediating_def
   197     "mediating(E,G,r,f,t) == emb(E,G,t) & (ALL n:nat. f(n) = t O r(n))"
   198 
   199 end