[STATEMENT]
theorem IFNTT_correct:
  assumes "length numbers = n"
  shows "IFNTT numbers = INTT numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IFNTT numbers = INTT numbers
[PROOF STEP]
using IFNTT_INTT_gen_eq INTT_gen_INTT_full_length assms n_two_pot
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?numbers = 2 ^ ?l; 2 ^ ?l \<le> n\<rbrakk> \<Longrightarrow> IFNTT ?numbers = INTT_gen (length ?numbers) ?numbers
length ?numbers = n \<Longrightarrow> INTT_gen n ?numbers = INTT ?numbers
length numbers = n
n = 2 ^ N

goal (1 subgoal):
 1. IFNTT numbers = INTT numbers
[PROOF STEP]
by force


[STATEMENT]
theorem IFNTT_inv_FNTT:
  assumes "length numbers = n"
  shows "IFNTT (FNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IFNTT (FNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers
[PROOF STEP]
by (simp add: FNTT_correct IFNTT_correct assms length_NTT ntt_correct)


[STATEMENT]
theorem FNTT_inv_IFNTT:
  assumes "length numbers = n"
  shows "FNTT (IFNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT (IFNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers
[PROOF STEP]
by (simp add: FNTT_correct IFNTT_correct assms inv_ntt_correct length_INTT)


[STATEMENT]
lemma map_filter_shift: " map f (filter even [0..<Suc g]) =
        f 0 #  map (\<lambda> x. f (x+1)) (filter odd [0..<g])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (filter even [0..<Suc g]) = f 0 # map (\<lambda>x. f (x + 1)) (filter odd [0..<g])
[PROOF STEP]
by (induction g) auto


[STATEMENT]
lemma map_filter_shift': " map f (filter odd [0..<Suc g]) =
          map (\<lambda> x. f (x+1)) (filter even [0..<g])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (filter odd [0..<Suc g]) = map (\<lambda>x. f (x + 1)) (filter even [0..<g])
[PROOF STEP]
by (induction g) auto


[STATEMENT]
lemma filter_compehension_evens_odds:
      "[xs ! i. i <- filter even [0..<length xs]] = evens_odds True xs \<and>
       [xs ! i. i <- filter odd [0..<length xs]] = evens_odds False xs "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs
[PROOF STEP]
apply(induction xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map ((!) []) (filter even [0..<length []]) = evens_odds True [] \<and> map ((!) []) (filter odd [0..<length []]) = evens_odds False []
 2. \<And>a xs. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (a # xs)) (filter even [0..<length (a # xs)]) = evens_odds True (a # xs) \<and> map ((!) (a # xs)) (filter odd [0..<length (a # xs)]) = evens_odds False (a # xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (a # xs)) (filter even [0..<length (a # xs)]) = evens_odds True (a # xs) \<and> map ((!) (a # xs)) (filter odd [0..<length (a # xs)]) = evens_odds False (a # xs)
[PROOF STEP]
subgoal for x xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = evens_odds True (x # xs) \<and> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = evens_odds False (x # xs)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = evens_odds True (x # xs)
 2. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = evens_odds False (x # xs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = evens_odds True (x # xs)
[PROOF STEP]
apply(subst evens_odds.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = x # evens_odds False xs
[PROOF STEP]
apply(rule trans[of _ "map ((!) (x # xs)) (filter even [0..<Suc (length xs)])"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = map ((!) (x # xs)) (filter even [0..<Suc (length xs)])
 2. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<Suc (length xs)]) = x # evens_odds False xs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<length (x # xs)]) = map ((!) (x # xs)) (filter even [0..<Suc (length xs)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter even [0..<Suc (length xs)]) = x # evens_odds False xs
[PROOF STEP]
apply(rule trans[OF  map_filter_shift[of "(!) (x # xs)" "length xs"]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> (x # xs) ! 0 # map (\<lambda>xa. (x # xs) ! (xa + 1)) (filter odd [0..<length xs]) = x # evens_odds False xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = evens_odds False (x # xs)
[PROOF STEP]
apply(subst evens_odds.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = evens_odds True xs
[PROOF STEP]
apply(rule trans[of _ "map ((!) (x # xs)) (filter odd [0..<Suc (length xs)])"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = map ((!) (x # xs)) (filter odd [0..<Suc (length xs)])
 2. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<Suc (length xs)]) = evens_odds True xs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<length (x # xs)]) = map ((!) (x # xs)) (filter odd [0..<Suc (length xs)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map ((!) (x # xs)) (filter odd [0..<Suc (length xs)]) = evens_odds True xs
[PROOF STEP]
apply(rule trans[OF  map_filter_shift'[of "(!) (x # xs)" "length xs"]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) xs) (filter even [0..<length xs]) = evens_odds True xs \<and> map ((!) xs) (filter odd [0..<length xs]) = evens_odds False xs \<Longrightarrow> map (\<lambda>xa. (x # xs) ! (xa + 1)) (filter even [0..<length xs]) = evens_odds True xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "length (evens_odds True vc) < Suc (length vc)"
              "length (evens_odds False vc) < Suc (length vc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds True vc) < Suc (length vc) &&& length (evens_odds False vc) < Suc (length vc)
[PROOF STEP]
by (metis filter_compehension_evens_odds le_imp_less_Suc length_filter_le length_map map_nth)+


[STATEMENT]
lemma FNTT'_FNTT: "FNTT' xs = FNTT xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT' xs = FNTT xs
[PROOF STEP]
apply(induction xs rule: FNTT'.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. FNTT' [] = FNTT []
 2. \<And>a. FNTT' [a] = FNTT [a]
 3. \<And>v vb vc. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> FNTT' (v # vb # vc) = FNTT (v # vb # vc)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT' [] = FNTT []
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. FNTT' [a] = FNTT [a]
 2. \<And>v vb vc. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> FNTT' (v # vb # vc) = FNTT (v # vb # vc)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT' [a_] = FNTT [a_]
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vb vc. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> FNTT' (v # vb # vc) = FNTT (v # vb # vc)
[PROOF STEP]
apply(subst FNTT'.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vb vc. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> (let nn = length (v # vb # vc); nums1 = evens_odds True (v # vb # vc); nums2 = evens_odds False (v # vb # vc); fntt1 = FNTT' nums1; fntt2 = FNTT' nums2; fntt2_omg = map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]; sum1 = map2 (+) fntt1 fntt2_omg in Let (map2 (-) fntt1 fntt2_omg) ((@) sum1)) = FNTT (v # vb # vc)
[PROOF STEP]
apply(subst FNTT.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vb vc. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> (let nn = length (v # vb # vc); nums1 = evens_odds True (v # vb # vc); nums2 = evens_odds False (v # vb # vc); fntt1 = FNTT' nums1; fntt2 = FNTT' nums2; fntt2_omg = map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]; sum1 = map2 (+) fntt1 fntt2_omg in Let (map2 (-) fntt1 fntt2_omg) ((@) sum1)) = (let nn = length (v # vb # vc); nums1 = map ((!) (v # vb # vc)) (filter even [0..<nn]); nums2 = map ((!) (v # vb # vc)) (filter odd [0..<nn]); fntt1 = FNTT nums1; fntt2 = FNTT nums2; sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) in Let (map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) ((@) sum1))
[PROOF STEP]
subgoal for a b xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (a # b # xs); xa = evens_odds True (a # b # xs); xb = evens_odds False (a # b # xs)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (a # b # xs); xa = evens_odds True (a # b # xs); xb = evens_odds False (a # b # xs); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> (let nn = length (a # b # xs); nums1 = evens_odds True (a # b # xs); nums2 = evens_odds False (a # b # xs); fntt1 = FNTT' nums1; fntt2 = FNTT' nums2; fntt2_omg = map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]; sum1 = map2 (+) fntt1 fntt2_omg in Let (map2 (-) fntt1 fntt2_omg) ((@) sum1)) = (let nn = length (a # b # xs); nums1 = map ((!) (a # b # xs)) (filter even [0..<nn]); nums2 = map ((!) (a # b # xs)) (filter odd [0..<nn]); fntt1 = FNTT nums1; fntt2 = FNTT nums2; sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) in Let (map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) ((@) sum1))
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa xb. \<lbrakk>x = length (a # b # xs); xa = evens_odds True (a # b # xs); xb = evens_odds False (a # b # xs)\<rbrakk> \<Longrightarrow> FNTT' xa = FNTT xa; \<And>x xa xb xc. \<lbrakk>x = length (a # b # xs); xa = evens_odds True (a # b # xs); xb = evens_odds False (a # b # xs); xc = FNTT' xa\<rbrakk> \<Longrightarrow> FNTT' xb = FNTT xb\<rbrakk> \<Longrightarrow> map2 (+) (FNTT' (evens_odds True (a # b # xs))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length (a # b # xs) * y)) (FNTT' (evens_odds False (a # b # xs))) [0..<length (a # b # xs) div 2]) @ map2 (-) (FNTT' (evens_odds True (a # b # xs))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length (a # b # xs) * y)) (FNTT' (evens_odds False (a # b # xs))) [0..<length (a # b # xs) div 2]) = map2 (+) (FNTT (map ((!) (a # b # xs)) (filter even [0..<length (a # b # xs)]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length (a # b # xs) * y)) (FNTT (map ((!) (a # b # xs)) (filter odd [0..<length (a # b # xs)]))) [0..<length (a # b # xs) div 2]) @ map2 (-) (FNTT (map ((!) (a # b # xs)) (filter even [0..<length (a # b # xs)]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length (a # b # xs) * y)) (FNTT (map ((!) (a # b # xs)) (filter odd [0..<length (a # b # xs)]))) [0..<length (a # b # xs) div 2])
[PROOF STEP]
apply (metis filter_compehension_evens_odds)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma T_eo_linear:  "T_\<^sub>e\<^sub>o b xs = length xs + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T_\<^sub>e\<^sub>o b xs = length xs + 1
[PROOF STEP]
by (induction b xs rule: T_\<^sub>e\<^sub>o.induct) auto


[STATEMENT]
lemma T_length_linear: "T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h xs = length xs +1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h xs = length xs + 1
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma T_nth_linear: "T\<^sub>n\<^sub>t\<^sub>h xs i \<le> length xs +1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>n\<^sub>t\<^sub>h xs i \<le> length xs + 1
[PROOF STEP]
by (induction xs i rule: T\<^sub>n\<^sub>t\<^sub>h.induct) auto


[STATEMENT]
lemma T_map_2_linear:
"c > 0 \<Longrightarrow>
       (\<And> x y. t x y \<le> c) \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys)  * (c+1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1
[PROOF STEP]
apply(induction t xs ys rule: T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t uu_. \<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t [] uu_ \<le> min (length []) (length uu_) * (c + 1) + 1
 2. \<And>t v va. \<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (v # va) [] \<le> min (length (v # va)) (length []) * (c + 1) + 1
 3. \<And>t x xs y ys. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (x # xs) (y # ys) \<le> min (length (x # xs)) (length (y # ys)) * (c + 1) + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; \<And>x y. t_ x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t_ [] uu_ \<le> min (length []) (length uu_) * (c + 1) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t v va. \<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (v # va) [] \<le> min (length (v # va)) (length []) * (c + 1) + 1
 2. \<And>t x xs y ys. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (x # xs) (y # ys) \<le> min (length (x # xs)) (length (y # ys)) * (c + 1) + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; \<And>x y. t_ x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t_ (v_ # va_) [] \<le> min (length (v_ # va_)) (length []) * (c + 1) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t x xs y ys. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (x # xs) (y # ys) \<le> min (length (x # xs)) (length (y # ys)) * (c + 1) + 1
[PROOF STEP]
subgoal for t x xs y ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (x # xs) (y # ys) \<le> min (length (x # xs)) (length (y # ys)) * (c + 1) + 1
[PROOF STEP]
apply(subst  T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.simps, subst length_Cons, subst length_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> t x y + 1 + T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (Suc (length xs)) (Suc (length ys)) * (c + 1) + 1
[PROOF STEP]
using min_add_distrib_right[of 1]
[PROOF STATE]
proof (prove)
using this:
(1::?'d1) + min ?y ?z = min ((1::?'d1) + ?y) ((1::?'d1) + ?z)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (length xs) (length ys) * (c + 1) + 1; 0 < c; \<And>x y. t x y \<le> c\<rbrakk> \<Longrightarrow> t x y + 1 + T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys \<le> min (Suc (length xs)) (Suc (length ys)) * (c + 1) + 1
[PROOF STEP]
by (smt (z3) Suc_eq_plus1 add.assoc add.commute add_le_mono le_numeral_extra(4) min_def mult.commute mult_Suc_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma T_map_2_linear':
"c > 0 \<Longrightarrow>
       (\<And> x y. t x y = c) \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys = min (length xs) (length ys)  * (c+1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; \<And>x y. t x y = c\<rbrakk> \<Longrightarrow> T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys = min (length xs) (length ys) * (c + 1) + 1
[PROOF STEP]
by(induction t xs ys rule: T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.induct) simp+


[STATEMENT]
lemma T_app_linear: " T\<^sub>a\<^sub>p\<^sub>p xs ys = length xs +1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>a\<^sub>p\<^sub>p xs ys = length xs + 1
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma mono:  "((f x)::nat) \<le> f y \<Longrightarrow> f y \<le> fz \<Longrightarrow> f x \<le> fz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f x \<le> f y; f y \<le> fz\<rbrakk> \<Longrightarrow> f x \<le> fz
[PROOF STEP]
by simp


[STATEMENT]
lemma evens_odds_length:
      "length (evens_odds True xs) = (length xs+1) div 2 \<and>
       length (evens_odds False xs) = (length xs) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds True xs) = (length xs + 1) div 2 \<and> length (evens_odds False xs) = length xs div 2
[PROOF STEP]
by(induction xs) simp+


[STATEMENT]
lemma FNTT_length: "length numbers = 2^l \<Longrightarrow> length (FNTT numbers) = length numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
proof(induction l arbitrary: numbers)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
length ?numbers = 2 ^ l \<Longrightarrow> length (FNTT ?numbers) = length ?numbers
length numbers = 2 ^ Suc l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define numbers1 where "numbers1 = [numbers!i .  i <- (filter even [0..<length numbers])]"
[PROOF STATE]
proof (state)
this:
numbers1 = map ((!) numbers) (filter even [0..<length numbers])

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define numbers2 where "numbers2 = [numbers!i .  i <- (filter odd [0..<length numbers])]"
[PROOF STATE]
proof (state)
this:
numbers2 = map ((!) numbers) (filter odd [0..<length numbers])

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define fntt1 where "fntt1 = FNTT numbers1"
[PROOF STATE]
proof (state)
this:
fntt1 = FNTT numbers1

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define fntt2 where "fntt2 = FNTT numbers2"
[PROOF STATE]
proof (state)
this:
fntt2 = FNTT numbers2

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define presum where
    "presum = (map2 ( \<lambda> x k.  x*(\<omega>^( (n div (length numbers)) * k)))
                   fntt2 [0..<((length numbers) div 2)])"
[PROOF STATE]
proof (state)
this:
presum = map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) fntt2 [0..<length numbers div 2]

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define sum1 where
    "sum1 = map2 (+) fntt1 presum"
[PROOF STATE]
proof (state)
this:
sum1 = map2 (+) fntt1 presum

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
define sum2 where
    "sum2 = map2 (-) fntt1 presum"
[PROOF STATE]
proof (state)
this:
sum2 = map2 (-) fntt1 presum

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
have "length numbers1  = 2^l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length numbers1 = 2 ^ l
[PROOF STEP]
by (metis Suc.prems numbers1_def diff_add_inverse2 length_even_filter mult_2 nonzero_mult_div_cancel_left power_Suc zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
length numbers1 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence "length fntt1 = 2^l"
[PROOF STATE]
proof (prove)
using this:
length numbers1 = 2 ^ l

goal (1 subgoal):
 1. length fntt1 = 2 ^ l
[PROOF STEP]
by (simp add: Suc.IH fntt1_def)
[PROOF STATE]
proof (state)
this:
length fntt1 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence "length presum = 2^l"
[PROOF STATE]
proof (prove)
using this:
length fntt1 = 2 ^ l

goal (1 subgoal):
 1. length presum = 2 ^ l
[PROOF STEP]
unfolding presum_def
[PROOF STATE]
proof (prove)
using this:
length fntt1 = 2 ^ l

goal (1 subgoal):
 1. length (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) fntt2 [0..<length numbers div 2]) = 2 ^ l
[PROOF STEP]
using map2_length Suc.IH Suc.prems fntt2_def length_odd_filter numbers2_def
[PROOF STATE]
proof (prove)
using this:
length fntt1 = 2 ^ l
length (map2 ?f ?xs ?ys) = min (length ?xs) (length ?ys)
length ?numbers = 2 ^ l \<Longrightarrow> length (FNTT ?numbers) = length ?numbers
length numbers = 2 ^ Suc l
fntt2 = FNTT numbers2
length (map ?f (filter odd [0..<?l])) = ?l div 2
numbers2 = map ((!) numbers) (filter odd [0..<length numbers])

goal (1 subgoal):
 1. length (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) fntt2 [0..<length numbers div 2]) = 2 ^ l
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
length presum = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence "length sum1 = 2^l"
[PROOF STATE]
proof (prove)
using this:
length presum = 2 ^ l

goal (1 subgoal):
 1. length sum1 = 2 ^ l
[PROOF STEP]
by (simp add: \<open>length fntt1 = 2 ^ l\<close> sum1_def)
[PROOF STATE]
proof (state)
this:
length sum1 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
have "length numbers2 = 2^l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length numbers2 = 2 ^ l
[PROOF STEP]
by (metis Suc.prems numbers2_def length_odd_filter nonzero_mult_div_cancel_left power_Suc zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
length numbers2 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence "length fntt2 = 2^l"
[PROOF STATE]
proof (prove)
using this:
length numbers2 = 2 ^ l

goal (1 subgoal):
 1. length fntt2 = 2 ^ l
[PROOF STEP]
by (simp add: Suc.IH fntt2_def)
[PROOF STATE]
proof (state)
this:
length fntt2 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence "length sum2 = 2^l"
[PROOF STATE]
proof (prove)
using this:
length fntt2 = 2 ^ l

goal (1 subgoal):
 1. length sum2 = 2 ^ l
[PROOF STEP]
unfolding sum2_def
[PROOF STATE]
proof (prove)
using this:
length fntt2 = 2 ^ l

goal (1 subgoal):
 1. length (map2 (-) fntt1 presum) = 2 ^ l
[PROOF STEP]
using \<open>length sum1 = 2 ^ l\<close> sum1_def
[PROOF STATE]
proof (prove)
using this:
length fntt2 = 2 ^ l
length sum1 = 2 ^ l
sum1 = map2 (+) fntt1 presum

goal (1 subgoal):
 1. length (map2 (-) fntt1 presum) = 2 ^ l
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
length sum2 = 2 ^ l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
hence final:"length (sum1@sum2) = 2^(Suc l)"
[PROOF STATE]
proof (prove)
using this:
length sum2 = 2 ^ l

goal (1 subgoal):
 1. length (sum1 @ sum2) = 2 ^ Suc l
[PROOF STEP]
by (simp add: \<open>length sum1 = 2 ^ l\<close>)
[PROOF STATE]
proof (state)
this:
length (sum1 @ sum2) = 2 ^ Suc l

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
obtain x y xs where xyxs_Def: "numbers = x#y#xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y xs. numbers = x # y # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>length numbers2 = 2 ^ l\<close> evens_odds.elims filter_compehension_evens_odds length_0_conv neq_Nil_conv numbers2_def power_eq_0_iff zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
numbers = x # y # xs

goal (2 subgoals):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
 2. \<And>l numbers. \<lbrakk>\<And>numbers. length numbers = 2 ^ l \<Longrightarrow> length (FNTT numbers) = length numbers; length numbers = 2 ^ Suc l\<rbrakk> \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (FNTT numbers) = length numbers
[PROOF STEP]
apply(subst xyxs_Def, subst FNTT.simps(3), subst xyxs_Def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (let nn = length numbers; nums1 = map ((!) (x # y # xs)) (filter even [0..<nn]); nums2 = map ((!) (x # y # xs)) (filter odd [0..<nn]); fntt1 = FNTT nums1; fntt2 = FNTT nums2; sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) in Let (map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) ((@) sum1)) = length numbers
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map2 (+) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = length numbers
[PROOF STEP]
using final
[PROOF STATE]
proof (prove)
using this:
length (sum1 @ sum2) = 2 ^ Suc l

goal (1 subgoal):
 1. length (map2 (+) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = length numbers
[PROOF STEP]
unfolding sum1_def sum2_def presum_def fntt1_def fntt2_def numbers1_def numbers2_def
[PROOF STATE]
proof (prove)
using this:
length (map2 (+) (FNTT (map ((!) numbers) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) numbers) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) numbers) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) numbers) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = 2 ^ Suc l

goal (1 subgoal):
 1. length (map2 (+) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = length numbers
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
length (map2 (+) (FNTT (map ((!) numbers) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) numbers) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) numbers) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) numbers) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = 2 ^ Suc l
length ?numbers = 2 ^ l \<Longrightarrow> length (FNTT ?numbers) = length ?numbers
length numbers = 2 ^ Suc l

goal (1 subgoal):
 1. length (map2 (+) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2]) @ map2 (-) (FNTT (map ((!) (x # y # xs)) (filter even [0..<length numbers]))) (map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) (FNTT (map ((!) (x # y # xs)) (filter odd [0..<length numbers]))) [0..<length numbers div 2])) = length numbers
[PROOF STEP]
by (metis xyxs_Def)
[PROOF STATE]
proof (state)
this:
length (FNTT numbers) = length numbers

goal (1 subgoal):
 1. \<And>numbers. length numbers = 2 ^ 0 \<Longrightarrow> length (FNTT numbers) = length numbers
[PROOF STEP]
qed (metis FNTT.simps(2) Suc_length_conv length_0_conv nat_power_eq_Suc_0_iff)


[STATEMENT]
lemma add_cong: "(a1::nat) + a2+a3 +a4= b \<Longrightarrow> a1 +a2+ c + a3+a4= c +b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a1 + a2 + a3 + a4 = b \<Longrightarrow> a1 + a2 + c + a3 + a4 = c + b
[PROOF STEP]
by simp


[STATEMENT]
lemma add_mono:"a \<le> (b::nat) \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b +d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> d\<rbrakk> \<Longrightarrow> a + c \<le> b + d
[PROOF STEP]
by simp


[STATEMENT]
lemma xyz: " Suc (Suc (length xs)) = 2 ^ l \<Longrightarrow> length (x # evens_odds True xs) = 2 ^ (l - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc (length xs)) = 2 ^ l \<Longrightarrow> length (x # evens_odds True xs) = 2 ^ (l - 1)
[PROOF STEP]
by (metis (no_types, lifting) Nat.add_0_right Suc_eq_plus1 div2_Suc_Suc div_mult_self2 evens_odds_length length_Cons nat.distinct(1) numeral_2_eq_2 one_div_two_eq_zero plus_1_eq_Suc power_eq_if)


[STATEMENT]
lemma zyx:" Suc (Suc (length xs)) = 2 ^ l  \<Longrightarrow> length (y # evens_odds False xs) = 2 ^ (l - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc (length xs)) = 2 ^ l \<Longrightarrow> length (y # evens_odds False xs) = 2 ^ (l - 1)
[PROOF STEP]
by (smt (z3) One_nat_def Suc_pred diff_Suc_1 div2_Suc_Suc evens_odds_length le_numeral_extra(4) length_Cons nat_less_le neq0_conv power_0 power_diff power_one_right zero_less_diff zero_neq_numeral)


[STATEMENT]
lemma evens_odds_power_2:
  fixes x::'b and y::'b
  assumes "Suc (Suc (length (xs::'b list))) = 2 ^ l"
  shows " Suc(length (evens_odds b xs)) = 2 ^ (l-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
have "Suc(length (evens_odds b xs)) = length (evens_odds b (x#y#xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = length (evens_odds b (x # y # xs))
[PROOF STEP]
by (metis (full_types)  evens_odds.simps(2) evens_odds.simps(3) length_Cons)
[PROOF STATE]
proof (state)
this:
Suc (length (evens_odds b xs)) = length (evens_odds b (x # y # xs))

goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
have "length (x#y#xs) = 2^l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (x # y # xs) = 2 ^ l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Suc (Suc (length xs)) = 2 ^ l

goal (1 subgoal):
 1. length (x # y # xs) = 2 ^ l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (x # y # xs) = 2 ^ l

goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
have "length (evens_odds b (x#y#xs))  = 2^(l-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)
[PROOF STEP]
apply (cases b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)
 2. \<not> b \<Longrightarrow> length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)
[PROOF STEP]
apply (smt (z3) Suc_eq_plus1 Suc_pred \<open>length (x # y # xs) = 2 ^ l\<close> add.commute add_diff_cancel_left' assms filter_compehension_evens_odds gr0I le_add1 le_imp_less_Suc length_even_filter mult_2 nat_less_le power_diff power_eq_if power_one_right zero_neq_numeral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)
[PROOF STEP]
by (smt (z3) One_nat_def Suc_inject \<open>length (x # y # xs) = 2 ^ l\<close> assms evens_odds_length le_zero_eq nat.distinct(1) neq0_conv not_less_eq_eq pos2 power_Suc0_right power_diff_power_eq power_eq_if)
[PROOF STATE]
proof (state)
this:
length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)

goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (evens_odds b (x # y # xs)) = 2 ^ (l - 1)

goal (1 subgoal):
 1. Suc (length (evens_odds b xs)) = 2 ^ (l - 1)
[PROOF STEP]
by (metis \<open>Suc (length (evens_odds b xs)) = length (evens_odds b (x # y # xs))\<close>)
[PROOF STATE]
proof (state)
this:
Suc (length (evens_odds b xs)) = 2 ^ (l - 1)

goal:
No subgoals!
[PROOF STEP]
qed