1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/types.ma".
17 (* all(P,l) holds when P holds for all members of l *)
18 let rec all (P:T→Prop) l on l ≝ match l with
20 | cons A D ⇒ P A ∧ all P D
23 (* Appl F l generalizes App applying F to a list of arguments
24 * The head of l is applied first
26 let rec Appl F l on l ≝ match l with
28 | cons A D ⇒ Appl (App F A) D
31 (* STRONGLY NORMALIZING TERMS *************************************************)
33 (* SN(t) holds when t is strongly normalizing *)
34 (* FG: we axiomatize it for now because we dont have reduction yet *)
37 (* axiomatization of SN *******************************************************)
39 axiom sn_sort: ∀l,n. all SN l → SN (Appl (Sort n) l).
41 axiom sn_rel: ∀l,i. all SN l → SN (Appl (Rel i) l).
43 axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
45 axiom sn_beta: ∀F,A,B,l. SN B → SN A →
46 SN (Appl F[0:=A] l) → SN (Appl (Lambda B F) (A::l)).