equal
deleted
inserted
replaced
33 "confluent R == diamond (R^**)" |
33 "confluent R == diamond (R^**)" |
34 |
34 |
35 |
35 |
36 subsection {* Basic lemmas *} |
36 subsection {* Basic lemmas *} |
37 |
37 |
38 subsubsection {* square *} |
38 subsubsection {* @{text "square"} *} |
39 |
39 |
40 lemma square_sym: "square R S T U ==> square S R U T" |
40 lemma square_sym: "square R S T U ==> square S R U T" |
41 apply (unfold square_def) |
41 apply (unfold square_def) |
42 apply blast |
42 apply blast |
43 done |
43 done |
68 apply (unfold commute_def) |
68 apply (unfold commute_def) |
69 apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]) |
69 apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]) |
70 done |
70 done |
71 |
71 |
72 |
72 |
73 subsubsection {* commute *} |
73 subsubsection {* @{text "commute"} *} |
74 |
74 |
75 lemma commute_sym: "commute R S ==> commute S R" |
75 lemma commute_sym: "commute R S ==> commute S R" |
76 apply (unfold commute_def) |
76 apply (unfold commute_def) |
77 apply (blast intro: square_sym) |
77 apply (blast intro: square_sym) |
78 done |
78 done |
87 apply (unfold commute_def square_def) |
87 apply (unfold commute_def square_def) |
88 apply blast |
88 apply blast |
89 done |
89 done |
90 |
90 |
91 |
91 |
92 subsubsection {* diamond, confluence, and union *} |
92 subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *} |
93 |
93 |
94 lemma diamond_Un: |
94 lemma diamond_Un: |
95 "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)" |
95 "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)" |
96 apply (unfold diamond_def) |
96 apply (unfold diamond_def) |
97 apply (blast intro: commute_Un commute_sym) |
97 apply (blast intro: commute_Un commute_sym) |