Theory Commutation

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

(*  Title:      HOL/Lambda/Commutation.thy
    ID:         $Id: Commutation.thy,v 1.1 2000/06/26 14:27:36 jjb Exp $
    Author:     Tobias Nipkow
    Copyright   1995  TU Muenchen

Abstract commutation and confluence notions.
*)

Commutation = Trancl +

consts
  square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
  commute :: "[('a*'a)set,('a*'a)set] => bool"
  confluent, diamond, Church_Rosser :: "('a*'a)set => bool"

defs
  square_def
 "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"

  commute_def "commute R S == square R S S R"
  diamond_def "diamond R   == commute R R"

  Church_Rosser_def "Church_Rosser(R) ==   
  !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"

translations
  "confluent R" == "diamond(R^*)"

end

theorem square_sym:

  square R S T U ==> square S R U T

theorem square_subset:

  [| square R S T U; T <= T' |] ==> square R S T' U

theorem square_reflcl:

  [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)

theorem square_rtrancl:

  square R S S T ==> square (R^*) S S (T^*)

theorem square_rtrancl_reflcl_commute:

  square R S (S^*) (R^=) ==> commute (R^*) (S^*)

theorem commute_sym:

  commute R S ==> commute S R

theorem commute_rtrancl:

  commute R S ==> commute (R^*) (S^*)

theorem commute_Un:

  [| commute R T; commute S T |] ==> commute (R Un S) T

theorem diamond_Un:

  [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)

theorem diamond_confluent:

  diamond R ==> confluent R

theorem square_reflcl_confluent:

  square R R (R^=) (R^=) ==> confluent R

theorem confluent_Un:

  [| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R Un S)

theorem diamond_to_confluence:

  [| diamond R; T <= R; R <= T^* |] ==> confluent T

theorem Church_Rosser_confluent:

  Church_Rosser R = confluent R