src/HOL/ex/Puzzle.ML
changeset 1266 3ae9fe3c0f68
parent 969 b051e2fc2e34
child 1465 5d7a7e439cec
equal deleted inserted replaced
1265:6ef9a9893fd6 1266:3ae9fe3c0f68
    14 qed "nat_exh";
    14 qed "nat_exh";
    15 
    15 
    16 goal Puzzle.thy "! n. k=f(n) --> n <= f(n)";
    16 goal Puzzle.thy "! n. k=f(n) --> n <= f(n)";
    17 by (res_inst_tac [("n","k")] less_induct 1);
    17 by (res_inst_tac [("n","k")] less_induct 1);
    18 by (rtac nat_exh 1);
    18 by (rtac nat_exh 1);
    19 by (simp_tac nat_ss 1);
    19 by (Simp_tac 1);
    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 (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
    24 by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
    25 by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
    25 by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
    26 bind_thm("lemma", result() RS spec RS mp);
    26 val lemma = result() RS spec RS mp;
    27 
    27 
    28 goal Puzzle.thy "n <= f(n)";
    28 goal Puzzle.thy "n <= f(n)";
    29 by (fast_tac (HOL_cs addIs [lemma]) 1);
    29 by (fast_tac (HOL_cs addIs [lemma]) 1);
    30 qed "lemma1";
    30 qed "lemma1";
    31 
    31 
    33 by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
    33 by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
    34 qed "lemma2";
    34 qed "lemma2";
    35 
    35 
    36 val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
    36 val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
    37 by (res_inst_tac[("n","n")]nat_induct 1);
    37 by (res_inst_tac[("n","n")]nat_induct 1);
    38 by (simp_tac nat_ss 1);
    38 by (Simp_tac 1);
    39 by (simp_tac nat_ss 1);
    39 by (Simp_tac 1);
    40 by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
    40 by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
    41 bind_thm("mono_lemma1", result() RS mp);
    41 bind_thm("mono_lemma1", result() RS mp);
    42 
    42 
    43 val [p1,p2] = goal Puzzle.thy
    43 val [p1,p2] = goal Puzzle.thy
    44     "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
    44     "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";