src/HOL/ex/Puzzle.ML
changeset 8021 9a400ba634b8
parent 8019 fead0dbf5b0a
child 8022 2855e262129c
equal deleted inserted replaced
8020:2823ce1753a5 8021:9a400ba634b8
    13 Goal "! n. k=f(n) --> n <= f(n)";
    13 Goal "! n. k=f(n) --> n <= f(n)";
    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 Auto_tac;
    18  by (Asm_simp_tac 1);
       
    19 by (rtac impI 1);
    19 by (subgoal_tac "f(nat) <= f(f(nat))" 1);
    20 by (subgoal_tac "f(nat) <= f(f(nat))" 1);
    20  by (Blast_tac 2);
    21  by (Blast_tac 2);
    21 by (blast_tac (claset() addIs [Suc_leI,le_less_trans]) 1);
    22 by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
    22 val lemma = result() RS spec RS mp;
    23 val lemma = result() RS spec RS mp;
    23 
    24 
    24 Goal "n <= f(n)";
    25 Goal "n <= f(n)";
    25 by (fast_tac (claset() addIs [lemma]) 1);
    26 by (fast_tac (claset() addIs [lemma]) 1);
    26 qed "lemma1";
    27 qed "lemma1";