Up to index of Isabelle/HOL/residual-beta-theory
theory MarkedLambda = Variables(* 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]