matita/matita/lib/lambda/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 "lambda/ext.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 theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
  38 #P #n #H @(H n (nil ?) …) //
  39 qed.
  40
  41 theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
  42 #P #i #H @(H i (nil ?) …) //
  43 qed.
  44
  45 (* axiomatization *************************************************************)
  46
  47 axiom sn_sort: SAT0 SN.
  48
  49 axiom sn_rel: SAT1 SN.
  50
  51 axiom sn_beta: SAT2 SN.
  52
  53 axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
  54
  55 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
  56
  57 axiom sn_dummy: ∀M. SN M → SN (D M).
  58
  59 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.