# HG changeset patch
# User nipkow
# Date 971762446 -7200
# Node ID e653cb93329315d7fa7ee563e5385afd22f95fca
# Parent  692e29b9d2b292786560c26903b5742deb2d8dca
added intermediate value thms

diff -r 692e29b9d2b2 -r e653cb933293 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Tue Oct 17 08:00:34 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Tue Oct 17 08:00:46 2000 +0200
@@ -18,6 +18,41 @@
 qed "triangle_ineq";
 
 
+(*** Intermediate value theorems ***)
+
+Goal "(ALL i<n. abs(f(i+1) - f i) <= #1) --> \
+\     f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))";
+by(induct_tac "n" 1);
+ by(Asm_simp_tac 1);
+by(strip_tac 1);
+by(etac impE 1);
+ by(Asm_full_simp_tac 1);
+by(eres_inst_tac [("x","n")] allE 1);
+by(Asm_full_simp_tac 1);
+by(case_tac "k = f(n+1)" 1);
+ by(Force_tac 1);
+by(etac impE 1);
+ by(asm_full_simp_tac (simpset() addsimps [zabs_def] addsplits [split_if_asm]) 1);
+ by(arith_tac 1);
+by(blast_tac (claset() addIs [le_SucI]) 1);
+val lemma = result();
+
+bind_thm("nat0_intermed_int_val", rulify_no_asm lemma);
+
+Goal "[| !i. m <= i & i < n --> abs(f(i+1) - f i) <= #1; m < n; \
+\        f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
+by(cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
+by(Asm_full_simp_tac 1);
+by(etac impE 1);
+ by(strip_tac 1);
+ by(eres_inst_tac [("x","i+m")] allE 1);
+ by(arith_tac 1);
+by(etac exE 1);
+by(res_inst_tac [("x","i+m")] exI 1);
+by(arith_tac 1);
+qed "nat_intermed_int_val";
+
+
 (*** Some convenient biconditionals for products of signs ***)
 
 Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";