--- a/src/HOL/Lambda/Confluence.ML Thu Jun 22 12:44:29 1995 +0200
+++ b/src/HOL/Lambda/Confluence.ML Thu Jun 22 12:45:08 1995 +0200
@@ -8,32 +8,28 @@
open Confluence;
-goalw Confluence.thy [confluent1_def,diamond_def]
- "!!R. confluent1(R) ==> diamond(R^*)";
-by(strip_tac 1);
-be rtrancl_induct 1;
-by(ALLGOALS(fast_tac (trancl_cs addEs [rtrancl_trans])));
-qed "confluent1_diamond";
-
-goalw Confluence.thy [confluent1_def,confluent2_def]
- "!!R. confluent2(R) ==> confluent1(R)";
-by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
-qed "confluent2_confluent1";
-
-goalw Confluence.thy [confluent2_def,diamond_def]
- "!!R. diamond(R) ==> confluent2(R)";
-by(strip_tac 1);
+goal Confluence.thy
+ "!!R. [| !x y z. (x,y):R --> (x,z):S --> (? u. (y,u):S & (z,u):R); \
+\ (x,y):R; (x,z):S^* |] ==> ? u. (y,u):S^* & (z,u):R";
be rtrancl_induct 1;
by(fast_tac trancl_cs 1);
by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
-qed "diamond_confluent2";
+qed "commute_rtrancl";
+
+goal HOL.thy "!!P. ? x.P(x) & Q(x) ==> ? x. Q(x) & P(x)";
+by(fast_tac HOL_cs 1);
+val lemma = result();
+
+goalw Confluence.thy [diamond_def]
+ "!!R. diamond(R) ==> diamond(R^*)";
+by(best_tac (HOL_cs addIs [commute_rtrancl,commute_rtrancl RS lemma]) 1);
+qed "diamond_diamond_rtrancl";
goalw Confluence.thy [confluent_def]
"!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
bd rtrancl_mono 1;
bd rtrancl_mono 1;
-by(fast_tac (HOL_cs addIs [diamond_confluent2, confluent2_confluent1,
- confluent1_diamond]
+by(fast_tac (HOL_cs addIs [diamond_diamond_rtrancl]
addDs [subset_antisym]
addss (HOL_ss addsimps [rtrancl_idemp])) 1);
qed "diamond_to_confluence";