src/ZF/Integ/Int.ML
changeset 9491 1a36151ee2fc
parent 9333 5cacc383157a
child 9496 07e33cac5d9c
     1.1 --- a/src/ZF/Integ/Int.ML	Tue Aug 01 13:43:22 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Tue Aug 01 15:28:21 2000 +0200
     1.3 @@ -16,20 +16,6 @@
     1.4  
     1.5  (*** Proving that intrel is an equivalence relation ***)
     1.6  
     1.7 -(*By luck, requires no typing premises for y1, y2,y3*)
     1.8 -val eqa::eqb::prems = goal Arith.thy 
     1.9 -    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    1.10 -\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    1.11 -by (cut_facts_tac prems 1);
    1.12 -by (res_inst_tac [("k","x2")] add_left_cancel 1);
    1.13 -by (rtac (add_left_commute RS trans) 1);
    1.14 -by Auto_tac;
    1.15 -by (stac eqb 1);
    1.16 -by (rtac (add_left_commute RS trans) 1);
    1.17 -by (stac eqa 3);
    1.18 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
    1.19 -qed "int_trans_lemma";
    1.20 -
    1.21  (** Natural deduction for intrel **)
    1.22  
    1.23  Goalw [intrel_def]
    1.24 @@ -64,6 +50,16 @@
    1.25  AddSIs [intrelI];
    1.26  AddSEs [intrelE];
    1.27  
    1.28 +val eqa::eqb::prems = goal Arith.thy 
    1.29 +    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    1.30 +by (res_inst_tac [("k","x2")] add_left_cancel 1);
    1.31 +by (rtac (add_left_commute RS trans) 1);
    1.32 +by Auto_tac;
    1.33 +by (stac eqb 1);
    1.34 +by (rtac (add_left_commute RS trans) 1);
    1.35 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
    1.36 +qed "int_trans_lemma";
    1.37 +
    1.38  Goalw [equiv_def, refl_def, sym_def, trans_def]
    1.39      "equiv(nat*nat, intrel)";
    1.40  by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    1.41 @@ -239,8 +235,7 @@
    1.42  (*The rest should be trivial, but rearranging terms is hard;
    1.43    add_ac does not help rewriting with the assumptions.*)
    1.44  by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
    1.45 -by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
    1.46 -by Auto_tac;
    1.47 +by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
    1.48  by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
    1.49  qed "zadd_congruent2";
    1.50