# 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 \ b \ dest_vec1 a \ 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)) \ - (\a\s. \b\s. \x. (\i. ((a$i \ x$i \ x$i \ b$i) \ (b$i \ x$i \ x$i \ a$i))) \ x \ s)" - -lemma is_interval_interval_new: "is_interval_new {a .. b}" (is ?th1) "is_interval_new {a<..x y z::real. x < y \ y < z \ 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\A \ A \ {}" by auto lemma norm_not_0:"(x::real^'n::finite)\0 \ norm x \ 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 \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" hence *:"u = 1 - v" "1 - v \ 0" and **:"v = 1 - u" "1 - u \ 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 \ b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } - ultimately show "u *s x + v *s y \ s" apply- apply(rule assms[unfolded is_interval_new_def, rule_format, OF as(1,2)]) + ultimately show "u *s x + v *s y \ 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 \ connected s" +lemma is_interval_connected: "is_interval s \ connected s" using is_interval_convex convex_connected by auto lemma convex_interval: "convex {a .. b}" "convex {a<.. (\a\s. \b\s. \ x. dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b \ x \ s)" - unfolding is_interval_new_def dest_vec1_def forall_1 by auto - -lemma is_interval_connected_1: "is_interval_new s \ connected (s::(real^1) set)" + "is_interval s \ (\a\s. \b\s. \ x. dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b \ x \ s)" + unfolding is_interval_def dest_vec1_def forall_1 by auto + +lemma is_interval_connected_1: "is_interval s \ 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 \ s" "b \ s" "dest_vec1 a \ dest_vec1 x" "dest_vec1 x \ dest_vec1 b" "x\s" @@ -2222,7 +2213,7 @@ by(auto simp add: basis_component field_simps) qed lemma is_interval_convex_1: - "is_interval_new s \ convex (s::(real^1) set)" + "is_interval s \ 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: - "\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: - "\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 \ s \ {} \ continuous_on s (vec1 o f) - ==> (\x \ s. \y \ s. f x \ f y)" + \ (\x \ s. \y \ s. f x \ f y)" using compact_attains_inf[of "f ` s"] using compact_continuous_image[of s "vec1 \ f"] unfolding image_compose by auto @@ -4325,8 +4325,12 @@ lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows "x \ {a<.. (\i. a$i < x$i \ x$i < b$i)" "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ 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 \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b)" + "(x \ {a<.. dest_vec1 a < dest_vec1 x \ 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} = {} \ (\i. b$i \ 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<.. {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 \ (\a\s. \b\s. \x. a \ x \ x \ b \ x \ s)" - -lemma is_interval_interval: fixes a::"real^'n::finite" shows - "is_interval {a<.. (\a\s. \b\s. \x. (\i. ((a$i \ x$i \ x$i \ b$i) \ (b$i \ x$i \ x$i \ a$i))) \ x \ s)" + +lemma is_interval_interval: "is_interval {a .. b::real^'n::finite}" (is ?th1) "is_interval {a<..x y z::real. x < y \ y < z \ 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:"(\x. m *s (x::real^'n::finite)) ` {a..b} = + (if {a..b} = {} then {} else if 0 \ 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 \ {}" and c:"0 \ c" "c < 1" and f:"(f ` s) \ 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