--- a/src/HOL/Lambda/Commutation.ML Tue Jan 02 10:46:50 1996 +0100
+++ b/src/HOL/Lambda/Commutation.ML Tue Jan 02 14:08:04 1996 +0100
@@ -15,6 +15,11 @@
qed "square_sym";
goalw Commutation.thy [square_def]
+ "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
+by(fast_tac set_cs 1);
+qed "square_subset";
+
+goalw Commutation.thy [square_def]
"!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
by(fast_tac rel_cs 1);
qed "square_reflcl";
@@ -66,6 +71,12 @@
be commute_rtrancl 1;
qed "diamond_confluent";
+goalw Commutation.thy [diamond_def]
+ "!!R. square R R (R^=) (R^=) ==> confluent R";
+by(fast_tac (trancl_cs addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
+ addEs [square_subset]) 1);
+qed "square_reflcl_confluent";
+
goal Commutation.thy
"!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
\ ==> confluent(R Un S)";