tidied freeness reasoning
authorpaulson
Tue Jan 19 12:59:55 1999 +0100 (1999-01-19)
changeset 61447d38744313c8
parent 6143 1eb364a68c54
child 6145 dea357e84ac9
tidied freeness reasoning
src/ZF/ex/BT.ML
src/ZF/ex/Comb.ML
     1.1 --- a/src/ZF/ex/BT.ML	Tue Jan 19 12:56:27 1999 +0100
     1.2 +++ b/src/ZF/ex/BT.ML	Tue Jan 19 12:59:55 1999 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
     1.6  by (induct_tac "l" 1);
     1.7 -by (ALLGOALS Asm_full_simp_tac);
     1.8 +by Auto_tac;
     1.9  qed_spec_mp "Br_neq_left";
    1.10  
    1.11  (*Proving a freeness theorem*)
     2.1 --- a/src/ZF/ex/Comb.ML	Tue Jan 19 12:56:27 1999 +0100
     2.2 +++ b/src/ZF/ex/Comb.ML	Tue Jan 19 12:59:55 1999 +0100
     2.3 @@ -40,7 +40,6 @@
     2.4  val Ap_E = comb.mk_cases "p#q : comb";
     2.5  
     2.6  AddSIs comb.intrs;
     2.7 -AddSEs comb.free_SEs;
     2.8  
     2.9  
    2.10  (*** Results about Contraction ***)
    2.11 @@ -87,11 +86,11 @@
    2.12  AddSEs [K_contractE, S_contractE, Ap_contractE];
    2.13  
    2.14  Goalw [I_def] "I -1-> r ==> P";
    2.15 -by (Blast_tac 1);
    2.16 +by Auto_tac;
    2.17  qed "I_contract_E";
    2.18  
    2.19  Goal "K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
    2.20 -by (Blast_tac 1);
    2.21 +by Auto_tac;
    2.22  qed "K1_contractD";
    2.23  
    2.24  Goal "[| p ---> q;  r: comb |] ==> p#r ---> q#r";
    2.25 @@ -156,31 +155,34 @@
    2.26  (*** Basic properties of parallel contraction ***)
    2.27  
    2.28  Goal "K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
    2.29 -by (Blast_tac 1);
    2.30 +by Auto_tac;
    2.31  qed "K1_parcontractD";
    2.32 +AddSDs [K1_parcontractD];
    2.33  
    2.34  Goal "S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
    2.35 -by (Blast_tac 1);
    2.36 +by Auto_tac;
    2.37  qed "S1_parcontractD";
    2.38 +AddSDs [S1_parcontractD];
    2.39  
    2.40  Goal "S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
    2.41 -by (blast_tac (claset() addSDs [S1_parcontractD]) 1);
    2.42 +by Auto_tac;
    2.43  qed "S2_parcontractD";
    2.44 +AddSDs [S2_parcontractD];
    2.45  
    2.46  (*Church-Rosser property for parallel contraction*)
    2.47  Goalw [diamond_def] "diamond(parcontract)";
    2.48  by (rtac (impI RS allI RS allI) 1);
    2.49  by (etac parcontract.induct 1);
    2.50  by (ALLGOALS 
    2.51 -    (blast_tac (claset() addSDs [K1_parcontractD, S2_parcontractD]
    2.52 -                        addIs  [parcontract_combD2])));
    2.53 +    (blast_tac (claset() addSEs comb.free_SEs
    2.54 +			 addIs [parcontract_combD2])));
    2.55  qed "diamond_parcontract";
    2.56  
    2.57  (*** Equivalence of p--->q and p===>q ***)
    2.58  
    2.59  Goal "p-1->q ==> p=1=>q";
    2.60  by (etac contract.induct 1);
    2.61 -by (ALLGOALS Blast_tac);
    2.62 +by Auto_tac;
    2.63  qed "contract_imp_parcontract";
    2.64  
    2.65  Goal "p--->q ==> p===>q";
    2.66 @@ -189,7 +191,7 @@
    2.67  by (etac rtrancl_induct 1);
    2.68  by (blast_tac (claset() addIs [r_into_trancl]) 1);
    2.69  by (blast_tac (claset() addIs [contract_imp_parcontract, 
    2.70 -			      r_into_trancl, trans_trancl RS transD]) 1);
    2.71 +			       r_into_trancl, trans_trancl RS transD]) 1);
    2.72  qed "reduce_imp_parreduce";
    2.73  
    2.74  
    2.75 @@ -200,8 +202,8 @@
    2.76  by (blast_tac (claset() addIs reduction_rls) 1);
    2.77  by (blast_tac 
    2.78      (claset() addIs [trans_rtrancl RS transD,
    2.79 -		    Ap_reduce1, Ap_reduce2, parcontract_combD1,
    2.80 -		    parcontract_combD2]) 1);
    2.81 +		     Ap_reduce1, Ap_reduce2, parcontract_combD1,
    2.82 +		     parcontract_combD2]) 1);
    2.83  qed "parcontract_imp_reduce";
    2.84  
    2.85  Goal "p===>q ==> p--->q";
    2.86 @@ -214,7 +216,7 @@
    2.87  qed "parreduce_imp_reduce";
    2.88  
    2.89  Goal "p===>q <-> p--->q";
    2.90 -by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
    2.91 +by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1);
    2.92  qed "parreduce_iff_reduce";
    2.93  
    2.94  writeln"Reached end of file.";