equal
deleted
inserted
replaced
140 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
140 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
141 \ |] ==> m le n --> P(m) --> P(n)"; |
141 \ |] ==> m le n --> P(m) --> P(n)"; |
142 by (nat_ind_tac "n" prems 1); |
142 by (nat_ind_tac "n" prems 1); |
143 by (ALLGOALS |
143 by (ALLGOALS |
144 (asm_simp_tac |
144 (asm_simp_tac |
145 (simpset() addsimps (prems@distrib_simps@[le0_iff, le_succ_iff])))); |
145 (simpset() addsimps prems @ distrib_simps @ [le0_iff, le_succ_iff]))); |
146 qed "nat_induct_from_lemma"; |
146 qed "nat_induct_from_lemma"; |
147 |
147 |
148 (*Induction starting from m rather than 0*) |
148 (*Induction starting from m rather than 0*) |
149 val prems = goal Nat.thy |
149 val prems = goal Nat.thy |
150 "[| m le n; m: nat; n: nat; \ |
150 "[| m le n; m: nat; n: nat; \ |