(**************************************************************************)
include "ground_2/relocation/rtmap_sor.ma".
-include "static_2/notation/relations/freestar_3.ma".
+include "static_2/notation/relations/freeplus_3.ma".
include "static_2/syntax/lenv.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
interpretation
"context-sensitive free variables (term)"
- 'FreeStar L T f = (frees L T f).
+ 'FreePlus L T f = (frees L T f).
(* Basic inversion lemmas ***************************************************)
-fact frees_inv_sort_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โx. X = โx โ ๐โฆfโฆ.
+fact frees_inv_sort_aux: โf,L,X. L โข ๐
+โฆXโฆ โ f โ โx. X = โx โ ๐โฆfโฆ.
#L #X #f #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
]
qed-.
-lemma frees_inv_sort: โf,L,s. L โข ๐
*โฆโsโฆ โ f โ ๐โฆfโฆ.
+lemma frees_inv_sort: โf,L,s. L โข ๐
+โฆโsโฆ โ f โ ๐โฆfโฆ.
/2 width=5 by frees_inv_sort_aux/ qed-.
-fact frees_inv_atom_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โi. L = โ โ X = #i โ
- โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
+fact frees_inv_atom_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โi. L = โ โ X = #i โ
+ โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
#f #L #X #H elim H -f -L -X
[ #f #L #s #_ #j #_ #H destruct
| #f #i #Hf #j #_ #H destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma frees_inv_atom: โf,i. โ โข ๐
*โฆ#iโฆ โ f โ โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
+lemma frees_inv_atom: โf,i. โ โข ๐
+โฆ#iโฆ โ f โ โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
/2 width=5 by frees_inv_atom_aux/ qed-.
-fact frees_inv_pair_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K,V. L = K.โ{I}V โ X = #0 โ
- โโg. K โข ๐
*โฆVโฆ โ g & f = โg.
+fact frees_inv_pair_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โI,K,V. L = K.โ{I}V โ X = #0 โ
+ โโg. K โข ๐
+โฆVโฆ โ g & f = โg.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #X #_ #H destruct
| #f #i #_ #Z #Y #X #H destruct
]
qed-.
-lemma frees_inv_pair: โf,I,K,V. K.โ{I}V โข ๐
*โฆ#0โฆ โ f โ โโg. K โข ๐
*โฆVโฆ โ g & f = โg.
+lemma frees_inv_pair: โf,I,K,V. K.โ{I}V โข ๐
+โฆ#0โฆ โ f โ โโg. K โข ๐
+โฆVโฆ โ g & f = โg.
/2 width=6 by frees_inv_pair_aux/ qed-.
-fact frees_inv_unit_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K. L = K.โค{I} โ X = #0 โ
- โโg. ๐โฆgโฆ & f = โg.
+fact frees_inv_unit_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โI,K. L = K.โค{I} โ X = #0 โ
+ โโg. ๐โฆgโฆ & f = โg.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #_ #H destruct
| #f #i #_ #Z #Y #H destruct
]
qed-.
-lemma frees_inv_unit: โf,I,K. K.โค{I} โข ๐
*โฆ#0โฆ โ f โ โโg. ๐โฆgโฆ & f = โg.
+lemma frees_inv_unit: โf,I,K. K.โค{I} โข ๐
+โฆ#0โฆ โ f โ โโg. ๐โฆgโฆ & f = โg.
/2 width=7 by frees_inv_unit_aux/ qed-.
-fact frees_inv_lref_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K,j. L = K.โ{I} โ X = #(โj) โ
- โโg. K โข ๐
*โฆ#jโฆ โ g & f = โซฏg.
+fact frees_inv_lref_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โI,K,j. L = K.โ{I} โ X = #(โj) โ
+ โโg. K โข ๐
+โฆ#jโฆ โ g & f = โซฏg.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #j #_ #H destruct
| #f #i #_ #Z #Y #j #H destruct
]
qed-.
-lemma frees_inv_lref: โf,I,K,i. K.โ{I} โข ๐
*โฆ#(โi)โฆ โ f โ
- โโg. K โข ๐
*โฆ#iโฆ โ g & f = โซฏg.
+lemma frees_inv_lref:
+ โf,I,K,i. K.โ{I} โข ๐
+โฆ#(โi)โฆ โ f โ
+ โโg. K โข ๐
+โฆ#iโฆ โ g & f = โซฏg.
/2 width=6 by frees_inv_lref_aux/ qed-.
-fact frees_inv_gref_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โx. X = ยงx โ ๐โฆfโฆ.
+fact frees_inv_gref_aux: โf,L,X. L โข ๐
+โฆXโฆ โ f โ โx. X = ยงx โ ๐โฆfโฆ.
#f #L #X #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
]
qed-.
-lemma frees_inv_gref: โf,L,l. L โข ๐
*โฆยงlโฆ โ f โ ๐โฆfโฆ.
+lemma frees_inv_gref: โf,L,l. L โข ๐
+โฆยงlโฆ โ f โ ๐โฆfโฆ.
/2 width=5 by frees_inv_gref_aux/ qed-.
-fact frees_inv_bind_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โp,I,V,T. X = โ{p,I}V.T โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L.โ{I}V โข ๐
*โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
+fact frees_inv_bind_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โp,I,V,T. X = โ{p,I}V.T โ
+ โโf1,f2. L โข ๐
+โฆVโฆ โ f1 & L.โ{I}V โข ๐
+โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
#f #L #X * -f -L -X
[ #f #L #s #_ #q #J #W #U #H destruct
| #f #i #_ #q #J #W #U #H destruct
]
qed-.
-lemma frees_inv_bind: โf,p,I,L,V,T. L โข ๐
*โฆโ{p,I}V.Tโฆ โ f โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L.โ{I}V โข ๐
*โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
+lemma frees_inv_bind:
+ โf,p,I,L,V,T. L โข ๐
+โฆโ{p,I}V.Tโฆ โ f โ
+ โโf1,f2. L โข ๐
+โฆVโฆ โ f1 & L.โ{I}V โข ๐
+โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
/2 width=4 by frees_inv_bind_aux/ qed-.
-fact frees_inv_flat_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,V,T. X = โ{I}V.T โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L โข ๐
*โฆTโฆ โ f2 & f1 โ f2 โ f.
+fact frees_inv_flat_aux: โf,L,X. L โข ๐
+โฆXโฆ โ f โ โI,V,T. X = โ{I}V.T โ
+ โโf1,f2. L โข ๐
+โฆVโฆ โ f1 & L โข ๐
+โฆTโฆ โ f2 & f1 โ f2 โ f.
#f #L #X * -f -L -X
[ #f #L #s #_ #J #W #U #H destruct
| #f #i #_ #J #W #U #H destruct
]
qed-.
-lemma frees_inv_flat: โf,I,L,V,T. L โข ๐
*โฆโ{I}V.Tโฆ โ f โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L โข ๐
*โฆTโฆ โ f2 & f1 โ f2 โ f.
+lemma frees_inv_flat:
+ โf,I,L,V,T. L โข ๐
+โฆโ{I}V.Tโฆ โ f โ
+ โโf1,f2. L โข ๐
+โฆVโฆ โ f1 & L โข ๐
+โฆTโฆ โ f2 & f1 โ f2 โ f.
/2 width=4 by frees_inv_flat_aux/ qed-.
(* Basic properties ********************************************************)
-lemma frees_eq_repl_back: โL,T. eq_repl_back โฆ (ฮปf. L โข ๐
*โฆTโฆ โ f).
+lemma frees_eq_repl_back: โL,T. eq_repl_back โฆ (ฮปf. L โข ๐
+โฆTโฆ โ f).
#L #T #f1 #H elim H -f1 -L -T
[ /3 width=3 by frees_sort, isid_eq_repl_back/
| #f1 #i #Hf1 #g2 #H
]
qed-.
-lemma frees_eq_repl_fwd: โL,T. eq_repl_fwd โฆ (ฮปf. L โข ๐
*โฆTโฆ โ f).
+lemma frees_eq_repl_fwd: โL,T. eq_repl_fwd โฆ (ฮปf. L โข ๐
+โฆTโฆ โ f).
#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
qed-.
-lemma frees_lref_push: โf,i. โ โข ๐
*โฆ#iโฆ โ f โ โ โข ๐
*โฆ#โiโฆ โ โซฏf.
+lemma frees_lref_push: โf,i. โ โข ๐
+โฆ#iโฆ โ f โ โ โข ๐
+โฆ#โiโฆ โ โซฏf.
#f #i #H
elim (frees_inv_atom โฆ H) -H #g #Hg #H destruct
/2 width=1 by frees_atom/
(* Forward lemmas with test for finite colength *****************************)
-lemma frees_fwd_isfin: โf,L,T. L โข ๐
*โฆTโฆ โ f โ ๐
โฆfโฆ.
+lemma frees_fwd_isfin: โf,L,T. L โข ๐
+โฆTโฆ โ f โ ๐
โฆfโฆ.
#f #L #T #H elim H -f -L -T
/4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
qed-.