author nipkow Fri, 23 Jun 1995 09:15:09 +0200 changeset 1156 b373cb33352f parent 1155 928a16e02f9f child 1157 da78c293e8dc
Put in direct proof of C-R w/o detour via cd.
 src/HOL/Lambda/Confluence.thy file | annotate | diff | comparison | revisions src/HOL/Lambda/ParRed.ML file | annotate | diff | comparison | revisions
--- 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^*)"

--- 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 @@
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 @@