Theory ResidualBeta

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

(*  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