src/HOL/ex/Puzzle.ML
changeset 3336 29ddef80bd49
parent 2609 4370e5f0fa3f
child 3842 b55686a7b22c
equal deleted inserted replaced
3335:b0139b83a5ee 3336:29ddef80bd49
    20 by (rtac impI 1);
    20 by (rtac impI 1);
    21 by (rtac classical 1);
    21 by (rtac classical 1);
    22 by (dtac not_leE 1);
    22 by (dtac not_leE 1);
    23 by (subgoal_tac "f(na) <= f(f(na))" 1);
    23 by (subgoal_tac "f(na) <= f(f(na))" 1);
    24 by (fast_tac (!claset addIs [Puzzle.f_ax]) 2);
    24 by (fast_tac (!claset addIs [Puzzle.f_ax]) 2);
    25 by (rtac lessD 1);
    25 by (rtac Suc_leI 1);
    26 by (fast_tac (!claset delrules [order_refl] 
    26 by (fast_tac (!claset delrules [order_refl] 
    27                       addIs [Puzzle.f_ax, le_less_trans]) 1);
    27                       addIs [Puzzle.f_ax, le_less_trans]) 1);
    28 val lemma = result() RS spec RS mp;
    28 val lemma = result() RS spec RS mp;
    29 
    29 
    30 goal Puzzle.thy "n <= f(n)";
    30 goal Puzzle.thy "n <= f(n)";
    54 qed "f_mono";
    54 qed "f_mono";
    55 
    55 
    56 goal Puzzle.thy "f(n) = n";
    56 goal Puzzle.thy "f(n) = n";
    57 by (rtac le_anti_sym 1);
    57 by (rtac le_anti_sym 1);
    58 by (rtac lemma1 2);
    58 by (rtac lemma1 2);
    59 by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
    59 by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
    60 result();
    60 result();