Theory ParBeta

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

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

- Parallel beta-reduction with appropriate side-conditions
- Complete developments function
- Definition of unique bindings on terms and the BCF predicate
*)


ParBeta = SubstLemmas + 

consts  par_beta :: "(lterm * lterm) set"
  
syntax  "-|>B" :: [lterm,lterm] => bool (infixl 50)
  
translations  "s -|>B t" == "(s,t) : par_beta"
  
inductive par_beta
intrs
  var   "Var x -|>B Var x"
  abs   "s -|>B t ==> Abs x s -|>B Abs x t"
  app   "[| s -|>B s'; t -|>B t' |] ==> s $ t -|>B s' $ t'"
  beta  "[| s -|>B s'; t -|>B t'; (Capt x s') Int FV(t') = {}|]
          ==> (Abs x s) $ t -|>B s'[x:=t']"  
  
end

theorem par_beta_refl:

  e -|>B e

theorem par_beta_FV_lemma:

  ALL t'. t -|>B t' --> FV t' <= FV t

theorem par_beta_FV_lemma:

  t -|>B t' ==> FV t' <= FV t

theorem par_beta_BV_lemma:

  ALL t'. t -|>B t' --> BV t' <= BV t

theorem par_beta_BV_lemma:

  t -|>B t' ==> BV t' <= BV t

theorem Capt_in_capt_subst_1:

  x ~= y | x : FV e' ==> Capt x e <= Capt x (e[y:=e'])

theorem key_induction_1:

  [| Capt x (e[y:=e1]) Int A = {}; Capt x (Abs y s) Int B = {}; FV e <= FV s;
     A <= B |]
  ==> Capt x (Abs y e) Int A = {}

theorem Capt_in_capt_subst_2:

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

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 Int_subst_lemma_1:

  [| A Int FV e = {}; A Int FV e' = {} |] ==> A Int FV (e[x:=e']) = {}

theorem subcase1_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 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 subcase2_lemma_1:

  [| y ~: FV e'; y ~= x |] ==> Capt y e = Capt y (e[x:=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 subcase3_lemma_1:

  [| Capt x (Abs xa s'a) Int FV t' = {}; xa : FV t'; x ~= xa |] ==> x ~: FV s'a

theorem par_beta_subst:

  ALL x s' t t'.
     t -|>B t' -->
     s -|>B s' -->
     Capt x s Int FV t = {} -->
     Capt x s' Int FV t' = {} --> s[x:=t] -|>B s'[x:=t']

theorem par_beta_subst:

  [| t -|>B t'; s -|>B s'; Capt x s Int FV t = {}; Capt x s' Int FV t' = {} |]
  ==> s[x:=t] -|>B s'[x:=t']