--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Fri Oct 11 14:15:10 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Fri Oct 11 15:17:37 2024 +0200
@@ -126,24 +126,10 @@
"_qinfsetsum" \<rightleftharpoons> infsetsum
translations
"\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
-let
- fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const \<^syntax_const>\<open>_qinfsetsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
-in [(\<^const_syntax>\<open>infsetsum\<close>, K sum_tr')] end
+ [(\<^const_syntax>\<open>infsetsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsetsum\<close>))]
\<close>
-
lemma restrict_count_space_subset:
"A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
by (subst restrict_count_space) (simp_all add: Int_absorb2)
--- a/src/HOL/Analysis/Infinite_Sum.thy Fri Oct 11 14:15:10 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Fri Oct 11 15:17:37 2024 +0200
@@ -74,21 +74,8 @@
"_qinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
-let
- fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const @{syntax_const "_qinfsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
-in [(@{const_syntax infsum}, K sum_tr')] end
+ [(\<^const_syntax>\<open>infsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsum\<close>))]
\<close>
subsection \<open>General properties\<close>
--- a/src/HOL/Analysis/Sparse_In.thy Fri Oct 11 14:15:10 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy Fri Oct 11 15:17:37 2024 +0200
@@ -177,23 +177,8 @@
"_qeventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"
-
print_translation \<open>
-let
- fun ev_cosparse_tr' [Abs (x, Tx, t),
- Const (\<^const_syntax>\<open>cosparse\<close>, _) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P))] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const \<^syntax_const>\<open>_qeventually_cosparse\<close> $
- Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | ev_cosparse_tr' _ = raise Match;
-in [(\<^const_syntax>\<open>eventually\<close>, K ev_cosparse_tr')] end
+ [(\<^const_syntax>\<open>eventually\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qeventually_cosparse\<close>))]
\<close>
lemma eventually_cosparse: "eventually P (cosparse A) \<longleftrightarrow> {x. \<not>P x} sparse_in A"
--- a/src/HOL/Groups_Big.thy Fri Oct 11 14:15:10 2024 +0200
+++ b/src/HOL/Groups_Big.thy Fri Oct 11 15:17:37 2024 +0200
@@ -671,24 +671,10 @@
syntax_consts
"_qsum" == sum
-
translations
"\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
- let
- fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const \<^syntax_const>\<open>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
- in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end
+ [(\<^const_syntax>\<open>sum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qsum\<close>))]
\<close>
@@ -1441,24 +1427,10 @@
syntax_consts
"_qprod" == prod
-
translations
"\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
-
print_translation \<open>
- let
- fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const \<^syntax_const>\<open>_qprod\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | prod_tr' _ = raise Match;
- in [(\<^const_syntax>\<open>prod\<close>, K prod_tr')] end
+ [(\<^const_syntax>\<open>prod\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qprod\<close>))]
\<close>
context comm_monoid_mult
--- a/src/HOL/Set.thy Fri Oct 11 14:15:10 2024 +0200
+++ b/src/HOL/Set.thy Fri Oct 11 15:17:37 2024 +0200
@@ -53,6 +53,18 @@
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
+ML \<open>
+ fun Collect_binder_tr' c [Abs (x, T, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, _, P)] =
+ if x = y then
+ let
+ val x' = Syntax_Trans.mark_bound_body (x, T);
+ val t' = subst_bound (x', t);
+ val P' = subst_bound (x', P);
+ in Syntax.const c $ Syntax_Trans.mark_bound_abs (x, T) $ P' $ t' end
+ else raise Match
+ | Collect_binder_tr' _ _ = raise Match
+\<close>
+
lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
by simp