helm/software/lambda-delta/automath/grundlagen_pn.aut

   1 # Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
   2 # Copyright (C) 1977, L.S. van Benthem Jutting
   3 #               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
   4
   5 +l
   6 [a:PROP][b:PROP]
   7 imp:=[x,a]b:PROP
   8 @con:=PRIM:PROP
   9 a@not:=imp(con):PROP
  10 wel:=not(not(a)):PROP
  11 [w:wel(a)]
  12 et:=PRIM:a
  13 b@ec:=imp(a,not(b)):PROP
  14 and:=not(ec(a,b)):PROP
  15 @[sigma:TYPE][p:[x,sigma]PROP]
  16 all:=p:PROP
  17 non:=[x,sigma]not(<x>p):[x,sigma]PROP
  18 some:=not(non(p)):PROP
  19 +e
  20 sigma@[s:sigma][t:sigma]
  21 is:=PRIM:PROP
  22 s@refis:=PRIM:is(s,s)
  23 p@[s:sigma][t:sigma][sp:<s>p][i:is(s,t)]
  24 isp:=PRIM:<t>p
  25 p@amone:=[x,sigma][y,sigma][u,<x>p][v,<y>p]is(x,y):PROP
  26 one:=and(amone(sigma,p),some(sigma,p)):PROP
  27 [o1:one(sigma,p)]
  28 ind:=PRIM:sigma
  29 oneax:=PRIM:<ind>p
  30 sigma@[tau:TYPE][f:[x,sigma]tau]
  31 injective:=all([x,sigma]all([y,sigma]imp(is(tau,<x>f,<y>f),is(x,y)))):PROP
  32 [t0:tau]
  33 image:=some([x,sigma]is(tau,t0,<x>f)):PROP
  34 tau@[f:[x,sigma]tau][g:[x,sigma]tau][i:[x,sigma]is(tau,<x>f,<x>g)]
  35 fisi:=PRIM:is([x,sigma]tau,f,g)
  36 p@ot:=PRIM:TYPE
  37 [o1:ot]
  38 in:=PRIM:sigma
  39 inp:=PRIM:<in>p
  40 p@otax1:=PRIM:injective(ot,sigma,[x,ot]in(x))
  41 [s:sigma][sp:<s>p]
  42 otax2:=PRIM:image(ot,sigma,[x,ot]in(x),s)
  43 tau@pairtype:=PRIM:TYPE
  44 [s:sigma][t:tau]
  45 pair:=PRIM:pairtype
  46 tau@[p1:pairtype]
  47 first:=PRIM:sigma
  48 second:=PRIM:tau
  49 pairis1:=PRIM:is(pairtype,pair(first,second),p1)
  50 t@firstis1:=PRIM:is(sigma,first(pair),s)
  51 secondis1:=PRIM:is(tau,second(pair),t)
  52 +st
  53 sigma@set:=PRIM:TYPE
  54 [s:sigma][s0:set]
  55 esti:=PRIM:PROP
  56 p@setof:=PRIM:set
  57 [s:sigma][sp:<s>p]
  58 estii:=PRIM:esti(s,setof(p))
  59 s@[e:esti(s,setof(p))]
  60 estie:=PRIM:<s>p
  61 sigma@[s0:set][t0:set]
  62 incl:=all([x,sigma]imp(esti(x,s0),esti(x,t0))):PROP
  63 [i:incl(s0,t0)][j:incl(t0,s0)]
  64 isseti:=PRIM:is(set,s0,t0)
  65 +eq
  66 +landau
  67 +n
  68 @nat:=PRIM:TYPE
  69 [x:nat][y:nat]
  70 is:=is(nat,x,y):PROP
  71 nis:=not(is(x,y)):PROP
  72 x@[s:set(nat)]
  73 in:=esti(nat,x,s):PROP
  74 @[p:[x,nat]PROP]
  75 all:=all(nat,p):PROP
  76 @1:=PRIM:nat
  77 suc:=PRIM:[x,nat]nat
  78 ax3:=PRIM:[x,nat]nis(<x>suc,1)
  79 ax4:=PRIM:[x,nat][y,nat][u,is(<x>suc,<y>suc)]is(x,y)
  80 [s:set(nat)]
  81 cond1:=in(1,s):PROP
  82 cond2:=all([x,nat]imp(in(x,s),in(<x>suc,s))):PROP
  83 @ax5:=PRIM:[s,set(nat)][u,cond1(s)][v,cond2(s)][x,nat]in(x,s)
  84 -n
  85 -landau
  86 -eq
  87 -st
  88 -e
  89 -l