Theory AbstractRewrites

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

(*  Title:      AbstractRewrites.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    7th December, 2000

- Properties of abstract rewrite systems and mappings between them.

*)

AbstractRewrites = Commutation +

consts
  onto :: "['a => 'b, 'a set, 'b set] => bool"
  homo :: "['a => 'b, 'a set, 'b set, ('a * 'a) set, ('b * 'b) set] => bool"
  struct_coll :: "['a => 'b, 'a set, 'b set, ('a * 'a) set, ('b * 'b) set] => bool"

defs
  onto_def "onto F A B == ALL y. y:B --> (EX x. x:A & F(x)=y)"
  
  homo_def "homo F A B RelA RelB == RelA <= A<*>A & RelB <= (B<*>B) & (ALL x x' y y'. ((x,y):RelA --> F(x)=x' --> F(y)=y' --> (x',y'):RelB))"
  
  struct_coll_def "struct_coll F A B RelA RelB == onto F A B & homo F A B RelA RelB"
  
end

theorem onto_lemma_1:

  [| onto F A B; RelB <= B <*> B; (x, y) : RelB |] ==> EX a. F a = x

theorem onto_lemma_2:

  [| onto F A B; RelB <= B <*> B; (x, u) : RelB |] ==> EX c. F c = u & c : A

theorem diamond_preservation:

  struct_coll F A B RelA RelB &
  (ALL x x' y'. (x', y') : RelB --> F x = x' --> (EX y. F y = y' & (x, y) : RelA))
  ==> diamond RelA --> diamond RelB

theorem diamond_reflection:

  struct_coll F A B RelA RelB &
  (ALL x y x' y'. (x', y') : RelB & F x = x' & F y = y' --> (x, y) : RelA)
  ==> diamond RelB --> diamond RelA

theorem lift_case3_premise_to_case4:

  struct_coll F A B RelA RelB &
  (ALL x y x' y'. (x', y') : RelB & F x = x' & F y = y' --> (x, y) : RelA)
  ==> ALL x x' y'.
         (x', y') : RelB --> F x = x' --> (EX y. F y = y' & (x, y) : RelA)

theorem diamond_equivalence:

  struct_coll F A B RelA RelB &
  (ALL x y x' y'. (x', y') : RelB & F x = x' & F y = y' --> (x, y) : RelA)
  ==> diamond RelB = diamond RelA