Up to index of Isabelle/HOL/raw-confluence-lambda
theory SubstLemmas = 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]