equal
deleted
inserted
replaced
7 |
7 |
8 Proof due to Herbert Ehler |
8 Proof due to Herbert Ehler |
9 *) |
9 *) |
10 |
10 |
11 (*specialized form of induction needed below*) |
11 (*specialized form of induction needed below*) |
12 val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n.P(n)"; |
12 val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)"; |
13 by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); |
13 by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); |
14 qed "nat_exh"; |
14 qed "nat_exh"; |
15 |
15 |
16 goal Puzzle.thy "! n. k=f(n) --> n <= f(n)"; |
16 goal Puzzle.thy "! n. k=f(n) --> n <= f(n)"; |
17 by (res_inst_tac [("n","k")] less_induct 1); |
17 by (res_inst_tac [("n","k")] less_induct 1); |
33 |
33 |
34 goal Puzzle.thy "f(n) < f(Suc(n))"; |
34 goal Puzzle.thy "f(n) < f(Suc(n))"; |
35 by (deepen_tac (!claset addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1); |
35 by (deepen_tac (!claset addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1); |
36 qed "lemma2"; |
36 qed "lemma2"; |
37 |
37 |
38 val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)"; |
38 val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)"; |
39 by (res_inst_tac[("n","n")]nat_induct 1); |
39 by (res_inst_tac[("n","n")]nat_induct 1); |
40 by (Simp_tac 1); |
40 by (Simp_tac 1); |
41 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
41 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
42 by (best_tac (!claset addIs (le_trans::prems)) 1); |
42 by (best_tac (!claset addIs (le_trans::prems)) 1); |
43 qed_spec_mp "mono_lemma1"; |
43 qed_spec_mp "mono_lemma1"; |