src/ZF/Integ/Int.ML
changeset 6153 bff90585cce5
parent 5758 27a2b36efd95
child 8201 a81d18b0a9b1
     1.1 --- a/src/ZF/Integ/Int.ML	Mon Jan 25 20:35:19 1999 +0100
     1.2 +++ b/src/ZF/Integ/Int.ML	Wed Jan 27 10:31:31 1999 +0100
     1.3 @@ -20,13 +20,14 @@
     1.4  val eqa::eqb::prems = goal Arith.thy 
     1.5      "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
     1.6  \       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
     1.7 +by (cut_facts_tac prems 1);
     1.8  by (res_inst_tac [("k","x2")] add_left_cancel 1);
     1.9 -by (resolve_tac prems 2);
    1.10 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    1.11 +by (rtac (add_left_commute RS trans) 1);
    1.12 +by Auto_tac;
    1.13  by (stac eqb 1);
    1.14 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    1.15 -by (stac eqa 1);
    1.16 -by (rtac (add_left_commute) 1 THEN typechk_tac prems);
    1.17 +by (rtac (add_left_commute RS trans) 1);
    1.18 +by (stac eqa 3);
    1.19 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
    1.20  qed "int_trans_lemma";
    1.21  
    1.22  (** Natural deduction for intrel **)
    1.23 @@ -79,15 +80,15 @@
    1.24  
    1.25  Goalw [int_def,quotient_def,int_of_def]
    1.26      "m : nat ==> $#m : int";
    1.27 -by (fast_tac (claset() addSIs [nat_0I]) 1);
    1.28 +by Auto_tac;
    1.29  qed "int_of_type";
    1.30  
    1.31  Addsimps [int_of_type];
    1.32 +AddTCs   [int_of_type];
    1.33  
    1.34  Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    1.35  by (dtac (sym RS eq_intrelD) 1);
    1.36 -by (typechk_tac [nat_0I, SigmaI]);
    1.37 -by (Asm_full_simp_tac 1);
    1.38 +by Auto_tac;
    1.39  qed "int_of_inject";
    1.40  
    1.41  AddSDs [int_of_inject];
    1.42 @@ -108,9 +109,9 @@
    1.43  val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
    1.44  
    1.45  Goalw [int_def,zminus_def] "z : int ==> $~z : int";
    1.46 -by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
    1.47 -                 quotientI]);
    1.48 +by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
    1.49  qed "zminus_type";
    1.50 +AddTCs [zminus_type];
    1.51  
    1.52  Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
    1.53  by (etac (zminus_ize UN_equiv_class_inject) 1);
    1.54 @@ -160,7 +161,7 @@
    1.55  
    1.56  Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
    1.57  by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
    1.58 -be natE 1;
    1.59 +by (etac natE 1);
    1.60  by (dres_inst_tac [("x","0")] spec 2);
    1.61  by Auto_tac;
    1.62  qed "not_znegative_imp_zero";
    1.63 @@ -178,9 +179,10 @@
    1.64  Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
    1.65  
    1.66  Goalw [zmagnitude_def] "zmagnitude(z) : nat";
    1.67 -br theI2 1;
    1.68 +by (rtac theI2 1);
    1.69  by Auto_tac;
    1.70  qed "zmagnitude_type";
    1.71 +AddTCs [zmagnitude_type];
    1.72  
    1.73  Goalw [int_def, znegative_def, int_of_def]
    1.74       "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
    1.75 @@ -188,14 +190,14 @@
    1.76  by (rename_tac "i j" 1);
    1.77  by (dres_inst_tac [("x", "i")] spec 1);
    1.78  by (dres_inst_tac [("x", "j")] spec 1);
    1.79 -br bexI 1;
    1.80 -br (add_diff_inverse2 RS sym) 1;
    1.81 +by (rtac bexI 1);
    1.82 +by (rtac (add_diff_inverse2 RS sym) 1);
    1.83  by Auto_tac;
    1.84  by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
    1.85  qed "not_zneg_int_of";
    1.86  
    1.87  Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
    1.88 -bd not_zneg_int_of 1;
    1.89 +by (dtac not_zneg_int_of 1);
    1.90  by Auto_tac;
    1.91  qed "not_zneg_mag"; 
    1.92  
    1.93 @@ -214,7 +216,7 @@
    1.94  qed "zneg_int_of";
    1.95  
    1.96  Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
    1.97 -bd zneg_int_of 1;
    1.98 +by (dtac zneg_int_of 1);
    1.99  by Auto_tac;
   1.100  qed "zneg_mag"; 
   1.101  
   1.102 @@ -236,7 +238,7 @@
   1.103    add_ac does not help rewriting with the assumptions.*)
   1.104  by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   1.105  by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
   1.106 -by (typechk_tac [add_type]);
   1.107 +by Auto_tac;
   1.108  by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   1.109  qed "zadd_congruent2";
   1.110  
   1.111 @@ -248,6 +250,7 @@
   1.112  by (simp_tac (simpset() addsimps [Let_def]) 3);
   1.113  by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   1.114  qed "zadd_type";
   1.115 +AddTCs [zadd_type];
   1.116  
   1.117  Goalw [zadd_def]
   1.118    "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   1.119 @@ -282,7 +285,8 @@
   1.120  
   1.121  (*For AC rewriting*)
   1.122  Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   1.123 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
   1.124 +by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   1.125 +by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   1.126  qed "zadd_left_commute";
   1.127  
   1.128  (*Integer addition is an AC operator*)
   1.129 @@ -343,6 +347,7 @@
   1.130                        split_type, add_type, mult_type, 
   1.131                        quotientI, SigmaI] 1));
   1.132  qed "zmult_type";
   1.133 +AddTCs [zmult_type];
   1.134  
   1.135  Goalw [zmult_def]
   1.136       "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   1.137 @@ -389,7 +394,8 @@
   1.138  
   1.139  (*For AC rewriting*)
   1.140  Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   1.141 -by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
   1.142 +by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   1.143 +by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   1.144  qed "zmult_left_commute";
   1.145  
   1.146  (*Integer multiplication is an AC operator*)