]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy_new/sn.ma
almost there
[helm.git] / matita / matita / lib / pts_dummy_new / sn.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "pts_dummy/ext_lambda.ma".
16 (*
17 (* STRONGLY NORMALIZING TERMS *************************************************)
18
19 (* SN(t) holds when t is strongly normalizing *)
20 (* FG: we axiomatize it for now because we dont have reduction yet *)
21 axiom SN: T → Prop.
22
23 (* lists of strongly normalizing terms *)
24 definition SNl ≝ all ? SN.
25
26 (* saturation conditions ******************************************************)
27
28 definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
29
30 definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l).
31
32 definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
33
34 definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
35                   P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
36
37 definition SAT3 ≝ λ(P:?→Prop). ∀M,N,l. P (Appl (D (App M N)) l) → 
38                                P (Appl (D M) (N::l)).
39
40 definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M).
41
42 lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
43 #P #n #HP @(HP n (nil ?) …) //
44 qed.
45
46 lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
47 #P #i #HP @(HP i (nil ?) …) //
48 qed.
49
50 lemma SAT3_1: ∀P,M,N. SAT3 P → P (D (App M N)) → P (App (D M) N).
51 #P #M #N #HP #H @(HP … ([])) @H
52 qed.
53
54 (* axiomatization *************************************************************)
55
56 axiom sn_sort: SAT0 SN.
57
58 axiom sn_rel: SAT1 SN.
59
60 axiom sn_beta: SAT2 SN.
61
62 axiom sn_dapp: SAT3 SN.
63
64 axiom sn_dummy: SAT4 SN.
65
66 axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
67
68 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
69
70 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.
71 *)