Theory MarkedLambda

Up to index of Isabelle/HOL/residual-beta-theory

(*  Title:      MarkedLambda.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    15th March, 2001

- Definition of marked lambda terms using one-sorted variable names
  (Note we take the theory of one-sorted variables from our raw confluence
   development.)
- Definition of bound, free and capturing variables
- Definition of substitution
- Definition of unique bindings on terms and the BCF predicate
*)

MarkedLambda = Variables +

datatype mlterm = Var var
                | "$" mlterm mlterm (infixl 200)
                | Abs var mlterm
                | Redex var mlterm mlterm ("<Abs _ _> @ _ " [200,0,0] 200)

consts
  BV     :: mlterm => var set
  FV     :: mlterm => var set
  Capt   :: [var,mlterm] => var set
  subst  :: [mlterm,var,mlterm] => mlterm ("_[_:=_]" [300,0,0] 300)
  UB     :: mlterm => bool
  BCF    :: mlterm => 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})"
  BV_Red "BV(<Abs x e1> @ e2) = (BV(e1) Un BV(e2) 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})"
  FV_Red "FV(<Abs x e1> @ e2) = (FV(e1) - {x}) Un FV(e2)"

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 {})"
  Capt_Red "Capt x (<Abs y e1> @ e2) = (if x~=y & x:FV(e1)
                                        then (Capt x e1) Un (Capt x e2) Un {y}
                                        else (Capt x e2))"
  
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)"
  subst_Red "(<Abs x e1> @ e2)[y:=e] = (if x~=y & x~:FV(e)
                                        then <Abs x (e1[y:=e])> @ e2[y:=e]
                                        else <Abs x e1> @ e2[y:=e])"
  
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))"
  UB_Red "UB(<Abs x e1> @ e2) = (UB(e1) & UB(e2) & x~:BV(e1) & x~:BV(e2) &
                                 (BV(e1) Int BV(e2) = {}))"

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

end

theorem FV_Capt_1:

  y : Capt x e ==> x : FV e

theorem FV_Capt_2:

  x ~: FV e ==> Capt x e = {}

theorem renaming_sanity_1:

  e[x:=Var x] = e

theorem renaming_sanity_2:

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

theorem Capt_in_BV:

  Capt x e <= BV e

theorem renaming_sanity_3:

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

theorem Capt_induct_1:

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

theorem Capt_induct_2:

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

theorem Capt_induct_3:

  Capt y (<Abs var e1> @ e2 ) Int A = {}
  ==> Capt y e2 Int A = {} &
      (var ~= y --> Capt y e1 Int A = {} & (y : FV e1 --> var ~: A))

theorem Capt_Int_FV_lemma_1:

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

theorem subset_lemma_1:

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

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 e; x ~: FV e' |] ==> x ~: FV (e[y:=e'])

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 FV_subst_lemma_7:

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

theorem Int_subst_lemma_1:

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

theorem BV_subst_lemma_1:

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

theorem Capt_in_capt_subst_1:

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

theorem Capt_in_capt_subst_2:

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

theorem Capt_subst_enabling:

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

theorem Capt_subst_enabling_2:

  [| Capt x (<Abs y e1> @ e2 ) Int FV e = {}; x ~= y |]
  ==> (<Abs y e1> @ e2 )[x:=e] = <Abs y e1[x:=e]> @ e2[x:=e] 

theorem Capt_subst_redex_1:

  Capt x ((<Abs z e1> @ e2 )[y:=e3]) Int A = {} ==> Capt x (e2[y:=e3]) Int A = {}

theorem Substitution_Lemma_1:

  [| Capt x e3 Int FV e2 = {}; y ~: FV e2; y ~= x; Capt y e1 Int FV e3 = {};
     Capt x e1 Int FV e2 = {}; Capt x (e1[y:=e3]) Int FV e2 = {} |]
  ==> e1[x:=e2][y:=e3[x:=e2]] = e1[y:=e3][x:=e2]

theorem Substitution_Lemma_2:

  [| Capt x e3 Int FV e2 = {}; y ~= x; Capt y e1 Int FV e3 = {};
     Capt y e1 Int FV (e3[x:=e2]) = {}; Capt x (e1[y:=e3]) Int FV e2 = {};
     x ~: FV e1 |]
  ==> e1[y:=e3[x:=e2]] = e1[y:=e3][x:=e2]