]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/subterms/booleanize.ma
f49a9533551bb9debf0998eb5fbd5ac6b6bf585b
[helm.git] / matita / matita / contribs / lambda / subterms / booleanize.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 (* BOOLEANIZE (EMPTY OR FILL)  **********************************************)
19
20 definition booleanize: bool → subterms → subterms ≝
21    λb,F. {b}⇑⇓F.
22
23 interpretation "make boolean (subterms)"
24    'ProjectSame b F = (booleanize 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 booleanize_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
31                            ∃∃b1. b = b0 & F = {b1}#j.
32 #j #b0 #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 booleanize_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
38                            ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
39 #U #b0 #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 booleanize_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
45                            ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
46 #W #U #b0 #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 booleanize_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
52 #b #h #M elim M -M normalize //
53 qed.
54
55 lemma booleanize_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.
56 #b #N #M elim M -M [2,3: normalize // ]
57 *)