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/subterms/carrier.ma".
17 include "lambda/notation/functions/projectup_2.ma".
19 include "lambda/xoa/ex_3_1.ma".
20 include "lambda/xoa/ex_4_2.ma".
22 (* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************)
24 let rec boolean b M on M ≝ match M with
26 | Abst A ⇒ {b}𝛌.(boolean b A)
27 | Appl B A ⇒ {b}@(boolean b B).(boolean b A)
30 interpretation "boolean subset (subterms)"
31 'ProjectUp b M = (boolean b M).
33 lemma boolean_inv_vref: ∀j,c,b,M. {b}⇑ M = {c}#j → b = c ∧ M = #j.
35 [ #i #H destruct /2 width=1/
41 lemma boolean_inv_abst: ∀U,c,b,M. {b}⇑ M = {c}𝛌.U →
42 ∃∃C. b = c & {b}⇑C = U & M = 𝛌.C.
45 | #A #H destruct /2 width=3/
50 lemma boolean_inv_appl: ∀W,U,c,b,M. {b}⇑ M = {c}@W.U →
51 ∃∃D,C. b = c & {b}⇑D = W & {b}⇑C = U & M = @D.C.
52 #W #U #c #b * normalize
55 | #B #A #H destruct /2 width=5/
59 lemma boolean_lift: ∀b,h,M,d. {b}⇑ ↑[d, h] M = ↑[d, h] {b}⇑ M.
60 #b #h #M elim M -M normalize //
63 lemma boolean_dsubst: ∀b,N,M,d. {b}⇑ [d ↙ N] M = [d ↙ {b}⇑ N] {b}⇑ M.
64 #b #N #M elim M -M [2,3: normalize // ]
65 #i #d elim (lt_or_eq_or_gt i d) #Hid
66 [ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
67 | destruct normalize //
68 | >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
72 lemma carrier_boolean: ∀b,M. ⇓ {b}⇑ M = M.
73 #b #M elim M -M normalize //