(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/syntax/bind.ma".
include "basic_2/static/frees.ma".

(* CONTEXT-SENSITIVE FREE VARIABLES FOR BINDERS *****************************)

inductive freesb (L): relation2 … ≝
| freesb_pair: ∀I,V,f. L ⊢ 𝐅*⦃V⦄ ≡ f → freesb L (BPair I V) f
| freesb_unit: ∀I,f. 𝐈⦃f⦄ → freesb L (BUnit I) f
.

interpretation
   "context-sensitive free variables (binder)"
   'FreeStar L I f = (freesb L I f).

(* Basic inversion lemmas ***************************************************)

fact frees_inv_pair_aux: ∀L,Z,f. L ⊢ 𝐅*⦃Z⦄ ≡ f →
                         ∀I,V. Z = BPair I V → L ⊢ 𝐅*⦃V⦄ ≡ f.
#L #Z #f * -Z -f
[ #I #V #f #Hf #Z #X #H destruct //
| #I #f #_ #Z #X #H destruct
]
qed-.

lemma frees_inv_pair: ∀L,I,V,f. L ⊢ 𝐅*⦃BPair I V⦄ ≡ f → L ⊢ 𝐅*⦃V⦄ ≡ f.
/2 width=4 by frees_inv_pair_aux/ qed-.

fact frees_inv_unit_aux: ∀L,Z,f. L ⊢ 𝐅*⦃Z⦄ ≡ f →
                         ∀I. Z = BUnit I → 𝐈⦃f⦄.
#L #Z #f * -Z -f
[ #I #V #f #_ #Z #H destruct
| #I #f #Hf #Z #H destruct //
]
qed-.

lemma frees_inv_unit: ∀L,I,f. L ⊢ 𝐅*⦃BUnit I⦄ ≡ f → 𝐈⦃f⦄.
/2 width=5 by frees_inv_unit_aux/ qed-.