Theory Lambda

Up to index of Isabelle/HOL/raw-confluence-lambda

(*  Title:      Lambda.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    3rd August, 2000

- Lambda terms using concrete variable names
- Definition of bound, free and capturing variables
- Definition of substitution
- Definition of "sharp" substitution which enables some case-splitting on
  substitution to be avoided under the correct side conditions
- Definition of unique bindings on terms and the BCF predicate
*)

Lambda = Variables +

datatype lterm = Var var | "$" lterm lterm (infixl 200) | Abs var lterm

consts
  BV     :: lterm => var set
  FV     :: lterm => var set
  Capt   :: [var,lterm] => var set
  subst  :: [lterm,var,lterm] => lterm ("_[_:=_]" [300,0,0] 300)
  subst2 :: [lterm,var,lterm] => lterm ("_<_:=_>" [300,0,0] 300)
  UB     :: lterm => bool
  BCF    :: lterm => bool

primrec
  BV_Var "BV(Var x) = {}"
  BV_App "BV(e1 $ e2) = (BV(e1) Un BV(e2))"
  BV_Abs "BV(Abs x e) = (BV(e) Un {x})"
  
primrec
  FV_Var "FV(Var x) = {x}"
  FV_App "FV(e1 $ e2) = (FV(e1) Un FV(e2))"
  FV_Abs "FV(Abs x e) = (FV(e) - {x})"

primrec
  Capt_Var "Capt x (Var y) = {}"
  Capt_App "Capt x (e1 $ e2) = (Capt x e1) Un (Capt x e2)"
  Capt_Abs "Capt x (Abs y e) = (if x~=y & x:FV(e)
                                then (Capt x e) Un {y}
                                else {})"
  
primrec
  subst_Var "(Var x)[y:=e] = (if x=y then e else Var x)"
  subst_App "(e1 $ e2)[y:=e] = e1[y:=e] $ e2[y:=e]"
  subst_Abs "(Abs x e1)[y:=e] = (if x~=y & x~:FV(e) 
                                 then Abs x (e1[y:=e])
                                 else Abs x e1)"

primrec
  subst2_Var "(Var x)<y:=e> = (if x=y then e else Var x)"
  subst2_App "(e1 $ e2)<y:=e> = e1<y:=e> $ e2<y:=e>"
  subst2_Abs "(Abs x e1)<y:=e> = (if x~=y then Abs x (e1<y:=e>) else Abs x e1)"

primrec
  UB_Var "UB(Var x) = True"
  UB_App "UB(e1 $ e2) = (UB(e1) & UB(e2) & (BV(e1) Int BV(e2) = {}))"
  UB_Abs "UB(Abs x e) = (UB(e) & x~:BV(e))"

defs
  BCF "BCF(e) == (UB(e) & (FV(e) Int BV(e) = {}))"

end

theorem aux_renaming_lemma_1:

  y : Capt x e --> x : FV e

theorem renaming_sanity_1:

  e[x:=Var x] = e

theorem renaming_sanity_2:

  x ~: FV e --> e[x:=e'] = e

theorem renaming_sanity_3:

  x ~: FV e' & Capt x e Int FV e' = {} --> x ~: FV (e[x:=e'])

theorem renaming_sanity_3:

  [| x ~: FV e'; Capt x e Int FV e' = {} |] ==> x ~: FV (e[x:=e'])

theorem renaming_sanity_4:

  y ~: FV e --> e[x:=Var y][y:=Var x] = e

theorem subset_lemma_1:

  [| A <= B; x ~: B |] ==> x ~: A

theorem subset_lemma_2:

  [| A - {x} <= B - {x}; y : A; x ~= y |] ==> y : B

theorem Capt_FV_lemma_1:

  y ~: FV e --> Capt y e = {}

theorem Capt_BV_lemma_1:

  y ~: BV e --> y ~: Capt x e

theorem Capt_Int_FV_lemma_1:

  [| Capt y (Abs z e) Int FV e' = {}; y ~= z |] ==> z ~: FV e' | y ~: FV e

theorem FV_subst_lemma_1:

  x : FV (e[y:=e']) ==> x : FV e' | x : FV e

theorem FV_subst_lemma_2:

  x : FV e --> x ~= y --> x : FV (e[y:=e'])

theorem FV_subst_lemma_3:

  x : FV e' ==> x : FV e --> x : FV (e[y:=e'])

theorem FV_subst_lemma_4:

  x : FV e1 --> y : FV e2 --> y : FV (e1[x:=e2]) | e1[x:=e2] = e1

theorem special_contrapositive:

  A --> B --> C ==> ¬ C --> ¬ A | ¬ B

theorem FV_subst_lemma_5:

  x ~: FV (e[y:=e']) ==> x ~: FV e | x = y

theorem FV_subst_lemma_6:

  x : FV e' ==> Capt y e Int FV e' = {} --> y : FV e --> x : FV (e[y:=e'])

theorem capt_in_bound_var:

  Capt x e <= BV e

theorem BV_subst_lemma_1:

  x : BV (e[y:=e']) ==> x : BV e | x : BV e'

theorem FV_lemma_1:

  x ~: FV e & x ~: FV e' --> x ~: FV (e[y:=e'])

theorem FV_var_subst_lemma_1:

  [| y ~: FV e; y ~= z |] ==> y ~: FV (e[x:=Var z])

theorem BV_var_subst_lemma_1:

  y ~: BV e ==> y ~: BV (e[x:=Var z])

theorem Capt_induct_1:

  Capt y (e1 $ e2) Int A = {} ==> Capt y e1 Int A = {} & Capt y e2 Int A = {}

theorem Capt_induct_2:

  (Capt x (e1 $ e2) Un A) Int B = {}
  ==> (Capt x e1 Un A) Int B = {} & (Capt x e2 Un A) Int B = {}

theorem Capt_induct_3:

  [| x ~= y; Capt y (Abs x e) Int A = {} |] ==> Capt y e Int A = {}

theorem Capt_induct_4:

  [| y ~= x; (Capt x (Abs y e) Un A) Int B = {} |] ==> (Capt x e Un A) Int B = {}

theorem Capt_induct_5:

  [| Capt x (Abs y (e1 $ e2)) Int A = {}; y ~= x |]
  ==> Capt x (Abs y e1) Int A = {} & Capt x (Abs y e2) Int A = {}

theorem Capt_induct_6:

  [| Capt x (Abs y (Abs z e)) Int A = {}; y ~= x; z ~= x |]
  ==> Capt x (Abs y e) Int A = {}

theorem subst_equivalence:

  Capt x e1 Int FV e2 = {} ==> e1[x:=e2] = e1<x:=e2>