X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fautomath%2Fgrundlagen_1.aut;h=8aeb9b909e73701268f71bd4466936b8ee791751;hb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;hp=4a856c2454454abafef49c36af35960d94636082;hpb=34e6104ef149e3776d0ab7f0930ae73f0e8de157;p=helm.git

diff --git a/helm/software/helena/examples/automath/grundlagen_1.aut b/helm/software/helena/examples/automath/grundlagen_1.aut
index 4a856c245..8aeb9b909 100644
--- a/helm/software/helena/examples/automath/grundlagen_1.aut
+++ b/helm/software/helena/examples/automath/grundlagen_1.aut
@@ -1,7 +1,8 @@
 # Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
 # Copyright (C) 1977, L.S. van Benthem Jutting
 #               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
-#               2008, revised by F. Guidi to remove the eta-reductions
+#               2008, revised by F. Guidi to remove eta-reductions
+#               2014, revised by F. Guidi to remove sort inclusions on binders of degree 1
 
 +l
 @[a:'prop'][b:'prop']
@@ -225,7 +226,7 @@ i@[o:orec(c,a)]
 thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
 -iff
 @[sigma:'type'][p:[x:sigma]'prop']
-%suggestion by van Daalen to remove the first eta-reduction
+%suggestion by van Daalen to remove eta-reduction
 %all:=p:'prop' %original line
 all:=[x:sigma]<x>p:'prop'
 %end of suggestion
@@ -236,26 +237,29 @@ p@[s:sigma][n:not(<s>p)]
 th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
 -all
 p@non:=[x:sigma]not(<x>p):[x:sigma]'prop'
-some:=not(non(p)):'prop'
+%suggestion by Guidi to remove sort inclusion of degree 1 by adding all-introduction
+none:=all(sigma,non(p)):'prop'
+%end of suggestion ("non" replaced by "none" where needed)
+some:=not(none(p)):'prop' %none
 [s:sigma][sp:<s>p]
 somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)
 +some
-p@[n:not(all(sigma,p))][m:non(non(p))][s:sigma]
+p@[n:not(all(sigma,p))][m:none(non(p))][s:sigma] %none 
 t1:=et(<s>p,<s>m):<s>p
 %set etared
 m@t2:=<[x:sigma]t1(x)>n:con
 %reset etared
-n@th1:=[x:non(non(p))]t2(x):some(non(p))
+n@th1:=[x:none(non(p))]t2(x):some(non(p)) %none 
 p@[s:some(non(p))][a1:all(sigma,p)][t:sigma]
 t3:=weli(<t>p,<t>a1):not(not(<t>p))
 a1@t4:=<[x:sigma]t3(x)>s:con
 s@th2:=[x:all(sigma,p)]t4(x):not(all(sigma,p))
 p@[n:not(some(sigma,p))]
-th3:=et(non(p),n):non(p)
+th3:=et(none(p),n):none(p) %none x 2 
 [s:sigma]
 th4:=<s>th3:not(<s>p)
-p@[n:non(p)]
-th5:=weli(non(p),n):not(some(sigma,p))
+p@[n:none(p)] %none
+th5:=weli(none(p),n):not(some(sigma,p)) %none
 -some
 p@[s:some(sigma,p)][x:'prop'][i:[y:sigma]imp(<y>p,x)]
 +*some
@@ -666,7 +670,7 @@ th6:=th1"e.bij"(sigma,sigma,tau,wissel(s0,t0),f,th3(s0,t0),b):bijective(changef)
 -e
 +r
 a@[b:[x:a]'prop']
-%suggestion by van Daalen to remove the second eta-reduction
+%suggestion by van Daalen to remove eta-reduction
 %imp:=b:'prop' %original line
 imp:=[x:a]<x>b:'prop'
 %end of suggestion
@@ -738,7 +742,7 @@ estii:='prim':esti(s,setof(p))
 s@[e:esti(s,setof(p))]
 estie:='prim':<s>p
 sigma@[s0:set]
-empty:=non([x:sigma]esti(x,s0)):'prop'
+empty:=none([x:sigma]esti(x,s0)):'prop' %none
 nonempty:=some([x:sigma]esti(x,s0)):'prop'
 [n:[x:sigma]not(esti(x,s0))]
 emptyi:=n:empty(s0)
@@ -788,11 +792,11 @@ th4:=symnotis(set,s0,t0,th3):not(is(set,t0,s0))
 s@nissetprop:=and(esti(s,s0),not(esti(s,t0))):'prop'
 [n:not(nissetprop(s0,t0,s))][e:esti(s,s0)]
 t1:=et(esti(s,t0),th3"l.and"(esti(s,s0),not(esti(s,t0)),n,e)):esti(s,t0)
-t0@[n:not(is(set,s0,t0))][m:not(some([x:sigma]nissetprop(s0,t0,x)))][l:non([x:sigma]nissetprop(t0,s0,x))][s:sigma]
+t0@[n:not(is(set,s0,t0))][m:not(some([x:sigma]nissetprop(s0,t0,x)))][l:none([x:sigma]nissetprop(t0,s0,x))][s:sigma] %none
 t2:=th4"l.some"([x:sigma]nissetprop(s0,t0,x),m,s):not(nissetprop(s0,t0,s))
 t3:=<s>l:not(nissetprop(t0,s0,s))
 l@t4:=isseti(s0,t0,[x:sigma][y:esti(x,s0)]t1(s0,t0,x,t2(x),y),[x:sigma][y:esti(x,t0)]t1(t0,s0,x,t3(x),y)):is(set,s0,t0)
-m@t5:=th3"l.imp"(non([x:sigma]nissetprop(t0,s0,x)),is(set,s0,t0),n,[y:non([x:sigma]nissetprop(t0,s0,x))]t4(y)):some([x:sigma]nissetprop(t0,s0,x))
+m@t5:=th3"l.imp"(none([x:sigma]nissetprop(t0,s0,x)),is(set,s0,t0),n,[y:none([x:sigma]nissetprop(t0,s0,x))]t4(y)):some([x:sigma]nissetprop(t0,s0,x)) %none x 2
 n@th5:=th1"l.or"(some([x:sigma]nissetprop(s0,t0,x)),some([x:sigma]nissetprop(t0,s0,x)),[y:not(some([x:sigma]nissetprop(s0,t0,x)))]t5(y)):or(some([x:sigma]nissetprop(s0,t0,x)),some([x:sigma]nissetprop(t0,s0,x)))
 -isset
 sigma@[alpha:'type'][sa:[x:alpha]set]
@@ -1452,12 +1456,12 @@ t5:=th4"l.imp"(<y>p,lessis(pl(y,1),y),yp,t4):not(lbprop(pl(y,1),y))
 t6:=th1"l.all"(nat,[x:nat]lbprop(pl(y,1),x),y,t5):not(lb(pl(y,1)))
 t7:=mp(lb(pl(y,1)),con,<pl(y,1)>l,t6):con
 l@t8:=someapp(nat,p,s,con,[x:nat][y:<x>p]t7(x,y)):con
-s@[n:non(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))][m:nat][l:lb(m)]
+s@[n:none(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))][m:nat][l:lb(m)] %none
 t9:=<m>n:not(and(lb(m),not(lb(pl(m,1)))))
 t10:=et(lb(pl(m,1)),th3"l.and"(lb(m),not(lb(pl(m,1))),t9,l)):lb(pl(m,1))
 t11:=isp(nat,[x:nat]lb(x),pl(m,1),<m>suc,t10,satz4a(m)):lb(<m>suc)
 n@t12:=[x:nat]induction([y:nat]lb(y),t2,[y:nat][z:lb(y)]t11(y,z),x):[x:nat]lb(x)
-s@t13:=[x:non(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))]t8(t12(x)):some([x:nat]and(lb(x),not(lb(pl(x,1)))))
+s@t13:=[x:none(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))]t8(t12(x)):some([x:nat]and(lb(x),not(lb(pl(x,1))))) %none
 [m:nat][a:and(lb(m),not(lb(pl(m,1))))]
 t14:=ande1(lb(m),not(lb(pl(m,1))),a):lb(m)
 t15:=ande2(lb(m),not(lb(pl(m,1))),a):not(lb(pl(m,1)))
@@ -1473,7 +1477,7 @@ t23:=andi(lb(m),<m>p,t14,t22):min(m)
 -327
 s@satz27:=th6"l.some"(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))),[x:nat]min(x),t13".327",[x:nat][y:and(lb(x),not(lb(pl(x,1))))]t23".327"(x,y)):some([x:nat]min(p,x))
 +*327
-p@[n:non(nat,[x:nat]min(x))][u:nat]
+p@[n:none(nat,[x:nat]min(x))][u:nat] %none
 t24:=[x:<u>p]satz24a(u):lbprop(1,u)
 n@t25:=[x:nat]t24(x):lb(1)
 u@[l:lb(u)]
@@ -1491,7 +1495,7 @@ p@[s:some(p)][u:nat][up:<u>p]
 t35:=satz10g(<u>suc,u,satz18b(u)):not(lessis(<u>suc,u))
 t36:=th4"l.imp"(<u>p,lessis(<u>suc,u),up,t35):not(lbprop(<u>suc,u))
 t37:=th1"l.all"(nat,[x:nat]lbprop(<u>suc,x),u,t36):not(lb(<u>suc))
-t38:=[y:non(nat,[x:nat]min(x))]mp(lb(<u>suc),con,t34(y,<u>suc),t37):some([x:nat]min(x))
+t38:=[y:none(nat,[x:nat]min(x))]mp(lb(<u>suc),con,t34(y,<u>suc),t37):some([x:nat]min(x)) %none
 s@anders:=someapp(nat,p,s,some([x:nat]min(x)),[x:nat][y:<x>p]t38(x,y)):some([x:nat]min(x))
 -327
 +*327