Up to index of Isabelle/HOL/residual-beta-theory
theory ResidualBeta = MarkedLambda(* Title: ResidualBeta.thy Author: James Brotherston / Rene Vestergaard Revised: 3rd April, 2001 - Definition of single and transitive-reflexive residual beta-reduction. - Definition of residual beta-completion. *) ResidualBeta = MarkedLambda + consts res_beta :: "(mlterm * mlterm) set" comp_res_beta :: "(mlterm * mlterm) set" syntax "->RB", "->>RB" :: [mlterm,mlterm] => bool (infixl 50) "->|RB" :: [mlterm,mlterm] => bool (infixl 50) translations "s ->RB t" == "(s,t) : res_beta" "s ->>RB t" == "(s,t) : res_beta^*" "s ->|RB t" == "(s,t) : comp_res_beta" inductive res_beta intrs rbeta "(Capt x s) Int FV(t) = {} ==> (<Abs x s> @ t ->RB s[x:=t])" rbappL "s ->RB t ==> s$u ->RB t$u" rbappR "s ->RB t ==> u$s ->RB u$t" rbabs "s ->RB t ==> Abs x s ->RB Abs x t" rbredL "s ->RB t ==> <Abs x s> @ u ->RB <Abs x t> @ u" rbredR "s ->RB t ==> <Abs x u> @ s ->RB <Abs x u> @ t" inductive comp_res_beta intrs crbeta1 "[|s ->|RB s'; t ->|RB t'; (Capt x s') Int FV(t') = {}; x:FV(s')|] ==> <Abs x s> @ t ->|RB s'[x:=t']" crbeta2 "[|s ->|RB s'; x~:FV(s')|] ==> <Abs x s> @ t ->|RB s'" crbvar "Var x ->|RB Var x" crbapp "[|s ->|RB s'; t ->|RB t'|] ==> s$t ->|RB s'$t'" crbabs "s ->|RB t ==> Abs x s ->|RB Abs x t" end
theorem BCF_abs:
BCF (Abs x e) ==> BCF e
theorem BCF_app:
BCF (e1 $ e2) ==> BCF e1 & BCF e2
theorem BCF_redex:
BCF (<Abs x e1> @ e2 ) ==> BCF e1 & BCF e2
theorem BCF_consq_1:
BCF (<Abs x e1> @ e2 ) ==> BV e1 Int FV e2 = {}
theorem comp_res_beta_BV_lemma:
s ->|RB t ==> BV t <= BV s
theorem comp_res_beta_FV_lemma:
s ->|RB t ==> FV t <= FV s
theorem BCF_residual_completion:
BCF s ==> EX t. s ->|RB t
theorem case1_lemma_1:
[| Capt y e Int FV e1 = {}; Capt y (e[x:=e1]) Int FV e2 = {} |] ==> Capt y e Int FV (e1[x:=e2]) = {}
theorem key_induction_2:
[| Capt x (e[y:=e']) Int A = {}; Capt y e Int FV e' = {}; y : FV e |] ==> Capt x e' Int A = {}
theorem subcase2_lemma_1:
[| y ~: FV e'; y ~= x |] ==> Capt y e = Capt y (e[x:=e'])
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 subcase2_lemma_2:
[| Capt y e Int FV e1 = {}; Capt x (e[y:=e1]) Int FV e2 = {}; x ~= y; y : FV e |] ==> Capt y e Int FV (e1[x:=e2]) = {}
theorem subcase1_lemma_2:
[| Capt x e Int FV e1 = {}; Capt x e Int FV (e1[x:=e2]) = {} |] ==> e[x:=e1][x:=e2] = e[x:=e1[x:=e2]]
theorem subset_lemma_2:
[| A <= B; B Int C = {} |] ==> A Int C = {}
theorem comp_res_beta_substitutivity:
[| s1 ->|RB t1; s2 ->|RB t2; Capt x s1 Int FV s2 = {}; Capt x t1 Int FV t2 = {} |] ==> s1[x:=s2] ->|RB t1[x:=t2]
theorem comp_res_beta_lazy_substitutivity:
[| s ->|RB s'; x ~: FV s'; Capt x s Int FV t = {} |] ==> s[x:=t] ->|RB s'
theorem comp_res_beta_triangle:
s ->|RB u ==> ALL t. s ->RB t --> t ->|RB u
theorem res_beta_completion_absorption:
s ->>RB t ==> s ->|RB u --> t ->|RB u
theorem non_blocked_beta_residual_theory:
[| BCF s; s ->>RB t |] ==> EX u. t ->|RB u