# HG changeset patch
# User huffman
# Date 1243543425 25200
# Node ID 4248748138405d9d7b5cf5d00df81053a449c0e5
# Parent  0a3f9ee4117c3c184703034a42409df4ee220265# Parent  4e87577544aeb10fce1cfffbdafc740a522d5422
merged

diff -r 0a3f9ee4117c -r 424874813840 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 28 13:41:41 2009 -0700
+++ b/src/HOL/IsaMakefile	Thu May 28 13:43:45 2009 -0700
@@ -315,7 +315,6 @@
   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
   Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML	\
-  Library/Convex_Euclidean_Space.thy \
   Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
   Library/Executable_Set.thy Library/Infinite_Set.thy			\
   Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
diff -r 0a3f9ee4117c -r 424874813840 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 13:43:45 2009 -0700
@@ -35,15 +35,6 @@
   "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
   by(auto simp add:vector_component_simps all_1 Cart_eq)
 
-definition 
-  "is_interval_new (s::((real^'n::finite) set)) \<longleftrightarrow>
-  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i)))  \<longrightarrow> x \<in> s)"
-
-lemma is_interval_interval_new: "is_interval_new {a .. b}" (is ?th1) "is_interval_new {a<..<b}" (is ?th2) proof - 
-  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
-  show ?th1 ?th2  unfolding is_interval_new_def mem_interval Ball_def atLeastAtMost_iff
-    by(meson real_le_trans le_less_trans less_le_trans *)+ qed
-
 lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
 
 lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
@@ -2178,7 +2169,7 @@
 
 subsection {* Convexity of general and special intervals. *}
 
-lemma is_interval_convex: assumes "is_interval_new s" shows "convex s"
+lemma is_interval_convex: assumes "is_interval s" shows "convex s"
   unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
   fix x y u v assume as:"x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
   hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
@@ -2191,22 +2182,22 @@
     hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps)
     hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps)
     hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
-  ultimately show "u *s x + v *s y \<in> s" apply- apply(rule assms[unfolded is_interval_new_def, rule_format, OF as(1,2)])
+  ultimately show "u *s x + v *s y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
     using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
 
-lemma is_interval_connected: "is_interval_new s \<Longrightarrow> connected s"
+lemma is_interval_connected: "is_interval s \<Longrightarrow> connected s"
   using is_interval_convex convex_connected by auto
 
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
-  apply(rule_tac[!] is_interval_convex) using is_interval_interval_new by auto
+  apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
 subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
 
 lemma is_interval_1:
-  "is_interval_new s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
-  unfolding is_interval_new_def dest_vec1_def forall_1 by auto
-
-lemma is_interval_connected_1: "is_interval_new s \<longleftrightarrow> connected (s::(real^1) set)"
+  "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
+  unfolding is_interval_def dest_vec1_def forall_1 by auto
+
+lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::(real^1) set)"
   apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1
   apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof-
   fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s"
@@ -2222,7 +2213,7 @@
     by(auto simp add: basis_component field_simps) qed 
 
 lemma is_interval_convex_1:
-  "is_interval_new s \<longleftrightarrow> convex (s::(real^1) set)" 
+  "is_interval s \<longleftrightarrow> convex (s::(real^1) set)" 
   using is_interval_convex convex_connected is_interval_connected_1 by auto
 
 lemma convex_connected_1:
diff -r 0a3f9ee4117c -r 424874813840 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu May 28 13:41:41 2009 -0700
+++ b/src/HOL/Library/Library.thy	Thu May 28 13:43:45 2009 -0700
@@ -14,7 +14,6 @@
   Commutative_Ring
   Continuity
   ContNotDenum
-  Convex_Euclidean_Space
   Countable
   Determinants
   Diagonalize
diff -r 0a3f9ee4117c -r 424874813840 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 13:43:45 2009 -0700
@@ -3817,11 +3817,11 @@
   unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_def ..
 
 lemma continuous_at_vec1_norm:
- "\<forall>x. continuous (at x) (vec1 o norm)"
+ "continuous (at x) (vec1 o norm)"
   unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast
 
 lemma continuous_on_vec1_norm:
- "\<forall>s. continuous_on s (vec1 o norm)"
+ "continuous_on s (vec1 o norm)"
 unfolding continuous_on_vec1_range norm_vec1[THEN sym] by (metis norm_vec1 order_le_less_trans real_abs_sub_norm)
 
 lemma continuous_at_vec1_component:
@@ -3886,7 +3886,7 @@
 
 lemma continuous_attains_inf:
  "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s (vec1 o f)
-        ==> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
+        \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
   using compact_attains_inf[of "f ` s"]
   using compact_continuous_image[of s "vec1 \<circ> f"] unfolding image_compose by auto
 
@@ -4325,8 +4325,12 @@
 lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows
   "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
   "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
-  using interval[of a b]
-  by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+  using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+
+lemma mem_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
+ "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)
 
 lemma interval_eq_empty: fixes a :: "real^'n::finite" shows
  "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
@@ -4383,7 +4387,6 @@
 apply (auto simp add: not_less less_imp_le)
 done
 
-
 lemma interval_open_subset_closed:  fixes a :: "'a::preorder^'n::finite" shows
  "{a<..<b} \<subseteq> {a .. b}"
 proof(simp add: subset_eq, rule)
@@ -4777,16 +4780,12 @@
 
 subsection{* Intervals in general, including infinite and mixtures of open and closed. *}
 
-definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
-
-lemma is_interval_interval: fixes a::"real^'n::finite" shows
-  "is_interval {a<..<b}" "is_interval {a .. b}"
-  unfolding is_interval_def apply(auto simp add: vector_less_def vector_less_eq_def)
-  apply(erule_tac x=i in allE)+ apply simp
-  apply(erule_tac x=i in allE)+ apply simp
-  apply(erule_tac x=i in allE)+ apply simp
-  apply(erule_tac x=i in allE)+ apply simp
-  done
+definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i)))  \<longrightarrow> x \<in> s)"
+
+lemma is_interval_interval: "is_interval {a .. b::real^'n::finite}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof - 
+  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
+  show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
+    by(meson real_le_trans le_less_trans less_le_trans *)+ qed
 
 lemma is_interval_empty:
  "is_interval {}"
@@ -5457,7 +5456,11 @@
   ultimately show ?thesis using False by auto
 qed
 
-subsection{* Banach fixed point theorem (not really topological...)                    *}
+lemma image_smult_interval:"(\<lambda>x. m *s (x::real^'n::finite)) ` {a..b} =
+  (if {a..b} = {} then {} else if 0 \<le> m then {m *s a..m *s b} else {m *s b..m *s a})"
+  using image_affinity_interval[of m 0 a b] by auto
+
+subsection{* Banach fixed point theorem (not really topological...) *}
 
 lemma banach_fix:
   assumes s:"complete s" "s \<noteq> {}" and c:"0 \<le> c" "c < 1" and f:"(f ` s) \<subseteq> s" and
diff -r 0a3f9ee4117c -r 424874813840 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu May 28 13:41:41 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML	Thu May 28 13:43:45 2009 -0700
@@ -965,6 +965,7 @@
   | select_sup _ 1 = [rtac @{thm supI1}]
   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
 
+(* FIXME: This function relies on the derivation of an induction rule *)
 fun get_nparams thy s = let
     val _ = tracing ("get_nparams: " ^ s)
   in