- predefined_virtuals: nwe characters

[helm.git] / matita / matita / lib / lambda / sn.ma

diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index 339aa424ab1dc145d5eba7bb028f8b0f39277d15..a9fbff3700afc50ae67e78db40b3e966bf60ebfd 100644 (file)
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -12,21 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/types.ma".
-
-(* all(P,l) holds when P holds for all members of l *)
-let rec all (P:T→Prop) l on l ≝ match l with 
-   [ nil ⇒ True
-   | cons A D ⇒ P A ∧ all P D
-   ].
-
-(* Appl F l generalizes App applying F to a list of arguments
- * The head of l is applied first
- *)
-let rec Appl F l on l ≝ match l with 
-   [ nil ⇒ F
-   | cons A D ⇒ Appl (App F A) D  
-   ].
+include "lambda/ext_lambda.ma".
 
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
@@ -34,13 +20,51 @@ let rec Appl F l on l ≝ match l with
 (* FG: we axiomatize it for now because we dont have reduction yet *)
 axiom SN: T → Prop.
 
-(* axiomatization of SN *******************************************************)
+(* lists of strongly normalizing terms *)
+definition SNl ≝ all ? SN.
 
-axiom sn_sort: ∀l,n. all SN l → SN (Appl (Sort n) l).
+(* saturation conditions ******************************************************)
 
-axiom sn_rel: ∀l,i. all SN l → SN (Appl (Rel i) l).
+definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
 
-axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
+definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l).
 
-axiom sn_beta: ∀F,A,B,l. SN B → SN A →
-               SN (Appl F[0:=A] l) → SN (Appl (Lambda B F) (A::l)).
+definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
+
+definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
+                  P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
+
+definition SAT3 ≝ λ(P:?→Prop). ∀M,N,l. P (Appl (D (App M N)) l) → 
+                               P (Appl (D M) (N::l)).
+
+definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M).
+
+lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
+#P #n #HP @(HP n (nil ?) …) //
+qed.
+
+lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
+#P #i #HP @(HP i (nil ?) …) //
+qed.
+
+lemma SAT3_1: ∀P,M,N. SAT3 P → P (D (App M N)) → P (App (D M) N).
+#P #M #N #HP #H @(HP … ([])) @H
+qed.
+
+(* axiomatization *************************************************************)
+
+axiom sn_sort: SAT0 SN.
+
+axiom sn_rel: SAT1 SN.
+
+axiom sn_beta: SAT2 SN.
+
+axiom sn_dapp: SAT3 SN.
+
+axiom sn_dummy: SAT4 SN.
+
+axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
+
+axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
+
+axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.