# HG changeset patch
# User nipkow
# Date 801674286 -7200
# Node ID 8e81ad0c6f12833b73dc07c461dc38eede5acfc7
# Parent  0df0df1685a8d56a185028a681d18341f44a11cf
Added Church-Rosser

diff -r 0df0df1685a8 -r 8e81ad0c6f12 src/HOL/Lambda/Confluence.ML
--- a/src/HOL/Lambda/Confluence.ML	Sun May 28 17:17:43 1995 +0200
+++ b/src/HOL/Lambda/Confluence.ML	Sun May 28 17:18:06 1995 +0200
@@ -12,7 +12,7 @@
   "!!R. confluent1(R) ==> diamond(R^*)";
 by(strip_tac 1);
 be rtrancl_induct 1;
-by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_trans])));
+by(ALLGOALS(fast_tac (trancl_cs addEs [rtrancl_trans])));
 qed "confluent1_diamond";
 
 goalw Confluence.thy [confluent1_def,confluent2_def]
@@ -24,7 +24,7 @@
   "!!R. diamond(R) ==> confluent2(R)";
 by(strip_tac 1);
 be rtrancl_induct 1;
-by(fast_tac (HOL_cs addSIs [rtrancl_refl]) 1);
+by(fast_tac trancl_cs 1);
 by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
 qed "diamond_confluent2";
 
@@ -37,3 +37,21 @@
                     addDs [subset_antisym]
                     addss (HOL_ss addsimps [rtrancl_idemp])) 1);
 qed "diamond_to_confluence";
+
+goalw Confluence.thy [confluent_def,diamond_def,Church_Rosser_def]
+  "Church_Rosser(R) = confluent(R)";
+br iffI 1;
+ by(safe_tac HOL_cs);
+ be allE 1;
+ be allE 1;
+ be mp 1;
+ br rtrancl_trans 1;
+  br (Un_upper2 RS rtrancl_mono RS subsetD) 1;
+  br rtrancl_converseI 1;
+  be converseI 1;
+ be (Un_upper1 RS rtrancl_mono RS subsetD) 1;
+be rtrancl_induct 1;
+ by(fast_tac trancl_cs 1);
+ by(slow_tac (rel_cs addIs [r_into_rtrancl]
+                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
+qed "Church_Rosser_confluent";
diff -r 0df0df1685a8 -r 8e81ad0c6f12 src/HOL/Lambda/Confluence.thy
--- a/src/HOL/Lambda/Confluence.thy	Sun May 28 17:17:43 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy	Sun May 28 17:18:06 1995 +0200
@@ -9,7 +9,8 @@
 Confluence = Trancl +
 
 consts
-  confluent, confluent1, confluent2, diamond :: "('a*'a)set => bool"
+  confluent, confluent1, confluent2, diamond, Church_Rosser ::
+  "('a*'a)set => bool"
 
 defs
   diamond_def
@@ -25,4 +26,6 @@
   "confluent2(R) ==
    !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
 
+  Church_Rosser_def "Church_Rosser(R) ==   \
+\ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
 end