Theory RawConfluence

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

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

- Syntax for the union of the alpha and beta relations

*)

RawConfluence = AlphaBetaDiamond + Beta +

syntax  "->AB"  :: [lterm,lterm] => bool (infixl 50)
        "->>AB" :: [lterm,lterm] => bool (infixl 50)

translations
  "s ->AB t"  == "(s,t) : alpha Un beta"
  "s ->>AB t" == "(s,t) : (alpha Un beta)^*"

end

theorem beta_subset_par_beta:

  beta <= par_beta

theorem alphabeta_subset_relation2:

  alpha Un beta <= relation2

theorem rtrancl_beta_abs:

  s ->>B t ==> Abs x s ->>B Abs x t

theorem rtrancl_beta_appL:

  s ->>B t ==> s $ u ->>B t $ u

theorem rtrancl_beta_appR:

  s ->>B t ==> u $ s ->>B u $ t

theorem par_beta_subset_rtrancl_beta:

  par_beta <= beta^*

theorem rtrancl_left_inclusion:

  (s, t) : R^* ==> (s, t) : (R Un T)^*

theorem rtrancl_right_inclusion:

  (s, t) : R^* ==> (s, t) : (T Un R)^*

theorem relation2_subset_alphabeta:

  relation2 <= (alpha Un beta)^*

theorem raw_confluence:

  confluent (alpha Un beta)