# HG changeset patch
# User nipkow
# Date 812974877 -3600
# Node ID 5e32f77c405406c55e1801a41c0c211440f8f6ab
# Parent  e3a391e848a9c9fe127515fc8c52ecd6bd87e6bd
Confluence became Commutation

diff -r e3a391e848a9 -r 5e32f77c4054 src/HOL/Lambda/Confluence.ML
--- a/src/HOL/Lambda/Confluence.ML	Fri Oct 06 11:20:04 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/Lambda/Confluence.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TU Muenchen
-
-Basic confluence lemmas.
-*)
-
-open Confluence;
-
-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 "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_diamond_rtrancl]
-                    addDs [subset_antisym]
-                    addss (!simpset 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(fast_tac (HOL_cs addIs
-      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
-       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
-by(safe_tac HOL_cs);
-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 e3a391e848a9 -r 5e32f77c4054 src/HOL/Lambda/Confluence.thy
--- a/src/HOL/Lambda/Confluence.thy	Fri Oct 06 11:20:04 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title: 	HOL/Lambda/Confluence.thy
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1995  TU Muenchen
-
-Abstract confluence notions.
-*)
-
-Confluence = Trancl +
-
-consts
-  confluent, confluent1, confluent2, diamond, Church_Rosser ::
-  "('a*'a)set => bool"
-
-defs
-  diamond_def
-  "diamond(R) == !x y.(x,y):R --> (!z.(x,z):R --> (EX u. (y,u):R & (z,u):R))" 
-
-  confluent_def "confluent(R) == diamond(R^*)"
-
-  Church_Rosser_def "Church_Rosser(R) ==   
-  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
-end