src/HOL/ex/Puzzle.ML
changeset 8022 2855e262129c
parent 8021 9a400ba634b8
child 8423 3c19160b6432
equal deleted inserted replaced
8021:9a400ba634b8 8022:2855e262129c
    14 by (res_inst_tac [("n","k")] less_induct 1);
    14 by (res_inst_tac [("n","k")] less_induct 1);
    15 by (rtac allI 1);
    15 by (rtac allI 1);
    16 by (rename_tac "i" 1);
    16 by (rename_tac "i" 1);
    17 by (exhaust_tac "i" 1);
    17 by (exhaust_tac "i" 1);
    18  by (Asm_simp_tac 1);
    18  by (Asm_simp_tac 1);
    19 by (rtac impI 1);
    19 by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
    20 by (subgoal_tac "f(nat) <= f(f(nat))" 1);
       
    21  by (Blast_tac 2);
       
    22 by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
       
    23 val lemma = result() RS spec RS mp;
    20 val lemma = result() RS spec RS mp;
    24 
    21 
    25 Goal "n <= f(n)";
    22 Goal "n <= f(n)";
    26 by (fast_tac (claset() addIs [lemma]) 1);
    23 by (fast_tac (claset() addIs [lemma]) 1);
    27 qed "lemma1";
    24 qed "lemma1";