126 translations |
126 translations |
127 "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}" |
127 "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}" |
128 |
128 |
129 print_translation \<open> |
129 print_translation \<open> |
130 let |
130 let |
131 fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = |
131 fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] = |
132 if x <> y then raise Match |
132 if x <> y then raise Match |
133 else |
133 else |
134 let |
134 let |
135 val x' = Syntax_Trans.mark_bound_body (x, Tx); |
135 val x' = Syntax_Trans.mark_bound_body (x, Tx); |
136 val t' = subst_bound (x', t); |
136 val t' = subst_bound (x', t); |
137 val P' = subst_bound (x', P); |
137 val P' = subst_bound (x', P); |
138 in |
138 in |
139 Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' |
139 Syntax.const \<^syntax_const>\<open>_qinfsetsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' |
140 end |
140 end |
141 | sum_tr' _ = raise Match; |
141 | sum_tr' _ = raise Match; |
142 in [(@{const_syntax infsetsum}, K sum_tr')] end |
142 in [(\<^const_syntax>\<open>infsetsum\<close>, K sum_tr')] end |
143 \<close> |
143 \<close> |
144 |
144 |
145 |
145 |
146 lemma restrict_count_space_subset: |
146 lemma restrict_count_space_subset: |
147 "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A" |
147 "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A" |