equal
deleted
inserted
replaced
499 by (rtac (mult_assoc RS trans) 1); |
499 by (rtac (mult_assoc RS trans) 1); |
500 by (rtac (mult_commute RS subst_context) 1); |
500 by (rtac (mult_commute RS subst_context) 1); |
501 qed "mult_left_commute"; |
501 qed "mult_left_commute"; |
502 |
502 |
503 bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); |
503 bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); |
|
504 |
|
505 |
|
506 Goal "[| m:nat; n:nat |] \ |
|
507 \ ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))"; |
|
508 by (induct_tac "m" 1); |
|
509 by Auto_tac; |
|
510 qed "lt_succ_eq_0_disj"; |
|
511 |
|
512 Goal "[| m:nat; n:nat |] ==> (m < succ(n)) <-> (m < n | m =n)"; |
|
513 by (induct_tac "n" 1); |
|
514 by (auto_tac (claset() addIs [leI], simpset())); |
|
515 by (dtac not_lt_imp_le 1); |
|
516 by Auto_tac; |
|
517 by (auto_tac (claset(), simpset() addsimps [le_iff])); |
|
518 qed "lt_succ_iff"; |
|
519 |
|
520 Goal "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"; |
|
521 by (eres_inst_tac [("m", "k")] diff_induct 1); |
|
522 by Auto_tac; |
|
523 qed_spec_mp "less_diff_conv"; |
|
524 |