more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
--- a/src/Doc/Isar_Ref/Generic.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Tue May 23 21:43:36 2023 +0200
@@ -840,9 +840,9 @@
(*<*)experiment begin(*>*)
simproc_setup unit ("x::unit") =
- \<open>fn _ => fn _ => fn ct =>
+ \<open>K (K (fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
- else SOME (mk_meta_eq @{thm unit_eq})\<close>
+ else SOME (mk_meta_eq @{thm unit_eq})))\<close>
(*<*)end(*>*)
text \<open>
--- a/src/HOL/Bali/Eval.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/Eval.thy Tue May 23 21:43:36 2023 +0200
@@ -851,28 +851,28 @@
by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))))\<close>
simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_var_eq}))))\<close>
simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))))\<close>
simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))))\<close>
ML \<open>
ML_Thms.bind_thms ("AbruptIs", sum3_instantiate \<^context> @{thm eval.Abrupt})
@@ -947,10 +947,10 @@
done
simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>None\<close>, _)) $ _) $ _ $ _ $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))))
\<close>
@@ -967,10 +967,10 @@
done
simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>, _) $ _)$ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm eval_abrupt}))))
\<close>
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
--- a/src/HOL/Bali/Evaln.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/Evaln.thy Tue May 23 21:43:36 2023 +0200
@@ -269,28 +269,28 @@
by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))))\<close>
simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))))\<close>
simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))))\<close>
simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))))\<close>
ML \<open>ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate \<^context> @{thm evaln.Abrupt})\<close>
declare evaln_AbruptIs [intro!]
@@ -356,11 +356,11 @@
done
simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>,_) $ _)$ _))
=> NONE
- | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))))
\<close>
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
--- a/src/HOL/Bali/WellType.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/WellType.thy Tue May 23 21:43:36 2023 +0200
@@ -605,28 +605,28 @@
by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))))\<close>
simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_var_eq}))))\<close>
simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))))\<close>
simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))))\<close>
lemma wt_elim_BinOp:
"\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
--- a/src/HOL/Boolean_Algebras.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Boolean_Algebras.thy Tue May 23 21:43:36 2023 +0200
@@ -513,10 +513,10 @@
ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
+ \<open>K (K (try Boolean_Algebra_Cancel.cancel_sup_conv))\<close>
simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
+ \<open>K (K (try Boolean_Algebra_Cancel.cancel_inf_conv))\<close>
context boolean_algebra
--- a/src/HOL/Data_Structures/Less_False.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Data_Structures/Less_False.thy Tue May 23 21:43:36 2023 +0200
@@ -6,7 +6,7 @@
imports Main
begin
-simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup less_False ("(x::'a::order) < y") = \<open>K (fn ctxt => fn ct =>
let
fun prp t thm = Thm.full_prop_of thm aconv t;
@@ -25,7 +25,7 @@
end
| SOME thm => NONE
end;
- in prove_less_False (Thm.term_of ct) end
+ in prove_less_False (Thm.term_of ct) end)
\<close>
end
--- a/src/HOL/Enum.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Enum.thy Tue May 23 21:43:36 2023 +0200
@@ -564,10 +564,10 @@
by(cases x) simp
simproc_setup finite_1_eq ("x::finite_1") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>a\<^sub>1\<close>, _) => NONE
- | _ => SOME (mk_meta_eq @{thm finite_1_eq}))
+ | _ => SOME (mk_meta_eq @{thm finite_1_eq}))))
\<close>
instantiation finite_1 :: complete_boolean_algebra
--- a/src/HOL/Finite_Set.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 23 21:43:36 2023 +0200
@@ -193,7 +193,7 @@
lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
by (rule rev_finite_subset)
-simproc_setup finite ("finite A") = \<open>fn _ =>
+simproc_setup finite ("finite A") = \<open>
let
val finite_subset = @{thm finite_subset}
val Eq_TrueI = @{thm Eq_TrueI}
@@ -209,17 +209,17 @@
fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
- fun proc ss ct =
+ fun proc ctxt ct =
(let
val _ $ A = Thm.term_of ct
- val prems = Simplifier.prems_of ss
+ val prems = Simplifier.prems_of ctxt
val fins = map_filter is_finite prems
val subsets = map_filter (is_subset A) prems
in case fold_product comb subsets fins [] of
(sub_th,fin_th) :: _ => SOME((fin_th RS (sub_th RS finite_subset)) RS Eq_TrueI)
| _ => NONE
end)
-in proc end
+in K proc end
\<close>
(* Needs to be used with care *)
--- a/src/HOL/Fun.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Fun.thy Tue May 23 21:43:36 2023 +0200
@@ -1353,7 +1353,7 @@
text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
-simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
+simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
let
fun gen_fun_upd NONE T _ _ = NONE
| gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
@@ -1380,7 +1380,7 @@
resolve_tac ctxt @{thms ext} 1 THEN
simp_tac (put_simpset ss ctxt) 1)))
end
- in proc end
+ in K proc end
\<close>
--- a/src/HOL/Groups.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Groups.thy Tue May 23 21:43:36 2023 +0200
@@ -178,8 +178,8 @@
| _ => false)
\<close>
-simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
-simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
+simproc_setup reorient_zero ("0 = x") = \<open>K Reorient_Proc.proc\<close>
+simproc_setup reorient_one ("1 = x") = \<open>K Reorient_Proc.proc\<close>
typed_print_translation \<open>
let
--- a/src/HOL/HOL.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOL.thy Tue May 23 21:43:36 2023 +0200
@@ -1236,7 +1236,7 @@
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
-simproc_setup neq ("x = y") = \<open>fn _ =>
+simproc_setup neq ("x = y") = \<open>
let
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
fun is_neq eq lhs rhs thm =
@@ -1252,7 +1252,7 @@
SOME thm => SOME (thm RS neq_to_EQ_False)
| NONE => NONE)
| _ => NONE);
- in proc end
+ in K proc end
\<close>
simproc_setup let_simp ("Let x f") = \<open>
@@ -1266,7 +1266,7 @@
Abs (_, _, t') => count_loose t' 0 <= 1
| _ => true);
in
- fn _ => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
if is_trivial_let (Thm.term_of ct)
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
else
@@ -1308,7 +1308,7 @@
in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
end
| _ => NONE)
- end
+ end)
end
\<close>
@@ -1649,7 +1649,7 @@
signature REORIENT_PROC =
sig
val add : (term -> bool) -> theory -> theory
- val proc : morphism -> Proof.context -> cterm -> thm option
+ val proc : Proof.context -> cterm -> thm option
end;
structure Reorient_Proc : REORIENT_PROC =
@@ -1664,7 +1664,7 @@
fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
- fun proc phi ctxt ct =
+ fun proc ctxt ct =
let
val thy = Proof_Context.theory_of ctxt;
in
@@ -1851,12 +1851,12 @@
declare [[coercion_args NO_MATCH - -]]
-simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>K (fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt
val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
- in if m then NONE else SOME @{thm NO_MATCH_def} end
+ in if m then NONE else SOME @{thm NO_MATCH_def} end)
\<close>
text \<open>
--- a/src/HOL/HOLCF/Cfun.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Tue May 23 21:43:36 2023 +0200
@@ -142,14 +142,14 @@
\<close>
simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
- fn phi => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
let
val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
- in SOME (perhaps (SINGLE (tac 1)) tr) end
+ in SOME (perhaps (SINGLE (tac 1)) tr) end)
\<close>
text \<open>Eta-equality for continuous functions\<close>
--- a/src/HOL/HOLCF/Pcpo.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Tue May 23 21:43:36 2023 +0200
@@ -157,7 +157,7 @@
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
-simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
+simproc_setup reorient_bottom ("\<bottom> = x") = \<open>K Reorient_Proc.proc\<close>
text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>
--- a/src/HOL/Library/Extended_Nat.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Tue May 23 21:43:36 2023 +0200
@@ -588,15 +588,15 @@
simproc_setup enat_eq_cancel
("(l::enat) + m = n" | "(l::enat) = m + n") =
- \<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup enat_le_cancel
("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
- \<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup enat_less_cancel
("(l::enat) + m < n" | "(l::enat) < m + n") =
- \<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
text \<open>TODO: add regression tests for these simprocs\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 23 21:43:36 2023 +0200
@@ -433,15 +433,15 @@
simproc_setup ennreal_eq_cancel
("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
- \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup ennreal_le_cancel
("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
- \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup ennreal_less_cancel
("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
- \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
subsection \<open>Order with top\<close>
--- a/src/HOL/Library/Multiset.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Multiset.thy Tue May 23 21:43:36 2023 +0200
@@ -1003,28 +1003,28 @@
"add_mset a m = n" | "m = add_mset a n" |
"replicate_mset p a = n" | "m = replicate_mset p a" |
"repeat_mset p m = n" | "m = repeat_mset p m") =
- \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
+ \<open>K Cancel_Simprocs.eq_cancel\<close>
simproc_setup msetsubset_cancel
("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
"add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
"replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
"repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
- \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
+ \<open>K Multiset_Simprocs.subset_cancel_msets\<close>
simproc_setup msetsubset_eq_cancel
("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
"add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
"replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
"repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
- \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
+ \<open>K Multiset_Simprocs.subseteq_cancel_msets\<close>
simproc_setup msetdiff_cancel
("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
"add_mset a m - n" | "m - add_mset a n" |
"replicate_mset p r - n" | "m - replicate_mset p r" |
"repeat_mset p m - n" | "m - repeat_mset p m") =
- \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
+ \<open>K Cancel_Simprocs.diff_cancel\<close>
subsubsection \<open>Conditionally complete lattice\<close>
--- a/src/HOL/Library/Multiset_Order.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Tue May 23 21:43:36 2023 +0200
@@ -776,14 +776,14 @@
"add_mset a m < n" | "m < add_mset a n" |
"replicate_mset p a < n" | "m < replicate_mset p a" |
"repeat_mset p m < n" | "m < repeat_mset p n") =
- \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
+ \<open>K Cancel_Simprocs.less_cancel\<close>
simproc_setup msetle_cancel
("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
"add_mset a m \<le> n" | "m \<le> add_mset a n" |
"replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
"repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
- \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
+ \<open>K Cancel_Simprocs.less_eq_cancel\<close>
subsection \<open>Additional facts and instantiations\<close>
--- a/src/HOL/List.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/List.thy Tue May 23 21:43:36 2023 +0200
@@ -1045,7 +1045,7 @@
else if lastl aconv lastr then rearr @{thm append_same_eq}
else NONE
end;
- in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end
+ in K (fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct)) end
\<close>
--- a/src/HOL/Nat.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Nat.thy Tue May 23 21:43:36 2023 +0200
@@ -1968,19 +1968,19 @@
simproc_setup nateq_cancel_sums
("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_eq_conv)\<close>
simproc_setup natless_cancel_sums
("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_less_conv)\<close>
simproc_setup natle_cancel_sums
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_le_conv)\<close>
simproc_setup natdiff_cancel_sums
("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_diff_conv)\<close>
context order
begin
--- a/src/HOL/Nonstandard_Analysis/NSA.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Tue May 23 21:43:36 2023 +0200
@@ -549,12 +549,12 @@
("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
\<open>
let val rule = @{thm approx_reorient} RS eq_reflection
- fun proc phi ss ct =
+ fun proc ct =
case Thm.term_of ct of
_ $ t $ u => if can HOLogic.dest_number u then NONE
else if can HOLogic.dest_number t then SOME rule else NONE
| _ => NONE
- in proc end
+ in K (K proc) end
\<close>
lemma Infinitesimal_approx_minus: "x - y \<in> Infinitesimal \<longleftrightarrow> x \<approx> y"
--- a/src/HOL/Num.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Num.thy Tue May 23 21:43:36 2023 +0200
@@ -1394,7 +1394,7 @@
\<close>
simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
- Reorient_Proc.proc
+ \<open>K Reorient_Proc.proc\<close>
subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
--- a/src/HOL/Numeral_Simprocs.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Numeral_Simprocs.thy Tue May 23 21:43:36 2023 +0200
@@ -104,17 +104,17 @@
simproc_setup semiring_assoc_fold
("(a::'a::comm_semiring_1_cancel) * b") =
- \<open>fn phi => Numeral_Simprocs.assoc_fold\<close>
+ \<open>K Numeral_Simprocs.assoc_fold\<close>
(* TODO: see whether the type class can be generalized further *)
simproc_setup int_combine_numerals
("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
- \<open>fn phi => Numeral_Simprocs.combine_numerals\<close>
+ \<open>K Numeral_Simprocs.combine_numerals\<close>
simproc_setup field_combine_numerals
("(i::'a::{field,ring_char_0}) + j"
|"(i::'a::{field,ring_char_0}) - j") =
- \<open>fn phi => Numeral_Simprocs.field_combine_numerals\<close>
+ \<open>K Numeral_Simprocs.field_combine_numerals\<close>
simproc_setup inteq_cancel_numerals
("(l::'a::comm_ring_1) + m = n"
@@ -125,7 +125,7 @@
|"(l::'a::comm_ring_1) = m * n"
|"- (l::'a::comm_ring_1) = m"
|"(l::'a::comm_ring_1) = - m") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_numerals\<close>
simproc_setup intless_cancel_numerals
("(l::'a::linordered_idom) + m < n"
@@ -136,7 +136,7 @@
|"(l::'a::linordered_idom) < m * n"
|"- (l::'a::linordered_idom) < m"
|"(l::'a::linordered_idom) < - m") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.less_cancel_numerals\<close>
simproc_setup intle_cancel_numerals
("(l::'a::linordered_idom) + m \<le> n"
@@ -147,138 +147,138 @@
|"(l::'a::linordered_idom) \<le> m * n"
|"- (l::'a::linordered_idom) \<le> m"
|"(l::'a::linordered_idom) \<le> - m") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.le_cancel_numerals\<close>
simproc_setup ring_eq_cancel_numeral_factor
("(l::'a::{idom,ring_char_0}) * m = n"
|"(l::'a::{idom,ring_char_0}) = m * n") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_numeral_factor\<close>
simproc_setup ring_less_cancel_numeral_factor
("(l::'a::linordered_idom) * m < n"
|"(l::'a::linordered_idom) < m * n") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.less_cancel_numeral_factor\<close>
simproc_setup ring_le_cancel_numeral_factor
("(l::'a::linordered_idom) * m <= n"
|"(l::'a::linordered_idom) <= m * n") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.le_cancel_numeral_factor\<close>
(* TODO: remove comm_ring_1 constraint if possible *)
simproc_setup int_div_cancel_numeral_factors
("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
|"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
- \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.div_cancel_numeral_factor\<close>
simproc_setup divide_cancel_numeral_factor
("((l::'a::{field,ring_char_0}) * m) / n"
|"(l::'a::{field,ring_char_0}) / (m * n)"
|"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
- \<open>fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.divide_cancel_numeral_factor\<close>
simproc_setup ring_eq_cancel_factor
("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_factor\<close>
simproc_setup linordered_ring_le_cancel_factor
("(l::'a::linordered_idom) * m <= n"
|"(l::'a::linordered_idom) <= m * n") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.le_cancel_factor\<close>
simproc_setup linordered_ring_less_cancel_factor
("(l::'a::linordered_idom) * m < n"
|"(l::'a::linordered_idom) < m * n") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.less_cancel_factor\<close>
simproc_setup int_div_cancel_factor
("((l::'a::euclidean_semiring_cancel) * m) div n"
|"(l::'a::euclidean_semiring_cancel) div (m * n)") =
- \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.div_cancel_factor\<close>
simproc_setup int_mod_cancel_factor
("((l::'a::euclidean_semiring_cancel) * m) mod n"
|"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
- \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.mod_cancel_factor\<close>
simproc_setup dvd_cancel_factor
("((l::'a::idom) * m) dvd n"
|"(l::'a::idom) dvd (m * n)") =
- \<open>fn phi => Numeral_Simprocs.dvd_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.dvd_cancel_factor\<close>
simproc_setup divide_cancel_factor
("((l::'a::field) * m) / n"
|"(l::'a::field) / (m * n)") =
- \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.divide_cancel_factor\<close>
ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
simproc_setup nat_combine_numerals
("(i::nat) + j" | "Suc (i + j)") =
- \<open>fn phi => Nat_Numeral_Simprocs.combine_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.combine_numerals\<close>
simproc_setup nateq_cancel_numerals
("(l::nat) + m = n" | "(l::nat) = m + n" |
"(l::nat) * m = n" | "(l::nat) = m * n" |
"Suc m = n" | "m = Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
simproc_setup natless_cancel_numerals
("(l::nat) + m < n" | "(l::nat) < m + n" |
"(l::nat) * m < n" | "(l::nat) < m * n" |
"Suc m < n" | "m < Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_numerals\<close>
simproc_setup natle_cancel_numerals
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
"(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
"Suc m \<le> n" | "m \<le> Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_numerals\<close>
simproc_setup natdiff_cancel_numerals
("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
"(l::nat) * m - n" | "(l::nat) - m * n" |
"Suc m - n" | "m - Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
simproc_setup nat_eq_cancel_numeral_factor
("(l::nat) * m = n" | "(l::nat) = m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
simproc_setup nat_less_cancel_numeral_factor
("(l::nat) * m < n" | "(l::nat) < m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
simproc_setup nat_le_cancel_numeral_factor
("(l::nat) * m <= n" | "(l::nat) <= m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
simproc_setup nat_div_cancel_numeral_factor
("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
simproc_setup nat_dvd_cancel_numeral_factor
("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
simproc_setup nat_eq_cancel_factor
("(l::nat) * m = n" | "(l::nat) = m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_factor\<close>
simproc_setup nat_less_cancel_factor
("(l::nat) * m < n" | "(l::nat) < m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_factor\<close>
simproc_setup nat_le_cancel_factor
("(l::nat) * m <= n" | "(l::nat) <= m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_factor\<close>
simproc_setup nat_div_cancel_factor
("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.div_cancel_factor\<close>
simproc_setup nat_dvd_cancel_factor
("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
declaration \<open>
K (Lin_Arith.add_simprocs
--- a/src/HOL/Product_Type.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Product_Type.thy Tue May 23 21:43:36 2023 +0200
@@ -73,9 +73,9 @@
\<close>
simproc_setup unit_eq ("x::unit") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
- else SOME (mk_meta_eq @{thm unit_eq})
+ else SOME (mk_meta_eq @{thm unit_eq})))
\<close>
free_constructors case_unit for "()"
@@ -570,9 +570,9 @@
end;
\<close>
simproc_setup case_prod_beta ("case_prod f z") =
- \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct))\<close>
simproc_setup case_prod_eta ("case_prod f") =
- \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct))\<close>
lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
by (auto simp: fun_eq_iff)
@@ -1326,7 +1326,7 @@
(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
simproc_setup Collect_mem ("Collect t") = \<open>
- fn _ => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
(case Thm.term_of ct of
S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
let val (u, _, ps) = HOLogic.strip_ptupleabs t in
@@ -1355,7 +1355,7 @@
else NONE)
| _ => NONE)
end
- | _ => NONE)
+ | _ => NONE))
\<close>
ML_file \<open>Tools/inductive_set.ML\<close>
--- a/src/HOL/Set.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Set.thy Tue May 23 21:43:36 2023 +0200
@@ -65,13 +65,13 @@
\<close>
simproc_setup defined_Collect ("{x. P x \<and> Q x}") = \<open>
- fn _ => Quantifier1.rearrange_Collect
+ K (Quantifier1.rearrange_Collect
(fn ctxt =>
resolve_tac ctxt @{thms Collect_cong} 1 THEN
resolve_tac ctxt @{thms iffI} 1 THEN
ALLGOALS
(EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
- DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
+ DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})])))
\<close>
lemmas CollectE = CollectD [elim_format]
@@ -330,13 +330,11 @@
\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>
simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>
lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
--- a/src/ZF/OrdQuant.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/ZF/OrdQuant.thy Tue May 23 21:43:36 2023 +0200
@@ -350,13 +350,11 @@
text \<open>Setting up the one-point-rule simproc\<close>
simproc_setup defined_rex ("\<exists>x[M]. P(x) \<and> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms rex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def}))
\<close>
simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms rall_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def}))
\<close>
end
--- a/src/ZF/pair.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/ZF/pair.thy Tue May 23 21:43:36 2023 +0200
@@ -19,13 +19,11 @@
ML \<open>val ZF_ss = simpset_of \<^context>\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) \<and> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>