# HG changeset patch
# User paulson
# Date 861785341 -7200
# Node ID f5554654d211d41b7b64b31aab99f96a14168989
# Parent  01a563785367222e2527d73e67e369505e36210f
Moved diamond_trancl (which is independent of the rest) to the top

diff -r 01a563785367 -r f5554654d211 src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Wed Apr 23 10:47:36 1997 +0200
+++ b/src/ZF/ex/Comb.ML	Wed Apr 23 10:49:01 1997 +0200
@@ -17,9 +17,33 @@
 
 open Comb;
 
+(*** Transitive closure preserves the Church-Rosser property ***)
+
+goalw Comb.thy [diamond_def]
+    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
+\    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
+by (etac trancl_induct 1);
+by (blast_tac (!claset addIs [r_into_trancl]) 1);
+by (slow_best_tac (!claset addSDs [spec RS mp]
+                           addIs  [r_into_trancl, trans_trancl RS transD]) 1);
+val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
+
+val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
+by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
+by (rtac (impI RS allI RS allI) 1);
+by (etac trancl_induct 1);
+by (ALLGOALS (*Seems to be a brittle, undirected search*)
+    (slow_best_tac (!claset addIs [r_into_trancl, trans_trancl RS transD]
+                            addEs [major RS diamond_strip_lemmaE])));
+qed "diamond_trancl";
+
+
 val [_,_,comb_Ap] = comb.intrs;
 val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
 
+AddSIs comb.intrs;
+AddSEs comb.free_SEs;
+
 
 (*** Results about Contraction ***)
 
@@ -38,19 +62,20 @@
 bind_thm ("rtrancl_into_rtrancl2",
     (r_into_rtrancl RS (trans_rtrancl RS transD)));
 
-val reduction_rls = [reduction_refl, contract.K, contract.S, 
-                     contract.K RS rtrancl_into_rtrancl2,
+AddSIs [reduction_refl, contract.K, contract.S];
+
+val reduction_rls = [contract.K RS rtrancl_into_rtrancl2,
                      contract.S RS rtrancl_into_rtrancl2,
                      contract.Ap1 RS rtrancl_into_rtrancl2,
                      contract.Ap2 RS rtrancl_into_rtrancl2];
 
 (*Example only: not used*)
 goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
-by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
+by (blast_tac (!claset addIs reduction_rls) 1);
 qed "reduce_I";
 
 goalw Comb.thy [I_def] "I: comb";
-by (REPEAT (ares_tac comb.intrs 1));
+by (Blast_tac 1);
 qed "comb_I";
 
 (** Non-contraction results **)
@@ -60,11 +85,8 @@
 val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
 val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
 
-AddSIs comb.intrs;
-AddIs  contract.intrs;
-AddSEs [contract_combD1,contract_combD2];     (*type checking*)
+AddIs  [contract.Ap1, contract.Ap2];
 AddSEs [K_contractE, S_contractE, Ap_contractE];
-AddSEs comb.free_SEs;
 
 goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
 by (Blast_tac 1);
@@ -80,7 +102,7 @@
 by (etac rtrancl_induct 1);
 by (blast_tac (!claset addIs reduction_rls) 1);
 by (etac (trans_rtrancl RS transD) 1);
-by (fast_tac (!claset addIs reduction_rls) 1);
+by (blast_tac (!claset addIs (contract_combD2::reduction_rls)) 1);
 qed "Ap_reduce1";
 
 goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> r#p ---> r#q";
@@ -89,7 +111,7 @@
 by (etac rtrancl_induct 1);
 by (blast_tac (!claset addIs reduction_rls) 1);
 by (etac (trans_rtrancl RS transD) 1);
-by (fast_tac (!claset addIs reduction_rls) 1);
+by (blast_tac (!claset addIs (contract_combD2::reduction_rls)) 1);
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
@@ -108,7 +130,7 @@
 
 goalw Comb.thy [diamond_def] "~ diamond(contract)";
 by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
-                    addSEs [I_contract_E]) 1);
+                       addSEs [I_contract_E]) 1);
 qed "not_diamond_contract";
 
 
@@ -130,11 +152,8 @@
 val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
 val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
 
-AddSIs comb.intrs;
 AddIs  parcontract.intrs;
 AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE];
-AddSEs [parcontract_combD1, parcontract_combD2];     (*type checking*)
-AddSEs comb.free_SEs;
 
 (*** Basic properties of parallel contraction ***)
 
@@ -156,30 +175,10 @@
 by (rtac (impI RS allI RS allI) 1);
 by (etac parcontract.induct 1);
 by (ALLGOALS 
-    (fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD])));
+    (blast_tac (!claset addSDs [K1_parcontractD, S2_parcontractD]
+                        addIs  [parcontract_combD2])));
 qed "diamond_parcontract";
 
-(*** Transitive closure preserves the Church-Rosser property ***)
-
-goalw Comb.thy [diamond_def]
-    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
-\    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
-by (etac trancl_induct 1);
-by (blast_tac (!claset addIs [r_into_trancl]) 1);
-by (slow_best_tac (!claset addSDs [spec RS mp]
-                           addIs  [r_into_trancl, trans_trancl RS transD]) 1);
-val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
-
-val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
-by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
-by (rtac (impI RS allI RS allI) 1);
-by (etac trancl_induct 1);
-by (ALLGOALS
-    (slow_best_tac (!claset addIs [r_into_trancl, trans_trancl RS transD]
-                          addEs [major RS diamond_strip_lemmaE])));
-qed "diamond_trancl";
-
-
 (*** Equivalence of p--->q and p===>q ***)
 
 goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
@@ -202,11 +201,10 @@
 by (blast_tac (!claset addIs reduction_rls) 1);
 by (blast_tac (!claset addIs reduction_rls) 1);
 by (blast_tac (!claset addIs reduction_rls) 1);
-by (rtac (trans_rtrancl RS transD) 1);
-by (ALLGOALS 
-    (blast_tac 
-     (!claset addIs [Ap_reduce1, Ap_reduce2, parcontract_combD1,
-		     parcontract_combD2])));
+by (blast_tac 
+    (!claset addIs [trans_rtrancl RS transD,
+		    Ap_reduce1, Ap_reduce2, parcontract_combD1,
+		    parcontract_combD2]) 1);
 qed "parcontract_imp_reduce";
 
 goal Comb.thy "!!p q. p===>q ==> p--->q";