added lemmas
authornipkow
Fri Aug 08 09:26:15 2008 +0200 (2008-08-08)
changeset 277891bf827e3258d
parent 27788 5def98c2646b
child 27790 37b4e65d1dbf
added lemmas
src/HOL/Nat.thy
src/HOL/ex/Puzzle.thy
     1.1 --- a/src/HOL/Nat.thy	Thu Aug 07 23:56:45 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Aug 08 09:26:15 2008 +0200
     1.3 @@ -1309,9 +1309,24 @@
     1.4  using `n < n'`
     1.5  by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
     1.6  
     1.7 +lemma lift_Suc_mono_less_iff:
     1.8 +  "(!!n. f n < f(Suc n)) \<Longrightarrow> f(n) < f(m) \<longleftrightarrow> n<m"
     1.9 +by(blast intro: less_asym' lift_Suc_mono_less[of f]
    1.10 +         dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq[THEN iffD1])
    1.11 +
    1.12  end
    1.13  
    1.14  
    1.15 +lemma mono_nat_linear_lb:
    1.16 +  "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
    1.17 +apply(induct_tac k)
    1.18 + apply simp
    1.19 +apply(erule_tac x="m+n" in meta_allE)
    1.20 +apply(erule_tac x="m+n+1" in meta_allE)
    1.21 +apply simp
    1.22 +done
    1.23 +
    1.24 +
    1.25  text{*Subtraction laws, mostly by Clemens Ballarin*}
    1.26  
    1.27  lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
     2.1 --- a/src/HOL/ex/Puzzle.thy	Thu Aug 07 23:56:45 2008 +0200
     2.2 +++ b/src/HOL/ex/Puzzle.thy	Fri Aug 08 09:26:15 2008 +0200
     2.3 @@ -1,47 +1,139 @@
     2.4  (*  Title:      HOL/ex/Puzzle.thy
     2.5      ID:         $Id$
     2.6      Author:     Tobias Nipkow
     2.7 -    Copyright   1993 TU Muenchen
     2.8 -
     2.9 -A question from "Bundeswettbewerb Mathematik"
    2.10 -
    2.11 -Proof due to Herbert Ehler
    2.12  *)
    2.13  
    2.14 -header {* A question from ``Bundeswettbewerb Mathematik'' *}
    2.15 +header {* Fun with Functions *}
    2.16  
    2.17  theory Puzzle imports Main begin
    2.18  
    2.19 -consts f :: "nat => nat"
    2.20 +text{* From \emph{Solving Mathematical Problems} by Terence Tao. He quotes
    2.21 +Greitzer's \emph{Interational Mathematical Olympiads 1959--1977} as the
    2.22 +original source. Was first brought to our attention by Herbert Ehler who
    2.23 +provided a similar proof. *}
    2.24 +
    2.25  
    2.26 -specification (f)
    2.27 -  f_ax [intro!]: "f(f(n)) < f(Suc(n))"
    2.28 -    by (rule exI [of _ id], simp)
    2.29 +theorem identity1: fixes f :: "nat \<Rightarrow> nat"
    2.30 +assumes fff: "!!n. f(f(n)) < f(Suc(n))"
    2.31 +shows "f(n) = n"
    2.32 +proof -
    2.33 +  { fix m n have key: "n \<le> m \<Longrightarrow> n \<le> f(m)"
    2.34 +    proof(induct n arbitrary: m)
    2.35 +      case 0 show ?case by simp
    2.36 +    next
    2.37 +      case (Suc n)
    2.38 +      hence "m \<noteq> 0" by simp
    2.39 +      then obtain k where [simp]: "m = Suc k" by (metis not0_implies_Suc)
    2.40 +      have "n \<le> f(k)" using Suc by simp
    2.41 +      hence "n \<le> f(f(k))" using Suc by simp
    2.42 +      also have "\<dots> < f(m)" using fff by simp
    2.43 +      finally show ?case by simp
    2.44 +    qed }
    2.45 +  hence "!!n. n \<le> f(n)" by simp
    2.46 +  hence "!!n. f(n) < f(Suc n)" by(metis fff order_le_less_trans)
    2.47 +  hence "f(n) < n+1" by (metis fff lift_Suc_mono_less_iff[of f] Suc_plus1)
    2.48 +  with `n \<le> f(n)` show "f n = n" by arith
    2.49 +qed
    2.50  
    2.51  
    2.52 -lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
    2.53 -apply (induct_tac "k" rule: nat_less_induct)
    2.54 -apply (rule allI)
    2.55 -apply (rename_tac "i")
    2.56 -apply (case_tac "i")
    2.57 - apply simp
    2.58 -apply (blast intro!: Suc_leI intro: le_less_trans)
    2.59 -done
    2.60 -
    2.61 -lemma lemma1: "n <= f(n)"
    2.62 -by (blast intro: lemma0)
    2.63 +text{* From \emph{Solving Mathematical Problems} by Terence Tao. He quotes
    2.64 +the \emph{Australian Mathematics Competition} 1984 as the original source.
    2.65 +Possible extension:
    2.66 +Should also hold if the range of @{text f} is the reals!
    2.67 +*}
    2.68  
    2.69 -lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
    2.70 -apply (induct_tac "n")
    2.71 - apply simp 
    2.72 - apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le)
    2.73 -done
    2.74 +lemma identity2: fixes f :: "nat \<Rightarrow> nat"
    2.75 +assumes "f(k) = k" and "k \<ge> 2"
    2.76 +and f_times: "\<And>m n. f(m*n) = f(m)*f(n)"
    2.77 +and f_mono: "\<And>m n. m<n \<Longrightarrow> f m < f n"
    2.78 +shows "f(n) = n"
    2.79 +proof -
    2.80 +  have 0: "f(0) = 0"
    2.81 +    by (metis f_mono f_times mult_1_right mult_is_0 nat_less_le nat_mult_eq_cancel_disj not_less_eq)
    2.82 +  have 1: "f(1) = 1"
    2.83 +    by (metis f_mono f_times gr_implies_not0 mult_eq_self_implies_10 nat_mult_1_right zero_less_one)
    2.84 +  have 2: "f 2 = 2"
    2.85 +  proof -
    2.86 +    have "2 + (k - 2) = k" using `k \<ge> 2` by arith
    2.87 +    hence "f(2) \<le> 2"
    2.88 +      using mono_nat_linear_lb[of f 2 "k - 2",OF f_mono] `f k = k`
    2.89 +      by simp arith
    2.90 +    thus "f 2 = 2" using 1 f_mono[of 1 2] by arith
    2.91 +  qed
    2.92 +  show ?thesis
    2.93 +  proof(induct rule:less_induct)
    2.94 +    case (less i)
    2.95 +    show ?case
    2.96 +    proof cases
    2.97 +      assume "i\<le>1" thus ?case using 0 1 by (auto simp add:le_Suc_eq)
    2.98 +    next
    2.99 +      assume "~i\<le>1"
   2.100 +      show ?case
   2.101 +      proof cases
   2.102 +	assume "i mod 2 = 0"
   2.103 +	hence "EX k. i=2*k" by arith
   2.104 +	then obtain k where "i = 2*k" ..
   2.105 +	hence "0 < k" and "k<i" using `~i\<le>1` by arith+
   2.106 +	hence "f(k) = k" using less(1) by blast
   2.107 +	thus "f(i) = i" using `i = 2*k` by(simp add:f_times 2)
   2.108 +      next
   2.109 +	assume "i mod 2 \<noteq> 0"
   2.110 +	hence "EX k. i=2*k+1" by arith
   2.111 +	then obtain k where "i = 2*k+1" ..
   2.112 +	hence "0<k" and "k+1<i" using `~i\<le>1` by arith+
   2.113 +	have "2*k < f(2*k+1)"
   2.114 +	proof -
   2.115 +	  have "2*k = 2*f(k)" using less(1) `i=2*k+1` by simp
   2.116 +	  also have "\<dots> = f(2*k)" by(simp add:f_times 2)
   2.117 +	  also have "\<dots> < f(2*k+1)" using f_mono[of "2*k" "2*k+1"] by simp
   2.118 +	  finally show ?thesis .
   2.119 +	qed
   2.120 +	moreover
   2.121 +	have "f(2*k+1) < 2*(k+1)"
   2.122 +	proof -
   2.123 +	  have "f(2*k+1) < f(2*k+2)" using f_mono[of "2*k+1" "2*k+2"] by simp
   2.124 +	  also have "\<dots> = f(2*(k+1))" by simp
   2.125 +	  also have "\<dots> = 2*f(k+1)" by(simp only:f_times 2)
   2.126 +	  also have "f(k+1) = k+1" using less(1) `i=2*k+1` `~i\<le>1` by simp
   2.127 +	  finally show ?thesis .
   2.128 +	qed
   2.129 +	ultimately show "f(i) = i" using `i = 2*k+1` by arith
   2.130 +      qed
   2.131 +    qed
   2.132 +  qed
   2.133 +qed
   2.134  
   2.135 -lemma f_id: "f(n) = n"
   2.136 -apply (rule order_antisym)
   2.137 -apply (rule_tac [2] lemma1) 
   2.138 -apply (blast intro: leI dest: leD f_mono Suc_leI)
   2.139 -done
   2.140 +
   2.141 +text{* The only total model of a naive recursion equation of factorial on
   2.142 +integers is 0 for all negative arguments: *}
   2.143 +
   2.144 +theorem ifac_neg0: fixes ifac :: "int \<Rightarrow> int"
   2.145 +assumes ifac_rec: "!!i. ifac i = (if i=0 then 1 else i*ifac(i - 1))"
   2.146 +shows "i<0 \<Longrightarrow> ifac i = 0"
   2.147 +proof(rule ccontr)
   2.148 +  assume 0: "i<0" "ifac i \<noteq> 0"
   2.149 +  { fix j assume "j \<le> i"
   2.150 +    have "ifac j \<noteq> 0"
   2.151 +      apply(rule int_le_induct[OF `j\<le>i`])
   2.152 +       apply(rule `ifac i \<noteq> 0`)
   2.153 +      apply (metis `i<0` ifac_rec linorder_not_le mult_eq_0_iff)
   2.154 +      done
   2.155 +  } note below0 = this
   2.156 +  { fix j assume "j<i"
   2.157 +    have "1 < -j" using `j<i` `i<0` by arith
   2.158 +    have "ifac(j - 1) \<noteq> 0" using `j<i` by(simp add: below0)
   2.159 +    then have "\<bar>ifac (j - 1)\<bar> < (-j) * \<bar>ifac (j - 1)\<bar>" using `j<i`
   2.160 +      mult_le_less_imp_less[OF order_refl[of "abs(ifac(j - 1))"] `1 < -j`]
   2.161 +      by(simp add:mult_commute)
   2.162 +    hence "abs(ifac(j - 1)) < abs(ifac j)"
   2.163 +      using `1 < -j` by(simp add: ifac_rec[of "j"] abs_mult)
   2.164 +  } note not_wf = this
   2.165 +  let ?f = "%j. nat(abs(ifac(i - int(j+1))))"
   2.166 +  obtain k where "\<not> ?f (Suc k) < ?f k"
   2.167 +    using wf_no_infinite_down_chainE[OF wf_less, of "?f"] by blast
   2.168 +  moreover have "i - int (k + 1) - 1 = i - int (Suc k + 1)" by arith
   2.169 +  ultimately show False using not_wf[of "i - int(k+1)"]
   2.170 +    by (simp only:) arith
   2.171 +qed
   2.172  
   2.173  end
   2.174 -