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