show "\<forall>i0\<in>set (digit_encode (d # ds) x). i0 < m"
using \<open>\<forall>i0\<in>set (digit_encode ds i1). i0 < m\<close> \<open>i0 < d\<close> \<open>i0 < m\<close> \<open>x = i0 + d * i1\<close> by auto
qed
next
fix x assume "x \<in> {i. low_digits (d # ds) i}"
then have "x < listprod (d # ds)" "\<forall>i0\<in>set (digit_encode (d # ds) x). i0 < m" using low_digits_def by auto
then have "x < prod_list (d # ds)" "\<forall>i0\<in>set (digit_encode (d # ds) x). i0 < m" using low_digits_def by auto
have "x mod d < m" using `\<forall>i0\<in>set (digit_encode (d # ds) x). i0 < m`[unfolded digit_encode.simps] by simp
have "x div d < listprod ds" using `x < listprod (d # ds)`[unfolded listprod.Cons]
have "x div d < prod_list ds" using `x < prod_list (d # ds)`[unfolded prod_list.Cons]
by (metis Divides.div_mult2_eq div_eq_0_iff gr_implies_not0 mult_0_right)
have "\<forall>i0\<in>set (digit_encode ds (x div d)). i0 < m" by (simp add: \<open>\<forall>i0\<in>set (digit_encode (d # ds) x). i0 < m\<close>)
have "f ((x mod d),(x div d)) = x" by (simp add: f_def)
show "x \<in> f ` ({..<m} \<times> {i. low_digits ds i})" by (metis SigmaI \<open>\<forall>i0\<in>set (digit_encode ds (x div d)). i0 < m\<close> \<open>f (x mod d, x div d) = x\<close> \<open>x div d < listprod ds\<close> \<open>x mod d < m\<close> image_eqI lessThan_iff low_digits_def mem_Collect_eq)
show "x \<in> f ` ({..<m} \<times> {i. low_digits ds i})" by (metis SigmaI \<open>\<forall>i0\<in>set (digit_encode ds (x div d)). i0 < m\<close> \<open>f (x mod d, x div d) = x\<close> \<open>x div d < prod_list ds\<close> \<open>x mod d < m\<close> image_eqI lessThan_iff low_digits_def mem_Collect_eq)
qed
then have "bij_betw f ({..<m} \<times> {i. low_digits ds i}) {i. low_digits (d # ds) i}"
by (simp add: \<open>inj_on f ({..<m} \<times> {i. low_digits ds i})\<close> bij_betw_def)
...
...
@@ -823,13 +823,13 @@ qed
lemma card_rows_with_1: "card {i\<in>rows_with_1. i<dim\<^sub>r Aw'} = r ^ N_half"
proof -
have 1:"{i\<in>rows_with_1. i<dim\<^sub>r Aw'} = {i. i < listprod (sublist (Tensor.dims Aw) (Collect even)) \<and>
have 1:"{i\<in>rows_with_1. i<dim\<^sub>r Aw'} = {i. i < prod_list (sublist (Tensor.dims Aw) (Collect even)) \<and>
using Input.prems(3) valid_index.Cons valid_index.Nil by auto
also have "... = inputs ! 0 $ j" using `length inputs = 1` by (simp add: setprod_lessThan_Suc)
also have "... = inputs ! 0 $ j" using `length inputs = 1` by (simp add: prod_lessThan_Suc)
also have "... = evaluate_net (Input M) inputs $ j" unfolding evaluate_net.simps
by (metis \<open>length inputs = 1\<close> hd_conv_nth list.size(3) zero_neq_one)
finally show ?case by auto
...
...
@@ -477,7 +477,7 @@ next
using vec_index_map by auto
show "(\<Prod>k<length inputs. inputs ! k $ (is ! k)) * lookup (tensors_from_net (Conv A m) $ j) is
= (\<Sum>i = 0..<dim\<^sub>v (tensors_from_net m). row A j $ i * ((\<Prod>k<length inputs. inputs ! k $ (is ! k)) * lookup (tensors_from_net m $ i) is))"
unfolding 0 setsum_right_distrib by (simp add: semiring_normalization_rules(19))
unfolding 0 sum_distrib_left by (simp add: semiring_normalization_rules(19))
qed
have "valid_net' m" by (metis Conv.prems(1) convnet.distinct(1) convnet.distinct(5) convnet.inject(2) remove_weights.simps(2) valid_net.simps)
have "map dim\<^sub>v inputs = input_sizes m" by (simp add: Conv.prems(2))
...
...
@@ -487,9 +487,9 @@ next
have "(\<Sum>is | is \<lhd> input_sizes (Conv A m). (\<Prod>k<length inputs. inputs ! k $ (is ! k)) * lookup (tensors_from_net (Conv A m) $ j) is)
= (\<Sum>i = 0..<dim\<^sub>v (tensors_from_net m). (\<Sum>is | is \<lhd> input_sizes (Conv A m). row A j $ i * ((\<Prod>k<length inputs. inputs ! k $ (is ! k)) * lookup (tensors_from_net m $ i) is)))"
using Groups_Big.comm_monoid_add_class.setsum.commute 0 by auto
using Groups_Big.comm_monoid_add_class.sum.commute 0 by auto
also have "... = (\<Sum>i = 0..<dim\<^sub>v (tensors_from_net m). row A j $ i * (\<Sum>is | is \<lhd> input_sizes (Conv A m). ((\<Prod>k<length inputs. inputs ! k $ (is ! k)) * lookup (tensors_from_net m $ i) is)))"
by (simp add: setsum_right_distrib)
by (simp add: sum_distrib_left)
also have "... = (\<Sum>i = 0..<dim\<^sub>v (tensors_from_net m). row A j $ i * evaluate_net m inputs $ i)" using 1 by auto
also have "... = row A j \<bullet> evaluate_net m inputs"
by (metis (full_types) \<open>map dim\<^sub>v inputs = input_sizes m\<close> \<open>output_size' m = dim\<^sub>v (tensors_from_net m)\<close>
...
...
@@ -521,13 +521,13 @@ next
using \<open>is2 \<lhd> input_sizes m2\<close> \<open>map dim\<^sub>v inputs2 = input_sizes m2\<close> valid_index_length by fastforce
have 1:"(\<Prod>k<length inputs1. (inputs1 @ inputs2) ! k $ ((is1 @ is2) ! k)) = (\<Prod>k<length inputs1. inputs1 ! k $ (is1 ! k))"
lemma vars_setsum: "finite S \<Longrightarrow> vars (\<Sum>m\<in>S. f m) \<subseteq> (\<Union>m\<in>S. vars (f m))"
proof (induction S rule:finite_induct)
case empty
then show ?case by (metis UN_empty eq_iff monom_zero setsum.empty single_zero vars_monom_single_cases)
then show ?case by (metis UN_empty eq_iff monom_zero sum.empty single_zero vars_monom_single_cases)
next
case (insert s S)
then have "vars (setsum f (insert s S)) = vars (f s + setsum f S)" by (metis setsum.insert)
also have "... \<subseteq> vars (f s) \<union> vars (setsum f S)" by (simp add: vars_add)
then have "vars (sum f (insert s S)) = vars (f s + sum f S)" by (metis sum.insert)
also have "... \<subseteq> vars (f s) \<union> vars (sum f S)" by (simp add: vars_add)
also have "... \<subseteq> (\<Union>m\<in>insert s S. vars (f m))" using insert.IH by auto
finally show ?case by metis
qed
...
...
@@ -311,7 +311,7 @@ section "MPoly extension"
lemma insertion_fun_single: "insertion_fun f (\<lambda>m. (a when (PP_Poly_Mapping.single (v::nat) (n::nat)) = m)) = a * f v ^ n" (is "?i = _")
proof -
have setsum_single:"\<And> a f. (\<Sum>m\<in>{a}. f m) = f a"
by (metis add.right_neutral empty_Diff finite.emptyI setsum.empty setsum.insert_remove)
by (metis add.right_neutral empty_Diff finite.emptyI sum.empty sum.insert_remove)
have 1:"?i = (\<Sum>m. (a when PP_Poly_Mapping.single v n = m) * (\<Prod>v. f v ^ lookup m v))"
unfolding insertion_fun_def by metis
...
...
@@ -431,7 +431,7 @@ proof-
qed
lemma extract_var_non_zero_coeff: "extract_var p v = (\<Sum>m\<in>{m'. coeff p m' \<noteq> 0}. monom (remove_key v m) (monom (PP_Poly_Mapping.single v (lookup m v)) (coeff p m)))"
using extract_var_finite_set coeff_def finite_lookup order_refl by (metis (no_types, lifting) Collect_cong setsum.cong)
using extract_var_finite_set coeff_def finite_lookup order_refl by (metis (no_types, lifting) Collect_cong sum.cong)
lemma extract_var_sum: "extract_var (p+p') v = extract_var p v + extract_var p' v"
proof -
...
...
@@ -442,7 +442,7 @@ proof -
extract_var_finite_set[OF subsets(1) `finite S`]
extract_var_finite_set[OF subsets(2) `finite S`]
extract_var_finite_set[OF subsets(3) `finite S`]
coeff_add[symmetric] monom_add setsum.distrib
coeff_add[symmetric] monom_add sum.distrib
by metis
qed
...
...
@@ -456,14 +456,14 @@ proof (cases "a = 0")
unfolding coeff_monom using \<open>a \<noteq> 0\<close> by auto