Theory DiamondPB

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

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