Theory SubstLemmas

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

(*  Title:      SubstLemmas.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    29th August, 2000

- Definition of bound variables, unique bindings, BCF, and beta-enabling on
  terms
*)

SubstLemmas = Lambda +

end

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 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]

theorem disjoint_monotinicity:

  (A Un B) Int C = {} ==> A Int C = {} & B Int C = {}

theorem Capt_subst_distribute:

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

theorem Capt_subst_var_lemma_1:

  [| Capt x e Int A = {}; y ~: FV e; y ~: BV e; x ~= y |]
  ==> Capt y (e[x:=Var y]) Int A = {}

theorem Substitution_Lemma_3:

  [| Capt x e Int FV e' = {}; y ~: FV e; y ~: BV e |]
  ==> e[x:=Var y][y:=e'] = e[x:=e']

theorem Substitution_Lemma_4:

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