equal
deleted
inserted
replaced
53 val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)"; |
53 val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)"; |
54 by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1); |
54 by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1); |
55 qed "f_mono"; |
55 qed "f_mono"; |
56 |
56 |
57 Goal "f(n) = n"; |
57 Goal "f(n) = n"; |
58 by (rtac le_anti_sym 1); |
58 by (rtac order_antisym 1); |
59 by (rtac lemma1 2); |
59 by (rtac lemma1 2); |
60 by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); |
60 by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); |
61 result(); |
61 result(); |