[STATEMENT]
lemma interpret_floatarith_norm[simp]:
  assumes [simp]: "length x = DIM('a)"
  shows "interpret_floatarith (Norm x) vs = norm (einterpret x vs::'a::executable_euclidean_space)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Norm x) vs = norm (einterpret x vs)
[PROOF STEP]
apply (auto simp: Norm_def norm_eq_sqrt_inner)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. interpret_floatarith i vs * interpret_floatarith i vs) = einterpret x vs \<bullet> einterpret x vs
[PROOF STEP]
apply (subst euclidean_inner[where 'a='a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. interpret_floatarith i vs * interpret_floatarith i vs) = (\<Sum>b\<in>Basis. einterpret x vs \<bullet> b * (einterpret x vs \<bullet> b))
[PROOF STEP]
apply (auto simp: power2_eq_square[symmetric] )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. (interpret_floatarith i vs)\<^sup>2) = (\<Sum>b\<in>Basis. (einterpret x vs \<bullet> b)\<^sup>2)
[PROOF STEP]
apply (subst sum_list_Basis_list[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. (interpret_floatarith i vs)\<^sup>2) = (\<Sum>b\<leftarrow>Basis_list. (einterpret x vs \<bullet> b)\<^sup>2)
[PROOF STEP]
apply (rule sum_list_nth_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (map (\<lambda>i. (interpret_floatarith i vs)\<^sup>2) x) = length (map (\<lambda>b. (einterpret x vs \<bullet> b)\<^sup>2) Basis_list)
 2. \<And>xa y. (xa, y) \<in> set (zip (map (\<lambda>i. (interpret_floatarith i vs)\<^sup>2) x) (map (\<lambda>b. (einterpret x vs \<bullet> b)\<^sup>2) Basis_list)) \<Longrightarrow> xa = y
[PROOF STEP]
by (auto simp: in_set_zip eucl_of_list_inner)