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 "Basic_2/grammar/item.ma".
17 (* TERMS ********************************************************************)
20 inductive term: Type[0] ≝
21 | TAtom: item0 → term (* atomic item construction *)
22 | TPair: item2 → term → term → term (* binary item construction *)
25 interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
27 interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
29 interpretation "global reference (term)" 'GRef p = (TAtom (GRef p)).
31 interpretation "term construction (atomic)" 'SItem I = (TAtom I).
33 interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
35 interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
37 interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).
39 (* Basic inversion lemmas ***************************************************)
41 lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
44 | #J #W #U #IHW #_ #H destruct
45 -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
50 (* Basic_1: was: thead_x_y_y *)
51 lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
54 | #J #W #U #_ #IHU #H destruct
55 -H (**) (* destruct: the destucted equality is not erased *)
60 (* Basic properties *********************************************************)
62 (* Basic_1: was: term_dec *)
63 axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2).
65 (* Basic_1: removed theorems 3:
66 not_void_abst not_abbr_void not_abst_void