1.1 --- a/NEWS Thu Aug 18 18:07:40 2011 +0200
1.2 +++ b/NEWS Thu Aug 18 23:43:22 2011 +0200
1.3 @@ -57,6 +57,9 @@
1.4 * Isabelle/Isar reference manual provides more formal references in
1.5 syntax diagrams.
1.6
1.7 +* Attribute case_names has been refined: the assumptions in each case can
1.8 +be named now by following the case name with [name1 name2 ...].
1.9 +
1.10
1.11 *** HOL ***
1.12
1.13 @@ -196,6 +199,19 @@
1.14 tendsto_vector ~> vec_tendstoI
1.15 Cauchy_vector ~> vec_CauchyI
1.16
1.17 +* Complex_Main: The locale interpretations for the bounded_linear and
1.18 +bounded_bilinear locales have been removed, in order to reduce the
1.19 +number of duplicate lemmas. Users must use the original names for
1.20 +distributivity theorems, potential INCOMPATIBILITY.
1.21 +
1.22 + divide.add ~> add_divide_distrib
1.23 + divide.diff ~> diff_divide_distrib
1.24 + divide.setsum ~> setsum_divide_distrib
1.25 + mult.add_right ~> right_distrib
1.26 + mult.diff_right ~> right_diff_distrib
1.27 + mult_right.setsum ~> setsum_right_distrib
1.28 + mult_left.diff ~> left_diff_distrib
1.29 +
1.30
1.31 *** Document preparation ***
1.32
2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 18:07:40 2011 +0200
2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 23:43:22 2011 +0200
2.3 @@ -157,8 +157,11 @@
2.4 \item @{text R.cases} is the case analysis (or elimination) rule;
2.5
2.6 \item @{text R.induct} or @{text R.coinduct} is the (co)induction
2.7 - rule.
2.8 -
2.9 + rule;
2.10 +
2.11 + \item @{text R.simps} is the equation unrolling the fixpoint of the
2.12 + predicate one step.
2.13 +
2.14 \end{description}
2.15
2.16 When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 18:07:40 2011 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 23:43:22 2011 +0200
3.3 @@ -225,8 +225,11 @@
3.4 \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
3.5
3.6 \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
3.7 - rule.
3.8 -
3.9 + rule;
3.10 +
3.11 + \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
3.12 + predicate one step.
3.13 +
3.14 \end{description}
3.15
3.16 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
4.1 --- a/src/HOL/Equiv_Relations.thy Thu Aug 18 18:07:40 2011 +0200
4.2 +++ b/src/HOL/Equiv_Relations.thy Thu Aug 18 23:43:22 2011 +0200
4.3 @@ -164,7 +164,7 @@
4.4
4.5 text{*A congruence-preserving function*}
4.6
4.7 -definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
4.8 +definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
4.9 "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
4.10
4.11 lemma congruentI:
4.12 @@ -229,7 +229,7 @@
4.13
4.14 text{*A congruence-preserving function of two arguments*}
4.15
4.16 -definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
4.17 +definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
4.18 "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
4.19
4.20 lemma congruent2I':
5.1 --- a/src/HOL/Fun.thy Thu Aug 18 18:07:40 2011 +0200
5.2 +++ b/src/HOL/Fun.thy Thu Aug 18 23:43:22 2011 +0200
5.3 @@ -10,15 +10,6 @@
5.4 uses ("Tools/enriched_type.ML")
5.5 begin
5.6
5.7 -text{*As a simplification rule, it replaces all function equalities by
5.8 - first-order equalities.*}
5.9 -lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
5.10 -apply (rule iffI)
5.11 -apply (simp (no_asm_simp))
5.12 -apply (rule ext)
5.13 -apply (simp (no_asm_simp))
5.14 -done
5.15 -
5.16 lemma apply_inverse:
5.17 "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
5.18 by auto
5.19 @@ -26,26 +17,22 @@
5.20
5.21 subsection {* The Identity Function @{text id} *}
5.22
5.23 -definition
5.24 - id :: "'a \<Rightarrow> 'a"
5.25 -where
5.26 +definition id :: "'a \<Rightarrow> 'a" where
5.27 "id = (\<lambda>x. x)"
5.28
5.29 lemma id_apply [simp]: "id x = x"
5.30 by (simp add: id_def)
5.31
5.32 lemma image_id [simp]: "id ` Y = Y"
5.33 -by (simp add: id_def)
5.34 + by (simp add: id_def)
5.35
5.36 lemma vimage_id [simp]: "id -` A = A"
5.37 -by (simp add: id_def)
5.38 + by (simp add: id_def)
5.39
5.40
5.41 subsection {* The Composition Operator @{text "f \<circ> g"} *}
5.42
5.43 -definition
5.44 - comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
5.45 -where
5.46 +definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
5.47 "f o g = (\<lambda>x. f (g x))"
5.48
5.49 notation (xsymbols)
5.50 @@ -54,9 +41,6 @@
5.51 notation (HTML output)
5.52 comp (infixl "\<circ>" 55)
5.53
5.54 -text{*compatibility*}
5.55 -lemmas o_def = comp_def
5.56 -
5.57 lemma o_apply [simp]: "(f o g) x = f (g x)"
5.58 by (simp add: comp_def)
5.59
5.60 @@ -71,7 +55,7 @@
5.61
5.62 lemma o_eq_dest:
5.63 "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
5.64 - by (simp only: o_def) (fact fun_cong)
5.65 + by (simp only: comp_def) (fact fun_cong)
5.66
5.67 lemma o_eq_elim:
5.68 "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
5.69 @@ -89,9 +73,7 @@
5.70
5.71 subsection {* The Forward Composition Operator @{text fcomp} *}
5.72
5.73 -definition
5.74 - fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
5.75 -where
5.76 +definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
5.77 "f \<circ>> g = (\<lambda>x. g (f x))"
5.78
5.79 lemma fcomp_apply [simp]: "(f \<circ>> g) x = g (f x)"
5.80 @@ -569,8 +551,7 @@
5.81
5.82 subsection{*Function Updating*}
5.83
5.84 -definition
5.85 - fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
5.86 +definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
5.87 "fun_upd f a b == % x. if x=a then b else f x"
5.88
5.89 nonterminal updbinds and updbind
5.90 @@ -634,9 +615,7 @@
5.91
5.92 subsection {* @{text override_on} *}
5.93
5.94 -definition
5.95 - override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
5.96 -where
5.97 +definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
5.98 "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
5.99
5.100 lemma override_on_emptyset[simp]: "override_on f g {} = f"
5.101 @@ -651,9 +630,7 @@
5.102
5.103 subsection {* @{text swap} *}
5.104
5.105 -definition
5.106 - swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
5.107 -where
5.108 +definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
5.109 "swap a b f = f (a := f b, b:= f a)"
5.110
5.111 lemma swap_self [simp]: "swap a a f = f"
5.112 @@ -716,7 +693,7 @@
5.113 subsection {* Inversion of injective functions *}
5.114
5.115 definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
5.116 -"the_inv_into A f == %x. THE y. y : A & f y = x"
5.117 + "the_inv_into A f == %x. THE y. y : A & f y = x"
5.118
5.119 lemma the_inv_into_f_f:
5.120 "[| inj_on f A; x : A |] ==> the_inv_into A f (f x) = x"
5.121 @@ -775,6 +752,11 @@
5.122 shows "the_inv f (f x) = x" using assms UNIV_I
5.123 by (rule the_inv_into_f_f)
5.124
5.125 +
5.126 +text{*compatibility*}
5.127 +lemmas o_def = comp_def
5.128 +
5.129 +
5.130 subsection {* Cantor's Paradox *}
5.131
5.132 lemma Cantors_paradox [no_atp]:
6.1 --- a/src/HOL/GCD.thy Thu Aug 18 18:07:40 2011 +0200
6.2 +++ b/src/HOL/GCD.thy Thu Aug 18 23:43:22 2011 +0200
6.3 @@ -531,11 +531,8 @@
6.4
6.5 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
6.6 apply(rule antisym)
6.7 - apply(rule Max_le_iff[THEN iffD2])
6.8 - apply simp
6.9 - apply fastsimp
6.10 - apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
6.11 -apply simp
6.12 + apply(rule Max_le_iff [THEN iffD2])
6.13 + apply (auto intro: abs_le_D1 dvd_imp_le_int)
6.14 done
6.15
6.16 lemma gcd_is_Max_divisors_nat:
7.1 --- a/src/HOL/HOL.thy Thu Aug 18 18:07:40 2011 +0200
7.2 +++ b/src/HOL/HOL.thy Thu Aug 18 23:43:22 2011 +0200
7.3 @@ -1394,6 +1394,11 @@
7.4 "f (if c then x else y) = (if c then f x else f y)"
7.5 by simp
7.6
7.7 +text{*As a simplification rule, it replaces all function equalities by
7.8 + first-order equalities.*}
7.9 +lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
7.10 + by auto
7.11 +
7.12
7.13 subsubsection {* Generic cases and induction *}
7.14
8.1 --- a/src/HOL/Import/HOLLightReal.thy Thu Aug 18 18:07:40 2011 +0200
8.2 +++ b/src/HOL/Import/HOLLightReal.thy Thu Aug 18 23:43:22 2011 +0200
8.3 @@ -112,7 +112,7 @@
8.4
8.5 lemma REAL_DIFFSQ:
8.6 "((x :: real) + y) * (x - y) = x * x - y * y"
8.7 - by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
8.8 + by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
8.9
8.10 lemma REAL_ABS_TRIANGLE_LE:
8.11 "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
8.12 @@ -295,7 +295,7 @@
8.13 (\<forall>(x :: real). 0 * x = 0) \<and>
8.14 (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
8.15 (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
8.16 - by (auto simp add: mult.add_right)
8.17 + by (auto simp add: right_distrib)
8.18
8.19 lemma REAL_COMPLETE:
8.20 "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
9.1 --- a/src/HOL/IsaMakefile Thu Aug 18 18:07:40 2011 +0200
9.2 +++ b/src/HOL/IsaMakefile Thu Aug 18 23:43:22 2011 +0200
9.3 @@ -1039,32 +1039,30 @@
9.4
9.5 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
9.6 Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
9.7 - ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
9.8 - ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
9.9 - ex/CTL.thy ex/Case_Product.thy \
9.10 - ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
9.11 - ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
9.12 - ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
9.13 - ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
9.14 - ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
9.15 - ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
9.16 + ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
9.17 + ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \
9.18 + ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \
9.19 + ex/CodegenSML_Test.thy ex/Coercion_Examples.thy ex/Coherent.thy \
9.20 + ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
9.21 + ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
9.22 + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
9.23 + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
9.24 + ex/Iff_Oracle.thy ex/Induction_Schema.thy \
9.25 ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
9.26 ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
9.27 ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
9.28 ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
9.29 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
9.30 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
9.31 - ex/Quickcheck_Narrowing_Examples.thy \
9.32 - ex/Quicksort.thy ex/ROOT.ML ex/Records.thy \
9.33 - ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
9.34 - ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
9.35 - ex/sledgehammer_tactics.ML ex/Sqrt.thy \
9.36 - ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
9.37 - ex/Transfer_Ex.thy ex/Tree23.thy \
9.38 + ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
9.39 + ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
9.40 + ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
9.41 + ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML \
9.42 + ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy \
9.43 + ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
9.44 ex/Unification.thy ex/While_Combinator_Example.thy \
9.45 - ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
9.46 - ex/svc_test.thy \
9.47 - ../Tools/interpretation_with_defs.ML
9.48 + ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
9.49 + ex/svc_test.thy ../Tools/interpretation_with_defs.ML
9.50 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
9.51
9.52
10.1 --- a/src/HOL/Library/Convex.thy Thu Aug 18 18:07:40 2011 +0200
10.2 +++ b/src/HOL/Library/Convex.thy Thu Aug 18 23:43:22 2011 +0200
10.3 @@ -129,7 +129,7 @@
10.4 have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
10.5 hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
10.6 hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
10.7 - hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
10.8 + hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
10.9 from this asms
10.10 have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
10.11 hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
10.12 @@ -410,7 +410,7 @@
10.13 have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
10.14 hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
10.15 hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
10.16 - hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
10.17 + hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
10.18 have "convex C" using asms by auto
10.19 hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
10.20 using asms convex_setsum[OF `finite s`
10.21 @@ -433,7 +433,7 @@
10.22 using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
10.23 OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
10.24 also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
10.25 - unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
10.26 + unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
10.27 also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
10.28 also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
10.29 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))"
11.1 --- a/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 18:07:40 2011 +0200
11.2 +++ b/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 23:43:22 2011 +0200
11.3 @@ -5,7 +5,7 @@
11.4 header {* Frechet Derivative *}
11.5
11.6 theory FrechetDeriv
11.7 -imports Lim Complex_Main
11.8 +imports Complex_Main
11.9 begin
11.10
11.11 definition
11.12 @@ -398,9 +398,11 @@
11.13 by (simp only: FDERIV_lemma)
11.14 qed
11.15
11.16 -lemmas FDERIV_mult = mult.FDERIV
11.17 +lemmas FDERIV_mult =
11.18 + bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
11.19
11.20 -lemmas FDERIV_scaleR = scaleR.FDERIV
11.21 +lemmas FDERIV_scaleR =
11.22 + bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
11.23
11.24
11.25 subsection {* Powers *}
11.26 @@ -427,10 +429,10 @@
11.27 subsection {* Inverse *}
11.28
11.29 lemmas bounded_linear_mult_const =
11.30 - mult.bounded_linear_left [THEN bounded_linear_compose]
11.31 + bounded_linear_mult_left [THEN bounded_linear_compose]
11.32
11.33 lemmas bounded_linear_const_mult =
11.34 - mult.bounded_linear_right [THEN bounded_linear_compose]
11.35 + bounded_linear_mult_right [THEN bounded_linear_compose]
11.36
11.37 lemma FDERIV_inverse:
11.38 fixes x :: "'a::real_normed_div_algebra"
11.39 @@ -510,7 +512,7 @@
11.40 fixes x :: "'a::real_normed_field" shows
11.41 "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
11.42 apply (unfold fderiv_def)
11.43 - apply (simp add: mult.bounded_linear_left)
11.44 + apply (simp add: bounded_linear_mult_left)
11.45 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
11.46 apply (subst diff_divide_distrib)
11.47 apply (subst times_divide_eq_left [symmetric])
12.1 --- a/src/HOL/Library/Inner_Product.thy Thu Aug 18 18:07:40 2011 +0200
12.2 +++ b/src/HOL/Library/Inner_Product.thy Thu Aug 18 23:43:22 2011 +0200
12.3 @@ -5,7 +5,7 @@
12.4 header {* Inner Product Spaces and the Gradient Derivative *}
12.5
12.6 theory Inner_Product
12.7 -imports Complex_Main FrechetDeriv
12.8 +imports FrechetDeriv
12.9 begin
12.10
12.11 subsection {* Real inner product spaces *}
12.12 @@ -43,6 +43,9 @@
12.13 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
12.14 by (simp add: diff_minus inner_add_left)
12.15
12.16 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
12.17 + by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
12.18 +
12.19 text {* Transfer distributivity rules to right argument. *}
12.20
12.21 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
12.22 @@ -60,6 +63,9 @@
12.23 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
12.24 using inner_diff_left [of y z x] by (simp only: inner_commute)
12.25
12.26 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
12.27 + using inner_setsum_left [of f A x] by (simp only: inner_commute)
12.28 +
12.29 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
12.30 lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right
12.31 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
12.32 @@ -148,8 +154,8 @@
12.33 setup {* Sign.add_const_constraint
12.34 (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
12.35
12.36 -interpretation inner:
12.37 - bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
12.38 +lemma bounded_bilinear_inner:
12.39 + "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
12.40 proof
12.41 fix x y z :: 'a and r :: real
12.42 show "inner (x + y) z = inner x z + inner y z"
12.43 @@ -167,15 +173,20 @@
12.44 qed
12.45 qed
12.46
12.47 -interpretation inner_left:
12.48 - bounded_linear "\<lambda>x::'a::real_inner. inner x y"
12.49 - by (rule inner.bounded_linear_left)
12.50 +lemmas tendsto_inner [tendsto_intros] =
12.51 + bounded_bilinear.tendsto [OF bounded_bilinear_inner]
12.52
12.53 -interpretation inner_right:
12.54 - bounded_linear "\<lambda>y::'a::real_inner. inner x y"
12.55 - by (rule inner.bounded_linear_right)
12.56 +lemmas isCont_inner [simp] =
12.57 + bounded_bilinear.isCont [OF bounded_bilinear_inner]
12.58
12.59 -declare inner.isCont [simp]
12.60 +lemmas FDERIV_inner =
12.61 + bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
12.62 +
12.63 +lemmas bounded_linear_inner_left =
12.64 + bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
12.65 +
12.66 +lemmas bounded_linear_inner_right =
12.67 + bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
12.68
12.69
12.70 subsection {* Class instances *}
12.71 @@ -260,29 +271,29 @@
12.72 by simp
12.73
12.74 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
12.75 - unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
12.76 + unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
12.77
12.78 lemma GDERIV_add:
12.79 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
12.80 \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
12.81 - unfolding gderiv_def inner_right.add by (rule FDERIV_add)
12.82 + unfolding gderiv_def inner_add_right by (rule FDERIV_add)
12.83
12.84 lemma GDERIV_minus:
12.85 "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
12.86 - unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
12.87 + unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
12.88
12.89 lemma GDERIV_diff:
12.90 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
12.91 \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
12.92 - unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
12.93 + unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
12.94
12.95 lemma GDERIV_scaleR:
12.96 "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
12.97 \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
12.98 :> (scaleR (f x) dg + scaleR df (g x))"
12.99 - unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
12.100 + unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
12.101 apply (rule FDERIV_subst)
12.102 - apply (erule (1) scaleR.FDERIV)
12.103 + apply (erule (1) FDERIV_scaleR)
12.104 apply (simp add: mult_ac)
12.105 done
12.106
12.107 @@ -306,7 +317,7 @@
12.108 assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
12.109 proof -
12.110 have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
12.111 - by (intro inner.FDERIV FDERIV_ident)
12.112 + by (intro FDERIV_inner FDERIV_ident)
12.113 have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
12.114 by (simp add: fun_eq_iff inner_commute)
12.115 have "0 < inner x x" using `x \<noteq> 0` by simp
13.1 --- a/src/HOL/Library/Product_Vector.thy Thu Aug 18 18:07:40 2011 +0200
13.2 +++ b/src/HOL/Library/Product_Vector.thy Thu Aug 18 23:43:22 2011 +0200
13.3 @@ -489,11 +489,11 @@
13.4
13.5 subsection {* Pair operations are linear *}
13.6
13.7 -interpretation fst: bounded_linear fst
13.8 +lemma bounded_linear_fst: "bounded_linear fst"
13.9 using fst_add fst_scaleR
13.10 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
13.11
13.12 -interpretation snd: bounded_linear snd
13.13 +lemma bounded_linear_snd: "bounded_linear snd"
13.14 using snd_add snd_scaleR
13.15 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
13.16
14.1 --- a/src/HOL/Lim.thy Thu Aug 18 18:07:40 2011 +0200
14.2 +++ b/src/HOL/Lim.thy Thu Aug 18 23:43:22 2011 +0200
14.3 @@ -321,17 +321,23 @@
14.4 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
14.5 by (rule tendsto_right_zero)
14.6
14.7 -lemmas LIM_mult = mult.LIM
14.8 +lemmas LIM_mult =
14.9 + bounded_bilinear.LIM [OF bounded_bilinear_mult]
14.10
14.11 -lemmas LIM_mult_zero = mult.LIM_prod_zero
14.12 +lemmas LIM_mult_zero =
14.13 + bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
14.14
14.15 -lemmas LIM_mult_left_zero = mult.LIM_left_zero
14.16 +lemmas LIM_mult_left_zero =
14.17 + bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
14.18
14.19 -lemmas LIM_mult_right_zero = mult.LIM_right_zero
14.20 +lemmas LIM_mult_right_zero =
14.21 + bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
14.22
14.23 -lemmas LIM_scaleR = scaleR.LIM
14.24 +lemmas LIM_scaleR =
14.25 + bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
14.26
14.27 -lemmas LIM_of_real = of_real.LIM
14.28 +lemmas LIM_of_real =
14.29 + bounded_linear.LIM [OF bounded_linear_of_real]
14.30
14.31 lemma LIM_power:
14.32 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
14.33 @@ -446,11 +452,11 @@
14.34 "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
14.35 unfolding isCont_def by (rule LIM)
14.36
14.37 -lemmas isCont_scaleR [simp] = scaleR.isCont
14.38 +lemmas isCont_scaleR [simp] =
14.39 + bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
14.40
14.41 -lemma isCont_of_real [simp]:
14.42 - "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
14.43 - by (rule of_real.isCont)
14.44 +lemmas isCont_of_real [simp] =
14.45 + bounded_linear.isCont [OF bounded_linear_of_real]
14.46
14.47 lemma isCont_power [simp]:
14.48 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
15.1 --- a/src/HOL/Limits.thy Thu Aug 18 18:07:40 2011 +0200
15.2 +++ b/src/HOL/Limits.thy Thu Aug 18 23:43:22 2011 +0200
15.3 @@ -510,9 +510,9 @@
15.4 "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
15.5 by (rule bounded_linear_right [THEN bounded_linear.Zfun])
15.6
15.7 -lemmas Zfun_mult = mult.Zfun
15.8 -lemmas Zfun_mult_right = mult.Zfun_right
15.9 -lemmas Zfun_mult_left = mult.Zfun_left
15.10 +lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
15.11 +lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
15.12 +lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
15.13
15.14
15.15 subsection {* Limits *}
15.16 @@ -752,7 +752,7 @@
15.17
15.18 subsubsection {* Linear operators and multiplication *}
15.19
15.20 -lemma (in bounded_linear) tendsto [tendsto_intros]:
15.21 +lemma (in bounded_linear) tendsto:
15.22 "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
15.23 by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
15.24
15.25 @@ -760,7 +760,7 @@
15.26 "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
15.27 by (drule tendsto, simp only: zero)
15.28
15.29 -lemma (in bounded_bilinear) tendsto [tendsto_intros]:
15.30 +lemma (in bounded_bilinear) tendsto:
15.31 "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
15.32 by (simp only: tendsto_Zfun_iff prod_diff_prod
15.33 Zfun_add Zfun Zfun_left Zfun_right)
15.34 @@ -779,7 +779,14 @@
15.35 "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
15.36 by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
15.37
15.38 -lemmas tendsto_mult = mult.tendsto
15.39 +lemmas tendsto_of_real [tendsto_intros] =
15.40 + bounded_linear.tendsto [OF bounded_linear_of_real]
15.41 +
15.42 +lemmas tendsto_scaleR [tendsto_intros] =
15.43 + bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
15.44 +
15.45 +lemmas tendsto_mult [tendsto_intros] =
15.46 + bounded_bilinear.tendsto [OF bounded_bilinear_mult]
15.47
15.48 lemma tendsto_power [tendsto_intros]:
15.49 fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
15.50 @@ -897,7 +904,7 @@
15.51 apply (erule (1) inverse_diff_inverse)
15.52 apply (rule Zfun_minus)
15.53 apply (rule Zfun_mult_left)
15.54 - apply (rule mult.Bfun_prod_Zfun)
15.55 + apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
15.56 apply (erule (1) Bfun_inverse)
15.57 apply (simp add: tendsto_Zfun_iff)
15.58 done
15.59 @@ -921,7 +928,7 @@
15.60 fixes a b :: "'a::real_normed_field"
15.61 shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
15.62 \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
15.63 - by (simp add: mult.tendsto tendsto_inverse divide_inverse)
15.64 + by (simp add: tendsto_mult tendsto_inverse divide_inverse)
15.65
15.66 lemma tendsto_sgn [tendsto_intros]:
15.67 fixes l :: "'a::real_normed_vector"
16.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 18:07:40 2011 +0200
16.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 23:43:22 2011 +0200
16.3 @@ -1202,7 +1202,7 @@
16.4 show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
16.5 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
16.6 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)"
16.7 - unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+
16.8 + unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
16.9 have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
16.10 unfolding norm_minus_commute by auto
16.11 also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
16.12 @@ -1234,7 +1234,7 @@
16.13 assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
16.14 { assume "x i = p \<or> x i = 0"
16.15 have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval
16.16 - apply safe unfolding euclidean_lambda_beta euclidean_component.zero
16.17 + apply safe unfolding euclidean_lambda_beta euclidean_component_zero
16.18 proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
16.19 hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
16.20 show "0 \<le> real (x (b' j)) / real p"
16.21 @@ -1262,11 +1262,11 @@
16.22 have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto
16.23 hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
16.24 hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
16.25 - unfolding euclidean_component.zero apply (simp_all only: if_P)
16.26 + unfolding euclidean_component_zero apply (simp_all only: if_P)
16.27 apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
16.28 hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
16.29 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)
16.30 - 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)
16.31 + 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)
16.32 also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
16.33 also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
16.34 finally show False using d_fz_z by auto qed then guess i .. note i=this
16.35 @@ -1276,15 +1276,15 @@
16.36 def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
16.37 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])
16.38 using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
16.39 - hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
16.40 + hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
16.41 apply (simp only: if_P)
16.42 apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
16.43 def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
16.44 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])
16.45 using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
16.46 - hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
16.47 + hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
16.48 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
16.49 - have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
16.50 + have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
16.51 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)
16.52 have *:"\<And>x. 1 + real x = real (Suc x)" by auto
16.53 { have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)"
17.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
17.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
17.3 @@ -1523,7 +1523,7 @@
17.4 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
17.5 show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"])
17.6 using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
17.7 - unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
17.8 + unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
17.9 qed
17.10
17.11 subsection {* Lemmas for working on @{typ "real^1"} *}
18.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
18.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
18.3 @@ -18,7 +18,7 @@
18.4 (* ------------------------------------------------------------------------- *)
18.5
18.6 lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
18.7 - by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
18.8 + by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
18.9
18.10 lemma injective_scaleR:
18.11 assumes "(c :: real) ~= 0"
18.12 @@ -128,7 +128,7 @@
18.13 proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
18.14 have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
18.15 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)"
18.16 - unfolding euclidean_component.setsum euclidean_scaleR basis_component *
18.17 + unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
18.18 apply(rule setsum_cong2) using assms by auto
18.19 show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
18.20 qed
18.21 @@ -1175,7 +1175,7 @@
18.22 have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
18.23 have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
18.24 apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
18.25 - also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
18.26 + also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
18.27 finally
18.28 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)
18.29 apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
18.30 @@ -2229,7 +2229,7 @@
18.31 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)
18.32 have "x : affine hull S" using assms hull_subset[of S] by auto
18.33 moreover have "1 / e + - ((1 - e) / e) = 1"
18.34 - using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
18.35 + using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
18.36 ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
18.37 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)
18.38 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)"
18.39 @@ -2957,7 +2957,7 @@
18.40 thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
18.41 using True using DIM_positive[where 'a='a] by auto
18.42 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
18.43 - apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
18.44 + apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
18.45
18.46 subsection {* Now set-to-set for closed/compact sets. *}
18.47
18.48 @@ -3053,7 +3053,7 @@
18.49 apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
18.50 apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
18.51 apply(rule assms[unfolded convex_def, rule_format]) prefer 6
18.52 - by (auto intro: tendsto_intros)
18.53 + by (auto intro!: tendsto_intros)
18.54
18.55 lemma convex_interior:
18.56 fixes s :: "'a::real_normed_vector set"
18.57 @@ -3221,13 +3221,13 @@
18.58 ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
18.59 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)
18.60 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
18.61 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
18.62 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
18.63 moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x"
18.64 apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
18.65 hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
18.66 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)
18.67 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
18.68 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
18.69 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
18.70 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
18.71 qed
18.72
18.73 @@ -4157,7 +4157,7 @@
18.74 let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
18.75 have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
18.76 { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
18.77 - unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
18.78 + unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
18.79 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
18.80 defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
18.81 note ** = this
18.82 @@ -4270,7 +4270,7 @@
18.83 { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
18.84 unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
18.85 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
18.86 - unfolding euclidean_component.setsum
18.87 + unfolding euclidean_component_setsum
18.88 apply(rule setsum_cong2)
18.89 using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
18.90 by (auto simp add: Euclidean_Space.basis_component[of i])}
18.91 @@ -4678,7 +4678,7 @@
18.92 hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
18.93 def x2 == "z+ e2 *\<^sub>R (z-x)"
18.94 hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
18.95 - have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
18.96 + have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
18.97 hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
18.98 using x1_def x2_def apply (auto simp add: algebra_simps)
18.99 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
19.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 18:07:40 2011 +0200
19.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 23:43:22 2011 +0200
19.3 @@ -93,13 +93,13 @@
19.4 proof -
19.5 have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
19.6 ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
19.7 - by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
19.8 + by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
19.9 also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
19.10 by (simp add: Lim_null[symmetric])
19.11 also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
19.12 by (intro Lim_cong_within) (simp_all add: field_simps)
19.13 finally show ?thesis
19.14 - by (simp add: mult.bounded_linear_right has_derivative_within)
19.15 + by (simp add: bounded_linear_mult_right has_derivative_within)
19.16 qed
19.17
19.18 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
19.19 @@ -140,10 +140,31 @@
19.20 apply (simp add: local.scaleR local.diff local.add local.zero)
19.21 done
19.22
19.23 +lemmas scaleR_right_has_derivative =
19.24 + bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
19.25 +
19.26 +lemmas scaleR_left_has_derivative =
19.27 + bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
19.28 +
19.29 +lemmas inner_right_has_derivative =
19.30 + bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
19.31 +
19.32 +lemmas inner_left_has_derivative =
19.33 + bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
19.34 +
19.35 +lemmas mult_right_has_derivative =
19.36 + bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
19.37 +
19.38 +lemmas mult_left_has_derivative =
19.39 + bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
19.40 +
19.41 +lemmas euclidean_component_has_derivative =
19.42 + bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
19.43 +
19.44 lemma has_derivative_neg:
19.45 assumes "(f has_derivative f') net"
19.46 shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
19.47 - using scaleR_right.has_derivative [where r="-1", OF assms] by auto
19.48 + using scaleR_right_has_derivative [where r="-1", OF assms] by auto
19.49
19.50 lemma has_derivative_add:
19.51 assumes "(f has_derivative f') net" and "(g has_derivative g') net"
19.52 @@ -181,9 +202,9 @@
19.53 has_derivative_id has_derivative_const
19.54 has_derivative_add has_derivative_sub has_derivative_neg
19.55 has_derivative_add_const
19.56 - scaleR_left.has_derivative scaleR_right.has_derivative
19.57 - inner_left.has_derivative inner_right.has_derivative
19.58 - euclidean_component.has_derivative
19.59 + scaleR_left_has_derivative scaleR_right_has_derivative
19.60 + inner_left_has_derivative inner_right_has_derivative
19.61 + euclidean_component_has_derivative
19.62
19.63 subsubsection {* Limit transformation for derivatives *}
19.64
19.65 @@ -459,7 +480,7 @@
19.66 "f differentiable net \<Longrightarrow>
19.67 (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
19.68 unfolding differentiable_def
19.69 - apply(erule exE, drule scaleR_right.has_derivative) by auto
19.70 + apply(erule exE, drule scaleR_right_has_derivative) by auto
19.71
19.72 lemma differentiable_neg [intro]:
19.73 "f differentiable net \<Longrightarrow>
19.74 @@ -693,7 +714,7 @@
19.75 show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
19.76 using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
19.77 unfolding mult_minus_left
19.78 - unfolding abs_mult diff_minus_eq_add scaleR.minus_left
19.79 + unfolding abs_mult diff_minus_eq_add scaleR_minus_left
19.80 unfolding algebra_simps by (auto intro: mult_pos_pos)
19.81 qed
19.82
19.83 @@ -769,7 +790,7 @@
19.84 fix x assume x:"x \<in> {a<..<b}"
19.85 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)"
19.86 by (intro has_derivative_intros assms(3)[rule_format,OF x]
19.87 - mult_right.has_derivative)
19.88 + mult_right_has_derivative)
19.89 qed(insert assms(1), auto simp add:field_simps)
19.90 then guess x ..
19.91 thus ?thesis apply(rule_tac x=x in bexI)
19.92 @@ -1740,7 +1761,7 @@
19.93 lemma has_vector_derivative_cmul:
19.94 "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
19.95 unfolding has_vector_derivative_def
19.96 - apply (drule scaleR_right.has_derivative)
19.97 + apply (drule scaleR_right_has_derivative)
19.98 by (auto simp add: algebra_simps)
19.99
19.100 lemma has_vector_derivative_cmul_eq:
19.101 @@ -1819,7 +1840,7 @@
19.102 shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
19.103 using assms(2) unfolding has_vector_derivative_def apply-
19.104 apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
19.105 - unfolding o_def scaleR.scaleR_left by auto
19.106 + unfolding o_def real_scaleR_def scaleR_scaleR .
19.107
19.108 lemma vector_diff_chain_within:
19.109 assumes "(f has_vector_derivative f') (at x within s)"
19.110 @@ -1827,6 +1848,6 @@
19.111 shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
19.112 using assms(2) unfolding has_vector_derivative_def apply-
19.113 apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
19.114 - unfolding o_def scaleR.scaleR_left by auto
19.115 + unfolding o_def real_scaleR_def scaleR_scaleR .
19.116
19.117 end
20.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
20.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
20.3 @@ -118,20 +118,38 @@
20.4 lemma bounded_linear_euclidean_component:
20.5 "bounded_linear (\<lambda>x. euclidean_component x i)"
20.6 unfolding euclidean_component_def
20.7 - by (rule inner.bounded_linear_right)
20.8 + by (rule bounded_linear_inner_right)
20.9
20.10 -interpretation euclidean_component:
20.11 - bounded_linear "\<lambda>x. euclidean_component x i"
20.12 - by (rule bounded_linear_euclidean_component)
20.13 +lemmas tendsto_euclidean_component [tendsto_intros] =
20.14 + bounded_linear.tendsto [OF bounded_linear_euclidean_component]
20.15
20.16 -declare euclidean_component.isCont [simp]
20.17 +lemmas isCont_euclidean_component [simp] =
20.18 + bounded_linear.isCont [OF bounded_linear_euclidean_component]
20.19 +
20.20 +lemma euclidean_component_zero: "0 $$ i = 0"
20.21 + unfolding euclidean_component_def by (rule inner_zero_right)
20.22 +
20.23 +lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
20.24 + unfolding euclidean_component_def by (rule inner_add_right)
20.25 +
20.26 +lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
20.27 + unfolding euclidean_component_def by (rule inner_diff_right)
20.28 +
20.29 +lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
20.30 + unfolding euclidean_component_def by (rule inner_minus_right)
20.31 +
20.32 +lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
20.33 + unfolding euclidean_component_def by (rule inner_scaleR_right)
20.34 +
20.35 +lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
20.36 + unfolding euclidean_component_def by (rule inner_setsum_right)
20.37
20.38 lemma euclidean_eqI:
20.39 fixes x y :: "'a::euclidean_space"
20.40 assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
20.41 proof -
20.42 from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
20.43 - by (simp add: euclidean_component.diff)
20.44 + by (simp add: euclidean_component_diff)
20.45 then show "x = y"
20.46 unfolding euclidean_component_def euclidean_all_zero by simp
20.47 qed
20.48 @@ -153,23 +171,19 @@
20.49 assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
20.50 unfolding euclidean_component_def basis_zero[OF assms] by simp
20.51
20.52 -lemma euclidean_scaleR:
20.53 - shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
20.54 - unfolding euclidean_component_def by auto
20.55 -
20.56 lemmas euclidean_simps =
20.57 - euclidean_component.add
20.58 - euclidean_component.diff
20.59 - euclidean_scaleR
20.60 - euclidean_component.minus
20.61 - euclidean_component.setsum
20.62 + euclidean_component_add
20.63 + euclidean_component_diff
20.64 + euclidean_component_scaleR
20.65 + euclidean_component_minus
20.66 + euclidean_component_setsum
20.67 basis_component
20.68
20.69 lemma euclidean_representation:
20.70 fixes x :: "'a::euclidean_space"
20.71 shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
20.72 apply (rule euclidean_eqI)
20.73 - apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
20.74 + apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
20.75 apply (simp add: if_distrib setsum_delta cong: if_cong)
20.76 done
20.77
20.78 @@ -180,7 +194,7 @@
20.79
20.80 lemma euclidean_lambda_beta [simp]:
20.81 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
20.82 - by (auto simp: euclidean_component.setsum euclidean_component.scaleR
20.83 + by (auto simp: euclidean_component_setsum euclidean_component_scaleR
20.84 Chi_def if_distrib setsum_cases intro!: setsum_cong)
20.85
20.86 lemma euclidean_lambda_beta':
20.87 @@ -201,7 +215,7 @@
20.88 lemma euclidean_inner:
20.89 "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
20.90 by (subst (1 2) euclidean_representation,
20.91 - simp add: inner_left.setsum inner_right.setsum
20.92 + simp add: inner_setsum_left inner_setsum_right
20.93 dot_basis if_distrib setsum_cases mult_commute)
20.94
20.95 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
21.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 18:07:40 2011 +0200
21.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 23:43:22 2011 +0200
21.3 @@ -66,7 +66,7 @@
21.4 apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
21.5 have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
21.6 thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
21.7 - unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
21.8 + unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
21.9 unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
21.10 note lem3 = this[rule_format]
21.11 have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
22.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 18:07:40 2011 +0200
22.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 23:43:22 2011 +0200
22.3 @@ -401,14 +401,15 @@
22.4 unfolding norm_vec_def
22.5 by (rule member_le_setL2) simp_all
22.6
22.7 -interpretation vec_nth: bounded_linear "\<lambda>x. x $ i"
22.8 +lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
22.9 apply default
22.10 apply (rule vector_add_component)
22.11 apply (rule vector_scaleR_component)
22.12 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
22.13 done
22.14
22.15 -declare vec_nth.isCont [simp]
22.16 +lemmas isCont_vec_nth [simp] =
22.17 + bounded_linear.isCont [OF bounded_linear_vec_nth]
22.18
22.19 instance vec :: (banach, finite) banach ..
22.20
23.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 18:07:40 2011 +0200
23.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 23:43:22 2011 +0200
23.3 @@ -16,7 +16,7 @@
23.4
23.5 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
23.6 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
23.7 - scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
23.8 + scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
23.9
23.10 lemma real_arch_invD:
23.11 "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
23.12 @@ -1225,7 +1225,7 @@
23.13 lemma has_integral_cmul:
23.14 shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
23.15 unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
23.16 - by(rule scaleR.bounded_linear_right)
23.17 + by(rule bounded_linear_scaleR_right)
23.18
23.19 lemma has_integral_neg:
23.20 shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
23.21 @@ -2262,7 +2262,7 @@
23.22 assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
23.23 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})"
23.24 apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
23.25 - unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto
23.26 + unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
23.27
23.28 lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
23.29 assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
23.30 @@ -2287,7 +2287,7 @@
23.31 lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
23.32 assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. (f x)$$i \<le> (g x)$$i"
23.33 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"
23.34 - unfolding euclidean_component.setsum apply(rule setsum_mono) apply safe
23.35 + unfolding euclidean_component_setsum apply(rule setsum_mono) apply safe
23.36 proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
23.37 from this(3) guess u v apply-by(erule exE)+ note b=this
23.38 show "(content b *\<^sub>R f a) $$ i \<le> (content b *\<^sub>R g a) $$ i" unfolding b
23.39 @@ -2988,7 +2988,7 @@
23.40 have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
23.41 norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
23.42 apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
23.43 - unfolding scaleR.diff_left by(auto simp add:algebra_simps)
23.44 + unfolding scaleR_diff_left by(auto simp add:algebra_simps)
23.45 also have "... \<le> e * norm (u - x) + e * norm (v - x)"
23.46 apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
23.47 apply(rule d(2)[of "x" "v",unfolded o_def])
23.48 @@ -3123,7 +3123,7 @@
23.49 assumes "continuous_on {a..b} f" "x \<in> {a..b}"
23.50 shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
23.51 unfolding has_vector_derivative_def has_derivative_within_alt
23.52 -apply safe apply(rule scaleR.bounded_linear_left)
23.53 +apply safe apply(rule bounded_linear_scaleR_left)
23.54 proof- fix e::real assume e:"e>0"
23.55 note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
23.56 from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
23.57 @@ -3223,8 +3223,8 @@
23.58 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
23.59 unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
23.60 apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
23.61 - 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]
23.62 - unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" .
23.63 + 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
23.64 + using assms(1) by auto finally have *:"?l = ?r" .
23.65 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
23.66 using assms(1) by(auto simp add:field_simps) qed qed qed
23.67
23.68 @@ -3256,7 +3256,7 @@
23.69 lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
23.70 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})"
23.71 apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a]
23.72 - unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym]
23.73 + unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR
23.74 defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
23.75 apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
23.76
23.77 @@ -3442,7 +3442,7 @@
23.78 show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[THEN sym] split_minus
23.79 unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
23.80 proof(rule norm_triangle_le,rule **)
23.81 - case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum)
23.82 + case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
23.83 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"
23.84 "e * (interval_upperbound k - interval_lowerbound k) / 2
23.85 < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
23.86 @@ -4159,7 +4159,7 @@
23.87 "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
23.88 "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
23.89 unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
23.90 - apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
23.91 + apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym]
23.92 apply(rule_tac[!] mult_nonneg_nonneg)
23.93 proof- fix a b assume ab:"(a,b) \<in> p1"
23.94 show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
23.95 @@ -4535,7 +4535,7 @@
23.96 show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
23.97 unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum)
23.98 apply(rule setsum_mono) unfolding split_paired_all split_conv
23.99 - unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
23.100 + unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym]
23.101 unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
23.102 proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
23.103 from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
23.104 @@ -5202,7 +5202,7 @@
23.105 proof- have *:"\<And>x. ((\<chi>\<chi> i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\<lambda>i.
23.106 (((\<lambda>y. (\<chi>\<chi> j. if j = i then y else 0)) o
23.107 (((\<lambda>x. (norm((\<chi>\<chi> j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..<DIM('c)})"
23.108 - unfolding euclidean_eq[where 'a='c] euclidean_component.setsum apply safe
23.109 + unfolding euclidean_eq[where 'a='c] euclidean_component_setsum apply safe
23.110 unfolding euclidean_lambda_beta'
23.111 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)) =
23.112 (if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto
23.113 @@ -5220,7 +5220,7 @@
23.114 apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm)
23.115 apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
23.116 apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c]
23.117 - by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def])
23.118 + by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def])
23.119 qed
23.120
23.121 lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
23.122 @@ -5266,7 +5266,7 @@
23.123 proof- fix k and i assume "k\<in>d" and i:"i<DIM('m)"
23.124 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
23.125 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)
23.126 - unfolding euclidean_component.minus[THEN sym] defer apply(subst integral_neg[THEN sym])
23.127 + unfolding euclidean_component_minus[THEN sym] defer apply(subst integral_neg[THEN sym])
23.128 defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
23.129 using integrable_on_subinterval[OF assms(1),of a b]
23.130 integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
23.131 @@ -5276,7 +5276,7 @@
23.132 using integrable_on_subdivision[OF d assms(2)] by auto
23.133 have "(\<Sum>i\<in>d. integral i (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j)
23.134 = integral (\<Union>d) (\<lambda>x. (\<chi>\<chi> j. abs(f x$$j)) ::'m::ordered_euclidean_space) $$ j"
23.135 - unfolding euclidean_component.setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
23.136 + unfolding euclidean_component_setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
23.137 also have "... \<le> integral UNIV (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j"
23.138 apply(rule integral_subset_component_le) using assms * by auto
23.139 finally show ?case .
24.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 18:07:40 2011 +0200
24.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 23:43:22 2011 +0200
24.3 @@ -198,8 +198,8 @@
24.4
24.5 text{* Dot product in terms of the norm rather than conversely. *}
24.6
24.7 -lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left
24.8 -inner.scaleR_left inner.scaleR_right
24.9 +lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
24.10 +inner_scaleR_left inner_scaleR_right
24.11
24.12 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
24.13 unfolding power2_norm_eq_inner inner_simps inner_commute by auto
24.14 @@ -1558,7 +1558,7 @@
24.15 unfolding independent_eq_inj_on [OF basis_inj]
24.16 apply clarify
24.17 apply (drule_tac f="inner (basis a)" in arg_cong)
24.18 - apply (simp add: inner_right.setsum dot_basis)
24.19 + apply (simp add: inner_setsum_right dot_basis)
24.20 done
24.21
24.22 lemma dimensionI:
24.23 @@ -1663,10 +1663,10 @@
24.24 have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
24.25 have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
24.26 using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP]
24.27 - unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
24.28 + unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
24.29 have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
24.30 using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i] fPs[OF PnP]
24.31 - unfolding euclidean_component.setsum euclidean_component.minus
24.32 + unfolding euclidean_component_setsum euclidean_component_minus
24.33 by(auto simp add: setsum_negf intro: abs_le_D1)
24.34 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"
24.35 apply (subst thp)
24.36 @@ -1756,7 +1756,7 @@
24.37 have Kp: "?K > 0" by arith
24.38 { assume C: "B < 0"
24.39 have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
24.40 - by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
24.41 + by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
24.42 hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
24.43 with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
24.44 by (simp add: mult_less_0_iff)
24.45 @@ -2829,7 +2829,7 @@
24.46 unfolding infnorm_def
24.47 unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
24.48 unfolding infnorm_set_image ball_simps
24.49 - apply(subst (1) euclidean_eq) unfolding euclidean_component.zero
24.50 + apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
24.51 by auto
24.52 then show ?thesis using infnorm_pos_le[of x] by simp
24.53 qed
24.54 @@ -2881,7 +2881,7 @@
24.55 lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
24.56 apply (subst infnorm_def)
24.57 unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
24.58 - unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult
24.59 + unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult
24.60 using component_le_infnorm[of x] by(auto intro: mult_mono)
24.61
24.62 lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
25.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 18:07:40 2011 +0200
25.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
25.3 @@ -14,7 +14,7 @@
25.4
25.5 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
25.6 unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
25.7 - apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
25.8 + apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
25.9
25.10 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
25.11 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
25.12 @@ -1912,7 +1912,7 @@
25.13 fixes S :: "'a::real_normed_vector set"
25.14 shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
25.15 apply (rule bounded_linear_image, assumption)
25.16 - apply (rule scaleR.bounded_linear_right)
25.17 + apply (rule bounded_linear_scaleR_right)
25.18 done
25.19
25.20 lemma bounded_translation:
25.21 @@ -3537,7 +3537,7 @@
25.22 proof-
25.23 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
25.24 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
25.25 - using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
25.26 + using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
25.27 unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
25.28 }
25.29 thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
25.30 @@ -4365,7 +4365,7 @@
25.31 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
25.32 proof-
25.33 let ?f = "\<lambda>x. scaleR c x"
25.34 - have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
25.35 + have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
25.36 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
25.37 using linear_continuous_at[OF *] assms by auto
25.38 qed
25.39 @@ -4951,7 +4951,7 @@
25.40 unfolding Lim_sequentially by(auto simp add: dist_norm)
25.41 hence "(f ---> x) sequentially" unfolding f_def
25.42 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]
25.43 - 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 }
25.44 + 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 }
25.45 ultimately have "x \<in> closure {a<..<b}"
25.46 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto }
25.47 thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
25.48 @@ -5571,7 +5571,7 @@
25.49 subsection {* Some properties of a canonical subspace *}
25.50
25.51 (** move **)
25.52 -declare euclidean_component.zero[simp]
25.53 +declare euclidean_component_zero[simp]
25.54
25.55 lemma subspace_substandard:
25.56 "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
25.57 @@ -6027,15 +6027,15 @@
25.58
25.59 lemmas Lim_ident_at = LIM_ident
25.60 lemmas Lim_const = tendsto_const
25.61 -lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
25.62 +lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
25.63 lemmas Lim_neg = tendsto_minus
25.64 lemmas Lim_add = tendsto_add
25.65 lemmas Lim_sub = tendsto_diff
25.66 -lemmas Lim_mul = scaleR.tendsto
25.67 -lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
25.68 +lemmas Lim_mul = tendsto_scaleR
25.69 +lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
25.70 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
25.71 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
25.72 -lemmas Lim_component = euclidean_component.tendsto
25.73 +lemmas Lim_component = tendsto_euclidean_component
25.74 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
25.75
25.76 end
26.1 --- a/src/HOL/Nat.thy Thu Aug 18 18:07:40 2011 +0200
26.2 +++ b/src/HOL/Nat.thy Thu Aug 18 23:43:22 2011 +0200
26.3 @@ -39,11 +39,20 @@
26.4 Zero_RepI: "Nat Zero_Rep"
26.5 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
26.6
26.7 -typedef (open Nat) nat = Nat
26.8 - by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
26.9 +typedef (open Nat) nat = "{n. Nat n}"
26.10 + using Nat.Zero_RepI by auto
26.11
26.12 -definition Suc :: "nat => nat" where
26.13 - "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
26.14 +lemma Nat_Rep_Nat:
26.15 + "Nat (Rep_Nat n)"
26.16 + using Rep_Nat by simp
26.17 +
26.18 +lemma Nat_Abs_Nat_inverse:
26.19 + "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
26.20 + using Abs_Nat_inverse by simp
26.21 +
26.22 +lemma Nat_Abs_Nat_inject:
26.23 + "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
26.24 + using Abs_Nat_inject by simp
26.25
26.26 instantiation nat :: zero
26.27 begin
26.28 @@ -55,9 +64,11 @@
26.29
26.30 end
26.31
26.32 +definition Suc :: "nat \<Rightarrow> nat" where
26.33 + "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
26.34 +
26.35 lemma Suc_not_Zero: "Suc m \<noteq> 0"
26.36 - by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
26.37 - Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
26.38 + by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
26.39
26.40 lemma Zero_not_Suc: "0 \<noteq> Suc m"
26.41 by (rule not_sym, rule Suc_not_Zero not_sym)
26.42 @@ -67,12 +78,12 @@
26.43
26.44 rep_datatype "0 \<Colon> nat" Suc
26.45 apply (unfold Zero_nat_def Suc_def)
26.46 - apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
26.47 - apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
26.48 - apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
26.49 - apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
26.50 - Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
26.51 - Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
26.52 + apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
26.53 + apply (erule Nat_Rep_Nat [THEN Nat.induct])
26.54 + apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
26.55 + apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
26.56 + Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
26.57 + Suc_Rep_not_Zero_Rep [symmetric]
26.58 Suc_Rep_inject' Rep_Nat_inject)
26.59 done
26.60
27.1 --- a/src/HOL/Nitpick.thy Thu Aug 18 18:07:40 2011 +0200
27.2 +++ b/src/HOL/Nitpick.thy Thu Aug 18 23:43:22 2011 +0200
27.3 @@ -76,19 +76,19 @@
27.4 definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
27.5 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
27.6
27.7 -definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
27.8 +definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
27.9 "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
27.10
27.11 -definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
27.12 +definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
27.13 "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
27.14
27.15 -definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
27.16 +definition card' :: "'a set \<Rightarrow> nat" where
27.17 "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
27.18
27.19 -definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
27.20 +definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
27.21 "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
27.22
27.23 -inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
27.24 +inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
27.25 "fold_graph' f z {} z" |
27.26 "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
27.27
28.1 --- a/src/HOL/Probability/Borel_Space.thy Thu Aug 18 18:07:40 2011 +0200
28.2 +++ b/src/HOL/Probability/Borel_Space.thy Thu Aug 18 23:43:22 2011 +0200
28.3 @@ -816,7 +816,7 @@
28.4 proof cases
28.5 assume "b \<noteq> 0"
28.6 with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
28.7 - by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
28.8 + by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
28.9 hence "?S \<in> sets borel"
28.10 unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
28.11 moreover
29.1 --- a/src/HOL/Probability/Independent_Family.thy Thu Aug 18 18:07:40 2011 +0200
29.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu Aug 18 23:43:22 2011 +0200
29.3 @@ -563,7 +563,7 @@
29.4 with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
29.5 by simp
29.6 moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
29.7 - by (intro mult_right.sums finite_measure_UNION F dis)
29.8 + by (intro sums_mult finite_measure_UNION F dis)
29.9 ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
29.10 by (auto dest!: sums_unique)
29.11 with F show "(\<Union>i. F i) \<in> sets ?D"
30.1 --- a/src/HOL/RealDef.thy Thu Aug 18 18:07:40 2011 +0200
30.2 +++ b/src/HOL/RealDef.thy Thu Aug 18 23:43:22 2011 +0200
30.3 @@ -121,7 +121,7 @@
30.4 subsection {* Cauchy sequences *}
30.5
30.6 definition
30.7 - cauchy :: "(nat \<Rightarrow> rat) set"
30.8 + cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
30.9 where
30.10 "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
30.11
31.1 --- a/src/HOL/RealVector.thy Thu Aug 18 18:07:40 2011 +0200
31.2 +++ b/src/HOL/RealVector.thy Thu Aug 18 23:43:22 2011 +0200
31.3 @@ -62,24 +62,28 @@
31.4 and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
31.5 and scale_left_diff_distrib [algebra_simps]:
31.6 "scale (a - b) x = scale a x - scale b x"
31.7 + and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)"
31.8 proof -
31.9 interpret s: additive "\<lambda>a. scale a x"
31.10 proof qed (rule scale_left_distrib)
31.11 show "scale 0 x = 0" by (rule s.zero)
31.12 show "scale (- a) x = - (scale a x)" by (rule s.minus)
31.13 show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
31.14 + show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum)
31.15 qed
31.16
31.17 lemma scale_zero_right [simp]: "scale a 0 = 0"
31.18 and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
31.19 and scale_right_diff_distrib [algebra_simps]:
31.20 "scale a (x - y) = scale a x - scale a y"
31.21 + and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))"
31.22 proof -
31.23 interpret s: additive "\<lambda>x. scale a x"
31.24 proof qed (rule scale_right_distrib)
31.25 show "scale a 0 = 0" by (rule s.zero)
31.26 show "scale a (- x) = - (scale a x)" by (rule s.minus)
31.27 show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
31.28 + show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum)
31.29 qed
31.30
31.31 lemma scale_eq_0_iff [simp]:
31.32 @@ -140,16 +144,16 @@
31.33 end
31.34
31.35 class real_vector = scaleR + ab_group_add +
31.36 - assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
31.37 - and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
31.38 + assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y"
31.39 + and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x"
31.40 and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
31.41 and scaleR_one: "scaleR 1 x = x"
31.42
31.43 interpretation real_vector:
31.44 vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
31.45 apply unfold_locales
31.46 -apply (rule scaleR_right_distrib)
31.47 -apply (rule scaleR_left_distrib)
31.48 +apply (rule scaleR_add_right)
31.49 +apply (rule scaleR_add_left)
31.50 apply (rule scaleR_scaleR)
31.51 apply (rule scaleR_one)
31.52 done
31.53 @@ -159,16 +163,25 @@
31.54 lemmas scaleR_left_commute = real_vector.scale_left_commute
31.55 lemmas scaleR_zero_left = real_vector.scale_zero_left
31.56 lemmas scaleR_minus_left = real_vector.scale_minus_left
31.57 -lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
31.58 +lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
31.59 +lemmas scaleR_setsum_left = real_vector.scale_setsum_left
31.60 lemmas scaleR_zero_right = real_vector.scale_zero_right
31.61 lemmas scaleR_minus_right = real_vector.scale_minus_right
31.62 -lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
31.63 +lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
31.64 +lemmas scaleR_setsum_right = real_vector.scale_setsum_right
31.65 lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
31.66 lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
31.67 lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
31.68 lemmas scaleR_cancel_left = real_vector.scale_cancel_left
31.69 lemmas scaleR_cancel_right = real_vector.scale_cancel_right
31.70
31.71 +text {* Legacy names *}
31.72 +
31.73 +lemmas scaleR_left_distrib = scaleR_add_left
31.74 +lemmas scaleR_right_distrib = scaleR_add_right
31.75 +lemmas scaleR_left_diff_distrib = scaleR_diff_left
31.76 +lemmas scaleR_right_diff_distrib = scaleR_diff_right
31.77 +
31.78 lemma scaleR_minus1_left [simp]:
31.79 fixes x :: "'a::real_vector"
31.80 shows "scaleR (-1) x = - x"
31.81 @@ -1059,8 +1072,8 @@
31.82
31.83 end
31.84
31.85 -interpretation mult:
31.86 - bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
31.87 +lemma bounded_bilinear_mult:
31.88 + "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
31.89 apply (rule bounded_bilinear.intro)
31.90 apply (rule left_distrib)
31.91 apply (rule right_distrib)
31.92 @@ -1070,19 +1083,21 @@
31.93 apply (simp add: norm_mult_ineq)
31.94 done
31.95
31.96 -interpretation mult_left:
31.97 - bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
31.98 -by (rule mult.bounded_linear_left)
31.99 +lemma bounded_linear_mult_left:
31.100 + "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
31.101 + using bounded_bilinear_mult
31.102 + by (rule bounded_bilinear.bounded_linear_left)
31.103
31.104 -interpretation mult_right:
31.105 - bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
31.106 -by (rule mult.bounded_linear_right)
31.107 +lemma bounded_linear_mult_right:
31.108 + "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)"
31.109 + using bounded_bilinear_mult
31.110 + by (rule bounded_bilinear.bounded_linear_right)
31.111
31.112 -interpretation divide:
31.113 - bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
31.114 -unfolding divide_inverse by (rule mult.bounded_linear_left)
31.115 +lemma bounded_linear_divide:
31.116 + "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
31.117 + unfolding divide_inverse by (rule bounded_linear_mult_left)
31.118
31.119 -interpretation scaleR: bounded_bilinear "scaleR"
31.120 +lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
31.121 apply (rule bounded_bilinear.intro)
31.122 apply (rule scaleR_left_distrib)
31.123 apply (rule scaleR_right_distrib)
31.124 @@ -1091,14 +1106,16 @@
31.125 apply (rule_tac x="1" in exI, simp)
31.126 done
31.127
31.128 -interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
31.129 -by (rule scaleR.bounded_linear_left)
31.130 +lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
31.131 + using bounded_bilinear_scaleR
31.132 + by (rule bounded_bilinear.bounded_linear_left)
31.133
31.134 -interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
31.135 -by (rule scaleR.bounded_linear_right)
31.136 +lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)"
31.137 + using bounded_bilinear_scaleR
31.138 + by (rule bounded_bilinear.bounded_linear_right)
31.139
31.140 -interpretation of_real: bounded_linear "\<lambda>r. of_real r"
31.141 -unfolding of_real_def by (rule scaleR.bounded_linear_left)
31.142 +lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
31.143 + unfolding of_real_def by (rule bounded_linear_scaleR_left)
31.144
31.145 subsection{* Hausdorff and other separation properties *}
31.146
32.1 --- a/src/HOL/Relation.thy Thu Aug 18 18:07:40 2011 +0200
32.2 +++ b/src/HOL/Relation.thy Thu Aug 18 23:43:22 2011 +0200
32.3 @@ -133,9 +133,8 @@
32.4 by blast
32.5
32.6 lemma Id_on_def' [nitpick_unfold, code]:
32.7 - "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
32.8 -by (auto simp add: fun_eq_iff
32.9 - elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
32.10 + "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
32.11 +by auto
32.12
32.13 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
32.14 by blast
33.1 --- a/src/HOL/SEQ.thy Thu Aug 18 18:07:40 2011 +0200
33.2 +++ b/src/HOL/SEQ.thy Thu Aug 18 23:43:22 2011 +0200
33.3 @@ -377,7 +377,7 @@
33.4 lemma LIMSEQ_mult:
33.5 fixes a b :: "'a::real_normed_algebra"
33.6 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
33.7 -by (rule mult.tendsto)
33.8 + by (rule tendsto_mult)
33.9
33.10 lemma increasing_LIMSEQ:
33.11 fixes f :: "nat \<Rightarrow> real"
34.1 --- a/src/HOL/Series.thy Thu Aug 18 18:07:40 2011 +0200
34.2 +++ b/src/HOL/Series.thy Thu Aug 18 23:43:22 2011 +0200
34.3 @@ -211,50 +211,54 @@
34.4 "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
34.5 by (intro sums_unique sums summable_sums)
34.6
34.7 +lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
34.8 +lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
34.9 +lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
34.10 +
34.11 lemma sums_mult:
34.12 fixes c :: "'a::real_normed_algebra"
34.13 shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
34.14 -by (rule mult_right.sums)
34.15 + by (rule bounded_linear.sums [OF bounded_linear_mult_right])
34.16
34.17 lemma summable_mult:
34.18 fixes c :: "'a::real_normed_algebra"
34.19 shows "summable f \<Longrightarrow> summable (%n. c * f n)"
34.20 -by (rule mult_right.summable)
34.21 + by (rule bounded_linear.summable [OF bounded_linear_mult_right])
34.22
34.23 lemma suminf_mult:
34.24 fixes c :: "'a::real_normed_algebra"
34.25 shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
34.26 -by (rule mult_right.suminf [symmetric])
34.27 + by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
34.28
34.29 lemma sums_mult2:
34.30 fixes c :: "'a::real_normed_algebra"
34.31 shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
34.32 -by (rule mult_left.sums)
34.33 + by (rule bounded_linear.sums [OF bounded_linear_mult_left])
34.34
34.35 lemma summable_mult2:
34.36 fixes c :: "'a::real_normed_algebra"
34.37 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
34.38 -by (rule mult_left.summable)
34.39 + by (rule bounded_linear.summable [OF bounded_linear_mult_left])
34.40
34.41 lemma suminf_mult2:
34.42 fixes c :: "'a::real_normed_algebra"
34.43 shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
34.44 -by (rule mult_left.suminf)
34.45 + by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
34.46
34.47 lemma sums_divide:
34.48 fixes c :: "'a::real_normed_field"
34.49 shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
34.50 -by (rule divide.sums)
34.51 + by (rule bounded_linear.sums [OF bounded_linear_divide])
34.52
34.53 lemma summable_divide:
34.54 fixes c :: "'a::real_normed_field"
34.55 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
34.56 -by (rule divide.summable)
34.57 + by (rule bounded_linear.summable [OF bounded_linear_divide])
34.58
34.59 lemma suminf_divide:
34.60 fixes c :: "'a::real_normed_field"
34.61 shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
34.62 -by (rule divide.suminf [symmetric])
34.63 + by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
34.64
34.65 lemma sums_add:
34.66 fixes a b :: "'a::real_normed_field"
34.67 @@ -423,7 +427,7 @@
34.68 by auto
34.69 have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
34.70 by simp
34.71 - thus ?thesis using divide.sums [OF 2, of 2]
34.72 + thus ?thesis using sums_divide [OF 2, of 2]
34.73 by simp
34.74 qed
34.75
35.1 --- a/src/HOL/String.thy Thu Aug 18 18:07:40 2011 +0200
35.2 +++ b/src/HOL/String.thy Thu Aug 18 23:43:22 2011 +0200
35.3 @@ -155,7 +155,7 @@
35.4
35.5 subsection {* Strings as dedicated type *}
35.6
35.7 -typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
35.8 +typedef (open) literal = "UNIV :: string set"
35.9 morphisms explode STR ..
35.10
35.11 instantiation literal :: size
36.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 18:07:40 2011 +0200
36.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 23:43:22 2011 +0200
36.3 @@ -465,7 +465,7 @@
36.4
36.5 (* setup *)
36.6
36.7 -val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
36.8 +val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
36.9
36.10 val setup =
36.11 Code.datatype_interpretation ensure_partial_term_of
36.12 @@ -474,4 +474,4 @@
36.13 (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
36.14 #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
36.15
36.16 -end;
36.17 \ No newline at end of file
36.18 +end;
37.1 --- a/src/HOL/Transcendental.thy Thu Aug 18 18:07:40 2011 +0200
37.2 +++ b/src/HOL/Transcendental.thy Thu Aug 18 23:43:22 2011 +0200
37.3 @@ -971,7 +971,7 @@
37.4
37.5 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
37.6 unfolding exp_def
37.7 -apply (subst of_real.suminf)
37.8 +apply (subst suminf_of_real)
37.9 apply (rule summable_exp_generic)
37.10 apply (simp add: scaleR_conv_of_real)
37.11 done
38.1 --- a/src/HOL/ex/ROOT.ML Thu Aug 18 18:07:40 2011 +0200
38.2 +++ b/src/HOL/ex/ROOT.ML Thu Aug 18 23:43:22 2011 +0200
38.3 @@ -48,7 +48,7 @@
38.4 "Primrec",
38.5 "Tarski",
38.6 "Classical",
38.7 - "set",
38.8 + "Set_Theory",
38.9 "Meson_Test",
38.10 "Termination",
38.11 "Coherent",
39.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
39.2 +++ b/src/HOL/ex/Set_Theory.thy Thu Aug 18 23:43:22 2011 +0200
39.3 @@ -0,0 +1,227 @@
39.4 +(* Title: HOL/ex/Set_Theory.thy
39.5 + Author: Tobias Nipkow and Lawrence C Paulson
39.6 + Copyright 1991 University of Cambridge
39.7 +*)
39.8 +
39.9 +header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
39.10 +
39.11 +theory Set_Theory
39.12 +imports Main
39.13 +begin
39.14 +
39.15 +text{*
39.16 + These two are cited in Benzmueller and Kohlhase's system description
39.17 + of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
39.18 + prove.
39.19 +*}
39.20 +
39.21 +lemma "(X = Y \<union> Z) =
39.22 + (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
39.23 + by blast
39.24 +
39.25 +lemma "(X = Y \<inter> Z) =
39.26 + (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
39.27 + by blast
39.28 +
39.29 +text {*
39.30 + Trivial example of term synthesis: apparently hard for some provers!
39.31 +*}
39.32 +
39.33 +schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
39.34 + by blast
39.35 +
39.36 +
39.37 +subsection {* Examples for the @{text blast} paper *}
39.38 +
39.39 +lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
39.40 + -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
39.41 + by blast
39.42 +
39.43 +lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
39.44 + -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
39.45 + by blast
39.46 +
39.47 +lemma singleton_example_1:
39.48 + "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
39.49 + by blast
39.50 +
39.51 +lemma singleton_example_2:
39.52 + "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
39.53 + -- {*Variant of the problem above. *}
39.54 + by blast
39.55 +
39.56 +lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
39.57 + -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
39.58 + by metis
39.59 +
39.60 +
39.61 +subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
39.62 +
39.63 +lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
39.64 + -- {* Requires best-first search because it is undirectional. *}
39.65 + by best
39.66 +
39.67 +schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
39.68 + -- {*This form displays the diagonal term. *}
39.69 + by best
39.70 +
39.71 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
39.72 + -- {* This form exploits the set constructs. *}
39.73 + by (rule notI, erule rangeE, best)
39.74 +
39.75 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
39.76 + -- {* Or just this! *}
39.77 + by best
39.78 +
39.79 +
39.80 +subsection {* The Schröder-Berstein Theorem *}
39.81 +
39.82 +lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
39.83 + by blast
39.84 +
39.85 +lemma surj_if_then_else:
39.86 + "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
39.87 + by (simp add: surj_def) blast
39.88 +
39.89 +lemma bij_if_then_else:
39.90 + "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
39.91 + h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
39.92 + apply (unfold inj_on_def)
39.93 + apply (simp add: surj_if_then_else)
39.94 + apply (blast dest: disj_lemma sym)
39.95 + done
39.96 +
39.97 +lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
39.98 + apply (rule exI)
39.99 + apply (rule lfp_unfold)
39.100 + apply (rule monoI, blast)
39.101 + done
39.102 +
39.103 +theorem Schroeder_Bernstein:
39.104 + "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
39.105 + \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
39.106 + apply (rule decomposition [where f=f and g=g, THEN exE])
39.107 + apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
39.108 + --{*The term above can be synthesized by a sufficiently detailed proof.*}
39.109 + apply (rule bij_if_then_else)
39.110 + apply (rule_tac [4] refl)
39.111 + apply (rule_tac [2] inj_on_inv_into)
39.112 + apply (erule subset_inj_on [OF _ subset_UNIV])
39.113 + apply blast
39.114 + apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
39.115 + done
39.116 +
39.117 +
39.118 +subsection {* A simple party theorem *}
39.119 +
39.120 +text{* \emph{At any party there are two people who know the same
39.121 +number of people}. Provided the party consists of at least two people
39.122 +and the knows relation is symmetric. Knowing yourself does not count
39.123 +--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
39.124 +at TPHOLs 2007.) *}
39.125 +
39.126 +lemma equal_number_of_acquaintances:
39.127 +assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
39.128 +shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
39.129 +proof -
39.130 + let ?N = "%a. card(R `` {a} - {a})"
39.131 + let ?n = "card A"
39.132 + have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
39.133 + have 0: "R `` A <= A" using `sym R` `Domain R <= A`
39.134 + unfolding Domain_def sym_def by blast
39.135 + have h: "ALL a:A. R `` {a} <= A" using 0 by blast
39.136 + hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
39.137 + by(blast intro: finite_subset)
39.138 + have sub: "?N ` A <= {0..<?n}"
39.139 + proof -
39.140 + have "ALL a:A. R `` {a} - {a} < A" using h by blast
39.141 + thus ?thesis using psubset_card_mono[OF `finite A`] by auto
39.142 + qed
39.143 + show "~ inj_on ?N A" (is "~ ?I")
39.144 + proof
39.145 + assume ?I
39.146 + hence "?n = card(?N ` A)" by(rule card_image[symmetric])
39.147 + with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
39.148 + using subset_card_intvl_is_intvl[of _ 0] by(auto)
39.149 + have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
39.150 + then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
39.151 + by (auto simp del: 2)
39.152 + have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
39.153 + have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
39.154 + hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
39.155 + hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
39.156 + hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
39.157 + have 4: "finite (A - {a,b})" using `finite A` by simp
39.158 + have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
39.159 + then show False using Nb `card A \<ge> 2` by arith
39.160 + qed
39.161 +qed
39.162 +
39.163 +text {*
39.164 + From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
39.165 + 293-314.
39.166 +
39.167 + Isabelle can prove the easy examples without any special mechanisms,
39.168 + but it can't prove the hard ones.
39.169 +*}
39.170 +
39.171 +lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
39.172 + -- {* Example 1, page 295. *}
39.173 + by force
39.174 +
39.175 +lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
39.176 + -- {* Example 2. *}
39.177 + by force
39.178 +
39.179 +lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
39.180 + -- {* Example 3. *}
39.181 + by force
39.182 +
39.183 +lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
39.184 + -- {* Example 4. *}
39.185 + by force
39.186 +
39.187 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
39.188 + -- {*Example 5, page 298. *}
39.189 + by force
39.190 +
39.191 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
39.192 + -- {* Example 6. *}
39.193 + by force
39.194 +
39.195 +lemma "\<exists>A. a \<notin> A"
39.196 + -- {* Example 7. *}
39.197 + by force
39.198 +
39.199 +lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
39.200 + \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
39.201 + -- {* Example 8 now needs a small hint. *}
39.202 + by (simp add: abs_if, force)
39.203 + -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
39.204 +
39.205 +text {* Example 9 omitted (requires the reals). *}
39.206 +
39.207 +text {* The paper has no Example 10! *}
39.208 +
39.209 +lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
39.210 + P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
39.211 + -- {* Example 11: needs a hint. *}
39.212 +by(metis nat.induct)
39.213 +
39.214 +lemma
39.215 + "(\<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)
39.216 + \<and> P n \<longrightarrow> P m"
39.217 + -- {* Example 12. *}
39.218 + by auto
39.219 +
39.220 +lemma
39.221 + "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
39.222 + (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
39.223 + -- {* Example EO1: typo in article, and with the obvious fix it seems
39.224 + to require arithmetic reasoning. *}
39.225 + apply clarify
39.226 + apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
39.227 + apply metis+
39.228 + done
39.229 +
39.230 +end
40.1 --- a/src/HOL/ex/set.thy Thu Aug 18 18:07:40 2011 +0200
40.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
40.3 @@ -1,225 +0,0 @@
40.4 -(* Title: HOL/ex/set.thy
40.5 - Author: Tobias Nipkow and Lawrence C Paulson
40.6 - Copyright 1991 University of Cambridge
40.7 -*)
40.8 -
40.9 -header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
40.10 -
40.11 -theory set imports Main begin
40.12 -
40.13 -text{*
40.14 - These two are cited in Benzmueller and Kohlhase's system description
40.15 - of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
40.16 - prove.
40.17 -*}
40.18 -
40.19 -lemma "(X = Y \<union> Z) =
40.20 - (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
40.21 - by blast
40.22 -
40.23 -lemma "(X = Y \<inter> Z) =
40.24 - (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
40.25 - by blast
40.26 -
40.27 -text {*
40.28 - Trivial example of term synthesis: apparently hard for some provers!
40.29 -*}
40.30 -
40.31 -schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
40.32 - by blast
40.33 -
40.34 -
40.35 -subsection {* Examples for the @{text blast} paper *}
40.36 -
40.37 -lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
40.38 - -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
40.39 - by blast
40.40 -
40.41 -lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
40.42 - -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
40.43 - by blast
40.44 -
40.45 -lemma singleton_example_1:
40.46 - "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
40.47 - by blast
40.48 -
40.49 -lemma singleton_example_2:
40.50 - "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
40.51 - -- {*Variant of the problem above. *}
40.52 - by blast
40.53 -
40.54 -lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
40.55 - -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
40.56 - by metis
40.57 -
40.58 -
40.59 -subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
40.60 -
40.61 -lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
40.62 - -- {* Requires best-first search because it is undirectional. *}
40.63 - by best
40.64 -
40.65 -schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
40.66 - -- {*This form displays the diagonal term. *}
40.67 - by best
40.68 -
40.69 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
40.70 - -- {* This form exploits the set constructs. *}
40.71 - by (rule notI, erule rangeE, best)
40.72 -
40.73 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
40.74 - -- {* Or just this! *}
40.75 - by best
40.76 -
40.77 -
40.78 -subsection {* The Schröder-Berstein Theorem *}
40.79 -
40.80 -lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
40.81 - by blast
40.82 -
40.83 -lemma surj_if_then_else:
40.84 - "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
40.85 - by (simp add: surj_def) blast
40.86 -
40.87 -lemma bij_if_then_else:
40.88 - "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
40.89 - h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
40.90 - apply (unfold inj_on_def)
40.91 - apply (simp add: surj_if_then_else)
40.92 - apply (blast dest: disj_lemma sym)
40.93 - done
40.94 -
40.95 -lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
40.96 - apply (rule exI)
40.97 - apply (rule lfp_unfold)
40.98 - apply (rule monoI, blast)
40.99 - done
40.100 -
40.101 -theorem Schroeder_Bernstein:
40.102 - "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
40.103 - \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
40.104 - apply (rule decomposition [where f=f and g=g, THEN exE])
40.105 - apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
40.106 - --{*The term above can be synthesized by a sufficiently detailed proof.*}
40.107 - apply (rule bij_if_then_else)
40.108 - apply (rule_tac [4] refl)
40.109 - apply (rule_tac [2] inj_on_inv_into)
40.110 - apply (erule subset_inj_on [OF _ subset_UNIV])
40.111 - apply blast
40.112 - apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
40.113 - done
40.114 -
40.115 -
40.116 -subsection {* A simple party theorem *}
40.117 -
40.118 -text{* \emph{At any party there are two people who know the same
40.119 -number of people}. Provided the party consists of at least two people
40.120 -and the knows relation is symmetric. Knowing yourself does not count
40.121 ---- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
40.122 -at TPHOLs 2007.) *}
40.123 -
40.124 -lemma equal_number_of_acquaintances:
40.125 -assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
40.126 -shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
40.127 -proof -
40.128 - let ?N = "%a. card(R `` {a} - {a})"
40.129 - let ?n = "card A"
40.130 - have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
40.131 - have 0: "R `` A <= A" using `sym R` `Domain R <= A`
40.132 - unfolding Domain_def sym_def by blast
40.133 - have h: "ALL a:A. R `` {a} <= A" using 0 by blast
40.134 - hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
40.135 - by(blast intro: finite_subset)
40.136 - have sub: "?N ` A <= {0..<?n}"
40.137 - proof -
40.138 - have "ALL a:A. R `` {a} - {a} < A" using h by blast
40.139 - thus ?thesis using psubset_card_mono[OF `finite A`] by auto
40.140 - qed
40.141 - show "~ inj_on ?N A" (is "~ ?I")
40.142 - proof
40.143 - assume ?I
40.144 - hence "?n = card(?N ` A)" by(rule card_image[symmetric])
40.145 - with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
40.146 - using subset_card_intvl_is_intvl[of _ 0] by(auto)
40.147 - have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
40.148 - then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
40.149 - by (auto simp del: 2)
40.150 - have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
40.151 - have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
40.152 - hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
40.153 - hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
40.154 - hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
40.155 - have 4: "finite (A - {a,b})" using `finite A` by simp
40.156 - have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
40.157 - then show False using Nb `card A \<ge> 2` by arith
40.158 - qed
40.159 -qed
40.160 -
40.161 -text {*
40.162 - From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
40.163 - 293-314.
40.164 -
40.165 - Isabelle can prove the easy examples without any special mechanisms,
40.166 - but it can't prove the hard ones.
40.167 -*}
40.168 -
40.169 -lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
40.170 - -- {* Example 1, page 295. *}
40.171 - by force
40.172 -
40.173 -lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
40.174 - -- {* Example 2. *}
40.175 - by force
40.176 -
40.177 -lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
40.178 - -- {* Example 3. *}
40.179 - by force
40.180 -
40.181 -lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
40.182 - -- {* Example 4. *}
40.183 - by force
40.184 -
40.185 -lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
40.186 - -- {*Example 5, page 298. *}
40.187 - by force
40.188 -
40.189 -lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
40.190 - -- {* Example 6. *}
40.191 - by force
40.192 -
40.193 -lemma "\<exists>A. a \<notin> A"
40.194 - -- {* Example 7. *}
40.195 - by force
40.196 -
40.197 -lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
40.198 - \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
40.199 - -- {* Example 8 now needs a small hint. *}
40.200 - by (simp add: abs_if, force)
40.201 - -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
40.202 -
40.203 -text {* Example 9 omitted (requires the reals). *}
40.204 -
40.205 -text {* The paper has no Example 10! *}
40.206 -
40.207 -lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
40.208 - P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
40.209 - -- {* Example 11: needs a hint. *}
40.210 -by(metis nat.induct)
40.211 -
40.212 -lemma
40.213 - "(\<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)
40.214 - \<and> P n \<longrightarrow> P m"
40.215 - -- {* Example 12. *}
40.216 - by auto
40.217 -
40.218 -lemma
40.219 - "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
40.220 - (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
40.221 - -- {* Example EO1: typo in article, and with the obvious fix it seems
40.222 - to require arithmetic reasoning. *}
40.223 - apply clarify
40.224 - apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
40.225 - apply metis+
40.226 - done
40.227 -
40.228 -end