# HG changeset patch # User wenzelm # Date 1314393276 -7200 # Node ID 534d7ee2644ac96fe4ec33165c9eea55036c6e16 # Parent 5e681762d53896849d2d2b0cc438147a9c8464b9# Parent 2f0a34fc4d2d62642be449330a2f54e5c53fb539 merged diff -r 2f0a34fc4d2d -r 534d7ee2644a NEWS --- 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 *** diff -r 2f0a34fc4d2d -r 534d7ee2644a doc-src/Sledgehammer/sledgehammer.tex --- 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. diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Hoare_Parallel/OG_Hoare.thy --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/IsaMakefile --- 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 \ diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Library/Extended_Real.thy --- 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 \ limsup Y" using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto -declare trivial_limit_sequentially[simp] - lemma fixes X :: "nat \ ereal" shows ereal_incseq_uminus[simp]: "incseq (\i. - X i) = decseq X" diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Lim.thy --- 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 "\f. (\n. f n \ s \ f n \ a) \ f ----> a \ + eventually (\n. P (f n)) sequentially" + shows "eventually P (at a within s)" +proof (rule ccontr) + let ?I = "\n. inverse (real (Suc n))" + def F \ "\n::nat. SOME x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" + assume "\ eventually P (at a within s)" + hence P: "\d>0. \x. x \ s \ x \ a \ dist x a < d \ \ P x" + unfolding Limits.eventually_within Limits.eventually_at by fast + hence "\n. \x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" by simp + hence F: "\n. F n \ s \ F n \ a \ dist (F n) a < ?I n \ \ P (F n)" + unfolding F_def by (rule someI_ex) + hence F0: "\n. F n \ s" and F1: "\n. F n \ a" + and F2: "\n. dist (F n) a < ?I n" and F3: "\n. \ 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 (\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 "\f. (\n. f n \ a) \ f ----> a \ + eventually (\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 \ 'b::topological_space" assumes f: "f -- a --> l" shows "\S. (\n. S n \ a) \ S ----> a \ (\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 "\S. (\n. S n \ a) \ S ----> a \ eventually (\x. P (S x)) sequentially" - shows "eventually P (at a)" -proof (rule ccontr) - let ?I = "\n. inverse (real (Suc n))" - let ?F = "\n::nat. SOME x. x \ a \ dist x a < ?I n \ \ P x" - assume "\ eventually P (at a)" - hence P: "\d>0. \x. x \ a \ dist x a < d \ \ P x" - unfolding eventually_at by simp - hence "\n. \x. x \ a \ dist x a < ?I n \ \ P x" by simp - hence F: "\n. ?F n \ a \ dist (?F n) a < ?I n \ \ P (?F n)" - by (rule someI_ex) - hence F1: "\n. ?F n \ a" - and F2: "\n. dist (?F n) a < ?I n" - and F3: "\n. \ 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 "\n. ?F n \ a" - by (rule allI) (rule F1) - ultimately have "eventually (\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 \ 'b::topological_space" assumes "\S. (\n. S n \ a) \ S ----> a \ (\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: "(\S. (\n. S n \ a) \ S ----> (a::'a::metric_space) \ (\n. X (S n)) ----> L) = diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/List.thy --- 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 \ acc r \ xs \ acc (listrel1 r) \ (x # xs) \ 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 *} diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Metis_Examples/Proxies.thy --- 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 "\ 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 \ 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 \ 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 \ P False \ 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 (\ a) \ \ 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 (\ \ a) \ 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 (\ (id (\ a))) \ 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 \ b) \ 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 \ b) \ 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 \ id b \ id (a \ 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 \ id (a \ 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 \ id (a \ 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 (\ a) \ id (\ b) \ id (\ (a \ 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 (\ a) \ id (a \ 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 \ b) \ id (\ a \ 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Metis_Examples/Type_Encodings.thy --- 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 = diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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; diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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\ (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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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) \ 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) \ closure ((op *\<^sub>R c) ` S)" + using bounded_linear_scaleR_right + by (rule closure_bounded_linear_image) + show "closure ((op *\<^sub>R c) ` S) \ (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 = "\(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y" + let ?T = "{0..1::real} \ (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 \ {}`] + 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 \ 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 \ {}" shows "\y\s. \x\(convex hull s). norm(x - a) \ 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 \ (\x\(convex hull s). \y\s. norm(x - a) \ 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 \ {}" shows "\u\s. \v\s. \x\convex hull s. \y \ convex hull s. norm(x - y) \ 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 \ x \ convex hull s \ y \ convex hull s \ (\u\s. \v\s. norm(x - y) \ 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 \ s" +lemma homeomorphic_convex_compact_lemma: + fixes s :: "('a::euclidean_space) set" + assumes "convex s" and "compact s" and "cball 0 1 \ 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 \ s" "0 \ u" "u < (1::real)" - hence "u *\<^sub>R x \ 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) \ 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 \ 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 \ s" and "0 \ u" and "u < (1::real)" + have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball) + moreover have "u *\<^sub>R x \ 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) \ s" + proof + fix y assume "y \ 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) \ 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) \ s" .. + with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \ s" + using `x \ s` `0 \ u` `u < 1` [THEN less_imp_le] by (rule mem_convex) + thus "y \ s" using `u < 1` by simp + qed + ultimately have "u *\<^sub>R x \ interior s" .. thus "u *\<^sub>R x \ 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 \ b" "continuous_on {a .. b} f" "(f b)$$k \ y" "y \ (f a)$$k" shows "\x\{a..b}. (f x)$$k = y" apply(subst neg_equal_iff_equal[THEN sym]) - using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] using assms using continuous_on_neg - by auto + using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] + using assms using continuous_on_minus by auto lemma ivt_decreasing_component_1: fixes f::"real \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f @@ -4042,7 +4064,7 @@ then obtain y where "y\s" and y:"norm (y - x) * (1 - e) < e * d" by auto def z \ "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\interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format]) + have "z\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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "\x\{a<..xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" apply(rule rolle[OF assms(1), of "\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 \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\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 \ ?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) diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- 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 "\i. i < DIM('a) \ x $$ i = y $$ i" shows "x = y" proof - from assms have "\i sqprojection \ ?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" diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ y1) \ interior(x1) \ interior(x1 \ y1) \ interior(y1) \ interior(x2 \ y2) \ interior(x2) \ interior(x2 \ y2) \ interior(y2) \ interior(x1 \ y1) \ interior(x2 \ y2) = {}" by auto - show "interior k1 \ interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior) + show "interior k1 \ 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 \ p2)" using d1(1) d2(1) by auto show "\(p1 \ p2) = s1 \ s2" using d1(6) d2(6) by auto { fix k1 k2 assume as:"k1 \ p1 \ p2" "k2 \ p1 \ p2" "k1 \ k2" moreover let ?g="interior k1 \ interior k2 = {}" - { assume as:"k1\p1" "k2\p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]] + { assume as:"k1\p1" "k2\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\p2" "k2\p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]] + { assume as:"k1\p2" "k2\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 \ p1 \ p2" show "k \ s1 \ s2" using k d1(2) d2(2) by auto @@ -573,7 +573,7 @@ show "finite (q k - {k})" "open (interior k)" "\t\q k - {k}. \a b. t = {a..b}" using qk by auto show "\t\q k - {k}. interior k \ interior t = {}" using qk(5) using q(2)[OF k] by auto have *:"\x s. x \ s \ \s \ x" by auto show "interior (\(\i. \(q i - {i})) ` p) \ interior (\(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 \ 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)\p1\p2" show "x\k" "\a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto show "k\s1\s2" using xk p1(3) p2(3) by blast fix x' k' assume xk':"(x',k')\p1\p2" "(x,k) \ (x',k')" - have *:"\a b. a\ s1 \ b\ s2 \ interior a \ interior b = {}" using assms(3) subset_interior by blast + have *:"\a b. a\ s1 \ b\ s2 \ interior a \ interior b = {}" using assms(3) interior_mono by blast show "interior k \ interior k' = {}" apply(cases "(x,k)\p1", case_tac[!] "(x',k')\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\k" "\a b. k = {a..b}" "k \ \iset" using assm(2-4)[OF i] using i(1) by auto fix x' k' assume xk':"(x',k')\\pfn ` iset" "(x, k) \ (x', k')" then obtain i' where i':"i' \ iset" "(x', k') \ pfn i'" by auto have *:"\a b. i\i' \ a\ i \ b\ i' \ interior a \ 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 \ 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 + (\\ i. if i = k then e/2 else 0) \ {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 "\ < 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} \ snd ` p" "{u..v} \ snd ` p" "{m..n} \ {u..v}" "{m..n} \ {x. \x $$ k - c\ \ d} = {u..v} \ {x. \x $$ k - c\ \ d}" have "({m..n} \ {x. \x $$ k - c\ \ d}) \ ({u..v} \ {x. \x $$ k - c\ \ d}) \ {m..n} \ {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} \ {x. \x $$ k - c\ \ d}) = {}" unfolding as Int_absorb by auto thus "content ({m..n} \ {x. \x $$ k - c\ \ 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) \ p" "( a, k') \ p" "content k \ 0" "content k' \ 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} \ k \ k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter] + have "{ a <..< ?v} \ k \ k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter] moreover have " ((a + ?v)/2) \ { a <..< ?v}" using k(3-) unfolding v v' content_eq_0 not_le by(auto simp add:not_le) ultimately have " ((a + ?v)/2) \ interior k \ interior k'" unfolding interior_open[OF open_interval] by auto @@ -3528,7 +3528,7 @@ proof- fix x k k' assume k:"( b, k) \ p" "( b, k') \ p" "content k \ 0" "content k' \ 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} \ k \ k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter] + have "{?v <..< b} \ k \ k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter] moreover have " ((b + ?v)/2) \ {?v <..< b}" using k(3-) unfolding v v' content_eq_0 not_le by auto ultimately have " ((b + ?v)/2) \ interior k \ 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\snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto hence "l\q" "k\q" "l\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 \ k`] by blast + note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \ 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 ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x)) @@ -4403,7 +4403,7 @@ have *:"interior (k \ 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 (\i. x^i) {0 .. n} = (1 - x^(Suc n))" +proof- + def y \ "1 - x" + have "y * (\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 \ 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 = (\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 "\ n < m" hence nm: "m \ n" by arith + {assume x: "x = 1" hence ?thesis by simp} + moreover + {assume x: "x \ 1" hence nz: "1 - x \ 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 \ 'n::ordered_euclidean_space \ real" diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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) \ (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) ==> \c\ * 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 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" - by (rule order_trans [OF norm_triangle_ineq add_mono]) - -lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \ b == a - b \ 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 \ norm x \ 0 \ n \ norm x" - by atomize auto - -lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith - -lemma norm_pths: - fixes x :: "'a::real_normed_vector" shows - "x = y \ norm (x - y) \ 0" - "x \ y \ \ (norm (x - y) \ 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 \ norm (y - x2) < e / 2 \ 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 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e" - by norm - lemma setsum_clauses: shows "setsum f {} = 0" and "finite S \ 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 \ setsum f S \ y = setsum (\x. f x \ y) S " - apply(induct rule: finite_induct) by(auto simp add: inner_add) - -lemma dot_rsum: "finite S \ y \ setsum f S = setsum (\x. y \ f x) S " - apply(induct rule: finite_induct) by(auto simp add: inner_add) - lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" proof assume "\x. x \ y = x \ z" @@ -702,65 +576,6 @@ then show ?thesis by blast qed -subsection {* Geometric progression *} - -lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\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\1" - hence x1': "x - 1 \ 0" "1 - x \ 0" "x - 1 = - (1 - x)" "- (1 - x) \ 0" by auto - from geometric_sum[OF x1, of "Suc n", unfolded x1'] - have "(- (1 - x)) * setsum (\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 \ 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 = (\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 "\ n < m" hence nm: "m \ n" by arith - {assume x: "x = 1" hence ?thesis by simp} - moreover - {assume x: "x \ 1" hence nz: "1 - x \ 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 \ subspace S \ 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 \ 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 \ subspace B ==> subspace (A \ B)" by (simp add: subspace_def) +lemma subspace_Times: "\subspace A; subspace B\ \ subspace (A \ B)" + unfolding subspace_def zero_prod_def by simp + +text {* Properties of span. *} + lemma (in real_vector) span_mono: "A \ B ==> span A \ 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: "\x. x \ S ==> x \ P" - and P: "subspace P" and x: "x \ span S" shows "x \ P" +lemma span_unique: + "\S \ T; subspace T; \T'. \S \ T'; subspace T'\ \ T \ T'\ \ span S = T" + unfolding span_def by (rule hull_unique) + +lemma span_minimal: "S \ T \ subspace T \ span S \ T" + unfolding span_def by (rule hull_minimal) + +lemma (in real_vector) span_induct: + assumes x: "x \ span S" and P: "subspace P" and SP: "\x. x \ S ==> x \ P" + shows "x \ P" proof- from SP have SP': "S \ 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 \ B \ A \ 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 \ span (f ` S)" - have "x \ 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 \ span S" - have "x \ {x. f x \ 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 \ span (f ` S)" by simp - } - ultimately show ?thesis by blast +proof (rule span_unique) + show "f ` S \ 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 \ T" and "subspace T" thus "f ` span S \ T" + unfolding image_subset_iff_subset_vimage + by (intro span_minimal subspace_linear_vimage lf) +qed + +lemma span_union: "span (A \ B) = (\(a, b). a + b) ` (span A \ span B)" +proof (rule span_unique) + show "A \ B \ (\(a, b). a + b) ` (span A \ span B)" + by safe (force intro: span_clauses)+ +next + have "linear (\(a, b). a + b)" + by (simp add: linear_def scaleR_add_right) + moreover have "subspace (span A \ span B)" + by (intro subspace_Times subspace_span) + ultimately show "subspace ((\(a, b). a + b) ` (span A \ span B))" + by (rule subspace_linear_image) +next + fix T assume "A \ B \ T" and "subspace T" + thus "(\(a, b). a + b) ` (span A \ span B) \ T" + by (auto intro!: subspace_add elim: span_induct) qed text {* The key breakdown property. *} +lemma span_singleton: "span {x} = range (\k. k *\<^sub>R x)" +proof (rule span_unique) + show "{x} \ range (\k. k *\<^sub>R x)" + by (fast intro: scaleR_one [symmetric]) + show "subspace (range (\k. k *\<^sub>R x))" + unfolding subspace_def + by (auto intro: scaleR_add_left [symmetric]) + fix T assume "{x} \ T" and "subspace T" thus "range (\k. k *\<^sub>R x) \ T" + unfolding subspace_def by auto +qed + +lemma span_insert: + "span (insert a S) = {x. \k. (x - k *\<^sub>R a) \ span S}" +proof - + have "span ({a} \ S) = {x. \k. (x - k *\<^sub>R a) \ 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 \ S" and aS: "a \ span S" - shows "\k. a - k *\<^sub>R b \ span (S - {b})" (is "?P a") -proof- - {fix x assume xS: "x \ 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 \ b" - then have "?P x" using xS - apply - - apply (rule exI[where x=0]) - apply (rule span_superset) - by simp} - ultimately have "x \ 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 \ Collect ?P" using aS by (rule span_induct) - thus "?P a" by simp -qed + shows "\k. a - k *\<^sub>R b \ span (S - {b})" + using assms span_insert [of b "S - {b}"] + by (simp add: insert_absorb) lemma span_breakdown_eq: - "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" (is "?lhs \ ?rhs") -proof- - {assume x: "x \ 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 \ 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 \ 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 \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" + by (simp add: span_insert) text {* Hence some "reversal" results. *} @@ -1122,26 +924,16 @@ text {* Transitivity property. *} +lemma span_redundant: "x \ span S \ span (insert x S) = span S" + unfolding span_def by (rule hull_redundant) + lemma span_trans: assumes x: "x \ span S" and y: "y \ span (insert x S)" shows "y \ span S" -proof- - from span_breakdown[of x "insert x S" y, OF insertI1 y] - obtain k where k: "y -k*\<^sub>R x \ 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 \ B) \ A = A" "(A \ B) \ B = B" by auto - -lemma span_union: "span (A \ B) = (\(a, b). a + b) ` (span A \ span B)" -proof safe - fix x assume "x \ span (A \ B)" - then obtain S u where S: "finite S" "S \ A \ B" and x: "x = (\v\S. u v *\<^sub>R v)" - unfolding span_explicit by auto - - let ?Sa = "\v\S\A. u v *\<^sub>R v" - let ?Sb = "(\v\S\(B - A). u v *\<^sub>R v)" - show "x \ (\(a, b). a + b) ` (span A \ span B)" - proof - show "x = (case (?Sa, ?Sb) of (a, b) \ a + b)" - unfolding x using S - by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) - - from S have "?Sa \ span A" unfolding span_explicit - by (auto intro!: exI[of _ "S \ A"]) - moreover from S have "?Sb \ span B" unfolding span_explicit - by (auto intro!: exI[of _ "S \ (B - A)"]) - ultimately show "(?Sa, ?Sb) \ span A \ span B" by simp - qed -next - fix a b assume "a \ span A" and "b \ span B" - then obtain Sa ua Sb ub where span: - "finite Sa" "Sa \ A" "a = (\v\Sa. ua v *\<^sub>R v)" - "finite Sb" "Sb \ B" "b = (\v\Sb. ub v *\<^sub>R v)" - unfolding span_explicit by auto - let "?u v" = "(if v \ Sa then ua v else 0) + (if v \ Sb then ub v else 0)" - from span have "finite (Sa \ Sb)" "Sa \ Sb \ A \ B" - and "a + b = (\v\(Sa\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 \ span (A \ 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 "\d. \ 0 < d; basis ` {d..} = {0::'a::euclidean_space}; - independent (basis ` {.. 'a) {.. \ 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 "\i. i < d \ basis i \ 0" - assumes "\i. d \ i \ basis i = 0" - shows "DIM('a) = d" -proof (rule linorder_cases [of "DIM('a)" d]) - assume "DIM('a) < d" - hence "basis DIM('a) \ 0" by (rule assms) - thus ?thesis by simp -next - assume "d < DIM('a)" - hence "basis d \ 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 ` {.. y \ (\i < DIM('a). x $$ i \ y $$ i)" - and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" - -lemma eucl_less_not_refl[simp, intro!]: "\ 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 \ y < z \ x < z" - and "x \ y \ y < z \ x < z" - and "x \ y \ y \ z \ x \ 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) \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" unfolding inner_simps by auto +lemma pairwise_orthogonal_insert: + assumes "pairwise orthogonal S" + assumes "\y. y \ S \ 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 "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \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 \ ?C" and yC: "y \ ?C" and xy: "x \ 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 \ ?a" "y \ 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 \ ?a" "x \ 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 \ C" and ya: "y \ 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 \ 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 \ 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 \ 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 \ y \ (\i < DIM('a). x $$ i \ y $$ i)" + and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" + +lemma eucl_less_not_refl[simp, intro!]: "\ 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 \ y < z \ x < z" + and "x \ y \ y < z \ x < z" + and "x \ y \ y \ z \ x \ 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 \ '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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Norm_Arith.thy --- /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) ==> \c\ * 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 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" + by (rule order_trans [OF norm_triangle_ineq add_mono]) + +lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \ b == a - b \ 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 \ norm x \ 0 \ n \ norm x" + by atomize auto + +lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith + +lemma norm_pths: + fixes x :: "'a::real_normed_vector" shows + "x = y \ norm (x - y) \ 0" + "x \ y \ \ (norm (x - y) \ 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 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e" + by norm + +end diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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) \ path g" proof- have *:"\g. path g \ path(reversepath g)" unfolding path_def reversepath_def apply(rule continuous_on_compose[unfolded o_def, of _ "\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 \ 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 \ 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 _ "\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 \ (\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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 L {} \ (\S T. L S \ L T \ L (S \ T)) \ (\K. Ball K L \ L (\ K))" typedef (open) 'a topology = "{L::('a set) \ bool. istopology L}" @@ -555,37 +555,61 @@ subsection {* Interior of a Set *} -definition "interior S = {x. \T. open T \ x \ T \ T \ S}" +definition "interior S = \{T. open T \ T \ S}" + +lemma interiorI [intro?]: + assumes "open T" and "x \ T" and "T \ S" + shows "x \ interior S" + using assms unfolding interior_def by fast + +lemma interiorE [elim?]: + assumes "x \ interior S" + obtains T where "open T" and "x \ T" and "T \ 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 \ S" + by (auto simp add: interior_def) + +lemma interior_maximal: "T \ S \ open T \ T \ interior S" + by (auto simp add: interior_def) + +lemma interior_open: "open S \ interior S = S" + by (intro equalityI interior_subset interior_maximal subset_refl) lemma interior_eq: "interior S = S \ 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 \ S" by (auto simp add: interior_def) -lemma subset_interior: "S \ T ==> (interior S) \ (interior T)" by (auto simp add: interior_def) -lemma interior_maximal: "T \ S \ open T ==> T \ (interior S)" by (auto simp add: interior_def) -lemma interior_unique: "T \ S \ open T \ (\T'. T' \ S \ open T' \ T' \ T) \ interior S = T" - by (metis equalityI interior_maximal interior_subset open_interior) -lemma mem_interior: "x \ interior S \ (\e. 0 < e \ ball x e \ 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 \ interior T \ S \ T" + by (metis open_interior interior_open) + +lemma open_subset_interior: "open S \ S \ interior T \ S \ T" by (metis interior_maximal interior_subset subset_trans) -lemma interior_inter[simp]: "interior(S \ T) = interior S \ 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 \ T \ interior S \ interior T" + by (auto simp add: interior_def) + +lemma interior_unique: + assumes "T \ S" and "open T" + assumes "\T'. T' \ S \ open T' \ T' \ T" + shows "interior S = T" + by (intro equalityI assms interior_subset open_interior interior_maximal) + +lemma interior_inter [simp]: "interior (S \ T) = interior S \ 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 \ interior S \ (\e>0. ball x e \ 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 \ T) = interior S" + shows "interior (S \ T) = interior S" proof - show "interior S \ interior (S\T)" - by (rule subset_interior, blast) + show "interior S \ interior (S \ T)" + by (rule interior_mono, rule Un_upper1) next show "interior (S \ T) \ interior S" proof fix x assume "x \ interior (S \ T)" - then obtain R where "open R" "x \ R" "R \ S \ T" - unfolding interior_def by fast + then obtain R where "open R" "x \ R" "R \ S \ T" .. show "x \ interior S" proof (rule ccontr) assume "x \ interior S" with `x \ R` `open R` obtain y where "y \ 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 \ S \ T` have "R - S \ T" by fast from `y \ R - S` `open (R - S)` `R - S \ T` `interior T = {}` @@ -628,15 +651,16 @@ by (intro Sigma_mono interior_subset) show "open (interior A \ interior B)" by (intro open_Times open_interior) - show "\T. T \ A \ B \ open T \ T \ interior A \ 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 \ A \ B" and "open T" thus "T \ interior A \ interior B" + proof (safe) + fix x y assume "(x, y) \ T" + then obtain C D where "open C" "open D" "C \ D \ T" "x \ C" "y \ D" + using `open T` unfolding open_prod_def by fast + hence "open C" "open D" "C \ A" "D \ B" "x \ C" "y \ D" + using `T \ A \ B` by auto + thus "x \ interior A" and "y \ interior B" + by (auto intro: interiorI) + qed qed @@ -644,119 +668,50 @@ definition "closure S = S \ {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\- interior (- S) \ x \ closure S" (is "?lhs = ?rhs") - proof - let ?exT = "\ y. (\T. open T \ y \ T \ T \ - S)" - assume "?lhs" - hence *:"\ ?exT x" - unfolding interior_def - by simp - { assume "\ ?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 \ interior S \ x \ - (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 \ closure S" + unfolding closure_def by simp lemma closure_hull: "closure S = closed hull S" -proof- - have "S \ closure S" - unfolding closure_def - by blast - moreover - have "closed (closure S)" - using closed_closure[of S] - by assumption - moreover - { fix t - assume *:"S \ 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 \ 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 \ closed S" - unfolding closure_hull - using hull_eq[of closed, OF closed_Inter, of S] - by metis - -lemma closure_closed[simp]: "closed S \ 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 \ closure S" - unfolding closure_hull - using hull_subset[of S closed] - by assumption - -lemma subset_closure: "S \ T \ closure S \ closure T" - unfolding closure_hull - using hull_mono[of S T closed] - by assumption - -lemma closure_minimal: "S \ T \ closed T \ closure S \ T" - using hull_minimal[of S T closed] - unfolding closure_hull - by simp - -lemma closure_unique: "S \ T \ closed T \ (\ T'. S \ T' \ closed T' \ T \ T') \ 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 \ 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 \ T \ closure S \ closure T" + unfolding closure_hull by (rule hull_mono) + +lemma closure_minimal: "S \ T \ closed T \ closure S \ T" + unfolding closure_hull by (rule hull_minimal) + +lemma closure_unique: + assumes "S \ T" and "closed T" + assumes "\T'. S \ T' \ closed T' \ T \ 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 \ T) = closure S \ closure T" + unfolding closure_interior by simp lemma closure_eq_empty: "closure S = {} \ 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 \ B) = closure A \ closure B" -proof (intro closure_unique conjI) +proof (rule closure_unique) show "A \ B \ closure A \ closure B" by (intro Sigma_mono closure_subset) show "closed (closure A \ closure B)" by (intro closed_Times closed_closure) - show "\T. A \ B \ T \ closed T \ closure A \ closure B \ T" + fix T assume "A \ B \ T" and "closed T" thus "closure A \ closure B \ 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 \ interior S" shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") proof- - from assms obtain T where T: "open T" "x \ T" "T \ S" - unfolding interior_def by fast + from assms obtain T where T: "open T" "x \ T" "T \ S" .. { assume "?lhs" then obtain A where "open A" "x \ A" "\y\A. y \ x \ y \ S \ 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 \ x \ 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 \ x \ interior s \ continuous (at x) f" + by (erule interiorE, drule (1) continuous_on_subset, + simp add: continuous_on_eq_continuous_at) lemma continuous_on_eq: "(\x \ s. f x = g x) \ continuous_on s f \ continuous_on s g" @@ -3363,56 +3309,41 @@ text {* Characterization of various kinds of continuity in terms of sequences. *} -(* \ could be generalized, but \ requires metric space *) lemma continuous_within_sequentially: - fixes f :: "'a::metric_space \ 'b::metric_space" + fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a within s) f \ (\x. (\n::nat. x n \ s) \ (x ---> a) sequentially --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs - { fix x::"nat \ 'a" assume x:"\n. x n \ s" "\e>0. \N. \n\N. dist (x n) a < e" - fix e::real assume "e>0" - from `?lhs` obtain d where "d>0" and d:"\x\s. 0 < dist x a \ dist x a < d \ 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:"\n\N. dist (x n) a < d" by auto - hence "\N. \n\N. dist ((f \ 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 \ 'a" assume x:"\n. x n \ s" "\e>0. eventually (\n. dist (x n) a < e) sequentially" + fix T::"'b set" assume "open T" and "f a \ T" + with `?lhs` obtain d where "d>0" and d:"\x\s. 0 < dist x a \ dist x a < d \ f x \ T" + unfolding continuous_within tendsto_def eventually_within by auto + have "eventually (\n. dist (x n) a < d) sequentially" + using x(2) `d>0` by simp + hence "eventually (\n. (f \ x) n \ T) sequentially" + proof (rule eventually_elim1) + fix n assume "dist (x n) a < d" thus "(f \ x) n \ T" + using d x(1) `f a \ 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 "\ (\d>0. \x\s. 0 < dist x a \ dist x a < d \ dist (f x) (f a) < e)" - hence "\d. \x. d>0 \ x\s \ (0 < dist x a \ dist x a < d \ \ dist (f x) (f a) < e)" by blast - then obtain x where x:"\d>0. x d \ s \ (0 < dist (x d) a \ dist (x d) a < d \ \ dist (f (x d)) (f a) < e)" - using choice[of "\d x.0 x\s \ (0 < dist x a \ dist x a < d \ \ dist (f x) (f a) < e)"] by auto - { fix d::real assume "d>0" - hence "\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\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 "\N::nat. \n\N. dist (x (inverse (real (n + 1)))) a < d" by auto - } - hence "(\n::nat. x (inverse (real (n + 1))) \ s) \ (\e>0. \N::nat. \n\N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto - hence "\e>0. \N::nat. \n\N. dist (f (x (inverse (real (n + 1))))) (f a) < e" using `?rhs`[THEN spec[where x="\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 \ 'b::metric_space" + fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a) f \ (\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 \ 'b::metric_space" + fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (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 (\x. c)" +lemma continuous_on_const: "continuous_on s (\x. c)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma continuous_on_cmul: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "continuous_on s f \ continuous_on s (\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 \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s (\x. - f x)" unfolding continuous_on_def by (auto intro: tendsto_intros) @@ -3547,12 +3472,46 @@ \ continuous_on s (\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 \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" unfolding continuous_on_def by (auto intro: tendsto_intros) +lemma (in bounded_linear) continuous_on: + "continuous_on s g \ continuous_on s (\x. f (g x))" + unfolding continuous_on_def by (fast intro: tendsto) + +lemma (in bounded_bilinear) continuous_on: + "\continuous_on s f; continuous_on s g\ \ continuous_on s (\x. f x ** g x)" + unfolding continuous_on_def by (fast intro: tendsto) + +lemma continuous_on_scaleR: + fixes g :: "'a::topological_space \ 'b::real_normed_vector" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ 'b::real_normed_algebra" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ 'b::real_inner" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ continuous_on s (\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 "\x. continuous (at x) f" "inj f" shows "interior (f ` s) \ f ` (interior s)" - apply rule unfolding interior_def mem_Collect_eq image_iff apply safe -proof- fix x T assume as:"open T" "x \ T" "T \ f ` s" - hence "x \ f ` s" by auto then guess y unfolding image_iff .. note y=this - thus "\xa\{x. \T. open T \ x \ T \ T \ s}. x = f xa" apply(rule_tac x=y in bexI) using assms as - apply safe apply(rule_tac x="{x. f x \ T}" in exI) apply(safe,rule continuous_open_preimage_univ) - proof- fix x assume "f x \ T" hence "f x \ f ` s" using as by auto - thus "x \ s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed +proof + fix x assume "x \ interior (f ` s)" + then obtain T where as: "open T" "x \ T" "T \ f ` s" .. + hence "x \ f ` s" by auto + then obtain y where y: "y \ s" "x = f y" by auto + have "open (vimage f T)" + using assms(1) `open T` by (rule continuous_open_vimage) + moreover have "y \ vimage f T" + using `x = f y` `x \ T` by simp + moreover have "vimage f T \ s" + using `T \ image f s` `inj f` unfolding inj_on_def subset_eq by auto + ultimately have "y \ interior s" .. + with `x = f y` show "x \ 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 \ real" and v :: "'b::real_normed_vector" - shows "continuous_on s c ==> continuous_on s (\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 \ real" - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "continuous_on s c \ continuous_on s f - ==> continuous_on s (\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 \ real" - fixes g :: "'a::metric_space \ real" - shows "continuous_on s f \ continuous_on s g - ==> continuous_on s (\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<.. ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto + show "?R \ ?L" using interval_open_subset_closed open_interval + by (rule interior_maximal) next - { fix x assume "\T. open T \ x \ T \ T \ {a..b}" - then obtain s where s:"open s" "x \ s" "s \ {a..b}" by auto + { fix x assume "x \ interior {a..b}" + then obtain s where s:"open s" "x \ s" "s \ {a..b}" .. then obtain e where "e>0" and e:"\x'. dist x' x < e \ x' \ {a..b}" unfolding open_dist and subset_eq by auto { fix i assume i:"iR 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 \ {a<.. ?R" unfolding interior_def and subset_eq by auto + thus "?L \ ?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 "((\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) (\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 \ b}" by (simp add: closed_Collect_le) @@ -5440,8 +5381,7 @@ unfolding homeomorphic_minimal apply(rule_tac x="\x. c *\<^sub>R x" in exI) apply(rule_tac x="\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 \ y" "y \ m *\<^sub>R b + c" hence "y \ (\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 \ y" "y \ m *\<^sub>R a + c" "m < 0" hence "y \ (\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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Quotient_Examples/FSet.thy --- 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 \ ===> op =) List.member List.member" - by (auto intro!: fun_relI simp add: mem_def) +proof + fix x y assume "x \ y" + then show "List.member x = List.member y" + unfolding fun_eq_iff by simp +qed lemma nil_rsp [quot_respect]: shows "(op \) Nil Nil" diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/SMT.thy --- 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 \ Q) = (\(\P \ \Q))" + "(P \ Q) = (\(\Q \ \P))" + "(\P \ Q) = (\(P \ \Q))" + "(\P \ Q) = (\(\Q \ P))" + "(P \ \Q) = (\(\P \ Q))" + "(P \ \Q) = (\(Q \ \P))" + "(\P \ \Q) = (\(P \ Q))" + "(\P \ \Q) = (\(Q \ P))" + by auto + +lemma [z3_rule]: "(P \ Q) = (Q \ \P)" "(\P \ Q) = (P \ Q)" "(\P \ Q) = (Q \ P)" + "(True \ P) = P" + "(P \ True) = True" + "(False \ P) = True" + "(P \ P) = True" by auto lemma [z3_rule]: @@ -339,8 +354,18 @@ by auto lemma [z3_rule]: + "(\True) = False" + "(\False) = True" + "(x = x) = True" + "(P = True) = P" + "(True = P) = P" + "(P = False) = (\P)" + "(False = P) = (\P)" "((\P) = P) = False" "(P = (\P)) = False" + "((\P) = (\Q)) = (P = Q)" + "\(P = (\Q)) = (P = Q)" + "\((\P) = Q) = (P = Q)" "(P \ Q) = (Q = (\P))" "(P = Q) = ((\P \ Q) \ (P \ \Q))" "(P \ Q) = ((\P \ \Q) \ (P \ Q))" @@ -351,11 +376,36 @@ "(if \P then \P else P) = True" "(if P then True else False) = P" "(if P then False else True) = (\P)" + "(if P then Q else True) = ((\P) \ Q)" + "(if P then Q else True) = (Q \ (\P))" + "(if P then Q else \Q) = (P = Q)" + "(if P then Q else \Q) = (Q = P)" + "(if P then \Q else Q) = (P = (\Q))" + "(if P then \Q else Q) = ((\Q) = P)" "(if \P then x else y) = (if P then y else x)" + "(if P then (if Q then x else y) else x) = (if P \ (\Q) then y else x)" + "(if P then (if Q then x else y) else x) = (if (\Q) \ P then y else x)" + "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" + "(if P then (if Q then x else y) else y) = (if Q \ 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 \ Q then x else y)" + "(if P then x else if Q then x else y) = (if Q \ 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 \ P \ Q" "P = Q \ \P \ \Q" "(\P) = Q \ \P \ Q" @@ -370,14 +420,18 @@ "P \ Q \ (\P) \ Q" "P \ \Q \ P \ Q" "\P \ Q \ P \ Q" - by auto - -lemma [z3_rule]: - "0 + (x::int) = x" - "x + 0 = x" - "0 * x = 0" - "1 * x = x" - "x + y = y + x" + "P \ y = (if P then x else y)" + "P \ (if P then x else y) = y" + "\P \ x = (if P then x else y)" + "\P \ (if P then x else y) = x" + "P \ R \ \(if P then Q else R)" + "\P \ Q \ \(if P then Q else R)" + "\(if P then Q else R) \ \P \ Q" + "\(if P then Q else R) \ P \ R" + "(if P then Q else R) \ \P \ \Q" + "(if P then Q else R) \ P \ \R" + "(if P then \Q else R) \ \P \ Q" + "(if P then Q else \R) \ P \ R" by auto diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Set.thy --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/ATP/atp_problem.ML --- 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)) = diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/ATP/atp_systems.ML --- 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 *) diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/ATP/atp_util.ML --- 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. *) diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/Metis/metis_tactics.ML --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/Metis/metis_translate.ML --- 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; diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/SMT/z3_proof_parser.ML --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 ^ "!" diff -r 2f0a34fc4d2d -r 534d7ee2644a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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