From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 24 Feb 2010 20:04:39 +0000 (+0000)
Subject: - a couple of new entities
X-Git-Tag: make_still_working~3027
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0fb1fa1948f85598a888392ce95d1a263be3b9ab;p=helm.git

- a couple of new entities
---

diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln
index 55b96e6c9..4b84f65fd 100644
--- a/helm/software/lambda-delta/examples/exp_math/L.hln
+++ b/helm/software/lambda-delta/examples/exp_math/L.hln
@@ -2,7 +2,7 @@
 
 \* Intuitionistic Predicate Logic with Equality *\
 
-\open elements \* [1] 2.1. 2.2. *\
+\open elements \* [1] 2.1. 2.2. 3.1 *\
 
    \decl "logical false" False: *Prop
 
diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln
index aab161e0e..8321246c6 100644
--- a/helm/software/lambda-delta/examples/exp_math/T0.hln
+++ b/helm/software/lambda-delta/examples/exp_math/T0.hln
@@ -39,7 +39,10 @@
 
 \close
 
-\open non_logical_abbreviations \* [1] 2.4. *\
+\open non_logical_abbreviations \* [1] 2.4. 2.7 *\
+
+   \def "object application"
+      OAt = [f:*Obj, x:*Obj] At(T(f), T(x)) : *Obj => *Obj -> *Term
 
    \def "convergence of a term to an object"
       Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
@@ -48,15 +51,38 @@
       Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
          : *Term => *Term -> *Prop
 
+   \def "classification membership of a term"
+      TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
+           : *Term => *Obj -> *Prop
+
+   \def "operation (rule with inhabited domain)"
+      Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
+
+   \def "classification inclusion"
+      ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
+           : *Obj => *Obj -> *Prop
+
+    \def "classification morphism"
+      ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
+          : *Obj => *Obj => *Obj -> *Prop
+
 \close
 
-\open non_logical_axioms \* [1] 2.4. *\
+\open non_logical_axioms \* [1] 2.4. 3.2 *\
 
 \* we axiomatize E because *Term is not inductively generated *\
    \ax e_refl: [y:*Obj] E(T(y), y)
-\*
-   \ax e_at_in: [f:*Obj][x:*Obj][y:*Obj] App(f,x,y) -> E(At(T(f), T(x)), y) 
 
+   \ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj] 
+                E(t1, f) -> E(t2, x) -> App(f, x, y) -> E(At(t1, t2), y) 
+\*
    \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y) 
 *\
+   \ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
+   
+   \ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
+                         E(OAt(f, x), y1) -> E(OAt(f, x), y2) -> Id(y1, y2)
+
+   \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] Eta(x, a) -> Cl(a)
+
 \close