Theory AlphaBetaDiamond

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

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

- Choice of the "middle relation" in Nipkow's confluence result as ->>A; -|>B

*)

AlphaBetaDiamond = Commutation + WeakABComm + FreshAlphaConf +
                   DiamondPB + ExistsBCF + 

consts  relation2 :: "(lterm * lterm) set"
  
syntax  "->2"   :: [lterm,lterm] => bool (infixl 50)

translations
  "s ->2 t"   == "(s,t) : relation2"

inductive relation2
intrs
  cons "[|e1 ->>A e2; e2 -|>B e3|] ==> e1 ->2 e3"

end

theorem diamond_relation2:

  diamond relation2