# HG changeset patch # User desharna # Date 1625726556 -7200 # Node ID fd21b4a9304300e317193bc58e1bde783e2b4aec # Parent 66bff50bc5f11adb68618e4adb07716b5d4fab6e added opaque_combs and renamed hide_lams to opaque_lifting diff -r 66bff50bc5f1 -r fd21b4a93043 src/Doc/Sledgehammer/document/root.tex --- 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, diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Coset.thy --- 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 \\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \\<^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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Free_Abelian_Groups.thy --- 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: "(\i. i \ I \ x i \ carrier (free_Abelian_group S)) \ sum x I \ 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: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Generated_Groups.thy --- 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 *: "\A. carrier G \ A \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Group.thy --- 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 "(\ \) \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = (\ \) \\<^bsub>H\<^esub> (\ \)" 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Polynomial_Divisibility.thy --- 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 \degree p = 1\ 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 \ K - { \ }" "b \ K" and in_carrier: "a \ carrier R" "b \ 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 \ carrier R" "a \ inv a = \" and "inv a \ K" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Product_Groups.thy --- 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 \ {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Subrings.thy --- 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 \ 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: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Abstract_Topology.thy --- 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 "\x'. x' \ topspace X' \ g x' \ 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: "\section_map X Y f; x \ topspace X; y \ topspace X\ \ f x = f y \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Abstract_Topology_2.thy --- 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: "\path_connected_space X; X homeomorphic_space Y\ \ 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 \ path_connected_space X \ path_connected_space Y" @@ -1351,7 +1351,7 @@ assume "U \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Arcwise_Connected.thy --- 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 \_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF) + unfolding \_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 \_def) @@ -1950,7 +1950,7 @@ then have "arc g" by (metis arc_def path_def inj_on_def) obtain u v where "u \ {0..1}" "a = g u" "v \ {0..1}" "b = g v" - by (metis (mono_tags, hide_lams) \\ T\ \_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) \\ T\ \_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 \ path_image g" "b \ path_image g" using path_image_def by blast+ have ph: "path_image h \ path_image p" @@ -2003,7 +2003,7 @@ assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \ pathfinish h" obtains i where "arc i" "path_image i \ path_image g \ 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) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Bochner_Integration.thy --- 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 "\ \ (\\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \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 "\ = ?S + ?T" by (rule nn_integral_add) auto diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Brouwer_Fixpoint.thy --- 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 "\x. x \ frontier (cball a B) \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Cartesian_Space.thy --- 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 \ f(0::'a::real_inner) = (0::'a) \ (\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) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Change_Of_Vars.thy --- 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 "\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ = \prod m UNIV\ * \z - measure lebesgue S\" - 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 "\ < e" using zless True by (simp add: field_simps) finally show "\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ < e" . @@ -563,7 +563,7 @@ by (simp add: bounded_plus [OF bo]) moreover have "?rfs \ ?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 \ \det (matrix (f' x))\" "\det (matrix (f' x))\ < (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 *: "\T (b *\<^sub>R axis k 1) \ (y - x)\ = b * \inv T y $ k - ?x' $ k\" for y proof - have "\T (b *\<^sub>R axis k 1) \ (y - x)\ = \(b *\<^sub>R axis k 1) \ inv T (y - x)\" - 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 "\ = b * \(axis k 1) \ inv T (y - x)\" using \b > 0\ by (simp add: abs_mult) also have "\ = b * \inv T y $ k - ?x' $ k\" @@ -1480,7 +1480,7 @@ (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" (is "\e>0. \d>0. \A. ?\ e d A") then have "\k. \d>0. \A. ?\ (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 \ A where \: "\k. \ k > 0" and Ab: "\k. A k $ m $ n < b" and A: "\k y. \y \ S; norm (y - x) < \ k\ \ @@ -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) \ e" @@ -2180,7 +2180,7 @@ using r12 by auto ultimately have "norm (v - u) \ 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 \ norm (v - u) ^ ?m" by (simp add: power_decreasing [OF mlen]) also have "\ \ ?\ K * real (?m ^ ?m)" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Complex_Transcendental.thy --- 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 \] 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>\tag unimportant\\Analytic properties of tangent function\ @@ -1333,7 +1333,7 @@ then have "\y. y \ V \ g' y = inv ((*) y)" by (metis exp_Ln g' g_eq_Ln) then have g': "g' z = (\x. x/z)" - by (metis (no_types, hide_lams) bij \z \ V\ bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz) + by (metis (no_types, opaque_lifting) bij \z \ V\ 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 \z \ V\] g' by (simp add: \z \ V\ field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative) @@ -3986,7 +3986,7 @@ also have "... \ (\z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))" by simp also have "... \ (\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 "... \ int j mod int n = int k mod int n" by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps) also have "... \ j mod n = k mod n" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Connected.thy --- 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 @@ \ 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: "\(connected_component_set S ` S) = S" @@ -335,7 +335,7 @@ by simp lemma connected_eq_connected_components_eq: "connected s \ (\c \ components s. \c' \ 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} \ connected s \ s \ {}" apply (rule iffI) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Cross3.thy --- 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 "... \ \x \ y\ = 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 "... \ collinear {0, x, y}" by (rule norm_cauchy_schwarz_equal) finally show ?thesis . diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Derivative.thy --- 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 "\x. x \ S \ vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)) = vector_derivative (g \ 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) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Determinants.thy --- 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 \ x = ?t_jk \ 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 \ (*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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- 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 \ 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 \ 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>\tag important\ prod :: (heine_borel, heine_borel) heine_borel proof diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 \ (x + c *\<^sub>R w) = b" "a \ (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 "\t\ < B" then show "a $ 1 \ t \ t \ 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: "(\x. if vec x \ S then f (vec x) else 0) = (\x. if x \ S then f x else 0) \ 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 \ 2^n" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy --- 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 (\ x) x \ BOX (\ y) y)" if "negligible (BOX2 (\ x) x \ BOX2 (\ 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: "\box. (\D. box (\ (tag D)) (tag D)) ` \ = (\t. box (\ t) t) ` tag ` \" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Extended_Real_Limits.thy --- 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 "(\i\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 \ 0" by auto moreover have "1/z < e" using \e>0\ \z>1/e\ 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 \ 0" "1/z < e" by auto } diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Fashoda_Theorem.thy --- 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 "(\x::real^2. x $ i) ` cbox (- 1) 1 \ {-1..1}" for i by (auto simp: mem_box_cart) show "{-1..1} \ (\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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Function_Metric.thy --- 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 "... \ (\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 "... = (\n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Further_Topology.thy --- 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 \U \ S\ 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: "\z. z \ ball 0 1 \ exp(j z) = (g \ 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]: "\x. x \ S \ h (k x) = x" using hk homeomorphism_apply2 by blast have "\\. continuous_on S \\ (\x\S. f x = exp (\ x))" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 "\x. x \ s \ 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 \ 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 \ \(qq ` r) tagged_division_of \(snd ` p) \ \r" proof (rule tagged_division_Un[OF ptag tagged_division_Union [OF \finite r\]]) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Homotopy.thy --- 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 \ 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: "\a b. \0 \ a; a \ 1; 0 \ b; b \ 1\ \ 0 \ (1 - a) * f b + a * b" using f01 by force have fb1: "\0 \ a; a \ 1; 0 \ b; b \ 1\ \ (1 - a) * f b + a * b \ 1" for a b @@ -1846,7 +1846,7 @@ have 2: "openin (top_of_set S) ?B" by (subst openin_subopen, blast) have \
: "?A \ ?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 \ ?A \ ?B" by clarsimp (meson opI) have "?A = {} \ ?B = {}" @@ -1916,7 +1916,7 @@ assume ?lhs then have "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x\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 "\ aff_dim (affine hull S) \ 1" using \\ collinear S\ collinear_aff_dim by auto then have "\ aff_dim (ball x r \ affine hull S) \ 1" - by (metis (no_types, hide_lams) aff_dim_convex_Int_open IntI open_ball \0 < r\ 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 \0 < r\ aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that) then have "\ collinear (ball x r \ affine hull S)" by (simp add: collinear_aff_dim) then have *: "path_connected ((ball x r \ affine hull S) - T)" @@ -5254,7 +5254,7 @@ and hj: "\x. j(h x) = x" "\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: "\x. x \ h ` K \ f x \ h ` U" and sub: "{x. \ (f x = x \ g x = x)} \ h ` S" @@ -5275,7 +5275,7 @@ using hom homeomorphism_def by (blast intro: continuous_on_compose cont_hj)+ show "(j \ f \ h) ` T \ T" "(j \ g \ h) ` T \ 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 "\x. x \ T \ (j \ g \ h) ((j \ f \ h) x) = x" using hj hom homeomorphism_apply1 by fastforce show "\y. y \ T \ (j \ f \ h) ((j \ g \ h) y) = y" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Jordan_Curve.thy --- 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 \ ?\2" and zout: "z \ outside(?\1 \ ?\)" apply (auto simp: outside_inside) using nonempty_simple_path_endless [OF \simple_path c2\] - 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 \ outside(?\1 \ ?\)" using zout op_out1c open_contains_ball_eq by blast have "z \ frontier (inside (?\2 \ ?\))" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Line_Segment.thy --- 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 "\ball a r \ T; T \ cball a r\ \ 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 \ 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 \ 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 = (\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Linear_Algebra.thy --- 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>\tag unimportant\ orthogonal_transformation_inv: "orthogonal_transformation f \ orthogonal_transformation (inv f)" for f :: "'a::euclidean_space \ '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>\tag unimportant\ orthogonal_transformation_norm: "orthogonal_transformation f \ norm (f x) = norm x" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Path_Connected.thy --- 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 = (\x. -a + x) \ ((\x. a + x) \ 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 "\x \ b\ = 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 \r > 0\ 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: "\connected T; inside S \ T \ {}; outside S \ T \ {}\ \ S \ T \ {}" 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" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Polytope.thy --- 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 \T \ S\ by blast then have "\y\S. x \ convex hull (S - {y})" using True affine_independent_iff_card [of S] - by (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 \a \ T\ \T \ S\ \x \ convex hull T\ hull_mono insert_Diff_single subsetCE) + by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_insert0 \a \ T\ \T \ S\ \x \ convex hull T\ hull_mono insert_Diff_single subsetCE) } note * = this have 1: "convex hull S \ (\ a\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 \ -1 \ 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 {} \ n = -1" proof diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Retracts.thy --- 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 @@ \U T. continuous_on T f \ f ` T \ S \ closedin (top_of_set U) T \ (\g. continuous_on U g \ g ` U \ S \ (\x \ 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 ((\) C ` \)" by (simp add: insert.hyps(1)) show "\Ca. Ca \ (\) C ` \ \ 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 "\Ca. Ca \ (\) C ` \ \ convex Ca" by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE) show "card ((\) C ` \) < n" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Starlike.thy --- 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 \ \(insert (U \ V) (\ - {U \ V}))" using \K \ \\\ by auto also have "... \ (U \ V) \ (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 \ K \ U \ V" by blast moreover have "connected(J \ K)" @@ -6366,7 +6366,7 @@ have "(adjoint f) -` {0} = {0}" by (metis \inj (adjoint f)\ adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV) then have "(range(f))\<^sup>\ = {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 \inj (adjoint f)\ adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj) next @@ -6387,7 +6387,7 @@ assume "\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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Tagged_Division.thy --- 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 \m\n\ 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) \ ?K0(n,w) \ ?K0(n,w) \ ?K0(m,v) \ interior(?K0(m,v)) \ interior(?K0(n,w)) = {}" by meson diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Topology_Euclidean_Space.thy --- 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 \ T" and "T \ f ` S" by (metis interiorE) then show "x \ ?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 \ interior S" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Uniform_Limit.thy --- 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 "\\<^sub>F x in F. \y\S. b/2 \ 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 "\\<^sub>F x in F. \y\S. b/2 \ norm (f x y) \ 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) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Auth/Message.thy --- 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) = (\x\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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Binomial.thy --- 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 = (\k\m. (- a gchoose k) * (- x) ^ k * (x + y) ^ (m - k))" by (simp add: gbinomial_partial_sum_poly) also have "... = (\k\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 . diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Cardinals/Wellorder_Constructions.thy --- 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) \ r \ (j,i) \ r \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Combinatorics/Cycles.thy --- 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 \ least_power p a - 1" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy --- 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: "\f holomorphic_on S; open S; x \ S\ \ ((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: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Complex_Singularities.thy --- 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 \z\ 0" apply (elim Lim_transform_within[OF _ \r1>0\]) - 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Conformal_Mappings.thy --- 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 "\B. \x. B \ cmod x \ dist ((inverse \ f) x) 0 \ 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 "\z. f z = (\i\n. a i * z^i)" using assms pole_at_infinity by blast diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Great_Picard.thy --- 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"] \2 \ n\ by (metis le_add_diff_inverse2) then have **: "4 + real n * 2 \ 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) \ 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 \ 0" "c \ 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 "\l. (\n. (f \ (r \ k1)) n (\ i)) \ l" "\j. N \ j \ \j'\j. k2 j = k1 j'" for i N and r k1 k2 :: "nat\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 \ that show ?thesis by force @@ -713,7 +713,7 @@ then show "\\<^sub>F n in sequentially. continuous_on S ((\ \ r) n)" by (simp add: eventually_sequentially) show "uniform_limit S (\ \ 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 \ S" and SR: "S \ closure R" @@ -933,7 +933,7 @@ using ex by blast then have "\ g i id (r \ k2)" using that - by (simp add: \_def) (metis (no_types, hide_lams) le_trans linear) + by (simp add: \_def) (metis (no_types, opaque_lifting) le_trans linear) then show ?thesis by metis qed @@ -1207,7 +1207,7 @@ by simp show "\\<^sub>F n in sequentially. \x\K. dist (\ n x - \ 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 "\ (\z. g z - g z1) constant_on S - {z1}" unfolding constant_on_def diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Riemann_Mapping.thy --- 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 (- {\}) p (r +++ q +++ reversepath r)" proof (rule homotopic_paths_imp_homotopic_loops) show "homotopic_paths (- {\}) p (r +++ q +++ reversepath r)" - by (metis (mono_tags, hide_lams) \path r\ L \p \q \path p\ \path q\ 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) \path r\ L \p \q \path p\ \path q\ 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 (- {\}) (r +++ q +++ reversepath r) q" using rim \q by (auto simp: homotopic_loops_conjugate paf \path q\ \path r\ loops) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Winding_Numbers.thy --- 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 \ loop, of "outside(path_image \)"] connected_outside by (metis DIM_complex bounded_path_image dual_order.refl \ outside_no_overlap) ultimately have "winding_number \ z = winding_number \ w" - by (metis (no_types, hide_lams) constant_on_def z) + by (metis (no_types, opaque_lifting) constant_on_def z) also have "\ = 0" proof - have wnot: "w \ path_image \" using wout by (simp add: outside_def) @@ -1577,7 +1577,7 @@ show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \ inside (path_image (linepath (a + e) (a - e)) \ path_image p) \ {}" 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 \ inside (path_image (linepath (a + e) (a - e)) \ path_image (linepath (a + e) c +++ linepath c (a - e)))" @@ -1625,7 +1625,7 @@ proof - have [simp]: "a + of_real x \ closed_segment (a - \) (a - \) \ x \ closed_segment (-\) (-\)" for x \ \::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 \ closed_segment (a + \) (a + \) \ -x \ closed_segment \ \" for x \ \::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 \ closed_segment (a + kde) (a + e)" and znotin_d_kde': "z \ 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 \ 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 \ 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 \0 \ t\ \simple_path q\ \t \ 1\ atLeastAtMost_iff zero_le_one diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Computational_Algebra/Polynomial.thy --- 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Deriv.thy --- 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 < \" "\ < b" "(\y. f' \ y - (f b - f a) / (b - a) * y) = (\v. 0)" by metis then show ?thesis - by (metis (no_types, hide_lams) that add.right_neutral add_diff_cancel_left' add_diff_eq \a < b\ + by (metis (no_types, opaque_lifting) that add.right_neutral add_diff_cancel_left' add_diff_eq \a < b\ less_irrefl nonzero_eq_divide_eq) qed diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Homology/Brouwer_Degree.thy --- 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: "\contractible_space X; S \ topspace X; p \ 0; S \ {}\ \ homology_group p (subtopology X S) \ 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: "\contractible_space X; contractible_space(subtopology X S); topspace X \ S \ {}\ @@ -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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Homology/Invariance_of_Domain.thy --- 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) \\<^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 \\<^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 \a \ b\ negab path_component_of_trans path_component_of_sym x) + by (metis (no_types, opaque_lifting) ** a b \a \ b\ 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)" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Homology/Simplices.thy --- 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 \ 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 \ @@ -1564,7 +1564,7 @@ have 3: "simplex_cone p (Sigp f) g \ ?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 \ 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 = "\(a,b). (a-1,b)" and k = "\(a,b). (Suc a,b)"]) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/IMP/Abs_Int2.thy --- 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 \ \\<^sub>o S1 \ s \ \\<^sub>o S2 \ s \ \\<^sub>o(S1 \ 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 \ 'av st option \ 'av" where "aval'' e None = \" | diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/IMP/Abs_Int3.thy --- 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 \ C2 \ (\i top_on_acom C1 (- vars C1) \ top_on_acom C2 (- vars C2) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Dlist.thy --- 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 \ \zs. Dlist.dlist_eq xs zs \ ys = map f zs \ set zs \ 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 \ set xs = set ys" by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Equipollence.thy --- 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 \ {()}" if "S \ {x}" for x using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2) show "\x. S \ {x}" if "S \ {()}" - 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: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Extended_Nonnegative_Real.thy --- 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 \ (a::real) \ a ^ n \ 1 \ (n = 0 \ a \ 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 \ b \ a - c \ (b::ennreal)" using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Extended_Real.thy --- 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Float.thy --- 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 \p + e < 0\ 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 \ 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 \ float" is "\x. real_of_int \x\" @@ -2404,7 +2404,7 @@ "floor_fl (Float m e) = (if 0 \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/FuncSet.thy --- 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 \ 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: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Interval.thy --- 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 \ max (la * lb) (max (la * ub) (max (lb * ua) (ua * ub)))" if "la \ 0" "0 \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Poly_Mapping.thy --- 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) \ Poly_Mapping.keys a \ 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 \ frag_extend f (\i\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]: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Word.thy --- 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 :: \'a word\ apply transfer apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def) - by (metis (no_types, hide_lams) "\
" 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) "\
" 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 \(1 + a) div 2 = a div 2\ if \even a\ for a :: \'a word\ @@ -2995,7 +2995,7 @@ 0 < K \ p \ p + K \ p + K \ 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 \1 + (int m + int n mod int LENGTH('a))\ \int LENGTH('a)\] 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 \int ((m + n) mod LENGTH('a)) = int (LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a)))\ diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/List.thy --- 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 @@ \ (xs' = [] \ ys' = [] \ hd xs' \ 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 \Trivial rules for solving \@\-equations automatically.\ @@ -1146,7 +1146,7 @@ by (iprover dest: map_injective injD intro: inj_onI) lemma inj_mapD: "inj (map f) \ 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) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Nominal/Examples/Class1.thy --- 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Nonstandard_Analysis/NSA.thy --- 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 \ HInfinite \ y \ HFinite \ x + y \ 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 \ HInfinite \ x \ y \ 0 \ x \ y \ HInfinite" for x y :: hypreal @@ -1141,7 +1141,7 @@ lemma HInfinite_HFinite_not_Infinitesimal_mult: "x \ HInfinite \ y \ HFinite - Infinitesimal \ x * y \ 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 \ HInfinite \ y \ HFinite - Infinitesimal \ y * x \ HInfinite" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Probability/Conditional_Expectation.thy --- 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 "... = (\ x. f x * max (g x) 0 - f x * max (-g x) 0 \M)" by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2) also have "... = (\x. f x * g x \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 "(\ x. f x * real_cond_exp M F g x \M) = (\x. f x * g x \M)" by simp qed @@ -728,7 +728,7 @@ also have "... = (\ x. fp x * g x - fm x * g x \M)" using intm intp by simp also have "... = (\ x. f x * g x \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 "(\ x. f x * real_cond_exp M F g x \M) = (\ x. f x * g x \M)" by simp qed diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Quotient_Examples/Lift_Fun.thy --- 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 "\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 "\a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" using fun_quotient3[OF a a, THEN Quotient3_rep_reflp] diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Real.thy --- 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]: "\- (1 / numeral b)::real\ = - 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]: diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Real_Vector_Spaces.thy --- 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 \ \ \ b \ \ \ a + b \ \" - 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 \ \ \ - a \ \" by (auto simp: Reals_def) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy --- 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 @@ \?X mod ?MM = ?X\ unfolding \?MM = 2 ^ LENGTH(32)\ 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 @@ \?X mod ?MM = ?X\ unfolding \?MM = 2 ^ LENGTH(32)\ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Series.thy --- 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 \ 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 \ m" then show ?thesis diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 "\ P x \ 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Tools/Metis/metis_generate.ML --- 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 ([], []) (* diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Tools/Metis/metis_tactic.ML --- 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 diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 => diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Transcendental.thy --- 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 \ (exp(-x) - inverse(exp(-x))) / 2" by (meson False linear neg_le_0_iff_le real_le_x_sinh) also have "\ \ \(exp x - inverse (exp x)) / 2\" - 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 \ x < pi/2 \ 0 < sin x" @@ -4987,7 +4987,7 @@ using arcsin_sin [of "- pi/2"] by simp lemma arcsin_minus: "- 1 \ x \ x \ 1 \ 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: "\x\ \ 1 \ \y\ \ 1 \ arcsin x = arcsin y \ x = y" by (metis abs_le_iff arcsin minus_le_iff) diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Vector_Spaces.thy --- 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 \ span T \ 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 \ span S = UNIV" diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/ex/Dedekind_Real.thy --- 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\Lemmas for proving that addition of two positive reals gives a positive real\ @@ -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\Multiplication of two positive reals gives a positive real.\ @@ -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). \x1 + y2 = x2 + y1\ \ 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: "(\p1 p2.