Up to index of Isabelle/HOL/raw-confluence-lambda
theory DiamondPB = ParBeta(* Title: DiamondPB.thy Author: James Brotherston / Rene Vestergaard Revised: 30th August, 2000 - Complete developments function - used to prove diamond property of parallel beta via the Takahashi prof method. *) DiamondPB = ParBeta + consts comp_dev :: "(lterm * lterm) set" syntax "->CD" :: [lterm,lterm] => bool (infixl 50) translations "s ->CD t" == "(s,t) : comp_dev" inductive comp_dev intrs var "Var x ->CD Var x" abs "s ->CD t ==> Abs x s ->CD Abs x t" appV "s ->CD t ==> Var x $ s ->CD Var x $ t" appA "[| (t1 $ t2) ->CD t'; s->CD s' |] ==> ((t1 $ t2) $ s) ->CD (t' $ s')" beta "[| s ->CD s'; t ->CD t'; (Capt x s') Int FV(t') = {} |] ==> (Abs x s) $ t ->CD s'[x:=t']" end
theorem par_beta_CD_triangle:
s ->CD t' ==> ALL t. s -|>B t --> t -|>B t'
theorem CD_subset_par_beta:
s ->CD t ==> s -|>B t
theorem BCF_abs:
BCF (Abs x e) ==> BCF e
theorem BCF_app:
BCF (e1 $ e2) ==> BCF e1 & BCF e2
theorem BCF_consq_1:
BCF (Abs x e1 $ e2) ==> BV e1 Int FV e2 = {}
theorem BCF_implies_exists_CD:
BCF s --> (EX t. s ->CD t)
theorem par_beta_diamond:
[| BCF s; s -|>B t; s -|>B t' |] ==> EX s'. t -|>B s' & t' -|>B s'