# HG changeset patch
# User nipkow
# Date 803891709 -7200
# Node ID b373cb33352fcbf8b9b1f27fc41fe324b06929cd
# Parent  928a16e02f9f88817df2371c9556a6ff0a2953e8
Put in direct proof of C-R w/o detour via cd.

diff -r 928a16e02f9f -r b373cb33352f src/HOL/Lambda/Confluence.thy
--- a/src/HOL/Lambda/Confluence.thy	Thu Jun 22 17:13:05 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy	Fri Jun 23 09:15:09 1995 +0200
@@ -14,7 +14,7 @@
 
 defs
   diamond_def
-  "diamond(R) == !x y z. (x,y):R --> (x,z):R --> (EX u. (y,u):R & (z,u):R)" 
+  "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^*)"
 
diff -r 928a16e02f9f -r b373cb33352f src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Thu Jun 22 17:13:05 1995 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Fri Jun 23 09:15:09 1995 +0200
@@ -49,22 +49,6 @@
         rtrancl_into_rtrancl] addEs [rtrancl_trans])));
 qed "par_beta_subset_beta";
 
-(*** cd ***)
-
-goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
-by(simp_tac (parred_ss addsimps [cd_App]) 1);
-qed"cd_App_Var";
-
-goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
-by(simp_tac (parred_ss addsimps [cd_App]) 1);
-qed"cd_App_App";
-
-goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
-by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
-qed"cd_App_Fun";
-
-val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
-
 (*** => ***)
 
 goal ParRed.thy "!s' n. s => s' --> lift s n => lift s' n";
@@ -87,6 +71,32 @@
 bind_thm("par_beta_subst",
          result()  RS spec RS spec RS spec RS spec RS mp RS mp);
 
+(*** Confluence (directly) ***)
+
+goalw ParRed.thy [diamond_def] "diamond(par_beta)";
+by(REPEAT(rtac allI 1));
+br impI 1;
+be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst])));
+qed "diamond_par_beta";
+
+
+(*** cd ***)
+
+goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
+by(simp_tac (parred_ss addsimps [cd_App]) 1);
+qed"cd_App_Var";
+
+goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
+by(simp_tac (parred_ss addsimps [cd_App]) 1);
+qed"cd_App_App";
+
+goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
+by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
+qed"cd_App_Fun";
+
+val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
+
 goal ParRed.thy "!t. s => t --> t => cd s";
 by(db.induct_tac "s" 1);
   by(simp_tac parred_ss 1);
@@ -95,7 +105,7 @@
  by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss parred_ss)));
 bind_thm("par_beta_cd", result() RS spec RS mp);
 
-(*** Confluence ***)
+(*** Confluence (via cd) ***)
 
 goalw ParRed.thy [diamond_def] "diamond(par_beta)";
 by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);