matita/matita/contribs/lambda/subterms/booleanized.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 "subterms/carrier.ma".
  16 include "subterms/boolean.ma".
  17
  18 (* BOOLEANIZED SUBSET (EMPTY OR FULL)  **************************************)
  19
  20 definition booleanized: bool → subterms → subterms ≝
  21    λb,F. {b}⇑⇓F.
  22
  23 interpretation "make boolean (subterms)"
  24    'ProjectSame b F = (booleanized b F).
  25
  26 notation "hvbox( { term 46 b } ⇕ break term 46 F)"
  27    non associative with precedence 46
  28    for @{ 'ProjectSame $b $F }.
  29
  30 lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j →
  31                             ∃∃b1. b = c & F = {b1}#j.
  32 #j #c #b #F #H
  33 elim (boolean_inv_vref … H) -H #H0 #H
  34 elim (carrier_inv_vref … H) -H /2 width=2/
  35 qed-.
  36
  37 lemma booleanized_inv_abst: ∀U,c,b,F. {b}⇕ F = {c}𝛌.U →
  38                             ∃∃b1,T. b = c & {b}⇕T = U & F = {b1}𝛌.T.
  39 #U #c #b #F #H
  40 elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
  41 elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
  42 qed-.
  43
  44 lemma booleanized_inv_appl: ∀W,U,c,b,F. {b}⇕ F = {c}@W.U →
  45                             ∃∃b1,V,T. b = c & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
  46 #W #U #c #b #F #H
  47 elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
  48 elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
  49 qed-.
  50
  51 lemma booleanized_booleanized: ∀c,b,F. {b}⇕ {c}⇕ F = {b}⇕ F.
  52 normalize //
  53 qed.
  54
  55 lemma booleanized_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
  56 normalize //
  57 qed.
  58
  59 lemma booleanized_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.
  60 normalize //
  61 qed.