matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.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 "ground/xoa/ex_1_4.ma".
  16 include "static_2/notation/relations/simple_1.ma".
  17 include "static_2/syntax/term.ma".
  18
  19 (* SIMPLE (NEUTRAL) TERMS ***************************************************)
  20
  21 inductive simple: predicate term ≝
  22    | simple_atom: ∀I. simple (⓪[I])
  23    | simple_flat: ∀I,V,T. simple (ⓕ[I]V.T)
  24 .
  25
  26 interpretation "simple (term)" 'Simple T = (simple T).
  27
  28 (* Basic inversion lemmas ***************************************************)
  29
  30 fact simple_inv_bind_aux: ∀T. 𝐒❨T❩ → ∀p,J,W,U. T = ⓑ[p,J]W.U → ⊥.
  31 #T * -T
  32 [ #I #p #J #W #U #H destruct
  33 | #I #V #T #a #J #W #U #H destruct
  34 ]
  35 qed-.
  36
  37 lemma simple_inv_bind: ∀p,I,V,T. 𝐒❨ⓑ[p,I] V. T❩ → ⊥.
  38 /2 width=7 by simple_inv_bind_aux/ qed-.
  39
  40 lemma simple_inv_pair: ∀I,V,T. 𝐒❨②[I]V.T❩ → ∃J. I = Flat2 J.
  41 * /2 width=2 by ex_intro/
  42 #p #I #V #T #H elim (simple_inv_bind … H)
  43 qed-.
  44
  45 (* Basic properties *********************************************************)
  46
  47 lemma simple_dec_ex (X): ∨∨ 𝐒❨X❩ | ∃∃p,I,T,U. X = ⓑ[p,I]T.U.
  48 * [ /2 width=1 by simple_atom, or_introl/ ]
  49 * [| /2 width=1 by simple_flat, or_introl/ ]
  50 /3 width=5 by ex1_4_intro, or_intror/
  51 qed-.