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 "basic_2/syntax/bind.ma".
16 include "basic_2/static/frees.ma".
18 (* CONTEXT-SENSITIVE FREE VARIABLES FOR BINDERS *****************************)
20 inductive freesb (L): relation2 β¦ β
21 | freesb_pair: βI,V,f. L β’ π
*β¦Vβ¦ β‘ f β freesb L (BPair I V) f
22 | freesb_unit: βI,f. πβ¦fβ¦ β freesb L (BUnit I) f
26 "context-sensitive free variables (binder)"
27 'FreeStar L I f = (freesb L I f).
29 (* Basic inversion lemmas ***************************************************)
31 fact frees_inv_pair_aux: βL,Z,f. L β’ π
*β¦Zβ¦ β‘ f β
32 βI,V. Z = BPair I V β L β’ π
*β¦Vβ¦ β‘ f.
34 [ #I #V #f #Hf #Z #X #H destruct //
35 | #I #f #_ #Z #X #H destruct
39 lemma frees_inv_pair: βL,I,V,f. L β’ π
*β¦BPair I Vβ¦ β‘ f β L β’ π
*β¦Vβ¦ β‘ f.
40 /2 width=4 by frees_inv_pair_aux/ qed-.
42 fact frees_inv_unit_aux: βL,Z,f. L β’ π
*β¦Zβ¦ β‘ f β
43 βI. Z = BUnit I β πβ¦fβ¦.
45 [ #I #V #f #_ #Z #H destruct
46 | #I #f #Hf #Z #H destruct //
50 lemma frees_inv_unit: βL,I,f. L β’ π
*β¦BUnit Iβ¦ β‘ f β πβ¦fβ¦.
51 /2 width=5 by frees_inv_unit_aux/ qed-.