--- a/NEWS Thu Aug 18 18:07:40 2011 +0200
+++ b/NEWS Thu Aug 18 23:43:22 2011 +0200
@@ -57,6 +57,9 @@
* Isabelle/Isar reference manual provides more formal references in
syntax diagrams.
+* Attribute case_names has been refined: the assumptions in each case can
+be named now by following the case name with [name1 name2 ...].
+
*** HOL ***
@@ -196,6 +199,19 @@
tendsto_vector ~> vec_tendstoI
Cauchy_vector ~> vec_CauchyI
+* Complex_Main: The locale interpretations for the bounded_linear and
+bounded_bilinear locales have been removed, in order to reduce the
+number of duplicate lemmas. Users must use the original names for
+distributivity theorems, potential INCOMPATIBILITY.
+
+ divide.add ~> add_divide_distrib
+ divide.diff ~> diff_divide_distrib
+ divide.setsum ~> setsum_divide_distrib
+ mult.add_right ~> right_distrib
+ mult.diff_right ~> right_diff_distrib
+ mult_right.setsum ~> setsum_right_distrib
+ mult_left.diff ~> left_diff_distrib
+
*** Document preparation ***
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 23:43:22 2011 +0200
@@ -157,8 +157,11 @@
\item @{text R.cases} is the case analysis (or elimination) rule;
\item @{text R.induct} or @{text R.coinduct} is the (co)induction
- rule.
-
+ rule;
+
+ \item @{text R.simps} is the equation unrolling the fixpoint of the
+ predicate one step.
+
\end{description}
When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 18:07:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 23:43:22 2011 +0200
@@ -225,8 +225,11 @@
\item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
\item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
- rule.
-
+ rule;
+
+ \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
+ predicate one step.
+
\end{description}
When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are
--- a/src/HOL/Equiv_Relations.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Equiv_Relations.thy Thu Aug 18 23:43:22 2011 +0200
@@ -164,7 +164,7 @@
text{*A congruence-preserving function*}
-definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
"congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
lemma congruentI:
@@ -229,7 +229,7 @@
text{*A congruence-preserving function of two arguments*}
-definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
+definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
"congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
lemma congruent2I':
--- a/src/HOL/Fun.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Fun.thy Thu Aug 18 23:43:22 2011 +0200
@@ -10,15 +10,6 @@
uses ("Tools/enriched_type.ML")
begin
-text{*As a simplification rule, it replaces all function equalities by
- first-order equalities.*}
-lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
-apply (rule iffI)
-apply (simp (no_asm_simp))
-apply (rule ext)
-apply (simp (no_asm_simp))
-done
-
lemma apply_inverse:
"f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
by auto
@@ -26,26 +17,22 @@
subsection {* The Identity Function @{text id} *}
-definition
- id :: "'a \<Rightarrow> 'a"
-where
+definition id :: "'a \<Rightarrow> 'a" where
"id = (\<lambda>x. x)"
lemma id_apply [simp]: "id x = x"
by (simp add: id_def)
lemma image_id [simp]: "id ` Y = Y"
-by (simp add: id_def)
+ by (simp add: id_def)
lemma vimage_id [simp]: "id -` A = A"
-by (simp add: id_def)
+ by (simp add: id_def)
subsection {* The Composition Operator @{text "f \<circ> g"} *}
-definition
- comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
-where
+definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
"f o g = (\<lambda>x. f (g x))"
notation (xsymbols)
@@ -54,9 +41,6 @@
notation (HTML output)
comp (infixl "\<circ>" 55)
-text{*compatibility*}
-lemmas o_def = comp_def
-
lemma o_apply [simp]: "(f o g) x = f (g x)"
by (simp add: comp_def)
@@ -71,7 +55,7 @@
lemma o_eq_dest:
"a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
- by (simp only: o_def) (fact fun_cong)
+ by (simp only: comp_def) (fact fun_cong)
lemma o_eq_elim:
"a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
@@ -89,9 +73,7 @@
subsection {* The Forward Composition Operator @{text fcomp} *}
-definition
- fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
-where
+definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
"f \<circ>> g = (\<lambda>x. g (f x))"
lemma fcomp_apply [simp]: "(f \<circ>> g) x = g (f x)"
@@ -569,8 +551,7 @@
subsection{*Function Updating*}
-definition
- fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
+definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
"fun_upd f a b == % x. if x=a then b else f x"
nonterminal updbinds and updbind
@@ -634,9 +615,7 @@
subsection {* @{text override_on} *}
-definition
- override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
-where
+definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
"override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
lemma override_on_emptyset[simp]: "override_on f g {} = f"
@@ -651,9 +630,7 @@
subsection {* @{text swap} *}
-definition
- swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
-where
+definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
"swap a b f = f (a := f b, b:= f a)"
lemma swap_self [simp]: "swap a a f = f"
@@ -716,7 +693,7 @@
subsection {* Inversion of injective functions *}
definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
-"the_inv_into A f == %x. THE y. y : A & f y = x"
+ "the_inv_into A f == %x. THE y. y : A & f y = x"
lemma the_inv_into_f_f:
"[| inj_on f A; x : A |] ==> the_inv_into A f (f x) = x"
@@ -775,6 +752,11 @@
shows "the_inv f (f x) = x" using assms UNIV_I
by (rule the_inv_into_f_f)
+
+text{*compatibility*}
+lemmas o_def = comp_def
+
+
subsection {* Cantor's Paradox *}
lemma Cantors_paradox [no_atp]:
--- a/src/HOL/GCD.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/GCD.thy Thu Aug 18 23:43:22 2011 +0200
@@ -531,11 +531,8 @@
lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
apply(rule antisym)
- apply(rule Max_le_iff[THEN iffD2])
- apply simp
- apply fastsimp
- apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
-apply simp
+ apply(rule Max_le_iff [THEN iffD2])
+ apply (auto intro: abs_le_D1 dvd_imp_le_int)
done
lemma gcd_is_Max_divisors_nat:
--- a/src/HOL/HOL.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/HOL.thy Thu Aug 18 23:43:22 2011 +0200
@@ -1394,6 +1394,11 @@
"f (if c then x else y) = (if c then f x else f y)"
by simp
+text{*As a simplification rule, it replaces all function equalities by
+ first-order equalities.*}
+lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
+ by auto
+
subsubsection {* Generic cases and induction *}
--- a/src/HOL/Import/HOLLightReal.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Import/HOLLightReal.thy Thu Aug 18 23:43:22 2011 +0200
@@ -112,7 +112,7 @@
lemma REAL_DIFFSQ:
"((x :: real) + y) * (x - y) = x * x - y * y"
- by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
+ by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
lemma REAL_ABS_TRIANGLE_LE:
"abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
@@ -295,7 +295,7 @@
(\<forall>(x :: real). 0 * x = 0) \<and>
(\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
(\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
- by (auto simp add: mult.add_right)
+ by (auto simp add: right_distrib)
lemma REAL_COMPLETE:
"(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
--- a/src/HOL/IsaMakefile Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/IsaMakefile Thu Aug 18 23:43:22 2011 +0200
@@ -1039,32 +1039,30 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
- ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
- ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
- ex/CTL.thy ex/Case_Product.thy \
- ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
- ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
- ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
- ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
- ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
- ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
+ ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
+ ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \
+ ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \
+ ex/CodegenSML_Test.thy ex/Coercion_Examples.thy ex/Coherent.thy \
+ ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
+ ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
+ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
+ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
+ ex/Iff_Oracle.thy ex/Induction_Schema.thy \
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
- ex/Quickcheck_Narrowing_Examples.thy \
- ex/Quicksort.thy ex/ROOT.ML ex/Records.thy \
- ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
- ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
- ex/sledgehammer_tactics.ML ex/Sqrt.thy \
- ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
- ex/Transfer_Ex.thy ex/Tree23.thy \
+ ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
+ ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
+ ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
+ ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML \
+ ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy \
+ ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
ex/Unification.thy ex/While_Combinator_Example.thy \
- ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
- ex/svc_test.thy \
- ../Tools/interpretation_with_defs.ML
+ ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
+ ex/svc_test.thy ../Tools/interpretation_with_defs.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/Library/Convex.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Library/Convex.thy Thu Aug 18 23:43:22 2011 +0200
@@ -129,7 +129,7 @@
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
- hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+ hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
from this asms
have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
@@ -410,7 +410,7 @@
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
- hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+ hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
have "convex C" using asms by auto
hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
using asms convex_setsum[OF `finite s`
@@ -433,7 +433,7 @@
using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
- unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
+ unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
--- a/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 23:43:22 2011 +0200
@@ -5,7 +5,7 @@
header {* Frechet Derivative *}
theory FrechetDeriv
-imports Lim Complex_Main
+imports Complex_Main
begin
definition
@@ -398,9 +398,11 @@
by (simp only: FDERIV_lemma)
qed
-lemmas FDERIV_mult = mult.FDERIV
+lemmas FDERIV_mult =
+ bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
-lemmas FDERIV_scaleR = scaleR.FDERIV
+lemmas FDERIV_scaleR =
+ bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
subsection {* Powers *}
@@ -427,10 +429,10 @@
subsection {* Inverse *}
lemmas bounded_linear_mult_const =
- mult.bounded_linear_left [THEN bounded_linear_compose]
+ bounded_linear_mult_left [THEN bounded_linear_compose]
lemmas bounded_linear_const_mult =
- mult.bounded_linear_right [THEN bounded_linear_compose]
+ bounded_linear_mult_right [THEN bounded_linear_compose]
lemma FDERIV_inverse:
fixes x :: "'a::real_normed_div_algebra"
@@ -510,7 +512,7 @@
fixes x :: "'a::real_normed_field" shows
"FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
apply (unfold fderiv_def)
- apply (simp add: mult.bounded_linear_left)
+ apply (simp add: bounded_linear_mult_left)
apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
apply (subst diff_divide_distrib)
apply (subst times_divide_eq_left [symmetric])
--- a/src/HOL/Library/Inner_Product.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Library/Inner_Product.thy Thu Aug 18 23:43:22 2011 +0200
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
-imports Complex_Main FrechetDeriv
+imports FrechetDeriv
begin
subsection {* Real inner product spaces *}
@@ -43,6 +43,9 @@
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
by (simp add: diff_minus inner_add_left)
+lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
+ by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
+
text {* Transfer distributivity rules to right argument. *}
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
@@ -60,6 +63,9 @@
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
using inner_diff_left [of y z x] by (simp only: inner_commute)
+lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
+ using inner_setsum_left [of f A x] by (simp only: inner_commute)
+
lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
@@ -148,8 +154,8 @@
setup {* Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
-interpretation inner:
- bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
+lemma bounded_bilinear_inner:
+ "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
proof
fix x y z :: 'a and r :: real
show "inner (x + y) z = inner x z + inner y z"
@@ -167,15 +173,20 @@
qed
qed
-interpretation inner_left:
- bounded_linear "\<lambda>x::'a::real_inner. inner x y"
- by (rule inner.bounded_linear_left)
+lemmas tendsto_inner [tendsto_intros] =
+ bounded_bilinear.tendsto [OF bounded_bilinear_inner]
+
+lemmas isCont_inner [simp] =
+ bounded_bilinear.isCont [OF bounded_bilinear_inner]
-interpretation inner_right:
- bounded_linear "\<lambda>y::'a::real_inner. inner x y"
- by (rule inner.bounded_linear_right)
+lemmas FDERIV_inner =
+ bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
-declare inner.isCont [simp]
+lemmas bounded_linear_inner_left =
+ bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
+
+lemmas bounded_linear_inner_right =
+ bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
subsection {* Class instances *}
@@ -260,29 +271,29 @@
by simp
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
- unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
+ unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
lemma GDERIV_add:
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
- unfolding gderiv_def inner_right.add by (rule FDERIV_add)
+ unfolding gderiv_def inner_add_right by (rule FDERIV_add)
lemma GDERIV_minus:
"GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
- unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
+ unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
lemma GDERIV_diff:
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
- unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
+ unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
lemma GDERIV_scaleR:
"\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
:> (scaleR (f x) dg + scaleR df (g x))"
- unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
+ unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
apply (rule FDERIV_subst)
- apply (erule (1) scaleR.FDERIV)
+ apply (erule (1) FDERIV_scaleR)
apply (simp add: mult_ac)
done
@@ -306,7 +317,7 @@
assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
proof -
have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
- by (intro inner.FDERIV FDERIV_ident)
+ by (intro FDERIV_inner FDERIV_ident)
have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
by (simp add: fun_eq_iff inner_commute)
have "0 < inner x x" using `x \<noteq> 0` by simp
--- a/src/HOL/Library/Product_Vector.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Library/Product_Vector.thy Thu Aug 18 23:43:22 2011 +0200
@@ -489,11 +489,11 @@
subsection {* Pair operations are linear *}
-interpretation fst: bounded_linear fst
+lemma bounded_linear_fst: "bounded_linear fst"
using fst_add fst_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
-interpretation snd: bounded_linear snd
+lemma bounded_linear_snd: "bounded_linear snd"
using snd_add snd_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
--- a/src/HOL/Lim.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Lim.thy Thu Aug 18 23:43:22 2011 +0200
@@ -321,17 +321,23 @@
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
by (rule tendsto_right_zero)
-lemmas LIM_mult = mult.LIM
+lemmas LIM_mult =
+ bounded_bilinear.LIM [OF bounded_bilinear_mult]
-lemmas LIM_mult_zero = mult.LIM_prod_zero
+lemmas LIM_mult_zero =
+ bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
-lemmas LIM_mult_left_zero = mult.LIM_left_zero
+lemmas LIM_mult_left_zero =
+ bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
-lemmas LIM_mult_right_zero = mult.LIM_right_zero
+lemmas LIM_mult_right_zero =
+ bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
-lemmas LIM_scaleR = scaleR.LIM
+lemmas LIM_scaleR =
+ bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
-lemmas LIM_of_real = of_real.LIM
+lemmas LIM_of_real =
+ bounded_linear.LIM [OF bounded_linear_of_real]
lemma LIM_power:
fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -446,11 +452,11 @@
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
unfolding isCont_def by (rule LIM)
-lemmas isCont_scaleR [simp] = scaleR.isCont
+lemmas isCont_scaleR [simp] =
+ bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
-lemma isCont_of_real [simp]:
- "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
- by (rule of_real.isCont)
+lemmas isCont_of_real [simp] =
+ bounded_linear.isCont [OF bounded_linear_of_real]
lemma isCont_power [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
--- a/src/HOL/Limits.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Limits.thy Thu Aug 18 23:43:22 2011 +0200
@@ -510,9 +510,9 @@
"Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
by (rule bounded_linear_right [THEN bounded_linear.Zfun])
-lemmas Zfun_mult = mult.Zfun
-lemmas Zfun_mult_right = mult.Zfun_right
-lemmas Zfun_mult_left = mult.Zfun_left
+lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
+lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
+lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
subsection {* Limits *}
@@ -752,7 +752,7 @@
subsubsection {* Linear operators and multiplication *}
-lemma (in bounded_linear) tendsto [tendsto_intros]:
+lemma (in bounded_linear) tendsto:
"(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
@@ -760,7 +760,7 @@
"(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
by (drule tendsto, simp only: zero)
-lemma (in bounded_bilinear) tendsto [tendsto_intros]:
+lemma (in bounded_bilinear) tendsto:
"\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
by (simp only: tendsto_Zfun_iff prod_diff_prod
Zfun_add Zfun Zfun_left Zfun_right)
@@ -779,7 +779,14 @@
"(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
-lemmas tendsto_mult = mult.tendsto
+lemmas tendsto_of_real [tendsto_intros] =
+ bounded_linear.tendsto [OF bounded_linear_of_real]
+
+lemmas tendsto_scaleR [tendsto_intros] =
+ bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
+
+lemmas tendsto_mult [tendsto_intros] =
+ bounded_bilinear.tendsto [OF bounded_bilinear_mult]
lemma tendsto_power [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -897,7 +904,7 @@
apply (erule (1) inverse_diff_inverse)
apply (rule Zfun_minus)
apply (rule Zfun_mult_left)
- apply (rule mult.Bfun_prod_Zfun)
+ apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
apply (erule (1) Bfun_inverse)
apply (simp add: tendsto_Zfun_iff)
done
@@ -921,7 +928,7 @@
fixes a b :: "'a::real_normed_field"
shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
\<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
- by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+ by (simp add: tendsto_mult tendsto_inverse divide_inverse)
lemma tendsto_sgn [tendsto_intros]:
fixes l :: "'a::real_normed_vector"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 23:43:22 2011 +0200
@@ -1202,7 +1202,7 @@
show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
show "\<bar>f x $$ i - x $$ i\<bar> \<le> norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as i by auto
show "\<bar>f x $$ i - f z $$ i\<bar> \<le> norm (f x - f z)" "\<bar>x $$ i - z $$ i\<bar> \<le> norm (x - z)"
- unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+
+ unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
unfolding norm_minus_commute by auto
also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
@@ -1234,7 +1234,7 @@
assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
{ assume "x i = p \<or> x i = 0"
have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval
- apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+ apply safe unfolding euclidean_lambda_beta euclidean_component_zero
proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
show "0 \<le> real (x (b' j)) / real p"
@@ -1262,11 +1262,11 @@
have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto
hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
- unfolding euclidean_component.zero apply (simp_all only: if_P)
+ unfolding euclidean_component_zero apply (simp_all only: if_P)
apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
case goal1 hence as:"\<forall>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar> < d / real n" using `n>0` by(auto simp add:not_le)
- have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component.diff[THEN sym] by(rule norm_le_l1)
+ have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component_diff[THEN sym] by(rule norm_le_l1)
also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
finally show False using d_fz_z by auto qed then guess i .. note i=this
@@ -1276,15 +1276,15 @@
def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
have "\<And>i. i<DIM('a) \<Longrightarrow> r (b' i) \<le> p" apply(rule order_trans) apply(rule rs(1)[OF b'_im,THEN conjunct2])
using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
- hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+ hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
apply (simp only: if_P)
apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
have "\<And>i. i<DIM('a) \<Longrightarrow> s (b' i) \<le> p" apply(rule order_trans) apply(rule rs(2)[OF b'_im,THEN conjunct2])
using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
- hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+ hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
- have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+ have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using q(1)[rule_format,OF b'_im] `p>0` by(auto intro:less_imp_le)
have *:"\<And>x. 1 + real x = real (Suc x)" by auto
{ have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
@@ -1523,7 +1523,7 @@
have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"])
using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
- unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
+ unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
qed
subsection {* Lemmas for working on @{typ "real^1"} *}
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
@@ -18,7 +18,7 @@
(* ------------------------------------------------------------------------- *)
lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
- by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
+ by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
lemma injective_scaleR:
assumes "(c :: real) ~= 0"
@@ -128,7 +128,7 @@
proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
- unfolding euclidean_component.setsum euclidean_scaleR basis_component *
+ unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
apply(rule setsum_cong2) using assms by auto
show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
qed
@@ -1175,7 +1175,7 @@
have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
- also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
+ also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
finally
show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
@@ -2229,7 +2229,7 @@
have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "x : affine hull S" using assms hull_subset[of S] by auto
moreover have "1 / e + - ((1 - e) / e) = 1"
- using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
+ using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
@@ -2957,7 +2957,7 @@
thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
using True using DIM_positive[where 'a='a] by auto
next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
- apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
+ apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
subsection {* Now set-to-set for closed/compact sets. *}
@@ -3053,7 +3053,7 @@
apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
apply(rule assms[unfolded convex_def, rule_format]) prefer 6
- by (auto intro: tendsto_intros)
+ by (auto intro!: tendsto_intros)
lemma convex_interior:
fixes s :: "'a::real_normed_vector set"
@@ -3221,13 +3221,13 @@
ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
apply(rule_tac x="{v \<in> c. u v < 0}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * - u y" in exI)
using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
- by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
+ by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x"
apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
apply(rule_tac x="{v \<in> c. 0 < u v}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * u y" in exI)
using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
- by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
+ by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
ultimately show ?thesis apply(rule_tac x="{v\<in>c. u v \<le> 0}" in exI, rule_tac x="{v\<in>c. u v > 0}" in exI) by auto
qed
@@ -4157,7 +4157,7 @@
let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
{ fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
- unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
+ unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
note ** = this
@@ -4270,7 +4270,7 @@
{ fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
- unfolding euclidean_component.setsum
+ unfolding euclidean_component_setsum
apply(rule setsum_cong2)
using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
by (auto simp add: Euclidean_Space.basis_component[of i])}
@@ -4678,7 +4678,7 @@
hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
def x2 == "z+ e2 *\<^sub>R (z-x)"
hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
- have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
+ have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
using x1_def x2_def apply (auto simp add: algebra_simps)
using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 23:43:22 2011 +0200
@@ -93,13 +93,13 @@
proof -
have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
- by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
+ by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
by (simp add: Lim_null[symmetric])
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
by (intro Lim_cong_within) (simp_all add: field_simps)
finally show ?thesis
- by (simp add: mult.bounded_linear_right has_derivative_within)
+ by (simp add: bounded_linear_mult_right has_derivative_within)
qed
lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
@@ -140,10 +140,31 @@
apply (simp add: local.scaleR local.diff local.add local.zero)
done
+lemmas scaleR_right_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
+
+lemmas scaleR_left_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
+
+lemmas inner_right_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
+
+lemmas inner_left_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
+
+lemmas mult_right_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
+
+lemmas mult_left_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
+
+lemmas euclidean_component_has_derivative =
+ bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
+
lemma has_derivative_neg:
assumes "(f has_derivative f') net"
shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
- using scaleR_right.has_derivative [where r="-1", OF assms] by auto
+ using scaleR_right_has_derivative [where r="-1", OF assms] by auto
lemma has_derivative_add:
assumes "(f has_derivative f') net" and "(g has_derivative g') net"
@@ -181,9 +202,9 @@
has_derivative_id has_derivative_const
has_derivative_add has_derivative_sub has_derivative_neg
has_derivative_add_const
- scaleR_left.has_derivative scaleR_right.has_derivative
- inner_left.has_derivative inner_right.has_derivative
- euclidean_component.has_derivative
+ scaleR_left_has_derivative scaleR_right_has_derivative
+ inner_left_has_derivative inner_right_has_derivative
+ euclidean_component_has_derivative
subsubsection {* Limit transformation for derivatives *}
@@ -459,7 +480,7 @@
"f differentiable net \<Longrightarrow>
(\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def
- apply(erule exE, drule scaleR_right.has_derivative) by auto
+ apply(erule exE, drule scaleR_right_has_derivative) by auto
lemma differentiable_neg [intro]:
"f differentiable net \<Longrightarrow>
@@ -693,7 +714,7 @@
show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
unfolding mult_minus_left
- unfolding abs_mult diff_minus_eq_add scaleR.minus_left
+ unfolding abs_mult diff_minus_eq_add scaleR_minus_left
unfolding algebra_simps by (auto intro: mult_pos_pos)
qed
@@ -769,7 +790,7 @@
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
by (intro has_derivative_intros assms(3)[rule_format,OF x]
- mult_right.has_derivative)
+ mult_right_has_derivative)
qed(insert assms(1), auto simp add:field_simps)
then guess x ..
thus ?thesis apply(rule_tac x=x in bexI)
@@ -1740,7 +1761,7 @@
lemma has_vector_derivative_cmul:
"(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
unfolding has_vector_derivative_def
- apply (drule scaleR_right.has_derivative)
+ apply (drule scaleR_right_has_derivative)
by (auto simp add: algebra_simps)
lemma has_vector_derivative_cmul_eq:
@@ -1819,7 +1840,7 @@
shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
using assms(2) unfolding has_vector_derivative_def apply-
apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
- unfolding o_def scaleR.scaleR_left by auto
+ unfolding o_def real_scaleR_def scaleR_scaleR .
lemma vector_diff_chain_within:
assumes "(f has_vector_derivative f') (at x within s)"
@@ -1827,6 +1848,6 @@
shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
using assms(2) unfolding has_vector_derivative_def apply-
apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
- unfolding o_def scaleR.scaleR_left by auto
+ unfolding o_def real_scaleR_def scaleR_scaleR .
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
@@ -118,20 +118,38 @@
lemma bounded_linear_euclidean_component:
"bounded_linear (\<lambda>x. euclidean_component x i)"
unfolding euclidean_component_def
- by (rule inner.bounded_linear_right)
+ by (rule bounded_linear_inner_right)
+
+lemmas tendsto_euclidean_component [tendsto_intros] =
+ bounded_linear.tendsto [OF bounded_linear_euclidean_component]
+
+lemmas isCont_euclidean_component [simp] =
+ bounded_linear.isCont [OF bounded_linear_euclidean_component]
+
+lemma euclidean_component_zero: "0 $$ i = 0"
+ unfolding euclidean_component_def by (rule inner_zero_right)
-interpretation euclidean_component:
- bounded_linear "\<lambda>x. euclidean_component x i"
- by (rule bounded_linear_euclidean_component)
+lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+ unfolding euclidean_component_def by (rule inner_add_right)
+
+lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+ unfolding euclidean_component_def by (rule inner_diff_right)
-declare euclidean_component.isCont [simp]
+lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+ unfolding euclidean_component_def by (rule inner_minus_right)
+
+lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+ unfolding euclidean_component_def by (rule inner_scaleR_right)
+
+lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+ unfolding euclidean_component_def by (rule inner_setsum_right)
lemma euclidean_eqI:
fixes x y :: "'a::euclidean_space"
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
proof -
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
- by (simp add: euclidean_component.diff)
+ by (simp add: euclidean_component_diff)
then show "x = y"
unfolding euclidean_component_def euclidean_all_zero by simp
qed
@@ -153,23 +171,19 @@
assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
unfolding euclidean_component_def basis_zero[OF assms] by simp
-lemma euclidean_scaleR:
- shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
- unfolding euclidean_component_def by auto
-
lemmas euclidean_simps =
- euclidean_component.add
- euclidean_component.diff
- euclidean_scaleR
- euclidean_component.minus
- euclidean_component.setsum
+ euclidean_component_add
+ euclidean_component_diff
+ euclidean_component_scaleR
+ euclidean_component_minus
+ euclidean_component_setsum
basis_component
lemma euclidean_representation:
fixes x :: "'a::euclidean_space"
shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
apply (rule euclidean_eqI)
- apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
+ apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
apply (simp add: if_distrib setsum_delta cong: if_cong)
done
@@ -180,7 +194,7 @@
lemma euclidean_lambda_beta [simp]:
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
- by (auto simp: euclidean_component.setsum euclidean_component.scaleR
+ by (auto simp: euclidean_component_setsum euclidean_component_scaleR
Chi_def if_distrib setsum_cases intro!: setsum_cong)
lemma euclidean_lambda_beta':
@@ -201,7 +215,7 @@
lemma euclidean_inner:
"inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
by (subst (1 2) euclidean_representation,
- simp add: inner_left.setsum inner_right.setsum
+ simp add: inner_setsum_left inner_setsum_right
dot_basis if_distrib setsum_cases mult_commute)
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 23:43:22 2011 +0200
@@ -66,7 +66,7 @@
apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
- unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
+ unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
note lem3 = this[rule_format]
have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 23:43:22 2011 +0200
@@ -401,14 +401,15 @@
unfolding norm_vec_def
by (rule member_le_setL2) simp_all
-interpretation vec_nth: bounded_linear "\<lambda>x. x $ i"
+lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
apply default
apply (rule vector_add_component)
apply (rule vector_scaleR_component)
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
-declare vec_nth.isCont [simp]
+lemmas isCont_vec_nth [simp] =
+ bounded_linear.isCont [OF bounded_linear_vec_nth]
instance vec :: (banach, finite) banach ..
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 23:43:22 2011 +0200
@@ -16,7 +16,7 @@
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
- scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
+ scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
lemma real_arch_invD:
"0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
@@ -1225,7 +1225,7 @@
lemma has_integral_cmul:
shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
- by(rule scaleR.bounded_linear_right)
+ by(rule bounded_linear_scaleR_right)
lemma has_integral_neg:
shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
@@ -2262,7 +2262,7 @@
assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> e * content({a..b})"
apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
- unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto
+ unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
@@ -2287,7 +2287,7 @@
lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. (f x)$$i \<le> (g x)$$i"
shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)$$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)$$i"
- unfolding euclidean_component.setsum apply(rule setsum_mono) apply safe
+ unfolding euclidean_component_setsum apply(rule setsum_mono) apply safe
proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
from this(3) guess u v apply-by(erule exE)+ note b=this
show "(content b *\<^sub>R f a) $$ i \<le> (content b *\<^sub>R g a) $$ i" unfolding b
@@ -2988,7 +2988,7 @@
have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
- unfolding scaleR.diff_left by(auto simp add:algebra_simps)
+ unfolding scaleR_diff_left by(auto simp add:algebra_simps)
also have "... \<le> e * norm (u - x) + e * norm (v - x)"
apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
apply(rule d(2)[of "x" "v",unfolded o_def])
@@ -3123,7 +3123,7 @@
assumes "continuous_on {a..b} f" "x \<in> {a..b}"
shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
unfolding has_vector_derivative_def has_derivative_within_alt
-apply safe apply(rule scaleR.bounded_linear_left)
+apply safe apply(rule bounded_linear_scaleR_left)
proof- fix e::real assume e:"e>0"
note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
@@ -3223,8 +3223,8 @@
have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
- also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym]
- unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" .
+ also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR
+ using assms(1) by auto finally have *:"?l = ?r" .
show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR
using assms(1) by(auto simp add:field_simps) qed qed qed
@@ -3256,7 +3256,7 @@
lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})"
apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a]
- unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym]
+ unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR
defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
@@ -3442,7 +3442,7 @@
show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[THEN sym] split_minus
unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
proof(rule norm_triangle_le,rule **)
- case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum)
+ case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \<in> p"
"e * (interval_upperbound k - interval_lowerbound k) / 2
< norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
@@ -4159,7 +4159,7 @@
"(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
"0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
- apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
+ apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym]
apply(rule_tac[!] mult_nonneg_nonneg)
proof- fix a b assume ab:"(a,b) \<in> p1"
show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
@@ -4535,7 +4535,7 @@
show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum)
apply(rule setsum_mono) unfolding split_paired_all split_conv
- unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
+ unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym]
unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
@@ -5202,7 +5202,7 @@
proof- have *:"\<And>x. ((\<chi>\<chi> i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\<lambda>i.
(((\<lambda>y. (\<chi>\<chi> j. if j = i then y else 0)) o
(((\<lambda>x. (norm((\<chi>\<chi> j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..<DIM('c)})"
- unfolding euclidean_eq[where 'a='c] euclidean_component.setsum apply safe
+ unfolding euclidean_eq[where 'a='c] euclidean_component_setsum apply safe
unfolding euclidean_lambda_beta'
proof- case goal1 have *:"\<And>i xa. ((if i = xa then f x $$ xa else 0) * (if i = xa then f x $$ xa else 0)) =
(if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto
@@ -5220,7 +5220,7 @@
apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm)
apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c]
- by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def])
+ by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def])
qed
lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
@@ -5266,7 +5266,7 @@
proof- fix k and i assume "k\<in>d" and i:"i<DIM('m)"
from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
show "\<bar>integral k f $$ i\<bar> \<le> integral k (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ i" apply(rule abs_leI)
- unfolding euclidean_component.minus[THEN sym] defer apply(subst integral_neg[THEN sym])
+ unfolding euclidean_component_minus[THEN sym] defer apply(subst integral_neg[THEN sym])
defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
using integrable_on_subinterval[OF assms(1),of a b]
integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
@@ -5276,7 +5276,7 @@
using integrable_on_subdivision[OF d assms(2)] by auto
have "(\<Sum>i\<in>d. integral i (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j)
= integral (\<Union>d) (\<lambda>x. (\<chi>\<chi> j. abs(f x$$j)) ::'m::ordered_euclidean_space) $$ j"
- unfolding euclidean_component.setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
+ unfolding euclidean_component_setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
also have "... \<le> integral UNIV (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j"
apply(rule integral_subset_component_le) using assms * by auto
finally show ?case .
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 23:43:22 2011 +0200
@@ -198,8 +198,8 @@
text{* Dot product in terms of the norm rather than conversely. *}
-lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left
-inner.scaleR_left inner.scaleR_right
+lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
+inner_scaleR_left inner_scaleR_right
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
unfolding power2_norm_eq_inner inner_simps inner_commute by auto
@@ -1558,7 +1558,7 @@
unfolding independent_eq_inj_on [OF basis_inj]
apply clarify
apply (drule_tac f="inner (basis a)" in arg_cong)
- apply (simp add: inner_right.setsum dot_basis)
+ apply (simp add: inner_setsum_right dot_basis)
done
lemma dimensionI:
@@ -1663,10 +1663,10 @@
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP]
- unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
+ unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i] fPs[OF PnP]
- unfolding euclidean_component.setsum euclidean_component.minus
+ unfolding euclidean_component_setsum euclidean_component_minus
by(auto simp add: setsum_negf intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
apply (subst thp)
@@ -1756,7 +1756,7 @@
have Kp: "?K > 0" by arith
{ assume C: "B < 0"
have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
- by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
+ by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
by (simp add: mult_less_0_iff)
@@ -2829,7 +2829,7 @@
unfolding infnorm_def
unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
- apply(subst (1) euclidean_eq) unfolding euclidean_component.zero
+ apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
by auto
then show ?thesis using infnorm_pos_le[of x] by simp
qed
@@ -2881,7 +2881,7 @@
lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
apply (subst infnorm_def)
unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult
+ unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult
using component_le_infnorm[of x] by(auto intro: mult_mono)
lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
@@ -14,7 +14,7 @@
lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
- apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
+ apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
@@ -1912,7 +1912,7 @@
fixes S :: "'a::real_normed_vector set"
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
apply (rule bounded_linear_image, assumption)
- apply (rule scaleR.bounded_linear_right)
+ apply (rule bounded_linear_scaleR_right)
done
lemma bounded_translation:
@@ -3537,7 +3537,7 @@
proof-
{ fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
- using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
+ using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
}
thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
@@ -4365,7 +4365,7 @@
assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
proof-
let ?f = "\<lambda>x. scaleR c x"
- have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
+ have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
using linear_continuous_at[OF *] assms by auto
qed
@@ -4951,7 +4951,7 @@
unfolding Lim_sequentially by(auto simp add: dist_norm)
hence "(f ---> x) sequentially" unfolding f_def
using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
- using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
+ using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
ultimately have "x \<in> closure {a<..<b}"
using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto }
thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
@@ -5571,7 +5571,7 @@
subsection {* Some properties of a canonical subspace *}
(** move **)
-declare euclidean_component.zero[simp]
+declare euclidean_component_zero[simp]
lemma subspace_substandard:
"subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
@@ -6027,15 +6027,15 @@
lemmas Lim_ident_at = LIM_ident
lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
+lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
lemmas Lim_neg = tendsto_minus
lemmas Lim_add = tendsto_add
lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = scaleR.tendsto
-lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
+lemmas Lim_mul = tendsto_scaleR
+lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = euclidean_component.tendsto
+lemmas Lim_component = tendsto_euclidean_component
lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
end
--- a/src/HOL/Nat.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Nat.thy Thu Aug 18 23:43:22 2011 +0200
@@ -39,11 +39,20 @@
Zero_RepI: "Nat Zero_Rep"
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
-typedef (open Nat) nat = Nat
- by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
+typedef (open Nat) nat = "{n. Nat n}"
+ using Nat.Zero_RepI by auto
+
+lemma Nat_Rep_Nat:
+ "Nat (Rep_Nat n)"
+ using Rep_Nat by simp
-definition Suc :: "nat => nat" where
- "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
+lemma Nat_Abs_Nat_inverse:
+ "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
+ using Abs_Nat_inverse by simp
+
+lemma Nat_Abs_Nat_inject:
+ "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
+ using Abs_Nat_inject by simp
instantiation nat :: zero
begin
@@ -55,9 +64,11 @@
end
+definition Suc :: "nat \<Rightarrow> nat" where
+ "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
+
lemma Suc_not_Zero: "Suc m \<noteq> 0"
- by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
- Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
+ by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
lemma Zero_not_Suc: "0 \<noteq> Suc m"
by (rule not_sym, rule Suc_not_Zero not_sym)
@@ -67,12 +78,12 @@
rep_datatype "0 \<Colon> nat" Suc
apply (unfold Zero_nat_def Suc_def)
- apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
- apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
- apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
- apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
- Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
- Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
+ apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
+ apply (erule Nat_Rep_Nat [THEN Nat.induct])
+ apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
+ apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
+ Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
+ Suc_Rep_not_Zero_Rep [symmetric]
Suc_Rep_inject' Rep_Nat_inject)
done
--- a/src/HOL/Nitpick.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Nitpick.thy Thu Aug 18 23:43:22 2011 +0200
@@ -76,19 +76,19 @@
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
-definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
"refl' r \<equiv> \<forall>x. (x, x) \<in> r"
-definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
"wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
-definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
+definition card' :: "'a set \<Rightarrow> nat" where
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
-definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
+definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
-inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
+inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |
"\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
--- a/src/HOL/Probability/Borel_Space.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Thu Aug 18 23:43:22 2011 +0200
@@ -816,7 +816,7 @@
proof cases
assume "b \<noteq> 0"
with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
- by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
+ by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
hence "?S \<in> sets borel"
unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
moreover
--- a/src/HOL/Probability/Independent_Family.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Thu Aug 18 23:43:22 2011 +0200
@@ -563,7 +563,7 @@
with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
by simp
moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
- by (intro mult_right.sums finite_measure_UNION F dis)
+ by (intro sums_mult finite_measure_UNION F dis)
ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
by (auto dest!: sums_unique)
with F show "(\<Union>i. F i) \<in> sets ?D"
--- a/src/HOL/RealDef.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/RealDef.thy Thu Aug 18 23:43:22 2011 +0200
@@ -121,7 +121,7 @@
subsection {* Cauchy sequences *}
definition
- cauchy :: "(nat \<Rightarrow> rat) set"
+ cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
where
"cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
--- a/src/HOL/RealVector.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/RealVector.thy Thu Aug 18 23:43:22 2011 +0200
@@ -62,24 +62,28 @@
and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
and scale_left_diff_distrib [algebra_simps]:
"scale (a - b) x = scale a x - scale b x"
+ and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)"
proof -
interpret s: additive "\<lambda>a. scale a x"
proof qed (rule scale_left_distrib)
show "scale 0 x = 0" by (rule s.zero)
show "scale (- a) x = - (scale a x)" by (rule s.minus)
show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
+ show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum)
qed
lemma scale_zero_right [simp]: "scale a 0 = 0"
and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
and scale_right_diff_distrib [algebra_simps]:
"scale a (x - y) = scale a x - scale a y"
+ and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))"
proof -
interpret s: additive "\<lambda>x. scale a x"
proof qed (rule scale_right_distrib)
show "scale a 0 = 0" by (rule s.zero)
show "scale a (- x) = - (scale a x)" by (rule s.minus)
show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
+ show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum)
qed
lemma scale_eq_0_iff [simp]:
@@ -140,16 +144,16 @@
end
class real_vector = scaleR + ab_group_add +
- assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
- and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
+ assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y"
+ and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x"
and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
and scaleR_one: "scaleR 1 x = x"
interpretation real_vector:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
apply unfold_locales
-apply (rule scaleR_right_distrib)
-apply (rule scaleR_left_distrib)
+apply (rule scaleR_add_right)
+apply (rule scaleR_add_left)
apply (rule scaleR_scaleR)
apply (rule scaleR_one)
done
@@ -159,16 +163,25 @@
lemmas scaleR_left_commute = real_vector.scale_left_commute
lemmas scaleR_zero_left = real_vector.scale_zero_left
lemmas scaleR_minus_left = real_vector.scale_minus_left
-lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
+lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
+lemmas scaleR_setsum_left = real_vector.scale_setsum_left
lemmas scaleR_zero_right = real_vector.scale_zero_right
lemmas scaleR_minus_right = real_vector.scale_minus_right
-lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
+lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
+lemmas scaleR_setsum_right = real_vector.scale_setsum_right
lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
lemmas scaleR_cancel_left = real_vector.scale_cancel_left
lemmas scaleR_cancel_right = real_vector.scale_cancel_right
+text {* Legacy names *}
+
+lemmas scaleR_left_distrib = scaleR_add_left
+lemmas scaleR_right_distrib = scaleR_add_right
+lemmas scaleR_left_diff_distrib = scaleR_diff_left
+lemmas scaleR_right_diff_distrib = scaleR_diff_right
+
lemma scaleR_minus1_left [simp]:
fixes x :: "'a::real_vector"
shows "scaleR (-1) x = - x"
@@ -1059,8 +1072,8 @@
end
-interpretation mult:
- bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
+lemma bounded_bilinear_mult:
+ "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
apply (rule right_distrib)
@@ -1070,19 +1083,21 @@
apply (simp add: norm_mult_ineq)
done
-interpretation mult_left:
- bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
-by (rule mult.bounded_linear_left)
+lemma bounded_linear_mult_left:
+ "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
+ using bounded_bilinear_mult
+ by (rule bounded_bilinear.bounded_linear_left)
-interpretation mult_right:
- bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
-by (rule mult.bounded_linear_right)
+lemma bounded_linear_mult_right:
+ "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)"
+ using bounded_bilinear_mult
+ by (rule bounded_bilinear.bounded_linear_right)
-interpretation divide:
- bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
-unfolding divide_inverse by (rule mult.bounded_linear_left)
+lemma bounded_linear_divide:
+ "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
+ unfolding divide_inverse by (rule bounded_linear_mult_left)
-interpretation scaleR: bounded_bilinear "scaleR"
+lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -1091,14 +1106,16 @@
apply (rule_tac x="1" in exI, simp)
done
-interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
-by (rule scaleR.bounded_linear_left)
+lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
+ using bounded_bilinear_scaleR
+ by (rule bounded_bilinear.bounded_linear_left)
-interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
-by (rule scaleR.bounded_linear_right)
+lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)"
+ using bounded_bilinear_scaleR
+ by (rule bounded_bilinear.bounded_linear_right)
-interpretation of_real: bounded_linear "\<lambda>r. of_real r"
-unfolding of_real_def by (rule scaleR.bounded_linear_left)
+lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
+ unfolding of_real_def by (rule bounded_linear_scaleR_left)
subsection{* Hausdorff and other separation properties *}
--- a/src/HOL/Relation.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Relation.thy Thu Aug 18 23:43:22 2011 +0200
@@ -133,9 +133,8 @@
by blast
lemma Id_on_def' [nitpick_unfold, code]:
- "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
-by (auto simp add: fun_eq_iff
- elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
+ "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
+by auto
lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
by blast
--- a/src/HOL/SEQ.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/SEQ.thy Thu Aug 18 23:43:22 2011 +0200
@@ -377,7 +377,7 @@
lemma LIMSEQ_mult:
fixes a b :: "'a::real_normed_algebra"
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
-by (rule mult.tendsto)
+ by (rule tendsto_mult)
lemma increasing_LIMSEQ:
fixes f :: "nat \<Rightarrow> real"
--- a/src/HOL/Series.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Series.thy Thu Aug 18 23:43:22 2011 +0200
@@ -211,50 +211,54 @@
"summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
by (intro sums_unique sums summable_sums)
+lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
+lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
+lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
+
lemma sums_mult:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
-by (rule mult_right.sums)
+ by (rule bounded_linear.sums [OF bounded_linear_mult_right])
lemma summable_mult:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> summable (%n. c * f n)"
-by (rule mult_right.summable)
+ by (rule bounded_linear.summable [OF bounded_linear_mult_right])
lemma suminf_mult:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
-by (rule mult_right.suminf [symmetric])
+ by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
lemma sums_mult2:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
-by (rule mult_left.sums)
+ by (rule bounded_linear.sums [OF bounded_linear_mult_left])
lemma summable_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
-by (rule mult_left.summable)
+ by (rule bounded_linear.summable [OF bounded_linear_mult_left])
lemma suminf_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
-by (rule mult_left.suminf)
+ by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
lemma sums_divide:
fixes c :: "'a::real_normed_field"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
-by (rule divide.sums)
+ by (rule bounded_linear.sums [OF bounded_linear_divide])
lemma summable_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
-by (rule divide.summable)
+ by (rule bounded_linear.summable [OF bounded_linear_divide])
lemma suminf_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
-by (rule divide.suminf [symmetric])
+ by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
lemma sums_add:
fixes a b :: "'a::real_normed_field"
@@ -423,7 +427,7 @@
by auto
have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
by simp
- thus ?thesis using divide.sums [OF 2, of 2]
+ thus ?thesis using sums_divide [OF 2, of 2]
by simp
qed
--- a/src/HOL/String.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/String.thy Thu Aug 18 23:43:22 2011 +0200
@@ -155,7 +155,7 @@
subsection {* Strings as dedicated type *}
-typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
+typedef (open) literal = "UNIV :: string set"
morphisms explode STR ..
instantiation literal :: size
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 23:43:22 2011 +0200
@@ -465,7 +465,7 @@
(* setup *)
-val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
val setup =
Code.datatype_interpretation ensure_partial_term_of
@@ -474,4 +474,4 @@
(((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Transcendental.thy Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/Transcendental.thy Thu Aug 18 23:43:22 2011 +0200
@@ -971,7 +971,7 @@
lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
unfolding exp_def
-apply (subst of_real.suminf)
+apply (subst suminf_of_real)
apply (rule summable_exp_generic)
apply (simp add: scaleR_conv_of_real)
done
--- a/src/HOL/ex/ROOT.ML Thu Aug 18 18:07:40 2011 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Aug 18 23:43:22 2011 +0200
@@ -48,7 +48,7 @@
"Primrec",
"Tarski",
"Classical",
- "set",
+ "Set_Theory",
"Meson_Test",
"Termination",
"Coherent",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Set_Theory.thy Thu Aug 18 23:43:22 2011 +0200
@@ -0,0 +1,227 @@
+(* Title: HOL/ex/Set_Theory.thy
+ Author: Tobias Nipkow and Lawrence C Paulson
+ Copyright 1991 University of Cambridge
+*)
+
+header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
+
+theory Set_Theory
+imports Main
+begin
+
+text{*
+ These two are cited in Benzmueller and Kohlhase's system description
+ of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
+ prove.
+*}
+
+lemma "(X = Y \<union> Z) =
+ (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+ by blast
+
+lemma "(X = Y \<inter> Z) =
+ (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
+ by blast
+
+text {*
+ Trivial example of term synthesis: apparently hard for some provers!
+*}
+
+schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
+ by blast
+
+
+subsection {* Examples for the @{text blast} paper *}
+
+lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
+ -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
+ by blast
+
+lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
+ -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
+ by blast
+
+lemma singleton_example_1:
+ "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+ by blast
+
+lemma singleton_example_2:
+ "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+ -- {*Variant of the problem above. *}
+ by blast
+
+lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+ -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
+ by metis
+
+
+subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
+
+lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
+ -- {* Requires best-first search because it is undirectional. *}
+ by best
+
+schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
+ -- {*This form displays the diagonal term. *}
+ by best
+
+schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+ -- {* This form exploits the set constructs. *}
+ by (rule notI, erule rangeE, best)
+
+schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+ -- {* Or just this! *}
+ by best
+
+
+subsection {* The Schröder-Berstein Theorem *}
+
+lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
+ by blast
+
+lemma surj_if_then_else:
+ "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
+ by (simp add: surj_def) blast
+
+lemma bij_if_then_else:
+ "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
+ h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
+ apply (unfold inj_on_def)
+ apply (simp add: surj_if_then_else)
+ apply (blast dest: disj_lemma sym)
+ done
+
+lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
+ apply (rule exI)
+ apply (rule lfp_unfold)
+ apply (rule monoI, blast)
+ done
+
+theorem Schroeder_Bernstein:
+ "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
+ \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
+ apply (rule decomposition [where f=f and g=g, THEN exE])
+ apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
+ --{*The term above can be synthesized by a sufficiently detailed proof.*}
+ apply (rule bij_if_then_else)
+ apply (rule_tac [4] refl)
+ apply (rule_tac [2] inj_on_inv_into)
+ apply (erule subset_inj_on [OF _ subset_UNIV])
+ apply blast
+ apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
+ done
+
+
+subsection {* A simple party theorem *}
+
+text{* \emph{At any party there are two people who know the same
+number of people}. Provided the party consists of at least two people
+and the knows relation is symmetric. Knowing yourself does not count
+--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
+at TPHOLs 2007.) *}
+
+lemma equal_number_of_acquaintances:
+assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
+shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
+proof -
+ let ?N = "%a. card(R `` {a} - {a})"
+ let ?n = "card A"
+ have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
+ have 0: "R `` A <= A" using `sym R` `Domain R <= A`
+ unfolding Domain_def sym_def by blast
+ have h: "ALL a:A. R `` {a} <= A" using 0 by blast
+ hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
+ by(blast intro: finite_subset)
+ have sub: "?N ` A <= {0..<?n}"
+ proof -
+ have "ALL a:A. R `` {a} - {a} < A" using h by blast
+ thus ?thesis using psubset_card_mono[OF `finite A`] by auto
+ qed
+ show "~ inj_on ?N A" (is "~ ?I")
+ proof
+ assume ?I
+ hence "?n = card(?N ` A)" by(rule card_image[symmetric])
+ with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
+ using subset_card_intvl_is_intvl[of _ 0] by(auto)
+ have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
+ then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
+ by (auto simp del: 2)
+ have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
+ have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
+ hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
+ hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
+ hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
+ have 4: "finite (A - {a,b})" using `finite A` by simp
+ have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
+ then show False using Nb `card A \<ge> 2` by arith
+ qed
+qed
+
+text {*
+ From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
+ 293-314.
+
+ Isabelle can prove the easy examples without any special mechanisms,
+ but it can't prove the hard ones.
+*}
+
+lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
+ -- {* Example 1, page 295. *}
+ by force
+
+lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
+ -- {* Example 2. *}
+ by force
+
+lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
+ -- {* Example 3. *}
+ by force
+
+lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
+ -- {* Example 4. *}
+ by force
+
+lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+ -- {*Example 5, page 298. *}
+ by force
+
+lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+ -- {* Example 6. *}
+ by force
+
+lemma "\<exists>A. a \<notin> A"
+ -- {* Example 7. *}
+ by force
+
+lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
+ \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
+ -- {* Example 8 now needs a small hint. *}
+ by (simp add: abs_if, force)
+ -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
+
+text {* Example 9 omitted (requires the reals). *}
+
+text {* The paper has no Example 10! *}
+
+lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
+ P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
+ -- {* Example 11: needs a hint. *}
+by(metis nat.induct)
+
+lemma
+ "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
+ \<and> P n \<longrightarrow> P m"
+ -- {* Example 12. *}
+ by auto
+
+lemma
+ "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
+ (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
+ -- {* Example EO1: typo in article, and with the obvious fix it seems
+ to require arithmetic reasoning. *}
+ apply clarify
+ apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
+ apply metis+
+ done
+
+end
--- a/src/HOL/ex/set.thy Thu Aug 18 18:07:40 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-(* Title: HOL/ex/set.thy
- Author: Tobias Nipkow and Lawrence C Paulson
- Copyright 1991 University of Cambridge
-*)
-
-header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
-
-theory set imports Main begin
-
-text{*
- These two are cited in Benzmueller and Kohlhase's system description
- of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
- prove.
-*}
-
-lemma "(X = Y \<union> Z) =
- (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
- by blast
-
-lemma "(X = Y \<inter> Z) =
- (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
- by blast
-
-text {*
- Trivial example of term synthesis: apparently hard for some provers!
-*}
-
-schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
- by blast
-
-
-subsection {* Examples for the @{text blast} paper *}
-
-lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
- -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
- by blast
-
-lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
- -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
- by blast
-
-lemma singleton_example_1:
- "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
- by blast
-
-lemma singleton_example_2:
- "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
- -- {*Variant of the problem above. *}
- by blast
-
-lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
- -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
- by metis
-
-
-subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
-
-lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
- -- {* Requires best-first search because it is undirectional. *}
- by best
-
-schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
- -- {*This form displays the diagonal term. *}
- by best
-
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
- -- {* This form exploits the set constructs. *}
- by (rule notI, erule rangeE, best)
-
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
- -- {* Or just this! *}
- by best
-
-
-subsection {* The Schröder-Berstein Theorem *}
-
-lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
- by blast
-
-lemma surj_if_then_else:
- "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
- by (simp add: surj_def) blast
-
-lemma bij_if_then_else:
- "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
- h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
- apply (unfold inj_on_def)
- apply (simp add: surj_if_then_else)
- apply (blast dest: disj_lemma sym)
- done
-
-lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
- apply (rule exI)
- apply (rule lfp_unfold)
- apply (rule monoI, blast)
- done
-
-theorem Schroeder_Bernstein:
- "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
- \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
- apply (rule decomposition [where f=f and g=g, THEN exE])
- apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
- --{*The term above can be synthesized by a sufficiently detailed proof.*}
- apply (rule bij_if_then_else)
- apply (rule_tac [4] refl)
- apply (rule_tac [2] inj_on_inv_into)
- apply (erule subset_inj_on [OF _ subset_UNIV])
- apply blast
- apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
- done
-
-
-subsection {* A simple party theorem *}
-
-text{* \emph{At any party there are two people who know the same
-number of people}. Provided the party consists of at least two people
-and the knows relation is symmetric. Knowing yourself does not count
---- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
-at TPHOLs 2007.) *}
-
-lemma equal_number_of_acquaintances:
-assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
-shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
-proof -
- let ?N = "%a. card(R `` {a} - {a})"
- let ?n = "card A"
- have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
- have 0: "R `` A <= A" using `sym R` `Domain R <= A`
- unfolding Domain_def sym_def by blast
- have h: "ALL a:A. R `` {a} <= A" using 0 by blast
- hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
- by(blast intro: finite_subset)
- have sub: "?N ` A <= {0..<?n}"
- proof -
- have "ALL a:A. R `` {a} - {a} < A" using h by blast
- thus ?thesis using psubset_card_mono[OF `finite A`] by auto
- qed
- show "~ inj_on ?N A" (is "~ ?I")
- proof
- assume ?I
- hence "?n = card(?N ` A)" by(rule card_image[symmetric])
- with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
- using subset_card_intvl_is_intvl[of _ 0] by(auto)
- have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
- then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
- by (auto simp del: 2)
- have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
- have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
- hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
- hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
- hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
- have 4: "finite (A - {a,b})" using `finite A` by simp
- have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
- then show False using Nb `card A \<ge> 2` by arith
- qed
-qed
-
-text {*
- From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
- 293-314.
-
- Isabelle can prove the easy examples without any special mechanisms,
- but it can't prove the hard ones.
-*}
-
-lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
- -- {* Example 1, page 295. *}
- by force
-
-lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
- -- {* Example 2. *}
- by force
-
-lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
- -- {* Example 3. *}
- by force
-
-lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
- -- {* Example 4. *}
- by force
-
-lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
- -- {*Example 5, page 298. *}
- by force
-
-lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
- -- {* Example 6. *}
- by force
-
-lemma "\<exists>A. a \<notin> A"
- -- {* Example 7. *}
- by force
-
-lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
- \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
- -- {* Example 8 now needs a small hint. *}
- by (simp add: abs_if, force)
- -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
-
-text {* Example 9 omitted (requires the reals). *}
-
-text {* The paper has no Example 10! *}
-
-lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
- P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
- -- {* Example 11: needs a hint. *}
-by(metis nat.induct)
-
-lemma
- "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
- \<and> P n \<longrightarrow> P m"
- -- {* Example 12. *}
- by auto
-
-lemma
- "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
- (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
- -- {* Example EO1: typo in article, and with the obvious fix it seems
- to require arithmetic reasoning. *}
- apply clarify
- apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
- apply metis+
- done
-
-end