equal
deleted
inserted
replaced
126 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
126 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
127 \ |] ==> m le n --> P(m) --> P(n)"; |
127 \ |] ==> m le n --> P(m) --> P(n)"; |
128 by (nat_ind_tac "n" prems 1); |
128 by (nat_ind_tac "n" prems 1); |
129 by (ALLGOALS |
129 by (ALLGOALS |
130 (asm_simp_tac |
130 (asm_simp_tac |
131 (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff])))); |
131 (ZF_ss addsimps (prems@distrib_simps@[le0_iff, le_succ_iff])))); |
132 qed "nat_induct_from_lemma"; |
132 qed "nat_induct_from_lemma"; |
133 |
133 |
134 (*Induction starting from m rather than 0*) |
134 (*Induction starting from m rather than 0*) |
135 val prems = goal Nat.thy |
135 val prems = goal Nat.thy |
136 "[| m le n; m: nat; n: nat; \ |
136 "[| m le n; m: nat; n: nat; \ |