# HG changeset patch
# User nipkow
# Date 820588084 -3600
# Node ID be7c6d77e19ccc52989f4276234a9140bb44bb3c
# Parent  439e1476a7f886d695c57966ed24575d874f5f64
Polished proofs.

diff -r 439e1476a7f8 -r be7c6d77e19c src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Tue Jan 02 10:46:50 1996 +0100
+++ b/src/HOL/Lambda/Commutation.ML	Tue Jan 02 14:08:04 1996 +0100
@@ -15,6 +15,11 @@
 qed "square_sym";
 
 goalw Commutation.thy [square_def]
+  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
+by(fast_tac set_cs 1);
+qed "square_subset";
+
+goalw Commutation.thy [square_def]
   "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
 by(fast_tac rel_cs 1);
 qed "square_reflcl";
@@ -66,6 +71,12 @@
 be commute_rtrancl 1;
 qed "diamond_confluent";
 
+goalw Commutation.thy [diamond_def]
+  "!!R. square R R (R^=) (R^=) ==> confluent R";
+by(fast_tac (trancl_cs addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
+                       addEs [square_subset]) 1);
+qed "square_reflcl_confluent";
+
 goal Commutation.thy
  "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
 \      ==> confluent(R Un S)";
diff -r 439e1476a7f8 -r be7c6d77e19c src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Tue Jan 02 10:46:50 1996 +0100
+++ b/src/HOL/Lambda/Eta.ML	Tue Jan 02 14:08:04 1996 +0100
@@ -118,22 +118,16 @@
 
 (*** Confluence of eta ***)
 
-goalw Eta.thy [id_def]
-  "!x y. x-e> y --> (!z. x-e>z --> (? u. y -e>= u & z -e>= u))";
+goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
 br eta.mutual_induct 1;
 by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
-val lemma = result() RS spec RS spec RS mp RS spec RS mp;
-
-goalw Eta.thy [diamond_def,commute_def,square_def] "diamond(eta^=)";
-by(fast_tac (eta_cs addEs [lemma]) 1);
-qed "diamond_refl_eta";
+val lemma = result();
 
 goal Eta.thy "confluent(eta)";
-by(stac (rtrancl_reflcl RS sym) 1);
-by(rtac (diamond_refl_eta RS diamond_confluent) 1);
+by(rtac (lemma RS square_reflcl_confluent) 1);
 qed "eta_confluent";
 
-(*** Congruence rules for ->> ***)
+(*** Congruence rules for -e>> ***)
 
 goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
 be rtrancl_induct 1;
@@ -157,10 +151,10 @@
 
 (*** Commutation of beta and eta ***)
 
-goal Eta.thy "!!s. s -> t ==> !i. free t i --> free s i";
-be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+goal Eta.thy "!s t. s -> t --> (!i. free t i --> free s i)";
+br beta.mutual_induct 1;
 by(ALLGOALS(Asm_full_simp_tac));
-bind_thm("free_beta", result() RS spec RS mp);
+bind_thm("free_beta", result() RS spec RS spec RS mp RS spec RS mp);
 
 goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
 br beta.mutual_induct 1;
diff -r 439e1476a7f8 -r be7c6d77e19c src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Tue Jan 02 10:46:50 1996 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Tue Jan 02 14:08:04 1996 +0100
@@ -32,16 +32,14 @@
 
 goal ParRed.thy "beta <= par_beta";
 br subsetI 1;
-by (res_inst_tac[("p","x")]PairE 1);
-by (hyp_subst_tac 1);
+by (split_all_tac 1);
 be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
 by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
 qed "beta_subset_par_beta";
 
 goal ParRed.thy "par_beta <= beta^*";
 br subsetI 1;
-by (res_inst_tac[("p","x")]PairE 1);
-by (hyp_subst_tac 1);
+by (split_all_tac 1);
 be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
 by (ALLGOALS(fast_tac (parred_cs addIs
        [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,