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