Up to index of Isabelle/HOL/raw-confluence-lambda
theory AbstractRewrites = Commutation(* 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