Streamlined it a bit.
authornipkow
Mon Nov 15 09:41:06 1999 +0100 (1999-11-15)
changeset 8018bedd0beabbae
parent 8017 058193827a52
child 8019 fead0dbf5b0a
Streamlined it a bit.
src/HOL/ex/Puzzle.ML
src/HOL/ex/Puzzle.thy
     1.1 --- a/src/HOL/ex/Puzzle.ML	Fri Nov 12 18:16:48 1999 +0100
     1.2 +++ b/src/HOL/ex/Puzzle.ML	Mon Nov 15 09:41:06 1999 +0100
     1.3 @@ -10,22 +10,18 @@
     1.4  
     1.5  AddSIs [Puzzle.f_ax];
     1.6  
     1.7 -(*specialized form of induction needed below*)
     1.8 -val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
     1.9 -by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
    1.10 -qed "nat_exh";
    1.11 -
    1.12  Goal "! n. k=f(n) --> n <= f(n)";
    1.13  by (res_inst_tac [("n","k")] less_induct 1);
    1.14 -by (rtac nat_exh 1);
    1.15 -by (Simp_tac 1);
    1.16 +by (rtac allI 1);
    1.17 +by (rename_tac "i" 1);
    1.18 +by (exhaust_tac "i" 1);
    1.19 + by (Asm_simp_tac 1);
    1.20  by (rtac impI 1);
    1.21  by (rtac classical 1);
    1.22  by (dtac not_leE 1);
    1.23 -by (subgoal_tac "f(na) <= f(f(na))" 1);
    1.24 -by (Blast_tac 2);
    1.25 -by (rtac Suc_leI 1);
    1.26 -by (blast_tac (claset() addSDs [spec] addIs [le_less_trans]) 1);
    1.27 +by (subgoal_tac "f(nat) <= f(f(nat))" 1);
    1.28 + by (Blast_tac 2);
    1.29 +by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
    1.30  val lemma = result() RS spec RS mp;
    1.31  
    1.32  Goal "n <= f(n)";
    1.33 @@ -36,26 +32,18 @@
    1.34  by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
    1.35  qed "lemma2";
    1.36  
    1.37 -val prems = Goal "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
    1.38 -by (res_inst_tac[("n","n")]nat_induct 1);
    1.39 -by (Simp_tac 1);
    1.40 -by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.41 -by (blast_tac (claset() addIs (le_trans::prems)) 1);
    1.42 -qed_spec_mp "mono_lemma1";
    1.43 -
    1.44 -val [p1,p2] = goal Puzzle.thy
    1.45 -    "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
    1.46 -by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
    1.47 -by (etac (p1 RS mono_lemma1) 1);
    1.48 -by (Fast_tac 1);
    1.49 -qed "mono_lemma";
    1.50 -
    1.51 -val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
    1.52 -by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1);
    1.53 -qed "f_mono";
    1.54 +Goal "m <= n --> f(m) <= f(n)";
    1.55 +by (induct_tac "n" 1);
    1.56 + by (Simp_tac 1);
    1.57 +by (rtac impI 1);
    1.58 +by (etac le_SucE 1);
    1.59 + by(cut_inst_tac [("n","n")]lemma2 1);
    1.60 + by(arith_tac 1);
    1.61 +by(Asm_simp_tac 1);
    1.62 +qed_spec_mp "f_mono";
    1.63  
    1.64  Goal "f(n) = n";
    1.65  by (rtac order_antisym 1);
    1.66  by (rtac lemma1 2);
    1.67 -by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
    1.68 -result();
    1.69 +by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);
    1.70 +qed "f_id";
     2.1 --- a/src/HOL/ex/Puzzle.thy	Fri Nov 12 18:16:48 1999 +0100
     2.2 +++ b/src/HOL/ex/Puzzle.thy	Mon Nov 15 09:41:06 1999 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  A question from "Bundeswettbewerb Mathematik"
     2.5  *)
     2.6  
     2.7 -Puzzle = Nat +
     2.8 +Puzzle = Main +
     2.9  consts f :: nat => nat
    2.10  rules  f_ax "f(f(n)) < f(Suc(n))"
    2.11  end