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 (* saturation conditions on an explicit subset ********************************)
  18
  19 definition SAT0 ≝ λP. ∀l,n. all P l → P (Appl (Sort n) l).
  20
  21 definition SAT1 ≝ λP. ∀l,i. all P l → P (Appl (Rel i) l).
  22
  23 definition SAT2 ≝ λ(P:?→Prop). ∀F,A,B,l. P B → P A →
  24                   P (Appl F[0:=A] l) → P (Appl (Lambda B F) (A::l)).
  25
  26 theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
  27 #P #n #H @(H (nil ?) …) //
  28 qed.
  29
  30 theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
  31 #P #i #H @(H (nil ?) …) //
  32 qed.
  33
  34 (* STRONGLY NORMALIZING TERMS *************************************************)
  35
  36 (* SN(t) holds when t is strongly normalizing *)
  37 (* FG: we axiomatize it for now because we dont have reduction yet *)
  38 axiom SN: T → Prop.
  39
  40 definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
  41
  42 axiom sn_sort: SAT0 SN.
  43
  44 axiom sn_rel: SAT1 SN.
  45
  46 axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
  47
  48 axiom sn_beta: SAT2 SN.
  49
  50 (* FG: do we need this?
  51 axiom sn_lift: ∀t,k,p. SN t → SN (lift t p k).
  52 *)