--- a/src/Doc/Sledgehammer/document/root.tex Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jul 08 08:42:36 2021 +0200
@@ -457,8 +457,8 @@
\textit{full\_types} option to \textit{metis} directly.
-\point{And what are the \textit{lifting} and \textit{hide\_lams} \\ arguments
-to Metis?}
+\point{And what are the \textit{lifting} and \textit{opaque\_lifting} \\
+arguments to Metis?}
Orthogonally to the encoding of types, it is important to choose an appropriate
translation of $\lambda$-abstractions. Metis supports three translation
@@ -614,7 +614,7 @@
with the same semantics as Sledgehammer's \textit{type\_enc} option
(\S\ref{problem-encoding}).
%
-The supported $\lambda$ translation schemes are \textit{hide\_lams},
+The supported $\lambda$ translation schemes are \textit{opaque\_lifting},
\textit{lifting}, and \textit{combs} (the default).
%
All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
@@ -975,9 +975,9 @@
translation schemes are listed below:
\begin{enum}
-\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
-by replacing them by unspecified fresh constants, effectively disabling all
-reasoning under $\lambda$-abstractions.
+\item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Hide the
+$\lambda$-abstractions by replacing them by unspecified fresh constants,
+effectively disabling all reasoning under $\lambda$-abstractions.
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
--- a/src/HOL/Algebra/Coset.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Coset.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1387,7 +1387,7 @@
moreover
have "y = f x \<otimes>\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y)"
using x y
- by (metis (no_types, hide_lams) assms(5) f group.inv_solve_left group.subgroup_self hom_carrier image_subset_iff subgroup_def that)
+ by (metis (no_types, opaque_lifting) assms(5) f group.inv_solve_left group.subgroup_self hom_carrier image_subset_iff subgroup_def that)
ultimately
show ?thesis
using x y by force
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy Thu Jul 08 08:42:36 2021 +0200
@@ -242,7 +242,7 @@
lemma sum_closed_free_Abelian_group:
"(\<And>i. i \<in> I \<Longrightarrow> x i \<in> carrier (free_Abelian_group S)) \<Longrightarrow> sum x I \<in> carrier (free_Abelian_group S)"
apply (induction I rule: infinite_finite_induct, auto)
- by (metis (no_types, hide_lams) UnE subsetCE keys_add)
+ by (metis (no_types, opaque_lifting) UnE subsetCE keys_add)
lemma (in comm_group) free_Abelian_group_universal:
--- a/src/HOL/Algebra/Generated_Groups.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy Thu Jul 08 08:42:36 2021 +0200
@@ -572,11 +572,11 @@
lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S"
proof -
have *: "\<And>A. carrier G \<inter> A \<subseteq> carrier (subgroup_generated (subgroup_generated G A) A)"
- by (metis (no_types, hide_lams) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff)
+ by (metis (no_types, opaque_lifting) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff)
show ?thesis
apply (auto intro!: monoid.equality)
using group.carrier_subgroup_generated_subset group_subgroup_generated apply blast
- apply (metis (no_types, hide_lams) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal
+ apply (metis (no_types, opaque_lifting) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal
subgroup_generated_restrict subgroup_subgroup_generated_iff subset_eq)
apply (simp add: subgroup_generated_def)
done
--- a/src/HOL/Algebra/Group.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Group.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1120,7 +1120,7 @@
have "(\<phi> \<one>) \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (\<phi> \<one>) \<otimes>\<^bsub>H\<^esub> (\<phi> \<one>)"
by (metis assms(2) image_eqI monoid.r_one one_closed phi_hom r_one surj(1))
thus ?thesis
- by (metis (no_types, hide_lams) Units_eq Units_one_closed assms(2) f_inv_into_f imageI
+ by (metis (no_types, opaque_lifting) Units_eq Units_one_closed assms(2) f_inv_into_f imageI
monoid.l_one monoid.one_closed phi_hom psi_def r_one surj)
qed
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1176,7 +1176,7 @@
from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
by simp
then obtain a b where p: "p = [ a, b ]"
- by (metis (no_types, hide_lams) Suc_length_conv length_0_conv)
+ by (metis (no_types, opaque_lifting) Suc_length_conv length_0_conv)
hence "a \<in> K - { \<zero> }" "b \<in> K" and in_carrier: "a \<in> carrier R" "b \<in> carrier R"
using assms(2) subfieldE(3)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
hence inv_a: "inv a \<in> carrier R" "a \<otimes> inv a = \<one>" and "inv a \<in> K"
--- a/src/HOL/Algebra/Product_Groups.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Product_Groups.thy Thu Jul 08 08:42:36 2021 +0200
@@ -468,7 +468,7 @@
using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
with x show "?g \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
- by (metis (no_types, hide_lams) iso_iff f inv_into_into)
+ by (metis (no_types, opaque_lifting) iso_iff f inv_into_into)
qed
qed
qed
--- a/src/HOL/Algebra/Subrings.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Subrings.thy Thu Jul 08 08:42:36 2021 +0200
@@ -357,7 +357,7 @@
using k' A(3) subring_props(6) by auto
thus "a \<in> K"
using m_assoc[of "inv k" k a] A(2) inv_k subring_props(1)
- by (metis (no_types, hide_lams) A(1) Diff_iff l_one subsetCE)
+ by (metis (no_types, opaque_lifting) A(1) Diff_iff l_one subsetCE)
qed
lemma (in ring) subfield_iff:
--- a/src/HOL/Analysis/Abstract_Topology.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2117,7 +2117,7 @@
proof (intro conjI ballI allI impI)
show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
using assms unfolding quotient_map_def
- by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
+ by (metis (no_types, opaque_lifting) continuous_map_image_subset_topspace image_comp image_subset_iff)
next
fix U'' :: "'c set"
assume U'': "openin X'' U''"
@@ -3802,7 +3802,7 @@
lemma section_imp_injective_map:
"\<lbrakk>section_map X Y f; x \<in> topspace X; y \<in> topspace X\<rbrakk> \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
- by (metis (mono_tags, hide_lams) retraction_maps_def section_map_def)
+ by (metis (mono_tags, opaque_lifting) retraction_maps_def section_map_def)
lemma retraction_maps_to_retract_maps:
"retraction_maps X Y r s
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1334,7 +1334,7 @@
lemma homeomorphic_path_connected_space_imp:
"\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
- by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
+ by (metis (no_types, opaque_lifting) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
lemma homeomorphic_path_connected_space:
"X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y"
@@ -1351,7 +1351,7 @@
assume "U \<subseteq> topspace X"
show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
using assms unfolding homeomorphic_eq_everything_map
- by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
+ by (metis (no_types, opaque_lifting) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
qed
lemma homeomorphic_map_path_connectedness_eq:
@@ -1525,7 +1525,7 @@
next
case False
then show ?thesis
- by (metis (no_types, hide_lams) Union_connected_components_of ccpo_Sup_singleton
+ by (metis (no_types, opaque_lifting) Union_connected_components_of ccpo_Sup_singleton
connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD
subsetI subset_singleton_iff)
qed
--- a/src/HOL/Analysis/Arcwise_Connected.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1792,7 +1792,7 @@
by (metis dist_norm dist_triangle_half_r order_less_irrefl)
qed (auto simp: open_segment_commute)
show ?thesis
- unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
+ unfolding \<phi>_def by (metis (no_types, opaque_lifting) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
qed
show "closed {0..1::real}" by auto
qed (meson \<phi>_def)
@@ -1950,7 +1950,7 @@
then have "arc g"
by (metis arc_def path_def inj_on_def)
obtain u v where "u \<in> {0..1}" "a = g u" "v \<in> {0..1}" "b = g v"
- by (metis (mono_tags, hide_lams) \<open>\<phi> T\<close> \<phi>_def a b fhim gfeq h_eq_p imageI path_image_def pathfinish_def pathfinish_in_path_image pathstart_def pathstart_in_path_image)
+ by (metis (mono_tags, opaque_lifting) \<open>\<phi> T\<close> \<phi>_def a b fhim gfeq h_eq_p imageI path_image_def pathfinish_def pathfinish_in_path_image pathstart_def pathstart_in_path_image)
then have "a \<in> path_image g" "b \<in> path_image g"
using path_image_def by blast+
have ph: "path_image h \<subseteq> path_image p"
@@ -2003,7 +2003,7 @@
assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \<noteq> pathfinish h"
obtains i where "arc i" "path_image i \<subseteq> path_image g \<union> path_image h"
"pathstart i = pathstart g" "pathfinish i = pathfinish h"
- by (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
+ by (metis (no_types, opaque_lifting) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
--- a/src/HOL/Analysis/Bochner_Integration.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Jul 08 08:42:36 2021 +0200
@@ -513,7 +513,7 @@
by (auto intro!: simple_bochner_integral_eq_nn_integral)
also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)"
by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
- (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
+ (metis (erased, opaque_lifting) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
norm_minus_commute norm_triangle_ineq4 order_refl)
also have "\<dots> = ?S + ?T"
by (rule nn_integral_add) auto
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2054,7 +2054,7 @@
show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
apply (auto simp: h_def algebra_simps)
apply (simp add: vector_add_divide_simps notga)
- by (metis (no_types, hide_lams) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq)
+ by (metis (no_types, opaque_lifting) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq)
qed
ultimately show False by simp
qed
--- a/src/HOL/Analysis/Cartesian_Space.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1158,7 +1158,7 @@
"orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
unfolding orthogonal_transformation
apply (auto simp: linear_0 isometry_linear)
- apply (metis (no_types, hide_lams) dist_norm linear_diff)
+ apply (metis (no_types, opaque_lifting) dist_norm linear_diff)
by (metis dist_0_norm)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 08 08:42:36 2021 +0200
@@ -198,7 +198,7 @@
by simp
have "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar>
= \<bar>prod m UNIV\<bar> * \<bar>z - measure lebesgue S\<bar>"
- by (metis (no_types, hide_lams) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
+ by (metis (no_types, opaque_lifting) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
also have "\<dots> < e"
using zless True by (simp add: field_simps)
finally show "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e" .
@@ -563,7 +563,7 @@
by (simp add: bounded_plus [OF bo])
moreover have "?rfs \<subseteq> ?B"
apply (auto simp: dist_norm image_iff dest!: ex_lessK)
- by (metis (no_types, hide_lams) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
+ by (metis (no_types, opaque_lifting) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
ultimately show "bounded (?rfs)"
by (rule bounded_subset)
qed
@@ -764,7 +764,7 @@
fix x
assume "e > 0" "m < n" "n * e \<le> \<bar>det (matrix (f' x))\<bar>" "\<bar>det (matrix (f' x))\<bar> < (1 + real m) * e"
then have "n < 1 + real m"
- by (metis (no_types, hide_lams) less_le_trans mult.commute not_le mult_le_cancel_iff2)
+ by (metis (no_types, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_iff2)
then show "False"
using less.hyps by linarith
qed
@@ -1402,7 +1402,7 @@
have *: "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = b * \<bar>inv T y $ k - ?x' $ k\<bar>" for y
proof -
have "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = \<bar>(b *\<^sub>R axis k 1) \<bullet> inv T (y - x)\<bar>"
- by (metis (no_types, hide_lams) b_def eqb invT orthogonal_transformation_def v)
+ by (metis (no_types, opaque_lifting) b_def eqb invT orthogonal_transformation_def v)
also have "\<dots> = b * \<bar>(axis k 1) \<bullet> inv T (y - x)\<bar>"
using \<open>b > 0\<close> by (simp add: abs_mult)
also have "\<dots> = b * \<bar>inv T y $ k - ?x' $ k\<bar>"
@@ -1480,7 +1480,7 @@
(\<forall>y\<in>S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x))"
(is "\<forall>e>0. \<exists>d>0. \<exists>A. ?\<Phi> e d A")
then have "\<forall>k. \<exists>d>0. \<exists>A. ?\<Phi> (1 / Suc k) d A"
- by (metis (no_types, hide_lams) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
+ by (metis (no_types, opaque_lifting) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
then obtain \<delta> A where \<delta>: "\<And>k. \<delta> k > 0"
and Ab: "\<And>k. A k $ m $ n < b"
and A: "\<And>k y. \<lbrakk>y \<in> S; norm (y - x) < \<delta> k\<rbrakk> \<Longrightarrow>
@@ -1997,7 +1997,7 @@
proof
have "T (inv T x - inv T t) = x - t"
using T linear_diff orthogonal_transformation_def
- by (metis (no_types, hide_lams) Tinv)
+ by (metis (no_types, opaque_lifting) Tinv)
then have "norm (inv T x - inv T t) = norm (x - t)"
by (metis T orthogonal_transformation_norm)
then show "norm (inv T x - inv T t) \<le> e"
@@ -2180,7 +2180,7 @@
using r12 by auto
ultimately have "norm (v - u) \<le> 1"
using norm_triangle_half_r [of x u 1 v]
- by (metis (no_types, hide_lams) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball)
+ by (metis (no_types, opaque_lifting) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball)
then have "norm (v - u) ^ ?n \<le> norm (v - u) ^ ?m"
by (simp add: power_decreasing [OF mlen])
also have "\<dots> \<le> ?\<mu> K * real (?m ^ ?m)"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1146,7 +1146,7 @@
proof (cases w rule: complex_split_polar)
case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
apply (simp add: norm_mult cmod_unit_one)
- by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
+ by (metis (no_types, opaque_lifting) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Analytic properties of tangent function\<close>
@@ -1333,7 +1333,7 @@
then have "\<And>y. y \<in> V \<Longrightarrow> g' y = inv ((*) y)"
by (metis exp_Ln g' g_eq_Ln)
then have g': "g' z = (\<lambda>x. x/z)"
- by (metis (no_types, hide_lams) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
+ by (metis (no_types, opaque_lifting) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
show "(g has_derivative (*) (inverse z)) (at z)"
using g [OF \<open>z \<in> V\<close>] g'
by (simp add: \<open>z \<in> V\<close> field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative)
@@ -3986,7 +3986,7 @@
also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
by simp
also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
- by (metis (mono_tags, hide_lams) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq)
+ by (metis (mono_tags, opaque_lifting) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq)
also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
also have "... \<longleftrightarrow> j mod n = k mod n"
--- a/src/HOL/Analysis/Connected.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Connected.thy Thu Jul 08 08:42:36 2021 +0200
@@ -240,7 +240,7 @@
\<Longrightarrow> connected_component_set S x = connected_component_set S y"
apply (simp add: ex_in_conv [symmetric])
apply (rule connected_component_eq)
-by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
+by (metis (no_types, opaque_lifting) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
@@ -335,7 +335,7 @@
by simp
lemma connected_eq_connected_components_eq: "connected s \<longleftrightarrow> (\<forall>c \<in> components s. \<forall>c' \<in> components s. c = c')"
- by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)
+ by (metis (no_types, opaque_lifting) components_iff connected_component_eq_eq connected_iff_connected_component)
lemma components_eq_sing_iff: "components s = {s} \<longleftrightarrow> connected s \<and> s \<noteq> {}"
apply (rule iffI)
--- a/src/HOL/Analysis/Cross3.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Cross3.thy Thu Jul 08 08:42:36 2021 +0200
@@ -141,7 +141,7 @@
using norm_cross [of x y] by (auto simp: power_mult_distrib)
also have "... \<longleftrightarrow> \<bar>x \<bullet> y\<bar> = norm x * norm y"
using power2_eq_iff
- by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def)
+ by (metis (mono_tags, opaque_lifting) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def)
also have "... \<longleftrightarrow> collinear {0, x, y}"
by (rule norm_cauchy_schwarz_equal)
finally show ?thesis .
--- a/src/HOL/Analysis/Derivative.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Derivative.thy Thu Jul 08 08:42:36 2021 +0200
@@ -3243,7 +3243,7 @@
apply (rule Limits.continuous_on_scaleR, assumption)
by (metis (mono_tags, lifting) continuous_at_imp_continuous_on continuous_on_compose continuous_on_cong differentiable_imp_continuous_within o_def)
show "\<And>x. x \<in> S \<Longrightarrow> vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)) = vector_derivative (g \<circ> f) (at x)"
- by (metis (mono_tags, hide_lams) C1_differentiable_on_eq fg imageI vector_derivative_chain_at)
+ by (metis (mono_tags, opaque_lifting) C1_differentiable_on_eq fg imageI vector_derivative_chain_at)
qed
ultimately show ?thesis
by (simp add: C1_differentiable_on_eq)
--- a/src/HOL/Analysis/Determinants.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Determinants.thy Thu Jul 08 08:42:36 2021 +0200
@@ -238,7 +238,7 @@
proof (unfold inj_on_def, auto)
fix x y assume x: "x permutes ?U" and even_x: "evenperm x"
and y: "y permutes ?U" and even_y: "evenperm y" and eq: "?t_jk \<circ> x = ?t_jk \<circ> y"
- show "x = y" by (metis (hide_lams, no_types) comp_assoc eq id_comp swap_id_idempotent)
+ show "x = y" by (metis (opaque_lifting, no_types) comp_assoc eq id_comp swap_id_idempotent)
qed
have tjk_permutes: "?t_jk permutes ?U"
by (auto simp add: permutes_def dest: transpose_eq_imp_eq) (meson transpose_involutory)
@@ -820,7 +820,7 @@
by simp
show "f \<circ> (*v) B = id"
using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
- by (metis (no_types, hide_lams))
+ by (metis (no_types, opaque_lifting))
qed
next
fix g
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1552,11 +1552,11 @@
lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
unfolding bounded_def
- by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
+ by (metis (erased, opaque_lifting) dist_fst_le image_iff order_trans)
lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
unfolding bounded_def
- by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
+ by (metis (no_types, opaque_lifting) dist_snd_le image_iff order.trans)
instance\<^marker>\<open>tag important\<close> prod :: (heine_borel, heine_borel) heine_borel
proof
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1298,7 +1298,7 @@
using assms by (metis euclidean_all_zero_iff inner_zero_right)
moreover have "c = 1" if "a \<bullet> (x + c *\<^sub>R w) = b" "a \<bullet> (x + w) = b" for c w
using that
- by (metis (no_types, hide_lams) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
+ by (metis (no_types, opaque_lifting) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
ultimately
show ?thesis
using starlike_negligible [OF closed_hyperplane, of x] by simp
@@ -3597,7 +3597,7 @@
fix t
assume "\<bar>t\<bar> < B" then show "a $ 1 \<le> t \<and> t \<le> b $ 1"
using subsetD [OF B]
- by (metis (mono_tags, hide_lams) mem_ball_0 mem_box_cart(2) norm_real vec_component)
+ by (metis (mono_tags, opaque_lifting) mem_ball_0 mem_box_cart(2) norm_real vec_component)
qed
have eq: "(\<lambda>x. if vec x \<in> S then f (vec x) else 0) = (\<lambda>x. if x \<in> S then f x else 0) \<circ> vec"
by force
@@ -4217,7 +4217,7 @@
finally show ?thesis .
qed
ultimately show ?thesis
- by (metis (no_types, hide_lams) m_def order_trans power2_eq_square power_even_eq)
+ by (metis (no_types, opaque_lifting) m_def order_trans power2_eq_square power_even_eq)
next
case False
with n N1 have "f x \<le> 2^n"
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jul 08 08:42:36 2021 +0200
@@ -349,7 +349,7 @@
proof (rule pairwise_mono)
show "negligible (BOX (\<eta> x) x \<inter> BOX (\<eta> y) y)"
if "negligible (BOX2 (\<eta> x) x \<inter> BOX2 (\<eta> y) y)" for x y
- by (metis (no_types, hide_lams) that Int_mono negligible_subset BOX_sub)
+ by (metis (no_types, opaque_lifting) that Int_mono negligible_subset BOX_sub)
qed auto
have eq: "\<And>box. (\<lambda>D. box (\<eta> (tag D)) (tag D)) ` \<G> = (\<lambda>t. box (\<eta> t) t) ` tag ` \<G>"
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Jul 08 08:42:36 2021 +0200
@@ -363,7 +363,7 @@
fixes a::ereal
shows "(\<Sum>i\<in>I. a) = a * card I"
apply (cases "finite I", induct set: finite, simp_all)
-apply (cases a, auto, metis (no_types, hide_lams) add.commute mult.commute semiring_normalization_rules(3))
+apply (cases a, auto, metis (no_types, opaque_lifting) add.commute mult.commute semiring_normalization_rules(3))
done
lemma real_lim_then_eventually_real:
@@ -677,7 +677,7 @@
then have "1/z \<ge> 0" by auto
moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
apply (cases z) apply auto
- by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
+ by (metis (mono_tags, opaque_lifting) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
ultimately have "1/z \<ge> 0" "1/z < e" by auto
}
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Thu Jul 08 08:42:36 2021 +0200
@@ -118,7 +118,7 @@
show "(\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 \<subseteq> {-1..1}" for i
by (auto simp: mem_box_cart)
show "{-1..1} \<subseteq> (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1" for i
- by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component)
+ by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, opaque_lifting) vec_component)
qed
{
fix x
--- a/src/HOL/Analysis/Function_Metric.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Function_Metric.thy Thu Jul 08 08:42:36 2021 +0200
@@ -274,7 +274,7 @@
also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
+ (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
apply (rule suminf_le)
- using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
+ using ineq apply (metis (no_types, opaque_lifting) add.right_neutral distrib_left
le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
by (auto simp add: summable_add)
also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
--- a/src/HOL/Analysis/Further_Topology.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2040,7 +2040,7 @@
unfolding image_comp [symmetric] using \<open>U \<subseteq> S\<close> fim
by (metis homeomorphism_image2 homeomorphism_of_subsets homkh subset_image_iff)
ultimately show ?thesis
- by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
+ by (metis (no_types, opaque_lifting) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
qed
lemma inv_of_domain_ss1:
@@ -5483,7 +5483,7 @@
by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest)
then obtain j where contj: "continuous_on (ball 0 1) j"
and j: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> exp(j z) = (g \<circ> h) z"
- by (metis (mono_tags, hide_lams) continuous_logarithm_on_ball comp_apply non0)
+ by (metis (mono_tags, opaque_lifting) continuous_logarithm_on_ball comp_apply non0)
have [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (k x) = x"
using hk homeomorphism_apply2 by blast
have "\<exists>\<zeta>. continuous_on S \<zeta>\<and> (\<forall>x\<in>S. f x = exp (\<zeta> x))"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 08 08:42:36 2021 +0200
@@ -799,7 +799,7 @@
assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
shows "integral s f = integral s g"
unfolding integral_def
-by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
+by (metis (full_types, opaque_lifting) assms has_integral_cong integrable_eq)
lemma integrable_on_cmult_left_iff [simp]:
assumes "c \<noteq> 0"
@@ -5695,7 +5695,7 @@
have "norm (?SUM ?p - integral (cbox a b) f) < e"
proof (rule less_e)
show "d fine ?p"
- by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
+ by (metis (mono_tags, opaque_lifting) qq fine_Un fine_Union imageE p(2))
note ptag = tagged_partial_division_of_Union_self[OF p(1)]
have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
proof (rule tagged_division_Un[OF ptag tagged_division_Union [OF \<open>finite r\<close>]])
--- a/src/HOL/Analysis/Homotopy.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Homotopy.thy Thu Jul 08 08:42:36 2021 +0200
@@ -551,7 +551,7 @@
then have "path q"
by (simp add: path_def) (metis q continuous_on_cong)
have piqs: "path_image q \<subseteq> s"
- by (metis (no_types, hide_lams) pips f01 image_subset_iff path_image_def q)
+ by (metis (no_types, opaque_lifting) pips f01 image_subset_iff path_image_def q)
have fb0: "\<And>a b. \<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> (1 - a) * f b + a * b"
using f01 by force
have fb1: "\<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> (1 - a) * f b + a * b \<le> 1" for a b
@@ -1846,7 +1846,7 @@
have 2: "openin (top_of_set S) ?B"
by (subst openin_subopen, blast)
have \<section>: "?A \<inter> ?B = {}"
- by (clarsimp simp: set_eq_iff) (metis (no_types, hide_lams) Int_iff opD openin_Int)
+ by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int)
have *: "S \<subseteq> ?A \<union> ?B"
by clarsimp (meson opI)
have "?A = {} \<or> ?B = {}"
@@ -1916,7 +1916,7 @@
assume ?lhs
then have "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x\<in>T. f x = f a)"
unfolding locally_def
- by (metis (mono_tags, hide_lams) constant_on_def constant_on_subset openin_subtopology_self)
+ by (metis (mono_tags, opaque_lifting) constant_on_def constant_on_subset openin_subtopology_self)
then show ?rhs
using assms
by (simp add: locally_constant_imp_constant)
@@ -4519,7 +4519,7 @@
have "\<not> aff_dim (affine hull S) \<le> 1"
using \<open>\<not> collinear S\<close> collinear_aff_dim by auto
then have "\<not> aff_dim (ball x r \<inter> affine hull S) \<le> 1"
- by (metis (no_types, hide_lams) aff_dim_convex_Int_open IntI open_ball \<open>0 < r\<close> aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that)
+ by (metis (no_types, opaque_lifting) aff_dim_convex_Int_open IntI open_ball \<open>0 < r\<close> aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that)
then have "\<not> collinear (ball x r \<inter> affine hull S)"
by (simp add: collinear_aff_dim)
then have *: "path_connected ((ball x r \<inter> affine hull S) - T)"
@@ -5254,7 +5254,7 @@
and hj: "\<And>x. j(h x) = x" "\<And>y. h(j y) = y"
and ranh: "surj h"
using isomorphisms_UNIV_UNIV
- by (metis (mono_tags, hide_lams) DIM_real UNIV_eq_I range_eqI)
+ by (metis (mono_tags, opaque_lifting) DIM_real UNIV_eq_I range_eqI)
obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
and f: "\<And>x. x \<in> h ` K \<Longrightarrow> f x \<in> h ` U"
and sub: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> h ` S"
@@ -5275,7 +5275,7 @@
using hom homeomorphism_def
by (blast intro: continuous_on_compose cont_hj)+
show "(j \<circ> f \<circ> h) ` T \<subseteq> T" "(j \<circ> g \<circ> h) ` T \<subseteq> T"
- by auto (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)+
+ by auto (metis (mono_tags, opaque_lifting) hj(1) hom homeomorphism_def imageE imageI)+
show "\<And>x. x \<in> T \<Longrightarrow> (j \<circ> g \<circ> h) ((j \<circ> f \<circ> h) x) = x"
using hj hom homeomorphism_apply1 by fastforce
show "\<And>y. y \<in> T \<Longrightarrow> (j \<circ> f \<circ> h) ((j \<circ> g \<circ> h) y) = y"
--- a/src/HOL/Analysis/Jordan_Curve.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Thu Jul 08 08:42:36 2021 +0200
@@ -582,7 +582,7 @@
obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
apply (auto simp: outside_inside)
using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
- by (metis (no_types, hide_lams) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
+ by (metis (no_types, opaque_lifting) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
using zout op_out1c open_contains_ball_eq by blast
have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
--- a/src/HOL/Analysis/Line_Segment.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Line_Segment.thy Thu Jul 08 08:42:36 2021 +0200
@@ -664,7 +664,7 @@
fixes a :: "'a :: euclidean_space"
shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
apply (simp add: convex_contains_open_segment, clarify)
-by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+by (metis (no_types, opaque_lifting) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
apply (clarsimp simp: midpoint_def in_segment)
@@ -707,7 +707,7 @@
fixes a b ::"'a::real_vector"
assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v"
shows "a=b"
- by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
+ by (metis (no_types, opaque_lifting) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
lemma closed_segment_image_interval:
"closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Jul 08 08:42:36 2021 +0200
@@ -347,7 +347,7 @@
lemma\<^marker>\<open>tag unimportant\<close> orthogonal_transformation_inv:
"orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
- by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+ by (metis (no_types, opaque_lifting) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
lemma\<^marker>\<open>tag unimportant\<close> orthogonal_transformation_norm:
"orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
--- a/src/HOL/Analysis/Path_Connected.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Jul 08 08:42:36 2021 +0200
@@ -55,7 +55,7 @@
have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
by (rule ext) simp
show ?thesis
- by (metis (no_types, hide_lams) g continuous_on_compose homeomorphism_def homeomorphism_translation)
+ by (metis (no_types, opaque_lifting) g continuous_on_compose homeomorphism_def homeomorphism_translation)
qed
lemma path_translation_eq:
@@ -2720,7 +2720,7 @@
with b have "\<bar>x \<bullet> b\<bar> = norm x"
using norm_Basis by (simp add: b)
with xb show ?thesis
- by (metis (mono_tags, hide_lams) abs_eq_iff abs_norm_cancel)
+ by (metis (mono_tags, opaque_lifting) abs_eq_iff abs_norm_cancel)
qed
with \<open>r > 0\<close> b show "sphere 0 r = {r *\<^sub>R b, - r *\<^sub>R b}"
by (force simp: sphere_def dist_norm)
@@ -3602,7 +3602,7 @@
lemma inside_outside_intersect_connected:
"\<lbrakk>connected T; inside S \<inter> T \<noteq> {}; outside S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> S \<inter> T \<noteq> {}"
apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
- by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
+ by (metis (no_types, opaque_lifting) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
lemma outside_bounded_nonempty:
fixes S :: "'a :: {real_normed_vector, perfect_space} set"
--- a/src/HOL/Analysis/Polytope.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Polytope.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2729,7 +2729,7 @@
using \<open>T \<subseteq> S\<close> by blast
then have "\<exists>y\<in>S. x \<in> convex hull (S - {y})"
using True affine_independent_iff_card [of S]
- by (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 \<open>a \<notin> T\<close> \<open>T \<subseteq> S\<close> \<open>x \<in> convex hull T\<close> hull_mono insert_Diff_single subsetCE)
+ by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_insert0 \<open>a \<notin> T\<close> \<open>T \<subseteq> S\<close> \<open>x \<in> convex hull T\<close> hull_mono insert_Diff_single subsetCE)
} note * = this
have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
by (subst caratheodory_aff_dim) (blast dest: *)
@@ -3044,7 +3044,7 @@
by (simp add: polytope_imp_polyhedron simplex_imp_polytope)
lemma simplex_dim_ge: "n simplex S \<Longrightarrow> -1 \<le> n"
- by (metis (no_types, hide_lams) aff_dim_geq affine_independent_iff_card diff_add_cancel diff_diff_eq2 simplex_def)
+ by (metis (no_types, opaque_lifting) aff_dim_geq affine_independent_iff_card diff_add_cancel diff_diff_eq2 simplex_def)
lemma simplex_empty [simp]: "n simplex {} \<longleftrightarrow> n = -1"
proof
--- a/src/HOL/Analysis/Retracts.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Retracts.thy Thu Jul 08 08:42:36 2021 +0200
@@ -150,7 +150,7 @@
\<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
closedin (top_of_set U) T \<longrightarrow>
(\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
- by (metis (mono_tags, hide_lams) AR_imp_absolute_extensor absolute_extensor_imp_AR)
+ by (metis (mono_tags, opaque_lifting) AR_imp_absolute_extensor absolute_extensor_imp_AR)
lemma AR_imp_retract:
fixes S :: "'a::euclidean_space set"
@@ -1445,7 +1445,7 @@
show "finite ((\<inter>) C ` \<U>)"
by (simp add: insert.hyps(1))
show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> closed Ca"
- by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2)
+ by (metis (no_types, opaque_lifting) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2)
show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> convex Ca"
by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE)
show "card ((\<inter>) C ` \<U>) < n"
--- a/src/HOL/Analysis/Starlike.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Starlike.thy Thu Jul 08 08:42:36 2021 +0200
@@ -3325,7 +3325,7 @@
assume ?rhs
then show ?lhs
unfolding between_mem_convex_hull
- by (metis (no_types, hide_lams) collinear_closed_segment collinear_subset hull_redundant hull_subset insert_commute segment_convex_hull)
+ by (metis (no_types, opaque_lifting) collinear_closed_segment collinear_subset hull_redundant hull_subset insert_commute segment_convex_hull)
qed
@@ -3404,7 +3404,7 @@
shows "f ` (open_segment a b) = open_segment (f a) (f b)"
proof -
have "f ` (open_segment a b) = f ` (closed_segment a b) - {f a, f b}"
- by (metis (no_types, hide_lams) empty_subsetI ends_in_segment image_insert image_is_empty inj_on_image_set_diff injf insert_subset open_segment_def segment_open_subset_closed)
+ by (metis (no_types, opaque_lifting) empty_subsetI ends_in_segment image_insert image_is_empty inj_on_image_set_diff injf insert_subset open_segment_def segment_open_subset_closed)
also have "... = open_segment (f a) (f b)"
using continuous_injective_image_segment_1 [OF assms]
by (simp add: open_segment_def inj_on_image_set_diff [OF injf])
@@ -3947,7 +3947,7 @@
have "K \<subseteq> \<Union>(insert (U \<union> V) (\<D> - {U \<union> V}))"
using \<open>K \<subseteq> \<Union>\<D>\<close> by auto
also have "... \<subseteq> (U \<union> V) \<union> (N - J)"
- by (metis (no_types, hide_lams) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
+ by (metis (no_types, opaque_lifting) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
finally have "J \<inter> K \<subseteq> U \<union> V"
by blast
moreover have "connected(J \<inter> K)"
@@ -6366,7 +6366,7 @@
have "(adjoint f) -` {0} = {0}"
by (metis \<open>inj (adjoint f)\<close> adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV)
then have "(range(f))\<^sup>\<bottom> = {0}"
- by (metis (no_types, hide_lams) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero)
+ by (metis (no_types, opaque_lifting) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero)
then show "surj f"
by (metis \<open>inj (adjoint f)\<close> adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj)
next
@@ -6387,7 +6387,7 @@
assume "\<not>inj f"
then show ?rhs
using all_zero_iff
- by (metis (no_types, hide_lams) adjoint_clauses(2) adjoint_linear assms
+ by (metis (no_types, opaque_lifting) adjoint_clauses(2) adjoint_linear assms
linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj)
next
assume ?rhs
--- a/src/HOL/Analysis/Tagged_Division.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2359,8 +2359,8 @@
using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
apply (simp_all add: power_add)
- apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
- apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
+ apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
+ apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
done
then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
by meson
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2222,7 +2222,7 @@
then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
by (metis interiorE)
then show "x \<in> ?rhs"
- by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
+ by (metis (no_types, opaque_lifting) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
next
fix x
assume x: "x \<in> interior S"
--- a/src/HOL/Analysis/Uniform_Limit.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Jul 08 08:42:36 2021 +0200
@@ -603,7 +603,7 @@
then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y)"
apply (rule eventually_mono)
using b apply (simp only: dist_norm)
- by (metis (no_types, hide_lams) diff_zero dist_commute dist_norm norm_triangle_half_l not_less)
+ by (metis (no_types, opaque_lifting) diff_zero dist_commute dist_norm norm_triangle_half_l not_less)
then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y) \<and> norm (f x y - l y) < e * b\<^sup>2 / 2"
apply (simp only: ball_conj_distrib dist_norm [symmetric])
apply (rule eventually_conj, assumption)
--- a/src/HOL/Auth/Message.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Auth/Message.thy Thu Jul 08 08:42:36 2021 +0200
@@ -214,7 +214,7 @@
lemma parts_image [simp]:
"parts (f ` A) = (\<Union>x\<in>A. parts {f x})"
apply auto
- apply (metis (mono_tags, hide_lams) image_iff parts_singleton)
+ apply (metis (mono_tags, opaque_lifting) image_iff parts_singleton)
apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono)
done
--- a/src/HOL/Binomial.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Binomial.thy Thu Jul 08 08:42:36 2021 +0200
@@ -933,7 +933,7 @@
have "?lhs = (\<Sum>k\<le>m. (- a gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
by (simp add: gbinomial_partial_sum_poly)
also have "... = (\<Sum>k\<le>m. (-1) ^ k * (of_nat k - - a - 1 gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
- by (metis (no_types, hide_lams) gbinomial_negated_upper)
+ by (metis (no_types, opaque_lifting) gbinomial_negated_upper)
also have "... = ?rhs"
by (intro sum.cong) (auto simp flip: power_mult_distrib)
finally show ?thesis .
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Thu Jul 08 08:42:36 2021 +0200
@@ -699,7 +699,7 @@
shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
apply safe
apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
- apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
+ apply (metis (opaque_lifting, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
apply (metis assms in_notinI succ_in_Field)
done
--- a/src/HOL/Combinatorics/Cycles.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Combinatorics/Cycles.thy Thu Jul 08 08:42:36 2021 +0200
@@ -436,7 +436,7 @@
hence "(tl (support p a) @ [ a ]) ! i = a"
by (metis (no_types, lifting) diff_zero length_map length_tl length_upt nth_append_length)
also have " ... = p ((p ^^ i) a)"
- by (metis (mono_tags, hide_lams) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply)
+ by (metis (mono_tags, opaque_lifting) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply)
finally show ?thesis .
next
assume "i \<noteq> least_power p a - 1"
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Thu Jul 08 08:42:36 2021 +0200
@@ -398,7 +398,7 @@
lemma has_field_derivative_higher_deriv:
"\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
\<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
-by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
+by (metis (no_types, opaque_lifting) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
lemma valid_path_compose_holomorphic:
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Jul 08 08:42:36 2021 +0200
@@ -542,7 +542,7 @@
using that by (auto intro!:tendsto_eq_intros)
then have "fg \<midarrow>z\<rightarrow> 0"
apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
- by (metis (no_types, hide_lams) Diff_iff cball_trivial dist_commute dist_self
+ by (metis (no_types, opaque_lifting) Diff_iff cball_trivial dist_commute dist_self
eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int
that)
then show ?thesis unfolding not_essential_def fg_def by auto
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Thu Jul 08 08:42:36 2021 +0200
@@ -852,7 +852,7 @@
show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
apply simp
apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
- by (metis (no_types, hide_lams) inverse_inverse_eq le_less_trans less_eq_real_def less_imp_inverse_less linordered_field_no_ub not_less)
+ by (metis (no_types, opaque_lifting) inverse_inverse_eq le_less_trans less_eq_real_def less_imp_inverse_less linordered_field_no_ub not_less)
qed
then obtain a n where "\<And>z. f z = (\<Sum>i\<le>n. a i * z^i)"
using assms pole_at_infinity by blast
--- a/src/HOL/Complex_Analysis/Great_Picard.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy Thu Jul 08 08:42:36 2021 +0200
@@ -120,7 +120,7 @@
using * [of "n-2"] \<open>2 \<le> n\<close>
by (metis le_add_diff_inverse2)
then have **: "4 + real n * 2 \<le> real n * (real n * 3)"
- by (metis (mono_tags, hide_lams) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral)
+ by (metis (mono_tags, opaque_lifting) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral)
have "sqrt ((1 + real n)\<^sup>2 - 1) \<le> 2 * sqrt ((real n)\<^sup>2 - 1)"
by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **)
then
@@ -540,7 +540,7 @@
by (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf]) auto
qed auto
then obtain "c \<noteq> 0" "c \<noteq> 1"
- by (metis (no_types, hide_lams) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
+ by (metis (no_types, opaque_lifting) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
have eq: "f(f x) - c * f x = x*(1 - c)" for x
using fun_cong [OF c, of x] by (simp add: field_simps)
have df_times_dff: "deriv f z * (deriv f (f z) - c) = 1 * (1 - c)" for z
@@ -684,7 +684,7 @@
if "\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k1)) n (\<sigma> i)) \<longlonglongrightarrow> l" "\<And>j. N \<le> j \<Longrightarrow> \<exists>j'\<ge>j. k2 j = k1 j'"
for i N and r k1 k2 :: "nat\<Rightarrow>nat"
using that
- by (simp add: lim_sequentially) (metis (no_types, hide_lams) le_cases order_trans)
+ by (simp add: lim_sequentially) (metis (no_types, opaque_lifting) le_cases order_trans)
qed auto
with \<sigma> that show ?thesis
by force
@@ -713,7 +713,7 @@
then show "\<forall>\<^sub>F n in sequentially. continuous_on S ((\<F> \<circ> r) n)"
by (simp add: eventually_sequentially)
show "uniform_limit S (\<F> \<circ> r) g sequentially"
- using that by (metis (mono_tags, hide_lams) comp_apply dist_norm uniform_limit_sequentially_iff)
+ using that by (metis (mono_tags, opaque_lifting) comp_apply dist_norm uniform_limit_sequentially_iff)
qed auto
moreover
obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
@@ -933,7 +933,7 @@
using ex by blast
then have "\<Phi> g i id (r \<circ> k2)"
using that
- by (simp add: \<Phi>_def) (metis (no_types, hide_lams) le_trans linear)
+ by (simp add: \<Phi>_def) (metis (no_types, opaque_lifting) le_trans linear)
then show ?thesis
by metis
qed
@@ -1207,7 +1207,7 @@
by simp
show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
apply (rule eventually_mono [OF eventually_conj [OF K z1]])
- by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half)
+ by (metis (no_types, opaque_lifting) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half)
qed
show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"
unfolding constant_on_def
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1726,7 +1726,7 @@
have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
proof (rule homotopic_paths_imp_homotopic_loops)
show "homotopic_paths (- {\<zeta>}) p (r +++ q +++ reversepath r)"
- by (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
+ by (metis (mono_tags, opaque_lifting) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
qed (use loops pas in auto)
moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Thu Jul 08 08:42:36 2021 +0200
@@ -837,7 +837,7 @@
using winding_number_constant [OF \<gamma> loop, of "outside(path_image \<gamma>)"] connected_outside
by (metis DIM_complex bounded_path_image dual_order.refl \<gamma> outside_no_overlap)
ultimately have "winding_number \<gamma> z = winding_number \<gamma> w"
- by (metis (no_types, hide_lams) constant_on_def z)
+ by (metis (no_types, opaque_lifting) constant_on_def z)
also have "\<dots> = 0"
proof -
have wnot: "w \<notin> path_image \<gamma>" using wout by (simp add: outside_def)
@@ -1577,7 +1577,7 @@
show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \<inter>
inside (path_image (linepath (a + e) (a - e)) \<union> path_image p) \<noteq> {}"
apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal)
- by (metis (no_types, hide_lams) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
+ by (metis (no_types, opaque_lifting) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
path_image_linepath pathstart_linepath pfp segment_convex_hull)
show zin_inside: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union>
path_image (linepath (a + e) c +++ linepath c (a - e)))"
@@ -1625,7 +1625,7 @@
proof -
have [simp]: "a + of_real x \<in> closed_segment (a - \<alpha>) (a - \<beta>) \<longleftrightarrow> x \<in> closed_segment (-\<alpha>) (-\<beta>)" for x \<alpha> \<beta>::real
using closed_segment_translation_eq [of a]
- by (metis (no_types, hide_lams) add_uminus_conv_diff of_real_minus of_real_closed_segment)
+ by (metis (no_types, opaque_lifting) add_uminus_conv_diff of_real_minus of_real_closed_segment)
have [simp]: "a - of_real x \<in> closed_segment (a + \<alpha>) (a + \<beta>) \<longleftrightarrow> -x \<in> closed_segment \<alpha> \<beta>" for x \<alpha> \<beta>::real
by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus)
have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p"
@@ -1803,7 +1803,7 @@
by (metis IntI UnCI emptyE inside_no_overlap path_image_join path_image_linepath pathstart_linepath pfp zzin)
have znotin_kde_e: "z \<notin> closed_segment (a + kde) (a + e)" and znotin_d_kde': "z \<notin> closed_segment (a - d) (a - kde)"
using clsub1 clsub2 zzin
- by (metis (no_types, hide_lams) IntI Un_iff emptyE inside_no_overlap path_image_join path_image_linepath pathstart_linepath pfp subsetD)+
+ by (metis (no_types, opaque_lifting) IntI Un_iff emptyE inside_no_overlap path_image_join path_image_linepath pathstart_linepath pfp subsetD)+
have "winding_number (linepath (a - d) (a + e)) z =
winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z"
proof (rule winding_number_split_linepath)
@@ -1952,7 +1952,7 @@
have z_notin_ed: "z \<notin> closed_segment (a + e) (a - d)"
using zin q01 by (simp add: path_image_join closed_segment_commute inside_def)
have z_notin_0t: "z \<notin> path_image (subpath 0 t q)"
- by (metis (no_types, hide_lams) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
+ by (metis (no_types, opaque_lifting) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin)
have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z"
by (metis \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> atLeastAtMost_iff zero_le_one
--- a/src/HOL/Computational_Algebra/Polynomial.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1838,7 +1838,7 @@
next
case (Suc n)
have "order a ([:- a, 1:] ^ Suc n) = order a ([:- a, 1:] ^ n) + order a [:-a,1:]"
- by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral
+ by (metis (no_types, opaque_lifting) One_nat_def add_Suc_right monoid_add_class.add.right_neutral
one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
moreover have "order a [:-a,1:] = 1"
unfolding order_def
--- a/src/HOL/Deriv.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Deriv.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1559,7 +1559,7 @@
"a < \<xi>" "\<xi> < b" "(\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
by metis
then show ?thesis
- by (metis (no_types, hide_lams) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close>
+ by (metis (no_types, opaque_lifting) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close>
less_irrefl nonzero_eq_divide_eq)
qed
--- a/src/HOL/Homology/Brouwer_Degree.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Homology/Brouwer_Degree.thy Thu Jul 08 08:42:36 2021 +0200
@@ -524,7 +524,7 @@
then show ?thesis
using homology_exactness_axiom_3 [of p X S] homology_exactness_axiom_1 [of p X S]
apply (simp add: mon_def epi_def hom_boundary_hom)
- by (metis (no_types, hide_lams) group_hom.trivial_hom_iff group_hom.trivial_ker_imp_inj group_hom_axioms_def group_hom_def group_relative_homology_group hom_boundary_hom)
+ by (metis (no_types, opaque_lifting) group_hom.trivial_hom_iff group_hom.trivial_ker_imp_inj group_hom_axioms_def group_hom_def group_relative_homology_group hom_boundary_hom)
qed
lemma short_exact_sequence_hom_induced_relativization:
@@ -625,7 +625,7 @@
lemma iso_homology_contractible_space_subtopology2:
"\<lbrakk>contractible_space X; S \<subseteq> topspace X; p \<noteq> 0; S \<noteq> {}\<rbrakk>
\<Longrightarrow> homology_group p (subtopology X S) \<cong> relative_homology_group (p + 1) X S"
- by (metis (no_types, hide_lams) add.commute isomorphic_group_reduced_homology_of_contractible topspace_subtopology topspace_subtopology_subset un_reduced_homology_group)
+ by (metis (no_types, opaque_lifting) add.commute isomorphic_group_reduced_homology_of_contractible topspace_subtopology topspace_subtopology_subset un_reduced_homology_group)
lemma trivial_relative_homology_group_contractible_spaces:
"\<lbrakk>contractible_space X; contractible_space(subtopology X S); topspace X \<inter> S \<noteq> {}\<rbrakk>
@@ -1230,7 +1230,7 @@
by fastforce
then show ?case
using eq iso_trans iso isomorphic_group_triviality neq
- by (metis (no_types, hide_lams) add.commute add_left_cancel diff_add_cancel group_reduced_homology_group of_nat_Suc)
+ by (metis (no_types, opaque_lifting) add.commute add_left_cancel diff_add_cancel group_reduced_homology_group of_nat_Suc)
qed
--- a/src/HOL/Homology/Invariance_of_Domain.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Thu Jul 08 08:42:36 2021 +0200
@@ -493,7 +493,7 @@
finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
= ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" .
have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
- by (metis (no_types, hide_lams) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff)
+ by (metis (no_types, opaque_lifting) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff)
moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg))
= un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff)
@@ -1518,7 +1518,7 @@
have "path_component_of ?ES x (?neg x)"
proof -
have "path_component_of ?ES x a"
- by (metis (no_types, hide_lams) ** a b \<open>a \<noteq> b\<close> negab path_component_of_trans path_component_of_sym x)
+ by (metis (no_types, opaque_lifting) ** a b \<open>a \<noteq> b\<close> negab path_component_of_trans path_component_of_sym x)
moreover
have pa_ab: "path_component_of ?ES a b" using "**" a b negab neg_neg by blast
then have "path_component_of ?ES a (?neg x)"
--- a/src/HOL/Homology/Simplices.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Homology/Simplices.thy Thu Jul 08 08:42:36 2021 +0200
@@ -410,7 +410,7 @@
lemma singular_relboundary_restrict [simp]:
"singular_relboundary p X (topspace X \<inter> S) = singular_relboundary p X S"
unfolding singular_relboundary_def
- by (metis (no_types, hide_lams) subtopology_subtopology subtopology_topspace)
+ by (metis (no_types, opaque_lifting) subtopology_subtopology subtopology_topspace)
lemma singular_relboundary_alt:
"singular_relboundary p X S c \<longleftrightarrow>
@@ -1564,7 +1564,7 @@
have 3: "simplex_cone p (Sigp f) g \<in> ?rhs"
proof -
have "simplicial_simplex p (f ` standard_simplex(Suc p)) g"
- by (metis (mono_tags, hide_lams) sc_sub mem_Collect_eq simplicial_chain_def simplicial_chain_simplicial_subdivision subsetD that)
+ by (metis (mono_tags, opaque_lifting) sc_sub mem_Collect_eq simplicial_chain_def simplicial_chain_simplicial_subdivision subsetD that)
then obtain m where m: "g ` standard_simplex p \<subseteq> f ` standard_simplex (Suc p)"
and geq: "g = oriented_simplex p m"
using ssf by (auto simp: simplicial_simplex)
@@ -3090,7 +3090,7 @@
have "i + j > 0"
using that by blast
then show ?thesis
- by (metis (no_types, hide_lams) One_nat_def Suc_diff_1 add.inverse_inverse mult.left_neutral mult_minus_left power_Suc)
+ by (metis (no_types, opaque_lifting) One_nat_def Suc_diff_1 add.inverse_inverse mult.left_neutral mult_minus_left power_Suc)
qed
show ?thesis
apply (rule sum.eq_general_inverses [where h = "\<lambda>(a,b). (a-1,b)" and k = "\<lambda>(a,b). (Suc a,b)"])
--- a/src/HOL/IMP/Abs_Int2.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Thu Jul 08 08:42:36 2021 +0200
@@ -65,7 +65,7 @@
lemma in_gamma_sup_UpI:
"s \<in> \<gamma>\<^sub>o S1 \<or> s \<in> \<gamma>\<^sub>o S2 \<Longrightarrow> s \<in> \<gamma>\<^sub>o(S1 \<squnion> S2)"
-by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
+by (metis (opaque_lifting, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
"aval'' e None = \<bottom>" |
--- a/src/HOL/IMP/Abs_Int3.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Thu Jul 08 08:42:36 2021 +0200
@@ -438,7 +438,7 @@
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
-by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
+by(metis (opaque_lifting, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
lemma n_c_narrow: "strip C1 = strip C2
\<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
--- a/src/HOL/Library/Dlist.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Dlist.thy Thu Jul 08 08:42:36 2021 +0200
@@ -279,7 +279,7 @@
qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
by(auto simp add: double.simps Dlist.dlist_eq_def vimage2p_def map_eq_append_conv)
- (metis (no_types, hide_lams) list.simps(9) map_append remdups.simps(2) remdups_append2 set_append set_eq_subset set_remdups)
+ (metis (no_types, opaque_lifting) list.simps(9) map_append remdups.simps(2) remdups_append2 set_append set_eq_subset set_remdups)
qualified lemma dlist_eq_set_eq: "Dlist.dlist_eq xs ys \<Longrightarrow> set xs = set ys"
by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups)
--- a/src/HOL/Library/Equipollence.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Equipollence.thy Thu Jul 08 08:42:36 2021 +0200
@@ -125,7 +125,7 @@
show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
- by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
+ by (metis (no_types, opaque_lifting) image_empty image_insert lepoll_iff that)
qed
lemma infinite_insert_lepoll:
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1888,7 +1888,7 @@
by (auto simp: ennreal_neg)
lemma power_le_one_iff: "0 \<le> (a::real) \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
- by (metis (mono_tags, hide_lams) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
+ by (metis (mono_tags, opaque_lifting) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
lemma ennreal_diff_le_mono_left: "a \<le> b \<Longrightarrow> a - c \<le> (b::ennreal)"
using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp
--- a/src/HOL/Library/Extended_Real.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1887,7 +1887,7 @@
subgoal
by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
subgoal
- by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+ by (metis (no_types, opaque_lifting) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
subgoal by force
subgoal
--- a/src/HOL/Library/Float.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Float.thy Thu Jul 08 08:42:36 2021 +0200
@@ -838,7 +838,7 @@
using \<open>p + e < 0\<close>
apply transfer
apply (simp add: round_down_def field_simps flip: floor_divide_of_int_eq)
- apply (metis (no_types, hide_lams) Float.rep_eq
+ apply (metis (no_types, opaque_lifting) Float.rep_eq
add.inverse_inverse compute_real_of_float diff_minus_eq_add
floor_divide_of_int_eq int_of_reals(1) linorder_not_le
minus_add_distrib of_int_eq_numeral_power_cancel_iff powr_add)
@@ -2394,7 +2394,7 @@
"int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
apply transfer
apply (simp add: powr_int floor_divide_of_int_eq)
- apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
+ apply (metis (no_types, opaque_lifting)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
done
lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int \<lfloor>x\<rfloor>"
@@ -2404,7 +2404,7 @@
"floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
apply transfer
apply (simp add: powr_int floor_divide_of_int_eq)
- apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
+ apply (metis (no_types, opaque_lifting)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
done
end
--- a/src/HOL/Library/FuncSet.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/FuncSet.thy Thu Jul 08 08:42:36 2021 +0200
@@ -631,7 +631,7 @@
then show ?rhs
apply (rule_tac x="f \<circ> inv_into (Collect P) g" in exI)
unfolding o_def
- by (metis (mono_tags, hide_lams) f_inv_into_f imageI inv_into_into mem_Collect_eq)
+ by (metis (mono_tags, opaque_lifting) f_inv_into_f imageI inv_into_into mem_Collect_eq)
qed auto
lemma function_factors_left:
--- a/src/HOL/Library/Interval.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Interval.thy Thu Jul 08 08:42:36 2021 +0200
@@ -649,7 +649,7 @@
"0 \<le> max (la * lb) (max (la * ub) (max (lb * ua) (ua * ub)))"
if "la \<le> 0" "0 \<le> ua"
for la lb ua ub:: "'a::linordered_idom"
- subgoal by (metis (no_types, hide_lams) that eq_iff min_le_iff_disj mult_zero_left mult_zero_right
+ subgoal by (metis (no_types, opaque_lifting) that eq_iff min_le_iff_disj mult_zero_left mult_zero_right
zero_le_mult_iff)
subgoal by (metis that le_max_iff_disj mult_zero_right order_refl zero_le_mult_iff)
done
--- a/src/HOL/Library/Poly_Mapping.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1693,7 +1693,7 @@
by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
lemma keys_minus [simp]: "Poly_Mapping.keys(-a) = Poly_Mapping.keys a"
- by (metis (no_types, hide_lams) in_keys_iff lookup_uminus neg_equal_0_iff_equal subsetI subset_antisym)
+ by (metis (no_types, opaque_lifting) in_keys_iff lookup_uminus neg_equal_0_iff_equal subsetI subset_antisym)
lemma keys_diff:
"Poly_Mapping.keys(a - b) \<subseteq> Poly_Mapping.keys a \<union> Poly_Mapping.keys b"
@@ -1780,7 +1780,7 @@
lemma frag_extend_diff:
"frag_extend f (a-b) = (frag_extend f a) - (frag_extend f b)"
- by (metis (no_types, hide_lams) add_uminus_conv_diff frag_extend_add frag_extend_minus)
+ by (metis (no_types, opaque_lifting) add_uminus_conv_diff frag_extend_add frag_extend_minus)
lemma frag_extend_sum:
"finite I \<Longrightarrow> frag_extend f (\<Sum>i\<in>I. g i) = sum (frag_extend f o g) I"
@@ -1818,7 +1818,7 @@
apply (simp_all add: assms frag_cmul_distrib)
by (metis add.left_neutral add_diff_cancel_right' add_uminus_conv_diff P)
then show ?thesis
- by (metis (no_types, hide_lams) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases)
+ by (metis (no_types, opaque_lifting) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases)
qed
lemma frag_induction [consumes 1, case_names zero one diff]:
--- a/src/HOL/Library/Word.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Word.thy Thu Jul 08 08:42:36 2021 +0200
@@ -849,7 +849,7 @@
for a b :: \<open>'a word\<close>
apply transfer
apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def)
- by (metis (no_types, hide_lams) "\<section>" Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign le_less_trans mult_eq_0_iff take_bit_eq_mod take_bit_nonnegative zdiv_eq_0_iff zmod_le_nonneg_dividend)
+ by (metis (no_types, opaque_lifting) "\<section>" Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign le_less_trans mult_eq_0_iff take_bit_eq_mod take_bit_nonnegative zdiv_eq_0_iff zmod_le_nonneg_dividend)
show \<open>(1 + a) div 2 = a div 2\<close>
if \<open>even a\<close>
for a :: \<open>'a word\<close>
@@ -2995,7 +2995,7 @@
0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
unfolding udvd_unfold_int
apply (simp add: uint_arith_simps split: if_split_asm)
- apply (metis (no_types, hide_lams) le_add_diff_inverse le_less_trans udvd_incr_lem)
+ apply (metis (no_types, opaque_lifting) le_add_diff_inverse le_less_trans udvd_incr_lem)
using uint_lt2p [of s] by simp
@@ -3915,8 +3915,8 @@
using zmod_zminus1_eq_if [of \<open>1 + (int m + int n mod int LENGTH('a))\<close> \<open>int LENGTH('a)\<close>]
apply simp_all
apply (auto simp add: algebra_simps)
- apply (metis (mono_tags, hide_lams) Abs_fnat_hom_add mod_Suc mod_mult_self2_is_0 of_nat_Suc of_nat_mod semiring_char_0_class.of_nat_neq_0)
- apply (metis (no_types, hide_lams) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod)
+ apply (metis (mono_tags, opaque_lifting) Abs_fnat_hom_add mod_Suc mod_mult_self2_is_0 of_nat_Suc of_nat_mod semiring_char_0_class.of_nat_neq_0)
+ apply (metis (no_types, opaque_lifting) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod)
done
then have \<open>int ((m + n) mod LENGTH('a)) =
int (LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a)))\<close>
--- a/src/HOL/List.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/List.thy Thu Jul 08 08:42:36 2021 +0200
@@ -990,7 +990,7 @@
\<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
by (induct xs ys rule: list_induct2')
(blast, blast, blast,
- metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
+ metis (no_types, opaque_lifting) append_Cons append_Nil list.sel(1))
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
@@ -1146,7 +1146,7 @@
by (iprover dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
- by (metis (no_types, hide_lams) injI list.inject list.simps(9) the_inv_f_f)
+ by (metis (no_types, opaque_lifting) injI list.inject list.simps(9) the_inv_f_f)
lemma inj_map[iff]: "inj (map f) = inj f"
by (blast dest: inj_mapD intro: inj_mapI)
--- a/src/HOL/Nominal/Examples/Class1.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1707,7 +1707,7 @@
case (AndR c1 M c2 M' c3)
then show ?case
apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
- apply (metis (erased, hide_lams))
+ apply (metis (erased, opaque_lifting))
by metis
next
case AndL1
--- a/src/HOL/Nonstandard_Analysis/NSA.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1128,7 +1128,7 @@
using HFinite_add HInfinite_HFinite_iff by blast
lemma HInfinite_HFinite_add: "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HInfinite"
- by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel)
+ by (metis (no_types, opaque_lifting) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel)
lemma HInfinite_ge_HInfinite: "x \<in> HInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y \<in> HInfinite"
for x y :: hypreal
@@ -1141,7 +1141,7 @@
lemma HInfinite_HFinite_not_Infinitesimal_mult:
"x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HInfinite"
for x y :: "'a::real_normed_div_algebra star"
- by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse)
+ by (metis (no_types, opaque_lifting) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse)
lemma HInfinite_HFinite_not_Infinitesimal_mult2:
"x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> y * x \<in> HInfinite"
--- a/src/HOL/Probability/Conditional_Expectation.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Probability/Conditional_Expectation.thy Thu Jul 08 08:42:36 2021 +0200
@@ -673,7 +673,7 @@
also have "... = (\<integral> x. f x * max (g x) 0 - f x * max (-g x) 0 \<partial>M)"
by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
also have "... = (\<integral>x. f x * g x \<partial>M)"
- by (metis (mono_tags, hide_lams) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib)
+ by (metis (mono_tags, opaque_lifting) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib)
finally show "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral>x. f x * g x \<partial>M)"
by simp
qed
@@ -728,7 +728,7 @@
also have "... = (\<integral> x. fp x * g x - fm x * g x \<partial>M)"
using intm intp by simp
also have "... = (\<integral> x. f x * g x \<partial>M)"
- unfolding fp_def fm_def by (metis (no_types, hide_lams) diff_0 diff_zero max.commute
+ unfolding fp_def fm_def by (metis (no_types, opaque_lifting) diff_0 diff_zero max.commute
max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
finally show "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)" by simp
qed
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Thu Jul 08 08:42:36 2021 +0200
@@ -78,7 +78,7 @@
shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
proof (intro Quotient3I)
show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
- by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
+ by (metis (opaque_lifting, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
next
show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
--- a/src/HOL/Real.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Real.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1466,7 +1466,7 @@
lemma floor_minus_one_divide_eq_div_numeral [simp]:
"\<lfloor>- (1 / numeral b)::real\<rfloor> = - 1 div numeral b"
-by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right
+by (metis (mono_tags, opaque_lifting) div_minus_right minus_divide_right
floor_divide_of_int_eq of_int_neg_numeral of_int_1)
lemma floor_divide_eq_div_numeral [simp]:
--- a/src/HOL/Real_Vector_Spaces.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Jul 08 08:42:36 2021 +0200
@@ -423,7 +423,7 @@
by (simp_all add: Reals_def)
lemma Reals_add [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a + b \<in> \<real>"
- by (metis (no_types, hide_lams) Reals_def Reals_of_real imageE of_real_add)
+ by (metis (no_types, opaque_lifting) Reals_def Reals_of_real imageE of_real_add)
lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
by (auto simp: Reals_def)
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Jul 08 08:42:36 2021 +0200
@@ -200,7 +200,7 @@
\<open>?X mod ?MM = ?X\<close>
unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq)
- apply (metis (mono_tags, hide_lams) of_int_of_nat_eq ucast_id uint_word_of_int_eq unsigned_of_int)
+ apply (metis (mono_tags, opaque_lifting) of_int_of_nat_eq ucast_id uint_word_of_int_eq unsigned_of_int)
done
qed
@@ -244,7 +244,7 @@
\<open>?X mod ?MM = ?X\<close>
unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq)
- apply (metis (mono_tags, hide_lams) of_nat_nat_take_bit_eq ucast_id unsigned_of_int)
+ apply (metis (mono_tags, opaque_lifting) of_nat_nat_take_bit_eq ucast_id unsigned_of_int)
done
qed
--- a/src/HOL/Series.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Series.thy Thu Jul 08 08:42:36 2021 +0200
@@ -713,7 +713,7 @@
proof (cases m n rule: linorder_class.le_cases)
assume "m \<le> n"
then show ?thesis
- by (metis (mono_tags, hide_lams) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
+ by (metis (mono_tags, opaque_lifting) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
next
assume "n \<le> m"
then show ?thesis
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 08 08:42:36 2021 +0200
@@ -35,12 +35,12 @@
type type_enc
val no_lamsN : string
- val hide_lamsN : string
+ val opaque_liftingN : string
val liftingN : string
+ val opaque_combsN : string
val combsN : string
val combs_and_liftingN : string
val combs_or_liftingN : string
- val lam_liftingN : string
val keep_lamsN : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -108,7 +108,7 @@
val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term
val unmangled_const : string -> string * (string, 'b) atp_term list
val unmangled_const_name : string -> string list
- val helper_table : ((string * bool) * (status * thm) list) list
+ val helper_table : bool -> ((string * bool) * (status * thm) list) list
val trans_lams_of_string :
Proof.context -> type_enc -> string -> term list -> term list * term list
val string_of_status : status -> string
@@ -201,13 +201,13 @@
| is_type_level_monotonicity_based _ = false
val no_lamsN = "no_lams" (* used internally; undocumented *)
-val hide_lamsN = "hide_lams"
+val opaque_liftingN = "opaque_lifting"
val liftingN = "lifting"
+val opaque_combsN = "opaque_combs"
val combsN = "combs"
val combs_and_liftingN = "combs_and_lifting"
val combs_or_liftingN = "combs_or_lifting"
val keep_lamsN = "keep_lams"
-val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *)
val bound_var_prefix = "B_"
val all_bound_var_prefix = "A_"
@@ -1727,24 +1727,24 @@
val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
(* The Boolean indicates that a fairly sound type encoding is needed. *)
-val base_helper_table =
- [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
- (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
- (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
- (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
- (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
- ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
+fun helper_table with_combs =
+ (if with_combs then
+ [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
+ (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
+ (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
+ (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
+ (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})])]
+ else
+ []) @
+ [((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
(("fFalse", false), [(General, not_ffalse)]),
(("fFalse", true), [(General, @{thm True_or_False})]),
(("fTrue", false), [(General, ftrue)]),
(("fTrue", true), [(General, @{thm True_or_False})]),
(("If", true),
[(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
- (General, @{thm True_or_False})])]
-
-val helper_table =
- base_helper_table @
- [(("fNot", false),
+ (General, @{thm True_or_False})]),
+ (("fNot", false),
@{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
|> map (pair Non_Rec_Def)),
@@ -1771,8 +1771,8 @@
(("fEx", false), [(General, @{lemma "\<not> P x \<or> fEx P" by (auto simp: fEx_def)})])]
|> map (apsnd (map (apsnd zero_var_indexes)))
-val completish_helper_table =
- helper_table @
+fun completish_helper_table with_combs =
+ helper_table with_combs @
[((predicator_name, true),
@{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
((app_op_name, true),
@@ -1827,7 +1827,7 @@
fun should_specialize_helper type_enc t =
could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t))
-fun add_helper_facts_of_sym ctxt format type_enc completish (s, {types, ...} : sym_info) =
+fun add_helper_facts_of_sym ctxt format type_enc lam_trans completish (s, {types, ...} : sym_info) =
(case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1854,6 +1854,7 @@
val make_facts = map_filter (make_fact ctxt format type_enc false)
val sound = is_type_enc_sound type_enc
val could_specialize = could_specialize_helpers type_enc
+ val with_combs = lam_trans <> opaque_combsN
in
fold (fn ((helper_s, needs_sound), ths) =>
if (needs_sound andalso not sound) orelse
@@ -1865,11 +1866,11 @@
|> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of))
|> make_facts
|> union (op = o apply2 #iformula))
- (if completish >= 3 then completish_helper_table else helper_table)
+ ((if completish >= 3 then completish_helper_table else helper_table) with_combs)
end
| NONE => I)
-fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
- Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab []
+fun helper_facts_of_sym_table ctxt format type_enc lam_trans completish sym_tab =
+ Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc lam_trans completish) sym_tab []
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
@@ -1908,11 +1909,11 @@
fun trans_lams_of_string ctxt type_enc lam_trans =
if lam_trans = no_lamsN then
rpair []
- else if lam_trans = hide_lamsN then
+ else if lam_trans = opaque_liftingN then
lift_lams ctxt type_enc ##> K []
- else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
+ else if lam_trans = liftingN then
lift_lams ctxt type_enc
- else if lam_trans = combsN then
+ else if lam_trans = opaque_combsN orelse lam_trans = combsN then
map (introduce_combinators ctxt type_enc) #> rpair []
else if lam_trans = combs_and_liftingN then
lift_lams_part_1 ctxt type_enc
@@ -2736,7 +2737,7 @@
|> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
uncurried_alias_eq_tms
val helpers =
- sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
+ sym_tab |> helper_facts_of_sym_table ctxt format type_enc lam_trans completish
|> map (firstorderize true)
val all_facts = helpers @ conjs @ facts
val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
--- a/src/HOL/Tools/Metis/metis_generate.ML Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Thu Jul 08 08:42:36 2021 +0200
@@ -171,7 +171,7 @@
else if String.isPrefix helper_prefix ident then
(case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
(needs_fairly_sound, _ :: const :: j :: _) =>
- nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
+ nth (AList.lookup (op =) (helper_table true) (const, needs_fairly_sound) |> the)
(the (Int.fromString j) - 1)
|> snd |> prepare_helper ctxt
|> Isa_Raw |> some
@@ -217,7 +217,7 @@
fold_rev (fn (name, th) => fn (old_skolems, props) =>
th |> Thm.prop_of |> Logic.strip_imp_concl
|> conceal_old_skolem_terms (length clauses) old_skolems
- ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
+ ||> lam_trans = liftingN ? eliminate_lam_wrappers
||> (fn prop => (name, prop) :: props))
clauses ([], [])
(*
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jul 08 08:42:36 2021 +0200
@@ -149,8 +149,7 @@
val thy = Proof_Context.theory_of ctxt
val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
- val do_lams =
- (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt
+ val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt
val th_cls_pairs =
map2 (fn j => fn th =>
(Thm.get_name_hint th,
@@ -280,14 +279,19 @@
(the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
end
-val metis_lam_transs = [hide_lamsN, liftingN, combsN]
+val metis_lam_transs = [opaque_liftingN, liftingN, combsN]
fun set_opt _ x NONE = SOME x
| set_opt get x (SOME x0) =
error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
fun consider_opt s =
- if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
+ if s = "hide_lams" then
+ error "\"hide_lams\" has been renamed \"opaque_lifting\""
+ else if member (op =) metis_lam_transs s then
+ apsnd (set_opt I s)
+ else
+ apfst (set_opt hd [s])
val parse_metis_options =
Scan.optional
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Jul 08 08:42:36 2021 +0200
@@ -356,7 +356,7 @@
val preferred_methss =
(Metis_Method (NONE, NONE),
bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types
- (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
+ (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN))
in
(used_facts, preferred_methss,
fn preplay =>
--- a/src/HOL/Transcendental.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Transcendental.thy Thu Jul 08 08:42:36 2021 +0200
@@ -2367,7 +2367,7 @@
have "-x \<le> (exp(-x) - inverse(exp(-x))) / 2"
by (meson False linear neg_le_0_iff_le real_le_x_sinh)
also have "\<dots> \<le> \<bar>(exp x - inverse (exp x)) / 2\<bar>"
- by (metis (no_types, hide_lams) abs_divide abs_le_iff abs_minus_cancel
+ by (metis (no_types, opaque_lifting) abs_divide abs_le_iff abs_minus_cancel
add.inverse_inverse exp_minus minus_diff_eq order_refl)
finally show ?thesis
using False by linarith
@@ -3942,7 +3942,7 @@
by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
lemma cos_2pi_minus [simp]: "cos (2 * pi - x) = cos x"
- by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi
+ by (metis (no_types, opaque_lifting) cos_add cos_minus cos_two_pi sin_minus sin_two_pi
diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
lemma sin_gt_zero2: "0 < x \<Longrightarrow> x < pi/2 \<Longrightarrow> 0 < sin x"
@@ -4987,7 +4987,7 @@
using arcsin_sin [of "- pi/2"] by simp
lemma arcsin_minus: "- 1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin (- x) = - arcsin x"
- by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
+ by (metis (no_types, opaque_lifting) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
lemma arcsin_eq_iff: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x = arcsin y \<longleftrightarrow> x = y"
by (metis abs_le_iff arcsin minus_le_iff)
--- a/src/HOL/Vector_Spaces.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Vector_Spaces.thy Thu Jul 08 08:42:36 2021 +0200
@@ -1193,7 +1193,7 @@
lemma dim_psubset:
"span S \<subset> span T \<Longrightarrow> dim S < dim T"
- by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
+ by (metis (no_types, opaque_lifting) dim_span less_le not_le subspace_dim_equal subspace_span)
lemma dim_eq_full:
shows "dim S = dimension \<longleftrightarrow> span S = UNIV"
--- a/src/HOL/ex/Dedekind_Real.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Thu Jul 08 08:42:36 2021 +0200
@@ -215,7 +215,7 @@
lemma preal_add_commute: "(x::preal) + y = y + x"
unfolding preal_add_def add_set_def
- by (metis (no_types, hide_lams) add.commute)
+ by (metis (no_types, opaque_lifting) add.commute)
text\<open>Lemmas for proving that addition of two positive reals gives
a positive real\<close>
@@ -301,7 +301,7 @@
lemma preal_mult_commute: "(x::preal) * y = y * x"
unfolding preal_mult_def mult_set_def
- by (metis (no_types, hide_lams) mult.commute)
+ by (metis (no_types, opaque_lifting) mult.commute)
text\<open>Multiplication of two positive reals gives a positive real.\<close>
@@ -373,7 +373,7 @@
lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
apply (simp add: preal_mult_def mem_mult_set Rep_preal)
apply (simp add: mult_set_def)
- apply (metis (no_types, hide_lams) ab_semigroup_mult_class.mult_ac(1))
+ apply (metis (no_types, opaque_lifting) ab_semigroup_mult_class.mult_ac(1))
done
instance preal :: ab_semigroup_mult
@@ -1087,7 +1087,7 @@
"!!(x1::preal). \<lbrakk>x1 + y2 = x2 + y1\<rbrakk> \<Longrightarrow>
x * x1 + y * y1 + (x * y2 + y * x2) =
x * x2 + y * y2 + (x * y1 + y * x1)"
- by (metis (no_types, hide_lams) add.left_commute preal_add_commute preal_add_mult_distrib2)
+ by (metis (no_types, opaque_lifting) add.left_commute preal_add_commute preal_add_mult_distrib2)
lemma real_mult_congruent2:
"(\<lambda>p1 p2.