--- a/NEWS Fri Aug 26 22:25:41 2011 +0200
+++ b/NEWS Fri Aug 26 23:14:36 2011 +0200
@@ -200,6 +200,38 @@
tendsto_vector ~> vec_tendstoI
Cauchy_vector ~> vec_CauchyI
+* Session Multivariate_Analysis: Several duplicate theorems have been
+removed, and other theorems have been renamed. INCOMPATIBILITY.
+
+ eventually_conjI ~> eventually_conj
+ eventually_and ~> eventually_conj_iff
+ eventually_false ~> eventually_False
+ Lim_ident_at ~> LIM_ident
+ Lim_const ~> tendsto_const
+ Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
+ Lim_neg ~> tendsto_minus
+ Lim_add ~> tendsto_add
+ Lim_sub ~> tendsto_diff
+ Lim_mul ~> tendsto_scaleR
+ Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
+ Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
+ Lim_linear ~> bounded_linear.tendsto
+ Lim_component ~> tendsto_euclidean_component
+ Lim_component_cart ~> tendsto_vec_nth
+ Lim_inner ~> tendsto_inner [OF tendsto_const]
+ dot_lsum ~> inner_setsum_left
+ dot_rsum ~> inner_setsum_right
+ continuous_on_neg ~> continuous_on_minus
+ continuous_on_sub ~> continuous_on_diff
+ continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
+ continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
+ continuous_on_mul ~> continuous_on_scaleR
+ continuous_on_mul_real ~> continuous_on_mult
+ continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
+ subset_interior ~> interior_mono
+ subset_closure ~> closure_mono
+ closure_univ ~> closure_UNIV
+
* Complex_Main: The locale interpretations for the bounded_linear and
bounded_bilinear locales have been removed, in order to reduce the
number of duplicate lemmas. Users must use the original names for
@@ -213,6 +245,16 @@
mult_right.setsum ~> setsum_right_distrib
mult_left.diff ~> left_diff_distrib
+* Complex_Main: Several redundant theorems about real numbers have
+been removed or generalized and renamed. INCOMPATIBILITY.
+
+ real_0_le_divide_iff ~> zero_le_divide_iff
+ realpow_two_disj ~> power2_eq_iff
+ real_squared_diff_one_factored ~> square_diff_one_factored
+ realpow_two_diff ~> square_diff_square_factored
+ exp_ln_eq ~> ln_unique
+ lemma_DERIV_subst ~> DERIV_cong
+
*** Document preparation ***
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 26 22:25:41 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 26 23:14:36 2011 +0200
@@ -896,7 +896,7 @@
arguments, to resolve overloading.
\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
+tagged with its type using a function $\mathit{type\/}(\tau, t)$.
\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
Like for \textit{poly\_guards} constants are annotated with their types to
@@ -905,8 +905,8 @@
\item[$\bullet$]
\textbf{%
-\textit{mono\_guards}, \textit{mono\_tags} (sound);
-\textit{mono\_args} (unsound):} \\
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
+\textit{raw\_mono\_args} (unsound):} \\
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
respectively, but the problem is additionally monomorphized, meaning that type
variables are instantiated with heuristically chosen ground types.
@@ -915,33 +915,34 @@
\item[$\bullet$]
\textbf{%
-\textit{mangled\_guards},
-\textit{mangled\_tags} (sound); \\
-\textit{mangled\_args} (unsound):} \\
+\textit{mono\_guards}, \textit{mono\_tags} (sound);
+\textit{mono\_args} (unsound):} \\
Similar to
-\textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_args},
-respectively but types are mangled in constant names instead of being supplied
-as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
-becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
-$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
-$\mathit{type\_info\_}\tau(t)$.
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
+\textit{raw\_mono\_args}, respectively but types are mangled in constant names
+instead of being supplied as ground term arguments. The binary predicate
+$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
+$\mathit{has\_type\_}\tau(t)$, and the binary function
+$\mathit{type\/}(\tau, t)$ becomes a unary function
+$\mathit{type\_}\tau(t)$.
\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
types if the prover supports the TFF or THF syntax; otherwise, fall back on
-\textit{mangled\_guards}. The problem is monomorphized.
+\textit{mono\_guards}. The problem is monomorphized.
\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
higher-order types if the prover supports the THF syntax; otherwise, fall back
-on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
+on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
monomorphized.
\item[$\bullet$]
\textbf{%
-\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
-\textit{mangled\_guards}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
+\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
+\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
+\textit{simple}? (quasi-sound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, and \textit{simple} are fully
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, and \textit{simple} are fully
typed and sound. For each of these, Sledgehammer also provides a lighter,
virtually sound variant identified by a question mark (`{?}')\ that detects and
erases monotonic types, notably infinite types. (For \textit{simple}, the types
@@ -952,12 +953,12 @@
\item[$\bullet$]
\textbf{%
-\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mangled\_guards}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
-(mildly unsound):} \\
+\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
+\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
+\textit{simple\_higher}! (mildly unsound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
a mildly unsound (but very efficient) variant identified by an exclamation mark
(`{!}') that detects and erases erases all types except those that are clearly
finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
@@ -973,7 +974,7 @@
available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
nonuniform variants are generally more efficient and are the default; the
uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
-\textit{mangled\_guards\_uniform}{?}).
+\textit{mono\_guards\_uniform}{?}).
For SMT solvers, the type encoding is always \textit{simple}, irrespective of
the value of this option.
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Fri Aug 26 23:14:36 2011 +0200
@@ -436,10 +436,10 @@
apply(rule TrueI)+
--{* Parallel *}
apply(simp add: SEM_def sem_def)
- apply clarify
+ apply(clarify, rename_tac x y i Ts')
apply(frule Parallel_length_post_PStar)
apply clarify
- apply(drule_tac j=xb in Parallel_Strong_Soundness)
+ apply(drule_tac j=i in Parallel_Strong_Soundness)
apply clarify
apply simp
apply force
--- a/src/HOL/IsaMakefile Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/IsaMakefile Fri Aug 26 23:14:36 2011 +0200
@@ -1175,6 +1175,7 @@
Multivariate_Analysis/L2_Norm.thy \
Multivariate_Analysis/Linear_Algebra.thy \
Multivariate_Analysis/Multivariate_Analysis.thy \
+ Multivariate_Analysis/Norm_Arith.thy \
Multivariate_Analysis/Operator_Norm.thy \
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/ROOT.ML \
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 26 23:14:36 2011 +0200
@@ -2391,8 +2391,6 @@
shows "limsup X \<le> limsup Y"
using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-declare trivial_limit_sequentially[simp]
-
lemma
fixes X :: "nat \<Rightarrow> ereal"
shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
--- a/src/HOL/Lim.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Lim.thy Fri Aug 26 23:14:36 2011 +0200
@@ -444,46 +444,51 @@
subsection {* Relation of LIM and LIMSEQ *}
+lemma sequentially_imp_eventually_within:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a within s)"
+proof (rule ccontr)
+ let ?I = "\<lambda>n. inverse (real (Suc n))"
+ def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+ assume "\<not> eventually P (at a within s)"
+ hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+ unfolding Limits.eventually_within Limits.eventually_at by fast
+ hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+ hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
+ unfolding F_def by (rule someI_ex)
+ hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
+ and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
+ by fast+
+ from LIMSEQ_inverse_real_of_nat have "F ----> a"
+ by (rule metric_tendsto_imp_tendsto,
+ simp add: dist_norm F2 less_imp_le)
+ hence "eventually (\<lambda>n. P (F n)) sequentially"
+ using assms F0 F1 by simp
+ thus "False" by (simp add: F3)
+qed
+
+lemma sequentially_imp_eventually_at:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a)"
+ using assms sequentially_imp_eventually_within [where s=UNIV]
+ unfolding within_UNIV by simp
+
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes f: "f -- a --> l"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
-lemma LIMSEQ_SEQ_conv2_lemma:
- fixes a :: "'a::metric_space"
- assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
- shows "eventually P (at a)"
-proof (rule ccontr)
- let ?I = "\<lambda>n. inverse (real (Suc n))"
- let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
- assume "\<not> eventually P (at a)"
- hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
- unfolding eventually_at by simp
- hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
- by (rule someI_ex)
- hence F1: "\<And>n. ?F n \<noteq> a"
- and F2: "\<And>n. dist (?F n) a < ?I n"
- and F3: "\<And>n. \<not> P (?F n)"
- by fast+
- have "?F ----> a"
- using LIMSEQ_inverse_real_of_nat
- by (rule metric_tendsto_imp_tendsto,
- simp add: dist_norm F2 [THEN less_imp_le])
- moreover have "\<forall>n. ?F n \<noteq> a"
- by (rule allI) (rule F1)
- ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
- using assms by simp
- thus "False" by (simp add: F3)
-qed
-
lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
shows "f -- a --> l"
using assms unfolding tendsto_def [where l=l]
- by (simp add: LIMSEQ_SEQ_conv2_lemma)
+ by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
--- a/src/HOL/List.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/List.thy Fri Aug 26 23:14:36 2011 +0200
@@ -4703,7 +4703,7 @@
qed
-text{* Accessible part of @{term listrel1} relations: *}
+text{* Accessible part and wellfoundedness: *}
lemma Cons_acc_listrel1I [intro!]:
"x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
@@ -4729,6 +4729,9 @@
apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
done
+lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
+by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
+
subsubsection {* Lifting Relations to Lists: all elements *}
--- a/src/HOL/Metis_Examples/Proxies.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Fri Aug 26 23:14:36 2011 +0200
@@ -62,10 +62,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
@@ -74,10 +74,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
@@ -86,10 +86,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
@@ -98,10 +98,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
@@ -110,10 +110,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -123,10 +123,10 @@
sledgehammer [type_enc = poly_tags, expect = some] ()
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] ()
-sledgehammer [type_enc = mangled_tags?, expect = some] ()
-sledgehammer [type_enc = mangled_tags, expect = some] ()
-sledgehammer [type_enc = mangled_guards?, expect = some] ()
-sledgehammer [type_enc = mangled_guards, expect = some] ()
+sledgehammer [type_enc = mono_tags?, expect = some] ()
+sledgehammer [type_enc = mono_tags, expect = some] ()
+sledgehammer [type_enc = mono_guards?, expect = some] ()
+sledgehammer [type_enc = mono_guards, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
@@ -135,10 +135,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
@@ -147,10 +147,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
@@ -159,10 +159,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
@@ -171,10 +171,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
@@ -183,10 +183,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
@@ -195,10 +195,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
@@ -207,10 +207,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
@@ -219,10 +219,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
@@ -231,10 +231,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
@@ -243,10 +243,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
@@ -255,10 +255,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Aug 26 23:14:36 2011 +0200
@@ -29,42 +29,42 @@
"poly_tags",
"poly_tags_uniform",
"poly_args",
+ "raw_mono_guards",
+ "raw_mono_guards_uniform",
+ "raw_mono_tags",
+ "raw_mono_tags_uniform",
+ "raw_mono_args",
"mono_guards",
"mono_guards_uniform",
"mono_tags",
"mono_tags_uniform",
"mono_args",
- "mangled_guards",
- "mangled_guards_uniform",
- "mangled_tags",
- "mangled_tags_uniform",
- "mangled_args",
"simple",
"poly_guards?",
"poly_guards_uniform?",
"poly_tags?",
"poly_tags_uniform?",
+ "raw_mono_guards?",
+ "raw_mono_guards_uniform?",
+ "raw_mono_tags?",
+ "raw_mono_tags_uniform?",
"mono_guards?",
"mono_guards_uniform?",
"mono_tags?",
"mono_tags_uniform?",
- "mangled_guards?",
- "mangled_guards_uniform?",
- "mangled_tags?",
- "mangled_tags_uniform?",
"simple?",
"poly_guards!",
"poly_guards_uniform!",
"poly_tags!",
"poly_tags_uniform!",
+ "raw_mono_guards!",
+ "raw_mono_guards_uniform!",
+ "raw_mono_tags!",
+ "raw_mono_tags_uniform!",
"mono_guards!",
"mono_guards_uniform!",
"mono_tags!",
"mono_tags_uniform!",
- "mangled_guards!",
- "mangled_guards_uniform!",
- "mangled_tags!",
- "mangled_tags_uniform!",
"simple!"]
fun metis_exhaust_tac ctxt ths =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 26 23:14:36 2011 +0200
@@ -484,9 +484,8 @@
case result of
SH_OK (time_isa, time_prover, names) =>
let
- fun get_thms (_, ATP_Translate.Chained) = NONE
- | get_thms (name, loc) =
- SOME ((name, loc), thms_of_name (Proof.context_of st) name)
+ fun get_thms (name, loc) =
+ SOME ((name, loc), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
if trivial then () else change_data id inc_sh_nontriv_success;
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 23:14:36 2011 +0200
@@ -792,7 +792,7 @@
have "subspace ?P"
by (auto simp add: subspace_def)
ultimately show ?thesis
- using x span_induct[of ?B ?P x] iS by blast
+ using x span_induct[of x ?B ?P] iS by blast
qed
lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
@@ -2001,8 +2001,4 @@
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 23:14:36 2011 +0200
@@ -229,12 +229,18 @@
from g(1) gS giS gBC show ?thesis by blast
qed
+lemma closure_bounded_linear_image:
+ assumes f: "bounded_linear f"
+ shows "f ` (closure S) \<subseteq> closure (f ` S)"
+ using linear_continuous_on [OF f] closed_closure closure_subset
+ by (rule image_closure_subset)
+
lemma closure_linear_image:
fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
assumes "linear f"
shows "f ` (closure S) <= closure (f ` S)"
-using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f]
-linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
+ using assms unfolding linear_conv_bounded_linear
+ by (rule closure_bounded_linear_image)
lemma closure_injective_linear_image:
fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
@@ -254,23 +260,16 @@
shows "closure (S <*> T) = closure S <*> closure T"
by (rule closure_Times)
-lemma closure_scaleR: (* TODO: generalize to real_normed_vector *)
-fixes S :: "('n::euclidean_space) set"
-shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
-proof-
-{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
- linear_scaleR injective_scaleR by auto
-}
-moreover
-{ assume zero: "c=0 & S ~= {}"
- hence "closure S ~= {}" using closure_subset by auto
- hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
- moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
- ultimately have ?thesis using zero by auto
-}
-moreover
-{ assume "S={}" hence ?thesis by auto }
-ultimately show ?thesis by blast
+lemma closure_scaleR:
+ fixes S :: "('a::real_normed_vector) set"
+ shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+proof
+ show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
+ using bounded_linear_scaleR_right
+ by (rule closure_bounded_linear_image)
+ show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
+ by (intro closure_minimal image_mono closure_subset
+ closed_scaling closed_closure)
qed
lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
@@ -859,9 +858,8 @@
qed
lemma cone_closure:
-fixes S :: "('m::euclidean_space) set"
-assumes "cone S"
-shows "cone (closure S)"
+ fixes S :: "('a::real_normed_vector) set"
+ assumes "cone S" shows "cone (closure S)"
proof-
{ assume "S = {}" hence ?thesis by auto }
moreover
@@ -2310,12 +2308,7 @@
lemma closure_affine_hull:
fixes S :: "('n::euclidean_space) set"
shows "closure S <= affine hull S"
-proof-
-have "closure S <= closure (affine hull S)" using subset_closure by auto
-moreover have "closure (affine hull S) = affine hull S"
- using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
-ultimately show ?thesis by auto
-qed
+ by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
lemma closure_same_affine_hull:
fixes S :: "('n::euclidean_space) set"
@@ -2580,6 +2573,37 @@
done
qed
+lemma finite_imp_compact_convex_hull:
+ fixes s :: "('a::real_normed_vector) set"
+ assumes "finite s" shows "compact (convex hull s)"
+proof (cases "s = {}")
+ case True thus ?thesis by simp
+next
+ case False with assms show ?thesis
+ proof (induct rule: finite_ne_induct)
+ case (singleton x) show ?case by simp
+ next
+ case (insert x A)
+ let ?f = "\<lambda>(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y"
+ let ?T = "{0..1::real} \<times> (convex hull A)"
+ have "continuous_on ?T ?f"
+ unfolding split_def continuous_on by (intro ballI tendsto_intros)
+ moreover have "compact ?T"
+ by (intro compact_Times compact_interval insert)
+ ultimately have "compact (?f ` ?T)"
+ by (rule compact_continuous_image)
+ also have "?f ` ?T = convex hull (insert x A)"
+ unfolding convex_hull_insert [OF `A \<noteq> {}`]
+ apply safe
+ apply (rule_tac x=a in exI, simp)
+ apply (rule_tac x="1 - a" in exI, simp)
+ apply fast
+ apply (rule_tac x="(u, b)" in image_eqI, simp_all)
+ done
+ finally show "compact (convex hull (insert x A))" .
+ qed
+qed
+
lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
assumes "compact s" shows "compact(convex hull s)"
proof(cases "s={}")
@@ -2654,11 +2678,6 @@
qed
qed
-lemma finite_imp_compact_convex_hull:
- fixes s :: "('a::euclidean_space) set"
- shows "finite s \<Longrightarrow> compact(convex hull s)"
-by (metis compact_convex_hull finite_imp_compact)
-
subsection {* Extremal points of a simplex are some vertices. *}
lemma dist_increases_online:
@@ -2738,7 +2757,7 @@
qed (auto simp add: assms)
lemma simplex_furthest_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
proof-
@@ -2754,12 +2773,12 @@
qed
lemma simplex_furthest_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
using simplex_furthest_le[of s] by (cases "s={}")auto
lemma simplex_extremal_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
proof-
@@ -2780,7 +2799,7 @@
qed
lemma simplex_extremal_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
\<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
@@ -3094,7 +3113,6 @@
subsection {* Convexity of cone hulls *}
lemma convex_cone_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "convex S"
shows "convex (cone hull S)"
proof-
@@ -3126,7 +3144,6 @@
qed
lemma cone_convex_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "cone S"
shows "cone (convex hull S)"
proof-
@@ -3453,22 +3470,27 @@
ultimately show ?thesis using injpi by auto qed qed
qed auto qed
-lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set"
- assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
+lemma homeomorphic_convex_compact_lemma:
+ fixes s :: "('a::euclidean_space) set"
+ assumes "convex s" and "compact s" and "cball 0 1 \<subseteq> s"
shows "s homeomorphic (cball (0::'a) 1)"
- apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
- fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
- hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq
- apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball)
- unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
- fix y assume "dist (u *\<^sub>R x) y < 1 - u"
- hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
- using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
- unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
- apply (rule mult_left_le_imp_le[of "1 - u"])
- unfolding mult_assoc[symmetric] using `u<1` by auto
- thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
- using as unfolding scaleR_scaleR by auto qed auto
+proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
+ fix x u assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+ have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball)
+ moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
+ unfolding centre_in_ball using `u < 1` by simp
+ moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+ proof
+ fix y assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
+ hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball .
+ with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
+ by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
+ with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
+ with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
+ using `x \<in> s` `0 \<le> u` `u < 1` [THEN less_imp_le] by (rule mem_convex)
+ thus "y \<in> s" using `u < 1` by simp
+ qed
+ ultimately have "u *\<^sub>R x \<in> interior s" ..
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set"
@@ -3621,8 +3643,8 @@
assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
- using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by auto
+ using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
+ using assms using continuous_on_minus by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -4042,7 +4064,7 @@
then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
- have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
+ have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
by(auto simp add:field_simps norm_minus_commute)
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
@@ -4380,7 +4402,7 @@
shows "closure(rel_interior S) = closure S"
proof-
have h1: "closure(rel_interior S) <= closure S"
- using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
+ using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S"
using rel_interior_convex_nonempty assms by auto
{ fix x assume x_def: "x : closure S"
@@ -4517,7 +4539,7 @@
proof-
have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
moreover have "?B --> (closure S1 <= closure S2)"
- by (metis assms(1) convex_closure_rel_interior subset_closure)
+ by (metis assms(1) convex_closure_rel_interior closure_mono)
moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
ultimately show ?thesis by blast
qed
@@ -4777,7 +4799,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4790,7 +4812,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4886,7 +4908,7 @@
proof-
have *: "S Int closure T = S" using assms by auto
have "~(rel_interior S <= rel_frontier T)"
- using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
+ using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
@@ -4911,8 +4933,8 @@
also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto
also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto
finally have "closure (f ` S) = closure (f ` rel_interior S)"
- using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
- subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
+ using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
+ closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"]
closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 23:14:36 2011 +0200
@@ -785,7 +785,7 @@
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
defer
- apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+ apply(rule continuous_on_intros assms(2))+
proof
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
@@ -869,7 +869,7 @@
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
by (auto simp add: algebra_simps)
hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
- apply(rule continuous_on_intros continuous_on_vmul)+
+ apply(rule continuous_on_intros)+
unfolding continuous_on_eq_continuous_within
apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 23:14:36 2011 +0200
@@ -149,7 +149,7 @@
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
proof -
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
- by (simp add: euclidean_component_diff)
+ by simp
then show "x = y"
unfolding euclidean_component_def euclidean_all_zero by simp
qed
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Aug 26 23:14:36 2011 +0200
@@ -44,7 +44,7 @@
have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
- apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+ apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 23:14:36 2011 +0200
@@ -378,7 +378,7 @@
interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
\<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
- show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
+ show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
using division_ofD(5)[OF assms(1) k1(2) k2(2)]
using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
@@ -407,9 +407,9 @@
show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
{ fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
- { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
+ { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
using assms(3) by blast } moreover
- { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
+ { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
using assms(3) by blast} ultimately
show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
fix k assume k:"k \<in> p1 \<union> p2" show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
@@ -573,7 +573,7 @@
show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
- apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+ apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
unfolding division_of_def by(metis bounded_Union bounded_interval)
@@ -823,7 +823,7 @@
fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
- have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
+ have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
using p1(3) p2(3) using xk xk' by auto qed
@@ -842,7 +842,7 @@
show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
- using assms(3)[rule_format] subset_interior by blast
+ using assms(3)[rule_format] interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
qed
@@ -1703,7 +1703,7 @@
by(rule le_less_trans[OF norm_le_l1])
hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
thus False unfolding mem_Collect_eq using e x k by auto
- qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
+ qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
thus "content b *\<^sub>R f a = 0" by auto
qed auto
also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
@@ -2563,7 +2563,7 @@
proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}" "{m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}"
have "({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
- note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
+ note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
thus "content ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[THEN sym] .
qed qed
@@ -3516,7 +3516,7 @@
proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
- have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
@@ -3528,7 +3528,7 @@
proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
- have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((b + ?v)/2) \<in> {?v <..< b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
@@ -4390,7 +4390,7 @@
from this(2) guess u v apply-by(erule exE)+ note uv=this
have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
- note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+ note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
@@ -4403,7 +4403,7 @@
have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
using as unfolding r_def by auto
have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
- apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+ apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto
qed(insert qq, auto)
@@ -4462,6 +4462,61 @@
proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
+subsection {* Geometric progression *}
+
+text {* FIXME: Should one or more of these theorems be moved to @{file
+"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+
+lemma sum_gp_basic:
+ fixes x :: "'a::ring_1"
+ shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+proof-
+ def y \<equiv> "1 - x"
+ have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
+ by (induct n, simp, simp add: algebra_simps)
+ thus ?thesis
+ unfolding y_def by simp
+qed
+
+lemma sum_gp_multiplied: assumes mn: "m <= n"
+ shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+ (is "?lhs = ?rhs")
+proof-
+ let ?S = "{0..(n - m)}"
+ from mn have mn': "n - m \<ge> 0" by arith
+ let ?f = "op + m"
+ have i: "inj_on ?f ?S" unfolding inj_on_def by auto
+ have f: "?f ` ?S = {m..n}"
+ using mn apply (auto simp add: image_iff Bex_def) by arith
+ have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
+ by (rule ext, simp add: power_add power_mult)
+ from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
+ have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
+ then show ?thesis unfolding sum_gp_basic using mn
+ by (simp add: field_simps power_add[symmetric])
+qed
+
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
+ (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
+ else (x^ m - x^ (Suc n)) / (1 - x))"
+proof-
+ {assume nm: "n < m" hence ?thesis by simp}
+ moreover
+ {assume "\<not> n < m" hence nm: "m \<le> n" by arith
+ {assume x: "x = 1" hence ?thesis by simp}
+ moreover
+ {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
+ from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+ ultimately have ?thesis by metis
+ }
+ ultimately show ?thesis by metis
+qed
+
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
+ (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+ unfolding sum_gp[of x m "m + n"] power_Suc
+ by (simp add: field_simps power_add)
+
subsection {* monotone convergence (bounded interval first). *}
lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 26 23:14:36 2011 +0200
@@ -8,11 +8,6 @@
imports
Euclidean_Space
"~~/src/HOL/Library/Infinite_Set"
- L2_Norm
- "~~/src/HOL/Library/Convex"
- "~~/src/HOL/Library/Sum_of_Squares"
-uses
- ("normarith.ML")
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -66,7 +61,7 @@
*)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
- by (simp add: setL2_def power2_eq_square)
+ by (simp add: power2_eq_square)
lemma norm_cauchy_schwarz:
shows "inner x y <= norm x * norm y"
@@ -154,111 +149,6 @@
then show "x = y" by (simp)
qed
-subsection{* General linear decision procedure for normed spaces. *}
-
-lemma norm_cmul_rule_thm:
- fixes x :: "'a::real_normed_vector"
- shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
- unfolding norm_scaleR
- apply (erule mult_left_mono)
- apply simp
- done
-
- (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm:
- fixes x1 x2 :: "'a::real_normed_vector"
- shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
- by (rule order_trans [OF norm_triangle_ineq add_mono])
-
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
- by (simp add: field_simps)
-
-lemma pth_1:
- fixes x :: "'a::real_normed_vector"
- shows "x == scaleR 1 x" by simp
-
-lemma pth_2:
- fixes x :: "'a::real_normed_vector"
- shows "x - y == x + -y" by (atomize (full)) simp
-
-lemma pth_3:
- fixes x :: "'a::real_normed_vector"
- shows "- x == scaleR (-1) x" by simp
-
-lemma pth_4:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
-
-lemma pth_5:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
-
-lemma pth_6:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (x + y) == scaleR c x + scaleR c y"
- by (simp add: scaleR_right_distrib)
-
-lemma pth_7:
- fixes x :: "'a::real_normed_vector"
- shows "0 + x == x" and "x + 0 == x" by simp_all
-
-lemma pth_8:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c x + scaleR d x == scaleR (c + d) x"
- by (simp add: scaleR_left_distrib)
-
-lemma pth_9:
- fixes x :: "'a::real_normed_vector" shows
- "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
- "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
- "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_a:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x + y == y" by simp
-
-lemma pth_b:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
- "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
- "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
- by (simp_all add: algebra_simps)
-
-lemma pth_c:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
- "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
- "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_d:
- fixes x :: "'a::real_normed_vector"
- shows "x + 0 == x" by simp
-
-lemma norm_imp_pos_and_ge:
- fixes x :: "'a::real_normed_vector"
- shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by atomize auto
-
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
-
-lemma norm_pths:
- fixes x :: "'a::real_normed_vector" shows
- "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
- "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_ge_zero[of "x - y"] by auto
-
-use "normarith.ML"
-
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "prove simple linear statements about vector norms"
-
-
-text{* Hence more metric properties. *}
-
lemma norm_triangle_half_r:
shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
@@ -274,16 +164,6 @@
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-lemma dist_triangle_add:
- fixes x y x' y' :: "'a::real_normed_vector"
- shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
- by norm
-
-lemma dist_triangle_add_half:
- fixes x x' y y' :: "'a::real_normed_vector"
- shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
- by norm
-
lemma setsum_clauses:
shows "setsum f {} = 0"
and "finite S \<Longrightarrow> setsum f (insert x S) =
@@ -311,12 +191,6 @@
apply (rule setsum_mono_zero_right[OF fT fST])
by (auto intro: setsum_0')
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
-lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
proof
assume "\<forall>x. x \<bullet> y = x \<bullet> z"
@@ -702,65 +576,6 @@
then show ?thesis by blast
qed
-subsection {* Geometric progression *}
-
-lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
- (is "?lhs = ?rhs")
-proof-
- {assume x1: "x = 1" hence ?thesis by simp}
- moreover
- {assume x1: "x\<noteq>1"
- hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
- from geometric_sum[OF x1, of "Suc n", unfolded x1']
- have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
- unfolding atLeastLessThanSuc_atLeastAtMost
- using x1' apply (auto simp only: field_simps)
- apply (simp add: field_simps)
- done
- then have ?thesis by (simp add: field_simps) }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_multiplied: assumes mn: "m <= n"
- shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
- (is "?lhs = ?rhs")
-proof-
- let ?S = "{0..(n - m)}"
- from mn have mn': "n - m \<ge> 0" by arith
- let ?f = "op + m"
- have i: "inj_on ?f ?S" unfolding inj_on_def by auto
- have f: "?f ` ?S = {m..n}"
- using mn apply (auto simp add: image_iff Bex_def) by arith
- have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
- by (rule ext, simp add: power_add power_mult)
- from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
- have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
- then show ?thesis unfolding sum_gp_basic using mn
- by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
- (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
- else (x^ m - x^ (Suc n)) / (1 - x))"
-proof-
- {assume nm: "n < m" hence ?thesis by simp}
- moreover
- {assume "\<not> n < m" hence nm: "m \<le> n" by arith
- {assume x: "x = 1" hence ?thesis by simp}
- moreover
- {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
- ultimately have ?thesis by metis
- }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- unfolding sum_gp[of x m "m + n"] power_Suc
- by (simp add: field_simps power_add)
-
-
subsection{* A bit of linear algebra. *}
definition (in real_vector)
@@ -807,6 +622,9 @@
apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
done
+lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
+ by (auto simp add: subspace_def linear_def linear_0[of f])
+
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
by (auto simp add: subspace_def linear_def linear_0[of f])
@@ -816,6 +634,11 @@
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
by (simp add: subspace_def)
+lemma subspace_Times: "\<lbrakk>subspace A; subspace B\<rbrakk> \<Longrightarrow> subspace (A \<times> B)"
+ unfolding subspace_def zero_prod_def by simp
+
+text {* Properties of span. *}
+
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
by (metis span_def hull_mono)
@@ -834,8 +657,16 @@
by (metis span_def hull_subset subset_eq)
(metis subspace_span subspace_def)+
-lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
- and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
+lemma span_unique:
+ "\<lbrakk>S \<subseteq> T; subspace T; \<And>T'. \<lbrakk>S \<subseteq> T'; subspace T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk> \<Longrightarrow> span S = T"
+ unfolding span_def by (rule hull_unique)
+
+lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
+ unfolding span_def by (rule hull_minimal)
+
+lemma (in real_vector) span_induct:
+ assumes x: "x \<in> span S" and P: "subspace P" and SP: "\<And>x. x \<in> S ==> x \<in> P"
+ shows "x \<in> P"
proof-
from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
@@ -967,105 +798,76 @@
text {* Mapping under linear image. *}
-lemma span_linear_image: assumes lf: "linear f"
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+ by auto (* TODO: move *)
+
+lemma span_linear_image:
+ assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
-proof-
- {fix x
- assume x: "x \<in> span (f ` S)"
- have "x \<in> f ` span S"
- apply (rule span_induct[where x=x and S = "f ` S"])
- apply (clarsimp simp add: image_iff)
- apply (frule span_superset)
- apply blast
- apply (rule subspace_linear_image[OF lf])
- apply (rule subspace_span)
- apply (rule x)
- done}
- moreover
- {fix x assume x: "x \<in> span S"
- have "x \<in> {x. f x \<in> span (f ` S)}"
- apply (rule span_induct[where S=S])
- apply simp
- apply (rule span_superset)
- apply simp
- apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
- apply (rule x)
- done
- hence "f x \<in> span (f ` S)" by simp
- }
- ultimately show ?thesis by blast
+proof (rule span_unique)
+ show "f ` S \<subseteq> f ` span S"
+ by (intro image_mono span_inc)
+ show "subspace (f ` span S)"
+ using lf subspace_span by (rule subspace_linear_image)
+next
+ fix T assume "f ` S \<subseteq> T" and "subspace T" thus "f ` span S \<subseteq> T"
+ unfolding image_subset_iff_subset_vimage
+ by (intro span_minimal subspace_linear_vimage lf)
+qed
+
+lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+proof (rule span_unique)
+ show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+ by safe (force intro: span_clauses)+
+next
+ have "linear (\<lambda>(a, b). a + b)"
+ by (simp add: linear_def scaleR_add_right)
+ moreover have "subspace (span A \<times> span B)"
+ by (intro subspace_Times subspace_span)
+ ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
+ by (rule subspace_linear_image)
+next
+ fix T assume "A \<union> B \<subseteq> T" and "subspace T"
+ thus "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
+ by (auto intro!: subspace_add elim: span_induct)
qed
text {* The key breakdown property. *}
+lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
+proof (rule span_unique)
+ show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
+ by (fast intro: scaleR_one [symmetric])
+ show "subspace (range (\<lambda>k. k *\<^sub>R x))"
+ unfolding subspace_def
+ by (auto intro: scaleR_add_left [symmetric])
+ fix T assume "{x} \<subseteq> T" and "subspace T" thus "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
+ unfolding subspace_def by auto
+qed
+
+lemma span_insert:
+ "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+proof -
+ have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+ unfolding span_union span_singleton
+ apply safe
+ apply (rule_tac x=k in exI, simp)
+ apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
+ apply simp
+ apply (rule right_minus)
+ done
+ thus ?thesis by simp
+qed
+
lemma span_breakdown:
assumes bS: "b \<in> S" and aS: "a \<in> span S"
- shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
-proof-
- {fix x assume xS: "x \<in> S"
- {assume ab: "x = b"
- then have "?P x"
- apply simp
- apply (rule exI[where x="1"], simp)
- by (rule span_0)}
- moreover
- {assume ab: "x \<noteq> b"
- then have "?P x" using xS
- apply -
- apply (rule exI[where x=0])
- apply (rule span_superset)
- by simp}
- ultimately have "x \<in> Collect ?P" by blast}
- moreover have "subspace (Collect ?P)"
- unfolding subspace_def
- apply auto
- apply (rule exI[where x=0])
- using span_0[of "S - {b}"]
- apply simp
- apply (rule_tac x="k + ka" in exI)
- apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
- apply (simp only: )
- apply (rule span_add)
- apply assumption+
- apply (simp add: algebra_simps)
- apply (rule_tac x= "c*k" in exI)
- apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
- apply (simp only: )
- apply (rule span_mul)
- apply assumption
- by (simp add: algebra_simps)
- ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
- thus "?P a" by simp
-qed
+ shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
+ using assms span_insert [of b "S - {b}"]
+ by (simp add: insert_absorb)
lemma span_breakdown_eq:
- "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume x: "x \<in> span (insert a S)"
- from x span_breakdown[of "a" "insert a S" "x"]
- have ?rhs apply clarsimp
- apply (rule_tac x= "k" in exI)
- apply (rule set_rev_mp[of _ "span (S - {a})" _])
- apply assumption
- apply (rule span_mono)
- apply blast
- done}
- moreover
- { fix k assume k: "x - k *\<^sub>R a \<in> span S"
- have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
- have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
- apply (rule span_add)
- apply (rule set_rev_mp[of _ "span S" _])
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- apply (rule span_superset)
- apply blast
- done
- then have ?lhs using eq by metis}
- ultimately show ?thesis by blast
-qed
+ "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)"
+ by (simp add: span_insert)
text {* Hence some "reversal" results. *}
@@ -1122,26 +924,16 @@
text {* Transitivity property. *}
+lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
+ unfolding span_def by (rule hull_redundant)
+
lemma span_trans:
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
shows "y \<in> span S"
-proof-
- from span_breakdown[of x "insert x S" y, OF insertI1 y]
- obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
- have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
- show ?thesis
- apply (subst eq)
- apply (rule span_add)
- apply (rule set_rev_mp)
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- by (rule x)
-qed
+ using assms by (simp only: span_redundant)
lemma span_insert_0[simp]: "span (insert 0 S) = span S"
- using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)
+ by (simp only: span_redundant span_0)
text {* An explicit expansion is sometimes needed. *}
@@ -1273,43 +1065,6 @@
ultimately show ?thesis by blast
qed
-lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
-
-lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
-proof safe
- fix x assume "x \<in> span (A \<union> B)"
- then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
- unfolding span_explicit by auto
-
- let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
- let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
- show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
- proof
- show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
- unfolding x using S
- by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
-
- from S have "?Sa \<in> span A" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> A"])
- moreover from S have "?Sb \<in> span B" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> (B - A)"])
- ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
- qed
-next
- fix a b assume "a \<in> span A" and "b \<in> span B"
- then obtain Sa ua Sb ub where span:
- "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
- "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
- unfolding span_explicit by auto
- let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
- from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
- and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
- unfolding setsum_addf scaleR_left_distrib
- by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
- thus "a + b \<in> span (A \<union> B)"
- unfolding span_explicit by (auto intro!: exI[of _ ?u])
-qed
-
text {* This is useful for building a basis step-by-step. *}
lemma independent_insert:
@@ -1495,30 +1250,6 @@
apply (simp add: inner_setsum_right dot_basis)
done
-lemma dimensionI:
- assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
- independent (basis ` {..<d} :: 'a set);
- inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
- shows "P DIM('a::euclidean_space)"
- using DIM_positive basis_finite independent_basis basis_inj
- by (rule assms)
-
-lemma (in euclidean_space) dimension_eq:
- assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
- assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
- shows "DIM('a) = d"
-proof (rule linorder_cases [of "DIM('a)" d])
- assume "DIM('a) < d"
- hence "basis DIM('a) \<noteq> 0" by (rule assms)
- thus ?thesis by simp
-next
- assume "d < DIM('a)"
- hence "basis d \<noteq> 0" by simp
- thus ?thesis by (simp add: assms)
-next
- assume "DIM('a) = d" thus ?thesis .
-qed
-
lemma (in euclidean_space) range_basis:
"range basis = insert 0 (basis ` {..<DIM('a)})"
proof -
@@ -1628,22 +1359,6 @@
ultimately show ?thesis by metis
qed
-subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
-
-class ordered_euclidean_space = ord + euclidean_space +
- assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
- and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
-
-lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
- unfolding eucl_less[where 'a='a] by auto
-
-lemma euclidean_trans[trans]:
- fixes x y z :: "'a::ordered_euclidean_space"
- shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
-
subsection {* Linearity and Bilinearity continued *}
lemma linear_bounded:
@@ -2035,8 +1750,15 @@
lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
unfolding inner_simps by auto
+lemma pairwise_orthogonal_insert:
+ assumes "pairwise orthogonal S"
+ assumes "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+ shows "pairwise orthogonal (insert x S)"
+ using assms unfolding pairwise_def
+ by (auto simp add: orthogonal_commute)
+
lemma basis_orthogonal:
- fixes B :: "('a::euclidean_space) set"
+ fixes B :: "('a::real_inner) set"
assumes fB: "finite B"
shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
(is " \<exists>C. ?P B C")
@@ -2064,48 +1786,20 @@
by (rule span_superset)}
then have SC: "span ?C = span (insert a B)"
unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
- thm pairwise_def
- {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
- {assume xa: "x = ?a" and ya: "y = ?a"
- have "orthogonal x y" using xa ya xy by blast}
- moreover
- {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C"
- from ya have Cy: "C = insert y (C - {y})" by blast
- have fth: "finite (C - {y})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cy)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a"
- from xa have Cx: "C = insert x (C - {x})" by blast
- have fth: "finite (C - {x})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cx)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (subst inner_commute[of x])
- apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<in> C" and ya: "y \<in> C"
- have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}
- ultimately have "orthogonal x y" using xC yC by blast}
- then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast
+ { fix y assume yC: "y \<in> C"
+ hence Cy: "C = insert y (C - {y})" by blast
+ have fth: "finite (C - {y})" using C by simp
+ have "orthogonal ?a y"
+ unfolding orthogonal_def
+ unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
+ unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
+ apply (clarsimp simp add: inner_commute[of y a])
+ apply (rule setsum_0')
+ apply clarsimp
+ apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
+ using `y \<in> C` by auto }
+ with `pairwise orthogonal C` have CPO: "pairwise orthogonal ?C"
+ by (rule pairwise_orthogonal_insert)
from fC cC SC CPO have "?P (insert a B) ?C" by blast
then show ?case by blast
qed
@@ -2166,7 +1860,7 @@
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
apply simp unfolding inner_simps
- apply (clarsimp simp add: inner_add dot_lsum)
+ apply (clarsimp simp add: inner_add inner_setsum_left)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
@@ -3017,7 +2711,23 @@
apply simp
done
-subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
+subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
+
+class ordered_euclidean_space = ord + euclidean_space +
+ assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
+ and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
+
+lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
+ unfolding eucl_less[where 'a='a] by auto
+
+lemma euclidean_trans[trans]:
+ fixes x y z :: "'a::ordered_euclidean_space"
+ shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+ unfolding eucl_less[where 'a='a] eucl_le[where 'a='a]
+ by (fast intro: less_trans, fast intro: le_less_trans,
+ fast intro: order_trans)
lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
@@ -3036,8 +2746,6 @@
shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
unfolding basis_complex_def by auto
-subsection {* Products Spaces *}
-
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
(* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
unfolding dimension_prod_def by (rule add_commute)
@@ -3051,5 +2759,4 @@
instance proof qed (auto simp: less_prod_def less_eq_prod_def)
end
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Fri Aug 26 23:14:36 2011 +0200
@@ -0,0 +1,124 @@
+(* Title: HOL/Multivariate_Analysis/Norm_Arith.thy
+ Author: Amine Chaieb, University of Cambridge
+*)
+
+header {* General linear decision procedure for normed spaces *}
+
+theory Norm_Arith
+imports "~~/src/HOL/Library/Sum_of_Squares"
+uses ("normarith.ML")
+begin
+
+lemma norm_cmul_rule_thm:
+ fixes x :: "'a::real_normed_vector"
+ shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+ unfolding norm_scaleR
+ apply (erule mult_left_mono)
+ apply simp
+ done
+
+ (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+lemma norm_add_rule_thm:
+ fixes x1 x2 :: "'a::real_normed_vector"
+ shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+ by (rule order_trans [OF norm_triangle_ineq add_mono])
+
+lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+ by (simp add: field_simps)
+
+lemma pth_1:
+ fixes x :: "'a::real_normed_vector"
+ shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+ fixes x :: "'a::real_normed_vector"
+ shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+ fixes x :: "'a::real_normed_vector"
+ shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+ by (simp add: scaleR_right_distrib)
+
+lemma pth_7:
+ fixes x :: "'a::real_normed_vector"
+ shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+ by (simp add: scaleR_left_distrib)
+
+lemma pth_9:
+ fixes x :: "'a::real_normed_vector" shows
+ "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+ "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+ "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_a:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+ "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+ "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+ by (simp_all add: algebra_simps)
+
+lemma pth_c:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+ "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+ "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_d:
+ fixes x :: "'a::real_normed_vector"
+ shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+ fixes x :: "'a::real_normed_vector"
+ shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+ by atomize auto
+
+lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+
+lemma norm_pths:
+ fixes x :: "'a::real_normed_vector" shows
+ "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+ "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+ using norm_ge_zero[of "x - y"] by auto
+
+use "normarith.ML"
+
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+*} "prove simple linear statements about vector norms"
+
+text{* Hence more metric properties. *}
+
+lemma dist_triangle_add:
+ fixes x y x' y' :: "'a::real_normed_vector"
+ shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+ by norm
+
+lemma dist_triangle_add_half:
+ fixes x x' y y' :: "'a::real_normed_vector"
+ shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+ by norm
+
+end
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 26 23:14:36 2011 +0200
@@ -92,7 +92,7 @@
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
have *:"\<And>g. path g \<Longrightarrow> path(reversepath g)" unfolding path_def reversepath_def
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
- apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
+ apply(intro continuous_on_intros)
apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
@@ -108,8 +108,9 @@
by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
- apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
- apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
+ apply (intro continuous_on_intros) defer
+ apply (intro continuous_on_intros)
+ apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
apply(rule) defer apply rule proof-
fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
@@ -132,10 +133,10 @@
done
show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
- unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
+ unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
- apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
+ apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
by (auto simp add: mult_ac) qed qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 23:14:36 2011 +0200
@@ -7,7 +7,7 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
begin
(* to be moved elsewhere *)
@@ -20,7 +20,7 @@
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
apply(rule member_le_setL2) by auto
-subsection {* General notion of a topologies as values *}
+subsection {* General notion of a topology as a value *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -555,37 +555,61 @@
subsection {* Interior of a Set *}
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+ assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+ shows "x \<in> interior S"
+ using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+ assumes "x \<in> interior S"
+ obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+ using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+ by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+ by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+ by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+ by (intro equalityI interior_subset interior_maximal subset_refl)
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
- apply (simp add: set_eq_iff interior_def)
- apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
- apply (simp add: interior_def)
- apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
- by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
- apply (simp add: interior_def)
- by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+ by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
by (metis interior_maximal interior_subset subset_trans)
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
- apply (rule equalityI, simp)
- apply (metis Int_lower1 Int_lower2 subset_interior)
- by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+ using open_empty by (rule interior_open)
+
+lemma interior_UNIV [simp]: "interior UNIV = UNIV"
+ using open_UNIV by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+ using open_interior by (rule interior_open)
+
+lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+ by (auto simp add: interior_def)
+
+lemma interior_unique:
+ assumes "T \<subseteq> S" and "open T"
+ assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+ shows "interior S = T"
+ by (intro equalityI assms interior_subset open_interior interior_maximal)
+
+lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+ by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
+ Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+ using open_contains_ball_eq [where S="interior S"]
+ by (simp add: open_subset_interior)
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
@@ -599,21 +623,20 @@
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S" and iT: "interior T = {}"
- shows "interior(S \<union> T) = interior S"
+ shows "interior (S \<union> T) = interior S"
proof
- show "interior S \<subseteq> interior (S\<union>T)"
- by (rule subset_interior, blast)
+ show "interior S \<subseteq> interior (S \<union> T)"
+ by (rule interior_mono, rule Un_upper1)
next
show "interior (S \<union> T) \<subseteq> interior S"
proof
fix x assume "x \<in> interior (S \<union> T)"
- then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
- unfolding interior_def by fast
+ then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
show "x \<in> interior S"
proof (rule ccontr)
assume "x \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
- unfolding interior_def set_eq_iff by fast
+ unfolding interior_def by fast
from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +651,16 @@
by (intro Sigma_mono interior_subset)
show "open (interior A \<times> interior B)"
by (intro open_Times open_interior)
- show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
- apply (simp add: open_prod_def, clarify)
- apply (drule (1) bspec, clarify, rename_tac C D)
- apply (simp add: interior_def, rule conjI)
- apply (rule_tac x=C in exI, clarsimp)
- apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
- apply (rule_tac x=D in exI, clarsimp)
- apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
- done
+ fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+ proof (safe)
+ fix x y assume "(x, y) \<in> T"
+ then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+ using `open T` unfolding open_prod_def by fast
+ hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+ using `T \<subseteq> A \<times> B` by auto
+ thus "x \<in> interior A" and "y \<in> interior B"
+ by (auto intro: interiorI)
+ qed
qed
@@ -644,119 +668,50 @@
definition "closure S = S \<union> {x | x. x islimpt S}"
+lemma interior_closure: "interior S = - (closure (- S))"
+ unfolding interior_def closure_def islimpt_def by auto
+
lemma closure_interior: "closure S = - interior (- S)"
-proof-
- { fix x
- have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs")
- proof
- let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
- assume "?lhs"
- hence *:"\<not> ?exT x"
- unfolding interior_def
- by simp
- { assume "\<not> ?rhs"
- hence False using *
- unfolding closure_def islimpt_def
- by blast
- }
- thus "?rhs"
- by blast
- next
- assume "?rhs" thus "?lhs"
- unfolding closure_def interior_def islimpt_def
- by blast
- qed
- }
- thus ?thesis
- by blast
-qed
-
-lemma interior_closure: "interior S = - (closure (- S))"
-proof-
- { fix x
- have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
- unfolding interior_def closure_def islimpt_def
- by auto
- }
- thus ?thesis
- by blast
-qed
+ unfolding interior_closure by simp
lemma closed_closure[simp, intro]: "closed (closure S)"
-proof-
- have "closed (- interior (-S))" by blast
- thus ?thesis using closure_interior[of S] by simp
-qed
+ unfolding closure_interior by (simp add: closed_Compl)
+
+lemma closure_subset: "S \<subseteq> closure S"
+ unfolding closure_def by simp
lemma closure_hull: "closure S = closed hull S"
-proof-
- have "S \<subseteq> closure S"
- unfolding closure_def
- by blast
- moreover
- have "closed (closure S)"
- using closed_closure[of S]
- by assumption
- moreover
- { fix t
- assume *:"S \<subseteq> t" "closed t"
- { fix x
- assume "x islimpt S"
- hence "x islimpt t" using *(1)
- using islimpt_subset[of x, of S, of t]
- by blast
- }
- with * have "closure S \<subseteq> t"
- unfolding closure_def
- using closed_limpt[of t]
- by auto
- }
- ultimately show ?thesis
- using hull_unique[of S, of "closure S", of closed]
- by simp
-qed
+ unfolding hull_def closure_interior interior_def by auto
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
- unfolding closure_hull
- using hull_eq[of closed, OF closed_Inter, of S]
- by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
- using closure_eq[of S]
- by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
- unfolding closure_hull
- using hull_hull[of closed S]
- by assumption
-
-lemma closure_subset: "S \<subseteq> closure S"
- unfolding closure_hull
- using hull_subset[of S closed]
- by assumption
-
-lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
- unfolding closure_hull
- using hull_mono[of S T closed]
- by assumption
-
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
- using hull_minimal[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
- using hull_unique[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
- using closed_empty closure_closed[of "{}"]
- by simp
-
-lemma closure_univ[simp]: "closure UNIV = UNIV"
- using closure_closed[of UNIV]
- by simp
+ unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+ unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
+ unfolding closure_hull by (rule hull_hull)
+
+lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
+ unfolding closure_hull by (rule hull_mono)
+
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
+ unfolding closure_hull by (rule hull_minimal)
+
+lemma closure_unique:
+ assumes "S \<subseteq> T" and "closed T"
+ assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+ shows "closure S = T"
+ using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
+ using closed_empty by (rule closure_closed)
+
+lemma closure_UNIV [simp]: "closure UNIV = UNIV"
+ using closed_UNIV by (rule closure_closed)
+
+lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+ unfolding closure_interior by simp
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
using closure_empty closure_subset[of S]
@@ -797,26 +752,19 @@
by blast
qed
-lemma closure_complement: "closure(- S) = - interior(S)"
-proof-
- have "S = - (- S)"
- by auto
- thus ?thesis
- unfolding closure_interior
- by auto
-qed
-
-lemma interior_complement: "interior(- S) = - closure(S)"
- unfolding closure_interior
- by blast
+lemma closure_complement: "closure (- S) = - interior S"
+ unfolding closure_interior by simp
+
+lemma interior_complement: "interior (- S) = - closure S"
+ unfolding closure_interior by simp
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
show "A \<times> B \<subseteq> closure A \<times> closure B"
by (intro Sigma_mono closure_subset)
show "closed (closure A \<times> closure B)"
by (intro closed_Times closed_closure)
- show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+ fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
apply (simp add: closed_def open_prod_def, clarify)
apply (rule ccontr)
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1090,8 +1038,7 @@
assumes "x \<in> interior S"
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
proof-
- from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
- unfolding interior_def by fast
+ from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2783,8 +2730,8 @@
fixes x :: "'a::t1_space"
shows "closure (insert x s) = insert x (closure s)"
apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
apply (simp add: closure_minimal)
done
@@ -3351,10 +3298,9 @@
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
-unfolding interior_def
-apply simp
-by (meson continuous_on_eq_continuous_at continuous_on_subset)
+ shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+ by (erule interiorE, drule (1) continuous_on_subset,
+ simp add: continuous_on_eq_continuous_at)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3363,56 +3309,41 @@
text {* Characterization of various kinds of continuity in terms of sequences. *}
-(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
lemma continuous_within_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a within s) f \<longleftrightarrow>
(\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
- fix e::real assume "e>0"
- from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
- from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
- hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
- apply(rule_tac x=N in exI) using N d apply auto using x(1)
- apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
- apply(erule_tac x="x n" in ballE) apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
+ { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
+ fix T::"'b set" assume "open T" and "f a \<in> T"
+ with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
+ unfolding continuous_within tendsto_def eventually_within by auto
+ have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
+ using x(2) `d>0` by simp
+ hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
+ proof (rule eventually_elim1)
+ fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+ using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+ qed
}
- thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
+ thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
next
- assume ?rhs
- { fix e::real assume "e>0"
- assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
- hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
- then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
- using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
- { fix d::real assume "d>0"
- hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
- then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
- { fix n::nat assume n:"n\<ge>N"
- hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
- moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
- ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
- hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e" using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
- hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
- }
- thus ?lhs unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
+ assume ?rhs thus ?lhs
+ unfolding continuous_within tendsto_def [where l="f a"]
+ by (simp add: sequentially_imp_eventually_within)
qed
lemma continuous_at_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)"
- using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
+ using continuous_within_sequentially[of a UNIV f]
+ unfolding within_UNIV by auto
lemma continuous_on_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous_on s f \<longleftrightarrow>
(\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3527,16 +3458,10 @@
text{* Same thing for setwise continuity. *}
-lemma continuous_on_const:
- "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_cmul:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_intros)
-
-lemma continuous_on_neg:
+lemma continuous_on_minus:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
@@ -3547,12 +3472,46 @@
\<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_sub:
+lemma continuous_on_diff:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g
\<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
+lemma (in bounded_linear) continuous_on:
+ "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) continuous_on:
+ "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma continuous_on_scaleR:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
+ using bounded_bilinear_scaleR assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_mult:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x * g x)"
+ using bounded_bilinear_mult assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_inner:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
+ using bounded_bilinear_inner assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_euclidean_component:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
+ using bounded_linear_euclidean_component
+ by (rule bounded_linear.continuous_on)
+
text{* Same thing for uniform continuity, using sequential formulations. *}
lemma uniformly_continuous_on_const:
@@ -3796,13 +3755,20 @@
lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
- apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s"
- hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
- thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
- apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
- proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
- thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+ fix x assume "x \<in> interior (f ` s)"
+ then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+ hence "x \<in> f ` s" by auto
+ then obtain y where y: "y \<in> s" "x = f y" by auto
+ have "open (vimage f T)"
+ using assms(1) `open T` by (rule continuous_open_vimage)
+ moreover have "y \<in> vimage f T"
+ using `x = f y` `x \<in> T` by simp
+ moreover have "vimage f T \<subseteq> s"
+ using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+ ultimately have "y \<in> interior s" ..
+ with `x = f y` show "x \<in> f ` interior s" ..
+qed
text {* Equality of continuous functions on closure and related results. *}
@@ -3989,28 +3955,10 @@
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-lemma continuous_on_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s c \<Longrightarrow> continuous_on s f
- ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
- unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemma continuous_on_mul_real:
- fixes f :: "'a::metric_space \<Rightarrow> real"
- fixes g :: "'a::metric_space \<Rightarrow> real"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- ==> continuous_on s (\<lambda>x. f x * g x)"
- using continuous_on_mul[of s f g] unfolding real_scaleR_def .
-
lemmas continuous_on_intros = continuous_on_add continuous_on_const
- continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
- continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
+ continuous_on_id continuous_on_compose continuous_on_minus
+ continuous_on_diff continuous_on_scaleR continuous_on_mult
+ continuous_on_inner continuous_on_euclidean_component
uniformly_continuous_on_add uniformly_continuous_on_const
uniformly_continuous_on_id uniformly_continuous_on_compose
uniformly_continuous_on_cmul uniformly_continuous_on_neg
@@ -4870,13 +4818,15 @@
finally show "closed {a .. b}" .
qed
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
- show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+ show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+ by (rule interior_maximal)
next
- { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
- then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+ { fix x assume "x \<in> interior {a..b}"
+ then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
{ fix i assume i:"i<DIM('a)"
have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4891,7 +4841,7 @@
hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
unfolding basis_component using `e>0` i by auto }
hence "x \<in> {a<..<b}" unfolding mem_interval by auto }
- thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+ thus "?L \<subseteq> ?R" ..
qed
lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"
@@ -5149,21 +5099,12 @@
finally show ?thesis .
qed
-lemma Lim_inner:
- assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
- by (intro tendsto_intros assms)
-
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
unfolding euclidean_component_def by (rule continuous_at_inner)
-lemma continuous_on_inner:
- fixes s :: "'a::real_inner set"
- shows "continuous_on s (inner a)"
- unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
by (simp add: closed_Collect_le)
@@ -5440,8 +5381,7 @@
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
- using assms apply auto
- using continuous_on_cmul[OF continuous_on_id] by auto
+ using assms by (auto simp add: continuous_on_intros)
lemma homeomorphic_translation:
fixes s :: "'a::real_normed_vector set"
@@ -5763,15 +5703,13 @@
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
@@ -6040,19 +5978,4 @@
declare tendsto_const [intro] (* FIXME: move *)
-text {* Legacy theorem names *}
-
-lemmas Lim_ident_at = LIM_ident
-lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
-lemmas Lim_neg = tendsto_minus
-lemmas Lim_add = tendsto_add
-lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = tendsto_scaleR
-lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
-lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
-lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = tendsto_euclidean_component
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
end
--- a/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 23:14:36 2011 +0200
@@ -196,7 +196,11 @@
lemma member_rsp [quot_respect]:
shows "(op \<approx> ===> op =) List.member List.member"
- by (auto intro!: fun_relI simp add: mem_def)
+proof
+ fix x y assume "x \<approx> y"
+ then show "List.member x = List.member y"
+ unfolding fun_eq_iff by simp
+qed
lemma nil_rsp [quot_respect]:
shows "(op \<approx>) Nil Nil"
--- a/src/HOL/SMT.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/SMT.thy Fri Aug 26 23:14:36 2011 +0200
@@ -329,9 +329,24 @@
if_True if_False not_not
lemma [z3_rule]:
+ "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
+ "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
+ "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
+ "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
+ "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
+ "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
+ by auto
+
+lemma [z3_rule]:
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
"(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+ "(True \<longrightarrow> P) = P"
+ "(P \<longrightarrow> True) = True"
+ "(False \<longrightarrow> P) = True"
+ "(P \<longrightarrow> P) = True"
by auto
lemma [z3_rule]:
@@ -339,8 +354,18 @@
by auto
lemma [z3_rule]:
+ "(\<not>True) = False"
+ "(\<not>False) = True"
+ "(x = x) = True"
+ "(P = True) = P"
+ "(True = P) = P"
+ "(P = False) = (\<not>P)"
+ "(False = P) = (\<not>P)"
"((\<not>P) = P) = False"
"(P = (\<not>P)) = False"
+ "((\<not>P) = (\<not>Q)) = (P = Q)"
+ "\<not>(P = (\<not>Q)) = (P = Q)"
+ "\<not>((\<not>P) = Q) = (P = Q)"
"(P \<noteq> Q) = (Q = (\<not>P))"
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
"(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
@@ -351,11 +376,36 @@
"(if \<not>P then \<not>P else P) = True"
"(if P then True else False) = P"
"(if P then False else True) = (\<not>P)"
+ "(if P then Q else True) = ((\<not>P) \<or> Q)"
+ "(if P then Q else True) = (Q \<or> (\<not>P))"
+ "(if P then Q else \<not>Q) = (P = Q)"
+ "(if P then Q else \<not>Q) = (Q = P)"
+ "(if P then \<not>Q else Q) = (P = (\<not>Q))"
+ "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
"(if \<not>P then x else y) = (if P then y else x)"
+ "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
+ "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
+ "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
+ "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
+ "(if P then x else if P then y else z) = (if P then x else z)"
+ "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
+ "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
+ "(if P then x = y else x = z) = (x = (if P then y else z))"
+ "(if P then x = y else y = z) = (y = (if P then x else z))"
+ "(if P then x = y else z = y) = (y = (if P then x else z))"
"f (if P then x else y) = (if P then f x else f y)"
by auto
lemma [z3_rule]:
+ "0 + (x::int) = x"
+ "x + 0 = x"
+ "x + x = 2 * x"
+ "0 * x = 0"
+ "1 * x = x"
+ "x + y = y + x"
+ by auto
+
+lemma [z3_rule]: (* for def-axiom *)
"P = Q \<or> P \<or> Q"
"P = Q \<or> \<not>P \<or> \<not>Q"
"(\<not>P) = Q \<or> \<not>P \<or> Q"
@@ -370,14 +420,18 @@
"P \<or> Q \<or> (\<not>P) \<noteq> Q"
"P \<or> \<not>Q \<or> P \<noteq> Q"
"\<not>P \<or> Q \<or> P \<noteq> Q"
- by auto
-
-lemma [z3_rule]:
- "0 + (x::int) = x"
- "x + 0 = x"
- "0 * x = 0"
- "1 * x = x"
- "x + y = y + x"
+ "P \<or> y = (if P then x else y)"
+ "P \<or> (if P then x else y) = y"
+ "\<not>P \<or> x = (if P then x else y)"
+ "\<not>P \<or> (if P then x else y) = x"
+ "P \<or> R \<or> \<not>(if P then Q else R)"
+ "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
+ "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
+ "\<not>(if P then Q else R) \<or> P \<or> R"
+ "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
+ "(if P then Q else R) \<or> P \<or> \<not>R"
+ "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
+ "(if P then Q else \<not>R) \<or> P \<or> R"
by auto
--- a/src/HOL/Set.thy Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Set.thy Fri Aug 26 23:14:36 2011 +0200
@@ -1378,6 +1378,9 @@
lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
by (fact compl_eq_compl_iff)
+lemma Compl_insert: "- insert x A = (-A) - {x}"
+ by blast
+
text {* \medskip Bounded quantifiers.
The following are not added to the default simpset because
--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 23:14:36 2011 +0200
@@ -19,12 +19,13 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+ datatype tff_flavor = Implicit | Explicit
datatype thf_flavor = Without_Choice | With_Choice
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF |
+ TFF of tff_flavor |
THF of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -50,6 +51,7 @@
val tptp_ho_forall : string
val tptp_exists : string
val tptp_ho_exists : string
+ val tptp_choice : string
val tptp_not : string
val tptp_and : string
val tptp_or : string
@@ -117,12 +119,14 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+datatype tff_flavor = Implicit | Explicit
datatype thf_flavor = Without_Choice | With_Choice
+
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF |
+ TFF of tff_flavor |
THF of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -147,6 +151,7 @@
val tptp_ho_forall = "!!"
val tptp_exists = "?"
val tptp_ho_exists = "??"
+val tptp_choice = "@+"
val tptp_not = "~"
val tptp_and = "&"
val tptp_or = "|"
@@ -197,10 +202,10 @@
fun formula_fold pos f =
let
- fun aux pos (AQuant (_, _, phi)) = aux pos phi
- | aux pos (AConn conn) = aconn_fold pos aux conn
- | aux pos (AAtom tm) = f pos tm
- in aux pos end
+ fun fld pos (AQuant (_, _, phi)) = fld pos phi
+ | fld pos (AConn conn) = aconn_fold pos fld conn
+ | fld pos (AAtom tm) = f pos tm
+ in fld pos end
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
@@ -208,7 +213,7 @@
fun is_format_thf (THF _) = true
| is_format_thf _ = false
-fun is_format_typed TFF = true
+fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
| is_format_typed _ = false
@@ -230,7 +235,7 @@
aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
|> not rhs ? enclose "(" ")"
in aux true ty end
- | string_for_type TFF ty =
+ | string_for_type (TFF _) ty =
(case strip_tff_type ty of
([], s) => s
| ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
@@ -264,13 +269,21 @@
space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
|> is_format_thf format ? enclose "(" ")"
else
- (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
- (true, [AAbs ((s', ty), tm)]) =>
+ (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
+ s = tptp_choice andalso format = THF With_Choice, ts) of
+ (true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
string_for_formula format
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
+ | (_, true, [AAbs ((s', ty), tm)]) =>
+ (*There is code in ATP_Translate to ensure that Eps is always applied
+ to an abstraction*)
+ tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
+ string_for_term format tm ^ ""
+ |> enclose "(" ")"
+
| _ =>
let val ss = map (string_for_term format) ts in
if is_format_thf format then
@@ -310,7 +323,7 @@
fun string_for_format CNF = tptp_cnf
| string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
- | string_for_format TFF = tptp_tff
+ | string_for_format (TFF _) = tptp_tff
| string_for_format (THF _) = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 23:14:36 2011 +0200
@@ -216,11 +216,11 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
- (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
+ [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
+ (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
+ (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
+ [(1.0, (true, (500, FOF, "mono_tags?", method)))]
end}
val e = (eN, e_config)
@@ -293,9 +293,9 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+ [(0.333, (false, (150, FOF, "mono_tags", sosN))),
(0.333, (false, (300, FOF, "poly_tags?", sosN))),
- (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
+ (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -304,8 +304,10 @@
(* Vampire *)
+(* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
+ SystemOnTPTP. *)
fun is_old_vampire_version () =
- string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
+ string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
@@ -324,7 +326,6 @@
[(GaveUp, "UNPROVABLE"),
(GaveUp, "CANNOT PROVE"),
(GaveUp, "SZS status GaveUp"),
- (ProofIncomplete, "predicate_definition_introduction,[]"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
@@ -336,12 +337,12 @@
(* FUDGE *)
(if is_old_vampire_version () then
[(0.333, (false, (150, FOF, "poly_guards", sosN))),
- (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
- (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+ (0.333, (false, (500, FOF, "mono_tags?", sosN))),
+ (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
else
- [(0.333, (false, (150, TFF, "poly_guards", sosN))),
- (0.334, (true, (50, TFF, "simple", no_sosN))),
- (0.333, (false, (500, TFF, "simple", sosN)))])
+ [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
+ (0.333, (false, (500, TFF Implicit, "simple", sosN))),
+ (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -360,16 +361,17 @@
[(GaveUp, "SZS status Satisfiable"),
(GaveUp, "SZS status CounterSatisfiable"),
(GaveUp, "SZS status GaveUp"),
+ (GaveUp, "SZS status Unknown"),
(ProofMissing, "SZS status Unsatisfiable"),
(ProofMissing, "SZS status Theorem")],
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, TFF, "simple", ""))),
- (0.25, (false, (125, TFF, "simple", ""))),
- (0.125, (false, (62, TFF, "simple", ""))),
- (0.125, (false, (31, TFF, "simple", "")))]}
+ K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
+ (0.25, (false, (125, FOF, "mono_guards?", ""))),
+ (0.125, (false, (62, TFF Implicit, "simple", ""))),
+ (0.125, (false, (31, TFF Implicit, "simple", "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -449,7 +451,7 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mangled_tags?") (* FUDGE *))
+ (K (750, FOF, "mono_tags?") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
(K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
@@ -457,26 +459,28 @@
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
(K (100, THF With_Choice, "simple_higher") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
+ remotify_atp vampire "Vampire" ["1.8"]
+ (K (250, TFF Implicit, "simple") (* FUDGE *))
val remote_z3_tptp =
- remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
+ remotify_atp z3_tptp "Z3" ["3.0"]
+ (K (250, TFF Implicit, "simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
+ Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, TFF, "simple") (* FUDGE *))
+ (K (100, TFF Explicit, "simple") (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
+ Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis Hypothesis
- (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
+ (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 23:14:36 2011 +0200
@@ -20,7 +20,7 @@
Chained
datatype order = First_Order | Higher_Order
- datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
@@ -35,6 +35,8 @@
Guards of polymorphism * type_level * type_uniformity |
Tags of polymorphism * type_level * type_uniformity
+ val type_tag_idempotence : bool Config.T
+ val type_tag_arguments : bool Config.T
val no_lambdasN : string
val concealedN : string
val liftingN : string
@@ -114,6 +116,11 @@
type name = string * string
+val type_tag_idempotence =
+ Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
+val type_tag_arguments =
+ Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
+
val no_lambdasN = "no_lambdas"
val concealedN = "concealed"
val liftingN = "lifting"
@@ -141,6 +148,7 @@
val tfree_prefix = "t_"
val const_prefix = "c_"
val type_const_prefix = "tc_"
+val simple_type_prefix = "s_"
val class_prefix = "cl_"
val polymorphic_free_prefix = "poly_free"
@@ -165,11 +173,10 @@
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
-val predicator_name = "p"
-val app_op_name = "a"
-val type_guard_name = "g"
-val type_tag_name = "t"
-val simple_type_prefix = "ty_"
+val predicator_name = "pp"
+val app_op_name = "aa"
+val type_guard_name = "gg"
+val type_tag_name = "tt"
val prefixed_predicator_name = const_prefix ^ predicator_name
val prefixed_app_op_name = const_prefix ^ app_op_name
@@ -308,8 +315,10 @@
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
(* "HOL.eq" is mapped to the ATP's equality. *)
-fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
- | make_fixed_const c = const_prefix ^ lookup_const c
+fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
+ | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
+ tptp_choice
+ | make_fixed_const _ c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
@@ -483,38 +492,38 @@
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
Also accumulates sort infomation. *)
-fun iterm_from_term thy bs (P $ Q) =
+fun iterm_from_term thy format bs (P $ Q) =
let
- val (P', P_atomics_Ts) = iterm_from_term thy bs P
- val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
+ val (P', P_atomics_Ts) = iterm_from_term thy format bs P
+ val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
- | iterm_from_term thy _ (Const (c, T)) =
- (IConst (`make_fixed_const c, T,
+ | iterm_from_term thy format _ (Const (c, T)) =
+ (IConst (`(make_fixed_const (SOME format)) c, T,
if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy),
atyps_of T)
- | iterm_from_term _ _ (Free (s, T)) =
+ | iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
if String.isPrefix polymorphic_free_prefix s then [T] else []),
atyps_of T)
- | iterm_from_term _ _ (Var (v as (s, _), T)) =
+ | iterm_from_term _ format _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val Ts = T |> strip_type |> swap |> op ::
val s' = new_skolem_const_name s (length Ts)
- in IConst (`make_fixed_const s', T, Ts) end
+ in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
else
IVar ((make_schematic_var v, s), T), atyps_of T)
- | iterm_from_term _ bs (Bound j) =
+ | iterm_from_term _ _ bs (Bound j) =
nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
- | iterm_from_term thy bs (Abs (s, T, t)) =
+ | iterm_from_term thy format bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
val name = `make_bound_var s
- val (tm, atomic_Ts) = iterm_from_term thy ((s, (name, T)) :: bs) t
+ val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
datatype locality =
@@ -522,7 +531,7 @@
Chained
datatype order = First_Order | Higher_Order
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
@@ -544,10 +553,10 @@
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
- case try (unprefix "mono_") s of
- SOME s => (SOME Monomorphic, s)
+ case try (unprefix "raw_mono_") s of
+ SOME s => (SOME Raw_Monomorphic, s)
| NONE =>
- case try (unprefix "mangled_") s of
+ case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
||> (fn s =>
@@ -612,7 +621,7 @@
| is_type_level_monotonicity_based _ = false
fun adjust_type_enc (THF _) type_enc = type_enc
- | adjust_type_enc TFF (Simple_Types (_, level)) =
+ | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
Simple_Types (First_Order, level)
| adjust_type_enc format (Simple_Types (_, level)) =
adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
@@ -882,15 +891,20 @@
| _ => IConst (name, T, [])
else
IConst (proxy_base |>> prefix const_prefix, T, T_args)
- | NONE => IConst (name, T, T_args))
+ | NONE => if s = tptp_choice then
+ (*this could be made neater by adding c_Eps as a proxy,
+ but we'd need to be able to "see" Hilbert_Choice.Eps
+ at this level in order to define fEps*)
+ tweak_ho_quant tptp_choice T args
+ else IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
| intro _ _ tm = tm
in intro true [] end
-fun iformula_from_prop thy type_enc eq_as_iff =
+fun iformula_from_prop thy format type_enc eq_as_iff =
let
fun do_term bs t atomic_types =
- iterm_from_term thy bs (Envir.eta_contract t)
+ iterm_from_term thy format bs (Envir.eta_contract t)
|>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q pos s T t' =
@@ -1006,7 +1020,7 @@
fun preprocess_abstractions_in_terms trans_lambdas facts =
let
val (facts, lambda_ts) =
- facts |> map (snd o snd) |> trans_lambdas
+ facts |> map (snd o snd) |> trans_lambdas
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
val lambda_facts =
map2 (fn t => fn j =>
@@ -1041,10 +1055,10 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy type_enc eq_as_iff name loc kind t =
+fun make_formula thy format type_enc eq_as_iff name loc kind t =
let
val (iformula, atomic_types) =
- iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
+ iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
in
{name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
@@ -1052,8 +1066,8 @@
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
- loc Axiom of
+ case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
+ name loc Axiom of
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
@@ -1065,7 +1079,7 @@
fun make_conjecture thy format type_enc =
map (fn ((name, loc), (kind, t)) =>
t |> kind = Conjecture ? s_not_trueprop
- |> make_formula thy type_enc (format <> CNF) name loc kind)
+ |> make_formula thy format type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
@@ -1081,12 +1095,9 @@
val known_infinite_types =
[@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
-fun is_type_surely_infinite' ctxt soundness cached_Ts T =
- (* Unlike virtually any other polymorphic fact whose type variables can be
- instantiated by a known infinite type, extensionality actually encodes a
- cardinality constraints. *)
+fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
soundness <> Sound andalso
- is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
+ is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1097,17 +1108,15 @@
| should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
(Noninf_Nonmono_Types soundness) T =
- exists (type_instance ctxt T orf type_generalization ctxt T)
- maybe_nonmono_Ts andalso
+ exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
not (exists (type_instance ctxt T) surely_infinite_Ts orelse
(not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
- is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
+ is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
maybe_nonmono_Ts, ...}
Fin_Nonmono_Types T =
- exists (type_instance ctxt T orf type_generalization ctxt T)
- maybe_nonmono_Ts andalso
- (exists (type_instance ctxt T) surely_finite_Ts orelse
+ exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+ (exists (type_generalization ctxt T) surely_finite_Ts orelse
(not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
is_type_surely_finite ctxt T))
| should_encode_type _ _ _ _ = false
@@ -1237,15 +1246,16 @@
end
in add true end
fun add_fact_syms_to_table ctxt explicit_apply =
- formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
- |> fact_lift
+ K (add_iterm_syms_to_table ctxt explicit_apply)
+ |> formula_fold NONE |> fact_lift
val tvar_a = TVar (("'a", 0), HOLogic.typeS)
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
- (make_fixed_const @{const_name undefined},
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
+ (* FIXME: needed? *) ::
+ (make_fixed_const NONE @{const_name undefined},
{pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
@@ -1282,7 +1292,7 @@
| NONE => false
val predicator_combconst =
- IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+ IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
fun predicator tm = IApp (predicator_combconst, tm)
fun introduce_predicators_in_iterm sym_tab tm =
@@ -1293,7 +1303,7 @@
fun list_app head args = fold (curry (IApp o swap)) args head
-val app_op = `make_fixed_const app_op_name
+val app_op = `(make_fixed_const NONE) app_op_name
fun explicit_app arg head =
let
@@ -1348,7 +1358,8 @@
| aux arity (IConst (name as (s, _), T, T_args)) =
(case strip_prefix_and_unascii const_prefix s of
NONE =>
- (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
+ (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
+ then [] else T_args)
| SOME s'' =>
let
val s'' = invert_const s''
@@ -1435,7 +1446,7 @@
|> bound_tvars type_enc atomic_Ts
|> close_formula_universally
-val type_tag = `make_fixed_const type_tag_name
+val type_tag = `(make_fixed_const NONE) type_tag_name
fun type_tag_idempotence_fact type_enc =
let
@@ -1449,7 +1460,7 @@
end
fun should_specialize_helper type_enc t =
- polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
+ polymorphism_of_type_enc type_enc <> Polymorphic andalso
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
@@ -1582,7 +1593,7 @@
(conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
end
-val type_guard = `make_fixed_const type_guard_name
+val type_guard = `(make_fixed_const NONE) type_guard_name
fun type_guard_iterm ctxt format type_enc T tm =
IApp (IConst (type_guard, T --> @{typ bool}, [T])
@@ -1661,8 +1672,7 @@
else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
let
val var = ATerm (name, [])
- val tagged_var =
- ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
+ val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
else
NONE
@@ -1779,7 +1789,7 @@
#> fold (add_iterm_syms in_conj) args
end
fun add_fact_syms in_conj =
- fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
+ K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
fun add_formula_var_types (AQuant (_, xs, phi)) =
fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
#> add_formula_var_types phi
@@ -1792,7 +1802,7 @@
fun add_undefined_const T =
let
val (s, s') =
- `make_fixed_const @{const_name undefined}
+ `(make_fixed_const (SOME format)) @{const_name undefined}
|> (case type_arg_policy type_enc @{const_name undefined} of
Mangled_Type_Args _ => mangled_const_name format type_enc [T]
| _ => I)
@@ -1831,8 +1841,8 @@
if exists (type_instance ctxt T) surely_infinite_Ts orelse
member (type_aconv ctxt) maybe_finite_Ts T then
mono
- else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
- T then
+ else if is_type_kind_of_surely_infinite ctxt soundness
+ surely_infinite_Ts T then
{maybe_finite_Ts = maybe_finite_Ts,
surely_finite_Ts = surely_finite_Ts,
maybe_infinite_Ts = maybe_infinite_Ts,
@@ -1875,6 +1885,22 @@
? fold (add_fact_mononotonicity_info ctxt level) facts
end
+fun add_iformula_monotonic_types ctxt mono type_enc =
+ let
+ val level = level_of_type_enc type_enc
+ val should_encode = should_encode_type ctxt mono level
+ fun add_type T = not (should_encode T) ? insert_type ctxt I T
+ fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
+ | add_args _ = I
+ and add_term tm = add_type (ityp_of tm) #> add_args tm
+ in formula_fold NONE (K add_term) end
+fun add_fact_monotonic_types ctxt mono type_enc =
+ add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
+fun monotonic_types_for_facts ctxt mono type_enc facts =
+ [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
+ is_type_level_monotonicity_based (level_of_type_enc type_enc))
+ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
+
fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
Formula (guards_sym_formula_prefix ^
ascii_of (mangled_type format type_enc T),
@@ -1992,7 +2018,8 @@
end
in
[] |> not pred_sym ? add_formula_for_res
- |> fold add_formula_for_arg (ary - 1 downto 0)
+ |> Config.get ctxt type_tag_arguments
+ ? fold add_formula_for_arg (ary - 1 downto 0)
end
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
@@ -2035,17 +2062,9 @@
end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
- sym_decl_tab =
+ mono_Ts sym_decl_tab =
let
val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
- val mono_Ts =
- if polymorphism_of_type_enc type_enc = Polymorphic then
- syms |> maps (map result_type_of_decl o snd)
- |> filter_out (should_encode_type ctxt mono
- (level_of_type_enc type_enc))
- |> rpair [] |-> fold (insert_type ctxt I)
- else
- []
val mono_lines =
problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
val decl_lines =
@@ -2054,11 +2073,12 @@
syms []
in mono_lines @ decl_lines end
-fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+ Config.get ctxt type_tag_idempotence andalso
poly <> Mangled_Monomorphic andalso
((level = All_Types andalso uniformity = Nonuniform) orelse
is_type_level_monotonicity_based level)
- | needs_type_tag_idempotence _ = false
+ | needs_type_tag_idempotence _ _ = false
fun offset_of_heading_in_problem _ [] j = j
| offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -2119,16 +2139,19 @@
val helpers =
repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map repair
+ val mono_Ts =
+ helpers @ conjs @ facts
+ |> monotonic_types_for_facts ctxt mono type_enc
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
- type_enc
+ type_enc mono_Ts
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt format helper_prefix I false true mono
type_enc)
- |> (if needs_type_tag_idempotence type_enc then
+ |> (if needs_type_tag_idempotence ctxt type_enc then
cons (type_tag_idempotence_fact type_enc)
else
I)
@@ -2153,7 +2176,7 @@
CNF => ensure_cnf_problem
| CNF_UEQ => filter_cnf_ueq_problem
| _ => I)
- |> (if is_format_typed format then
+ |> (if is_format_typed format andalso format <> TFF Implicit then
declare_undeclared_syms_in_atp_problem type_decl_prefix
implicit_declsN
else
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 23:14:36 2011 +0200
@@ -17,6 +17,7 @@
val string_from_time : Time.time -> string
val type_instance : Proof.context -> typ -> typ -> bool
val type_generalization : Proof.context -> typ -> typ -> bool
+ val type_intersect : Proof.context -> typ -> typ -> bool
val type_aconv : Proof.context -> typ * typ -> bool
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
@@ -117,6 +118,8 @@
fun type_instance ctxt T T' =
Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
fun type_generalization ctxt T T' = type_instance ctxt T' T
+fun type_intersect ctxt T T' =
+ type_instance ctxt T T' orelse type_generalization ctxt T T'
fun type_aconv ctxt (T, T') =
type_instance ctxt T T' andalso type_instance ctxt T' T
@@ -158,16 +161,14 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt inst_tvars assigns default_card T =
+fun tiny_card_of_type ctxt sound assigns default_card T =
let
val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
- val type_cmp =
- if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
fun aux slack avoid T =
if member (op =) avoid T then
0
- else case AList.lookup type_cmp assigns T of
+ else case AList.lookup (type_aconv ctxt) assigns T of
SOME k => k
| NONE =>
case T of
@@ -215,13 +216,14 @@
(* Very slightly unsound: Type variables are assumed not to be
constrained to cardinality 1. (In practice, the user would most
likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
+ | TFree _ =>
+ if not sound andalso default_card = 1 then 2 else default_card
| TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
-fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
- tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0
+fun is_type_surely_infinite ctxt sound infinite_Ts T =
+ tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Aug 26 23:14:36 2011 +0200
@@ -9,14 +9,16 @@
signature METIS_RECONSTRUCT =
sig
+ type type_enc = ATP_Translate.type_enc
+
exception METIS of string * string
val hol_clause_from_metis :
- Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
- -> term
+ Proof.context -> type_enc -> int Symtab.table -> (string * term) list
+ -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val replay_one_inference :
- Proof.context -> (string * term) list -> int Symtab.table
+ Proof.context -> type_enc -> (string * term) list -> int Symtab.table
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -33,38 +35,39 @@
exception METIS of string * string
-fun atp_name_from_metis s =
- case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
+fun atp_name_from_metis type_enc s =
+ case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
SOME ((s, _), (_, swap)) => (s, swap)
| _ => (s, false)
-fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
- let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
- ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
+fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
+ let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
+ ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
end
- | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
+ | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
-fun hol_term_from_metis ctxt sym_tab =
- atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
+fun hol_term_from_metis ctxt type_enc sym_tab =
+ atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
-fun atp_literal_from_metis (pos, atom) =
- atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
- | atp_clause_from_metis lits =
- lits |> map atp_literal_from_metis |> mk_aconns AOr
+fun atp_literal_from_metis type_enc (pos, atom) =
+ atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
+ |> AAtom |> not pos ? mk_anot
+fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
+ | atp_clause_from_metis type_enc lits =
+ lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
fun reveal_old_skolems_and_infer_types ctxt old_skolems =
map (reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-fun hol_clause_from_metis ctxt sym_tab old_skolems =
+fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
Metis_Thm.clause
#> Metis_LiteralSet.toList
- #> atp_clause_from_metis
+ #> atp_clause_from_metis type_enc
#> prop_from_atp ctxt false sym_tab
#> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
-fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
- let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
+fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
+ let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -111,10 +114,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
in cterm_instantiate substs th end;
-fun assume_inference ctxt old_skolems sym_tab atom =
+fun assume_inference ctxt type_enc old_skolems sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+ (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -122,7 +125,7 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
let val thy = Proof_Context.theory_of ctxt
val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -130,7 +133,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolems_and_infer_types" below. *)
- val t = hol_term_from_metis ctxt sym_tab y
+ val t = hol_term_from_metis ctxt type_enc sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -255,7 +258,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 =
let
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
@@ -271,7 +274,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+ singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -300,10 +303,11 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inference ctxt old_skolems sym_tab t =
+fun refl_inference ctxt type_enc old_skolems sym_tab t =
let
val thy = Proof_Context.theory_of ctxt
- val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
+ val i_t =
+ singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -313,11 +317,11 @@
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
-fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atom
val [i_atom, i_tm] =
- hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
+ hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -336,7 +340,8 @@
#> the #> unmangled_const_name))
in
if s = metis_predicator orelse s = predicator_name orelse
- s = metis_type_tag orelse s = type_tag_name then
+ s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
+ orelse s = type_tag_name then
path_finder tm ps (nth ts p)
else if s = metis_app_op orelse s = app_op_name then
let
@@ -377,21 +382,22 @@
val factor = Seq.hd o distinct_subgoals_tac
-fun one_step ctxt old_skolems sym_tab th_pairs p =
+fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
| (_, Metis_Proof.Assume f_atom) =>
- assume_inference ctxt old_skolems sym_tab f_atom
+ assume_inference ctxt type_enc old_skolems sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
+ inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
|> factor
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
- resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
+ resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
+ f_th2
|> factor
| (_, Metis_Proof.Refl f_tm) =>
- refl_inference ctxt old_skolems sym_tab f_tm
+ refl_inference ctxt type_enc old_skolems sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
+ equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -443,7 +449,8 @@
end
end
-fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
+fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
+ th_pairs =
if not (null th_pairs) andalso
prop_of (snd (hd th_pairs)) aconv @{prop False} then
(* Isabelle sometimes identifies literals (premises) that are distinct in
@@ -458,7 +465,7 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
+ val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Aug 26 23:14:36 2011 +0200
@@ -39,7 +39,7 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_enc = "mangled_tags_uniform"
+val really_full_type_enc = "mono_tags_uniform"
val full_type_enc = "poly_guards_uniform_query"
val partial_type_enc = "poly_args"
val no_type_enc = "erased"
@@ -74,9 +74,9 @@
"t => t'", where "t" and "t'" are the same term modulo type tags.
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt sym_tab old_skolems mth of
+ case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -91,14 +91,7 @@
fun clause_params type_enc =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals =
- (* Type axioms seem to benefit from the positive literal order, but for
- compatibility we keep the unsigned order for Metis's default
- "partial_types" mode. *)
- if is_type_enc_fairly_sound type_enc then
- Metis_Clause.PositiveLiteralOrder
- else
- Metis_Clause.UnsignedLiteralOrder,
+ orderLiterals = Metis_Clause.UnsignedLiteralOrder,
orderTerms = true}
fun active_params type_enc =
{clause = clause_params type_enc,
@@ -133,7 +126,7 @@
val (sym_tab, axioms, old_skolems) =
prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
+ reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
@@ -155,7 +148,7 @@
val proof = Metis_Proof.proof mth
val result =
axioms
- |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
+ |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
val used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Aug 26 23:14:36 2011 +0200
@@ -18,13 +18,14 @@
val metis_equal : string
val metis_predicator : string
val metis_app_op : string
- val metis_type_tag : string
+ val metis_systematic_type_tag : string
+ val metis_ad_hoc_type_tag : string
val metis_generated_var_prefix : string
val trace : bool Config.T
val verbose : bool Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose_warning : Proof.context -> string -> unit
- val metis_name_table : ((string * int) * (string * bool)) list
+ val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
Proof.context -> type_enc -> thm list -> thm list
@@ -39,8 +40,10 @@
val metis_equal = "="
val metis_predicator = "{}"
-val metis_app_op = "."
-val metis_type_tag = ":"
+val metis_app_op = Metis_Name.toString Metis_Term.appName
+val metis_systematic_type_tag =
+ Metis_Name.toString Metis_Term.hasTypeFunctionName
+val metis_ad_hoc_type_tag = "**"
val metis_generated_var_prefix = "_"
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
@@ -51,11 +54,13 @@
if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
val metis_name_table =
- [((tptp_equal, 2), (metis_equal, false)),
- ((tptp_old_equal, 2), (metis_equal, false)),
- ((prefixed_predicator_name, 1), (metis_predicator, false)),
- ((prefixed_app_op_name, 2), (metis_app_op, false)),
- ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
+ [((tptp_equal, 2), (K metis_equal, false)),
+ ((tptp_old_equal, 2), (K metis_equal, false)),
+ ((prefixed_predicator_name, 1), (K metis_predicator, false)),
+ ((prefixed_app_op_name, 2), (K metis_app_op, false)),
+ ((prefixed_type_tag_name, 2),
+ (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
+ | _ => metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^
@@ -114,32 +119,34 @@
val prepare_helper =
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
-fun metis_term_from_atp (ATerm (s, tms)) =
+fun metis_term_from_atp type_enc (ATerm (s, tms)) =
if is_tptp_variable s then
Metis_Term.Var (Metis_Name.fromString s)
else
- let
- val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
- |> the_default (s, false)
- in
- Metis_Term.Fn (Metis_Name.fromString s,
- tms |> map metis_term_from_atp |> swap ? rev)
- end
-fun metis_atom_from_atp (AAtom tm) =
- (case metis_term_from_atp tm of
+ (case AList.lookup (op =) metis_name_table (s, length tms) of
+ SOME (f, swap) => (f type_enc, swap)
+ | NONE => (s, false))
+ |> (fn (s, swap) =>
+ Metis_Term.Fn (Metis_Name.fromString s,
+ tms |> map (metis_term_from_atp type_enc)
+ |> swap ? rev))
+fun metis_atom_from_atp type_enc (AAtom tm) =
+ (case metis_term_from_atp type_enc tm of
Metis_Term.Fn x => x
| _ => raise Fail "non CNF -- expected function")
- | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
-fun metis_literal_from_atp (AConn (ANot, [phi])) =
- (false, metis_atom_from_atp phi)
- | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
-fun metis_literals_from_atp (AConn (AOr, phis)) =
- maps metis_literals_from_atp phis
- | metis_literals_from_atp phi = [metis_literal_from_atp phi]
-fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
+ | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
+ (false, metis_atom_from_atp type_enc phi)
+ | metis_literal_from_atp type_enc phi =
+ (true, metis_atom_from_atp type_enc phi)
+fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
+ maps (metis_literals_from_atp type_enc) phis
+ | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
+fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
let
fun some isa =
- SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+ SOME (phi |> metis_literals_from_atp type_enc
+ |> Metis_LiteralSet.fromList
|> Metis_Thm.axiom, isa)
in
if ident = type_tag_idempotence_helper_name orelse
@@ -164,7 +171,7 @@
in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
| NONE => TrueI |> Isa_Raw |> some
end
- | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
+ | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
@@ -205,8 +212,8 @@
*)
(* "rev" is for compatibility. *)
val axioms =
- atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
- |> rev
+ atp_problem
+ |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
in (sym_tab, axioms, old_skolems) end
end;
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Fri Aug 26 23:14:36 2011 +0200
@@ -152,16 +152,14 @@
fun prep (ct, vars) (maxidx, all_vars) =
let
- val maxidx' = maxidx_of ct + maxidx + 1
+ val maxidx' = maxidx + maxidx_of ct + 1
fun part (v as (i, cv)) =
(case AList.lookup (op =) all_vars i of
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
| NONE =>
- if not (exists (equal_var cv) all_vars) then apsnd (cons v)
- else
- let val cv' = Thm.incr_indexes_cterm maxidx' cv
- in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
+ let val cv' = Thm.incr_indexes_cterm maxidx cv
+ in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
val (inst, vars') =
if null vars then ([], vars)
@@ -170,7 +168,7 @@
in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
in
fun mk_fun f ts =
- let val (cts, (_, vars)) = fold_map prep ts (~1, [])
+ let val (cts, (_, vars)) = fold_map prep ts (0, [])
in f cts |> Option.map (rpair vars) end
end
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 26 23:14:36 2011 +0200
@@ -147,13 +147,15 @@
val remove_weight = mk_meta_eq @{thm SMT.weight_def}
val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
- fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
- (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
+ fun rewrite_conv _ [] = Conv.all_conv
+ | rewrite_conv ctxt eqs = Simplifier.full_rewrite
+ (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
remove_fun_app, Z3_Proof_Literals.rewrite_true]
- fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+ fun rewrite _ [] = I
+ | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
@@ -630,7 +632,8 @@
in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
val sk_rules = @{lemma
- "(EX x. P x) = P (SOME x. P x)" "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
+ "c = (SOME x. P x) ==> (EX x. P x) = P c"
+ "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
by (metis someI_ex)+}
in
@@ -638,9 +641,10 @@
apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
fun discharge_sk_tac i st = (
- Tactic.rtac @{thm trans}
- THEN' Tactic.resolve_tac sk_rules
- THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
+ Tactic.rtac @{thm trans} i
+ THEN Tactic.resolve_tac sk_rules i
+ THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+ THEN Tactic.rtac @{thm refl} i) st
end
@@ -654,7 +658,7 @@
Z3_Proof_Tools.by_tac (
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
ORELSE' NAMED ctxt' "simp+arith" (
- Simplifier.simp_tac simpset
+ Simplifier.asm_full_simp_tac simpset
THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
@@ -717,13 +721,15 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
@@ -731,7 +737,8 @@
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 26 23:14:36 2011 +0200
@@ -148,7 +148,7 @@
| _ => value)
| NONE => (name, value)
-(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
+(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
correctly. *)
fun implode_param [s, "?"] = s ^ "?"
| implode_param [s, "!"] = s ^ "!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 22:25:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 23:14:36 2011 +0200
@@ -536,6 +536,11 @@
#> Config.put Monomorph.max_new_instances max_new_instances
#> Config.put Monomorph.keep_partial_instances false
+fun suffix_for_mode Auto_Try = "_auto_try"
+ | suffix_for_mode Try = "_try"
+ | suffix_for_mode Normal = ""
+ | suffix_for_mode Minimize = "_min"
+
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
Linux appears to be the only ATP that does not honor its time limit. *)
val atp_timeout_slack = seconds 1.0
@@ -557,7 +562,7 @@
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
val problem_file_name =
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
- "_" ^ string_of_int subgoal)
+ suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
val problem_path_name =
if dest_dir = "" then
File.tmp_path problem_file_name