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 "ground_2/relocation/trace_sor.ma".
16 include "ground_2/relocation/trace_isun.ma".
17 include "basic_2/notation/relations/freestar_3.ma".
18 include "basic_2/grammar/lenv.ma".
20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
22 inductive frees: relation3 lenv term trace ≝
23 | frees_atom: ∀I. frees (⋆) (⓪{I}) (◊)
24 | frees_sort: ∀I,L,V,s,t. frees L (⋆s) t →
25 frees (L.ⓑ{I}V) (⋆s) (Ⓕ @ t)
26 | frees_zero: ∀I,L,V,t. frees L V t →
27 frees (L.ⓑ{I}V) (#0) (Ⓣ @ t)
28 | frees_lref: ∀I,L,V,i,t. frees L (#i) t →
29 frees (L.ⓑ{I}V) (#⫯i) (Ⓕ @ t)
30 | frees_gref: ∀I,L,V,p,t. frees L (§p) t →
31 frees (L.ⓑ{I}V) (§p) (Ⓕ @ t)
32 | frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) →
33 t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t
34 | frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 →
35 t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t
39 "context-sensitive free variables (term)"
40 'FreeStar L T t = (frees L T t).
42 (* Basic forward lemmas *****************************************************)
44 fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄.
45 #L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
46 [ #_ #L #V #t #_ #_ #x #H destruct
47 | #_ #L #_ #i #t #_ #_ #x #H destruct
48 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
49 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
53 lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄.
54 /2 width=5 by frees_fwd_sort_aux/ qed-.
56 fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄.
57 #L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
58 [ #_ #L #V #t #_ #_ #x #H destruct
59 | #_ #L #_ #i #t #_ #_ #x #H destruct
60 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
61 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
65 lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄.
66 /2 width=5 by frees_fwd_gref_aux/ qed-.
68 (* Basic inversion lemmas ***************************************************)
70 fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 →
72 ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
74 [ /3 width=1 by or_introl, conj/
75 | #I #L #V #s #t #_ #H destruct
76 | /3 width=7 by ex3_4_intro, or_intror/
77 | #I #L #V #i #t #_ #H destruct
78 | #I #L #V #p #t #_ #H destruct
79 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct
80 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct
84 lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t →
86 ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
87 /2 width=3 by frees_inv_zero_aux/ qed-.
89 fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) →
91 ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
93 [ /3 width=1 by or_introl, conj/
94 | #I #L #V #s #t #_ #j #H destruct
95 | #I #L #V #t #_ #j #H destruct
96 | #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
97 | #I #L #V #p #t #_ #j #H destruct
98 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct
99 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct
103 lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t →
105 ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
106 /2 width=3 by frees_inv_lref_aux/ qed-.