diff --git a/thys/Number_Theoretic_Transform/Butterfly.thy b/thys/Number_Theoretic_Transform/Butterfly.thy
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/Butterfly.thy
@@ -0,0 +1,1323 @@
+(*
+Title: Butterfly Algorithm for Number Theoretic Transform
+Author: Thomas Ammer
+*)
+
+theory Butterfly
+  imports NTT "HOL-Library.Discrete"
+begin
+
+text \<open>\pagebreak\<close>
+
+section \<open>Butterfly Algorithms\<close>
+text \<open>\label{Butterfly}\<close>
+
+text \<open>\indent Several recursive algorithms for $FFT$ based on 
+the divide and conquer principle have been developed in order to speed up the transform.
+A method for reducing complexity is the butterfly scheme. 
+In this formalization, we consider the butterfly algorithm by Cooley 
+and Tukey~\parencite{Good1997} adapted to the setting of \textit{NTT}.
+\<close>
+
+text \<open>\noindent We additionally assume that $n$ is power of two.\<close>
+
+locale butterfly = ntt +
+  fixes N
+  assumes n_two_pot: "n = 2^N"
+begin
+
+subsection \<open>Recursive Definition\<close>
+
+text \<open>Let's recall the definition of a transformed vector element:
+\begin{equation*}
+\mathsf{NTT}(\vec{x})_i = \sum _{j = 0} ^{n-1} x_j \cdot \omega ^{i\cdot j} 
+\end{equation*}
+
+We assume $n = 2^N$ and obtain:
+
+\begin{align*}
+\sum _{j = 0} ^{< 2^N} x_j \cdot \omega ^{i\cdot j} \\ &= 
+\sum _{j = 0} ^{< 2^{N-1}} x_{2j} \cdot \omega ^{i\cdot 2j} +
+ \sum _{j = 0} ^{< 2^{N-1}} x_{2j+1} \cdot \omega ^{i\cdot (2j+1)} \\
+& = \sum _{j = 0} ^{< 2^{N-1}} x_{2j} \cdot (\omega^2) ^{i\cdot j} +
+ \omega^i \cdot \sum _{j = 0} ^{< 2^{N-1}} x_{2j+1} \cdot (\omega^2) ^{i\cdot j}\\
+& = (\sum _{j = 0} ^{< 2^{N-2}} x_{4j} \cdot (\omega^4) ^{i\cdot j}  +
+ \omega^i \cdot \sum _{j = 0} ^{< 2^{N-2}} x_{4j+2} \cdot (\omega^4) ^{i\cdot j}) \\
+& \hspace{1cm}+ \omega^i \cdot (\sum _{j = 0} ^{< 2^{N-2}} x_{4j+1} \cdot (\omega^4) ^{i\cdot j}  +
+ \omega^i \cdot \sum _{j = 0} ^{< 2^{N-2}} x_{4j+3} \cdot (\omega^4) ^{i\cdot j}) \text{ etc.}
+\end{align*}
+
+which gives us a recursive algorithm:
+
+\begin{itemize}
+\item Compose vectors consisting of elements at even and odd indices respectively
+\item Compute a transformation of these vectors recursively where the dimensions are halved.
+\item Add results after scaling the second subresult by $\omega^i$
+\end{itemize}
+
+\<close>
+
+text \<open>Now we give a functional definition of the analogue to $FFT$ adapted to finite fields. 
+A gentle introduction to $FFT$ can be found in~\parencite{10.5555/1614191}. 
+For the fast implementation of Number Theoretic Transform in particular, have a look at~\parencite{cryptoeprint:2016/504}.\<close>
+
+text \<open>(The following lemma is needed to obtain an automated termination proof of $FNTT$.)\<close>
+lemma FNTT_termination_aux [simp]: "length (filter P [0..<l]) < Suc l"
+  by (metis diff_zero le_imp_less_Suc length_filter_le length_upt)
+
+text \<open>Please note that we closely adhere to the textbook definition which just 
+talks about elements at even and odd indices. We model the informal definition by predefined functions, 
+since this seems to be more handy during proofs. 
+An algorithm splitting the elements smartly will be presented afterwards.\<close>
+
+fun FNTT::"('a mod_ring) list \<Rightarrow> ('a mod_ring) list" where
+"FNTT [] = []"|
+"FNTT [a] = [a]"|
+"FNTT nums = (let nn = length nums;
+                  nums1 = [nums!i.  i \<leftarrow> filter even [0..<nn]];
+                  nums2 = [nums!i.  i \<leftarrow> filter odd [0..<nn]];
+                  fntt1 = FNTT nums1;
+                  fntt2 = FNTT nums2;
+                  sum1 = map2 (+) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)]);
+                  sum2 = map2 (-) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)])
+                   in sum1@sum2)"
+
+lemmas [simp del] = FNTT_termination_aux
+
+
+text \<open>
+Finally, we want to prove correctness, i.e. $FNTT\; xs = NTT\;xs$. 
+Since we consider a recursive algorithm, some kind of induction is appropriate:
+Assume the claim for $\frac{2^d}{2} = 2^{d-1}$ and prove it for $2^d$, where $2^d$ is the vector length. 
+This implies that we have to talk about \textit{NTT}s with respect to some powers of $\omega$.
+In particular, we decide to annotate \textit{NTT} with a degree $degr$ 
+indicating the referred vector length. There is a correspondence to the current level $l$ of recursion:
+
+\begin{equation*}
+degr = 2^{N-l}
+\end{equation*}
+
+\<close>
+
+text \<open>\noindent A generalized version of \textit{NTT} keeps track of all levels during recursion:\<close>
+
+definition "ntt_gen numbers degr i = (\<Sum>j=0..<(length numbers). (numbers ! j) * \<omega>^((n div degr)*i*j)) "
+
+definition "NTT_gen degr numbers = map (ntt_gen numbers (degr)) [0..< length numbers]"
+
+text \<open>Whenever generalized \textit{NTT} is applied to a list of full length,
+ then its actually equal to the defined \textit{NTT}.\<close>
+
+lemma NTT_gen_NTT_full_length: 
+  assumes "length numbers =n"
+  shows "NTT_gen n numbers = NTT numbers"
+  unfolding NTT_gen_def ntt_gen_def NTT_def ntt_def 
+  using assms by simp
+
+subsection \<open>Arguments on Correctness\<close>
+text \<open>First some general lemmas on list operations.\<close>
+
+lemma length_even_filter: "length [f i .  i <- (filter even [0..<l])] = l-l div 2"
+  by(induction l) auto
+
+lemma length_odd_filter: "length [f i .  i <- (filter odd [0..<l])] = l div 2"
+  by(induction l) auto
+
+lemma map2_length: "length (map2 f xs ys) =  min (length xs) (length ys)"
+  by (induction xs arbitrary: ys) auto
+
+lemma map2_index: "i < length xs \<Longrightarrow> i < length ys \<Longrightarrow> (map2 f xs ys) ! i = f (xs ! i) (ys ! i)"
+  by (induction xs arbitrary: ys i) auto
+
+lemma filter_last_not: "\<not> P x \<Longrightarrow> filter P (xs@[x]) = filter P xs"
+  by simp
+
+lemma filter_even_map: "filter even [0..<2*(x::nat)] = map ((*) (2::nat)) [0..<x]"
+  by(induction x) simp+
+
+lemma filter_even_nth: "2*j < l \<Longrightarrow> 2*x = l \<Longrightarrow> (filter even [0..<l] ! j) = (2*j)"
+  using filter_even_map[of x] nth_map[of j "filter even [0..<l]" "(*) 2"] by auto
+
+lemma filter_odd_map: "filter odd [0..<2*(x::nat)] = map (\<lambda> y. (2::nat)*y +1) [0..<x]"
+  by(induction x) simp+
+
+lemma filter_odd_nth: "2*j < l \<Longrightarrow> 2*x = l \<Longrightarrow> (filter odd [0..<l] ! j) = (2*j+1)"
+  using filter_odd_map[of x] nth_map[of j "filter even [0..<l]" "(*) 2"] by auto
+
+text \<open>\noindent Lemmas by using the assumption $n = 2^N$.\<close>
+
+text \<open>\noindent ($-1$ denotes the additive inverse of $1$ in the finite field.)\<close>
+
+lemma n_min1_2: "n = 2  \<Longrightarrow> \<omega>  = -1" 
+  using omega_properties(1) omega_properties(2) power2_eq_1_iff by blast
+
+lemma n_min1_gr2:
+  assumes "n > 2"
+  shows "\<omega>^(n div 2) = -1"
+proof-
+  have "\<omega>^(n div 2) \<noteq> -1 \<Longrightarrow> False"
+  proof-
+  assume "\<omega>^(n div 2) \<noteq> -1"
+  hence False
+  proof(cases "\<omega>^(n div 2) = 1")
+case True
+  then show ?thesis using  omega_properties(3)
+    by (metis Euclidean_Division.div_eq_0_iff div_less_dividend leD less_le_trans n_lst2 one_less_numeral_iff pos2 semiring_norm(76) zero_neq_numeral)
+next
+  case False
+  hence "(\<omega>^(n div 2)) ^ (2::nat) \<noteq> 1" 
+    by (smt (verit, ccfv_threshold) n_two_pot One_nat_def \<open>\<omega> ^ (n div 2) \<noteq> - 1\<close> diff_zero leD n_lst2 not_less_eq omega_properties(1) one_less_numeral_iff one_power2 power2_eq_square power_mult power_one_right power_strict_increasing_iff semiring_norm(76) square_eq_iff two_powr_div two_powrs_div)
+  moreover have "(n div 2) * 2  = n" using n_two_pot n_lst2  
+    by (metis One_nat_def Suc_lessD assms div_by_Suc_0 one_less_numeral_iff power_0 power_one_right power_strict_increasing_iff semiring_norm(76) two_powrs_div)
+  ultimately show ?thesis  using omega_properties(1)
+    by (metis power_mult)
+qed
+  thus False by simp
+qed
+  then show ?thesis by auto
+qed
+
+lemma div_exp_sub: "2^l  < n \<Longrightarrow> n div (2^l) = 2^(N-l)"using n_two_pot
+    by (smt (z3) One_nat_def diff_is_0_eq diff_le_diff_pow div_if div_le_dividend eq_imp_le le_0_eq le_Suc_eq n_lst2 nat_less_le not_less_eq_eq numeral_2_eq_2 power_0 two_powr_div) 
+
+lemma omega_div_exp_min1:
+  assumes "2^(Suc l) \<le> n"
+  shows "(\<omega> ^(n div 2^(Suc l)))^(2^l) = -1" 
+proof-
+  have "(\<omega> ^(n div 2^(Suc l)))^(2^l) = \<omega> ^((n div 2^(Suc l))*2^l)"
+    by (simp add: power_mult)
+  moreover have "(n div 2^(Suc l)) = 2^(N - Suc l)" using assms div_exp_sub 
+    by (metis n_two_pot eq_imp_le le_neq_implies_less one_less_numeral_iff power_diff power_inject_exp semiring_norm(76) zero_neq_numeral)
+  moreover have "N \<ge> Suc l" using assms n_two_pot 
+    by (metis diff_is_0_eq diff_le_diff_pow gr0I leD le_refl)
+  moreover hence "(2::nat)^(N - Suc l)*2^l = 2^(N- 1)" 
+    by (metis Nat.add_diff_assoc diff_Suc_1 diff_diff_cancel diff_le_self le_add1 le_add_diff_inverse plus_1_eq_Suc power_add) 
+  ultimately show ?thesis 
+    by (metis n_two_pot One_nat_def \<open>n div 2 ^ Suc l = 2 ^ (N - Suc l)\<close> diff_Suc_1 div_exp_sub n_lst2 n_min1_2 n_min1_gr2 nat_less_le nat_power_eq_Suc_0_iff one_less_numeral_iff power_inject_exp power_one_right semiring_norm(76))
+qed
+
+lemma omg_n_2_min1:  "\<omega>^(n div 2) = -1" 
+  by (metis n_lst2 n_min1_2 n_min1_gr2 nat_less_le numeral_Bit0_div_2 numerals(1) power_one_right)
+
+lemma neg_cong: "-(x::('a mod_ring)) = - y \<Longrightarrow> x = y" by simp
+
+text \<open>Generalized \textit{NTT} indeed describes all recursive levels, 
+and thus, it is actually equivalent to the ordinary \textit{NTT} definition.\<close>
+
+theorem FNTT_NTT_gen_eq: "length numbers = 2^l \<Longrightarrow> 2^l \<le> n \<Longrightarrow> FNTT numbers = NTT_gen (length numbers) numbers"
+proof(induction l arbitrary: numbers)
+  case 0
+  then show ?case unfolding NTT_gen_def ntt_gen_def 
+    by (auto simp: length_Suc_conv)
+next
+  case (Suc l)
+  text \<open>We define some lists that are used during the recursive call.\<close>
+  define numbers1 where "numbers1 = [numbers!i .  i <- (filter even [0..<length numbers])]" 
+  define numbers2 where "numbers2 = [numbers!i .  i <- (filter odd [0..<length numbers])]" 
+  define fntt1 where "fntt1 = FNTT numbers1"
+  define fntt2 where "fntt2 = FNTT numbers2" 
+  define sum1 where 
+    "sum1 = map2 (+) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div (length numbers)) * k))) 
+                   fntt2 [0..<((length numbers) div 2)])" 
+  define sum2 where  
+    "sum2 = map2 (-) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div (length numbers)) * k))) 
+                   fntt2 [0..<((length numbers) div 2)])" 
+  define l1 where "l1 = length numbers1"
+  define l2 where "l2 = length numbers2"
+  define llen where "llen = length numbers"
+
+  text \<open>Properties of those lists.\<close>
+  have numbers1_even: "length numbers1 = 2^l" 
+     using numbers1_def length_even_filter Suc by simp
+   have numbers2_even: "length numbers2 = 2^l"
+     using numbers2_def length_odd_filter Suc by simp
+  have numbers1_fntt: "fntt1 = NTT_gen (2^l) numbers1" 
+    using fntt1_def Suc.IH[of numbers1] numbers1_even Suc(3) by simp
+  hence fntt1_by_index: "fntt1 ! i = ntt_gen numbers1 (2^l) i" if "i < 2^l" for i
+    unfolding NTT_gen_def by (simp add: numbers1_even that)
+  have numbers2_fntt: "fntt2 = NTT_gen (2^l) numbers2" 
+    using fntt2_def Suc.IH[of numbers2] numbers2_even Suc(3) by simp
+  hence fntt2_by_index: "fntt2 ! i = ntt_gen numbers2 (2^l) i" if "i < 2^l" for i
+    unfolding NTT_gen_def
+    by (simp add: numbers2_even that)
+  have fntt1_length: "length fntt1 = 2^l" unfolding numbers1_fntt NTT_gen_def numbers1_def
+    using numbers1_def numbers1_even by force
+   have fntt2_length: "length fntt2 = 2^l" unfolding numbers2_fntt NTT_gen_def numbers2_def
+     using numbers2_def numbers2_even by force
+
+   text \<open>We show that the list resulting from $FNTT$ is equal to the $NTT$ list.
+         First, we prove $FNTT$ and $NTT$ to be equal concerning their first halves.\<close>
+   have before_half: "map (ntt_gen numbers llen) [0..<(llen div 2)] = sum1"
+   proof-
+ 
+     text \<open>Length is important, since we want to use list lemmas later on.\<close>
+     have 00:"length (map (ntt_gen numbers llen) [0..<(llen div 2)]) =  length sum1"
+       unfolding sum1_def llen_def
+       using Suc(2) map2_length[of _ fntt2 "[0..<length numbers div 2]"]
+       map2_length[of "(+)" fntt1 "(map2 (\<lambda>x y. x * \<omega> ^ (n div length numbers * y)) fntt2 [0..<length numbers div 2])"]
+       fntt1_length fntt2_length by (simp add: mult_2)
+     have 01:"length sum1 = 2^l" unfolding sum1_def 
+       using "00" Suc.prems(1) sum1_def unfolding llen_def by auto
+
+     text \<open>We show equality by extensionality w.r.t. indices.\<close>
+     have 02:"(map (ntt_gen numbers llen) [0..<(llen div 2)]) ! i = sum1 ! i" 
+       if "i < 2^l" for i
+     proof-
+       text \<open>First simplify this term.\<close>
+       have 000:"(map (ntt_gen numbers llen) [0..<(llen div 2)]) ! i =
+                   ntt_gen numbers llen i" 
+         using "00" "01" that by auto
+
+       text \<open>Expand the definition of $sum1$ and massage the result.\<close>
+       moreover have 001:"sum1 ! i = (fntt1!i) + (fntt2!i) * (\<omega>^((n div llen) * i))"
+         unfolding sum1_def using map2_index
+         "00" "01" NTT_gen_def add.left_neutral diff_zero fntt1_length length_map length_upt map2_map_map map_nth nth_upt numbers2_even numbers2_fntt that llen_def by force
+       moreover have 002:"(fntt1!i) = (\<Sum>j=0..<l1. (numbers1 ! j) * \<omega>^((n div (2^l))*i*j))"
+         unfolding l1_def
+         using fntt1_by_index[of i] that unfolding ntt_gen_def by simp
+       have 003:"... = (\<Sum>j=0..<l1. (numbers ! (2*j)) * \<omega>^((n div llen)*i*(2*j)))"
+         apply (rule sum_rules(2))
+         subgoal for j unfolding numbers1_def 
+           apply(subst llen_def[symmetric])
+         proof-
+           assume ass: "j < l1 "
+           hence "map ((!) numbers) (filter even [0..<length numbers]) ! j = numbers ! (filter even [0..<length numbers] ! j)"
+             using  nth_map[of j "filter even [0..<length numbers]" "(!) numbers" ] 
+             unfolding l1_def numbers1_def
+             by (metis length_map)
+           moreover have "filter even [0..<llen] ! j = 2 * j" using
+            filter_even_nth[of j "llen" "2^l"] Suc(2)  ass numbers1_def numbers1_even 
+             unfolding llen_def l1_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show "map ((!) numbers) (filter even [0..<llen]) ! j * \<omega> ^ (n div 2 ^ l * i * j) =
+                   numbers ! (2 * j) * \<omega> ^ (n div llen * i * (2 * j))" 
+             unfolding llen_def l1_def l2_def by (metis (mono_tags, lifting) mult.assoc mult.left_commute)
+         qed
+         done
+       moreover have 004:
+          "(fntt2!i) * (\<omega>^((n div llen) * i)) = 
+               (\<Sum>j=0..<l2.(numbers2 ! j) * \<omega>^((n div (2^l))*i*j+ (n div llen) * i))"
+            apply(rule trans[where s = "(\<Sum>j = 0..<l2. numbers2 ! j * \<omega> ^ (n div 2 ^ l * i * j) * \<omega> ^ (n div llen * i))"])
+         subgoal 
+            unfolding l2_def llen_def
+            using fntt2_by_index[of i] that sum_in[of _ "(\<omega>^((n div llen) * i))" "l2"] comm_semiring_1_class.semiring_normalization_rules(26)[of \<omega>]
+            unfolding ntt_gen_def
+            using sum_rules  apply presburger
+            done
+          apply (rule sum_rules(2))
+          subgoal for j
+            using fntt2_by_index[of i] that sum_in[of _ "(\<omega>^((n div llen) * i))" "l2"] comm_semiring_1_class.semiring_normalization_rules(26)[of \<omega>]
+            unfolding ntt_gen_def
+            apply auto
+            done
+          done
+     have 005: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<omega>^((n div llen)*i*(2*j+1))))"
+      apply (rule sum_rules(2))
+       subgoal for j unfolding numbers2_def 
+         apply(subst llen_def[symmetric])
+           proof-
+           assume ass: "j < l2 "
+           hence "map ((!) numbers) (filter odd [0..<llen]) ! j = numbers ! (filter odd [0..<llen] ! j)"
+             using  nth_map unfolding l2_def numbers2_def llen_def by (metis length_map)
+           moreover have "filter odd [0..<llen] ! j = 2 * j +1" using
+            filter_odd_nth[of j "length numbers" "2^l"] Suc(2)  ass numbers2_def numbers2_even
+             unfolding l2_def numbers2_def llen_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+            " map ((!) numbers) (filter odd [0..<llen]) ! j * \<omega> ^ (n div 2 ^ l * i * j + n div llen * i) 
+                = numbers ! (2 * j + 1) * \<omega> ^ (n div llen * i * (2 * j + 1))" unfolding llen_def
+             by (smt (z3) Groups.mult_ac(2) distrib_left mult.right_neutral mult_2 mult_cancel_left)
+         qed
+         done
+       then show ?thesis 
+         using 000 001 002 003 004 005 
+         unfolding sum1_def llen_def l1_def l2_def
+         using sum_splice_other_way_round[of "\<lambda> d.  numbers ! d  * \<omega> ^ (n div length numbers * i * d)" "2^l"] Suc(2)
+         unfolding ntt_gen_def 
+         by (smt (z3) Groups.mult_ac(2) numbers1_even numbers2_even power_Suc2)
+     qed
+     then show ?thesis 
+       by  (metis "00" "01" nth_equalityI)
+   qed
+
+   text \<open>We show equality for the indices in the second halves.\<close>
+   have after_half: "map (ntt_gen numbers llen) [(llen div 2)..<llen] = sum2"
+   proof-
+     have 00:"length (map (ntt_gen numbers llen) [(llen div 2)..<llen]) =  length sum2"
+       unfolding sum2_def llen_def 
+       using Suc(2) map2_length map2_length fntt1_length fntt2_length by (simp add: mult_2)
+     have 01:"length sum2 = 2^l" unfolding sum1_def 
+       using "00" Suc.prems(1) sum1_def llen_def  by auto
+     text \<open>Equality for every index.\<close>
+     have 02:"(map (ntt_gen numbers llen)  [(llen div 2)..<llen]) ! i = sum2 ! i" 
+       if "i < 2^l" for i
+     proof-
+       have 000:"(map (ntt_gen numbers llen)  [(llen div 2)..<llen]) ! i =  ntt_gen numbers llen (2^l+i)"
+         unfolding llen_def by (simp add: Suc.prems(1) that)
+       have 001:" (map2 (\<lambda>x y. x * \<omega> ^ (n div llen * y)) fntt2 [0..<llen div 2]) ! i =
+                  fntt2 ! i * \<omega> ^ (n div llen * i)"
+         using  Suc(2) that by (simp add:  fntt2_length  llen_def)
+       have 003: "- fntt2 ! i * \<omega> ^ (n div llen * i) = 
+                    fntt2 ! i * \<omega> ^ (n div llen * (i+ llen div 2))" 
+         using Suc(2) omega_div_exp_min1[of l] unfolding llen_def
+         by (smt (z3) Suc.prems(2) mult.commute mult.left_commute mult_1s_ring_1(2) neq0_conv nonzero_mult_div_cancel_left numeral_One pos2 power_Suc power_add power_mult)
+       hence 004:"sum2 ! i = (fntt1!i) - (fntt2!i) * (\<omega>^((n div llen) * i))"
+         unfolding sum2_def llen_def 
+         by (simp add: Suc.prems(1) fntt1_length fntt2_length that)
+       have 005:"(fntt1!i) = 
+                     (\<Sum>j=0..<l1. (numbers1 ! j) * \<omega>^((n div (2^l))*i*j))"
+        using fntt1_by_index that unfolding ntt_gen_def l1_def by simp
+      have 006:"\<dots> =(\<Sum>j=0..<l1. (numbers ! (2*j)) * \<omega>^((n div llen)*i*(2*j)))"
+         apply (rule sum_rules(2))
+        subgoal for j unfolding numbers1_def 
+          apply(subst llen_def[symmetric])
+         proof-
+           assume ass: "j < l1 "
+           hence "map ((!) numbers) (filter even [0..<llen]) ! j = numbers ! (filter even [0..<llen] ! j)"
+             using  nth_map unfolding llen_def l1_def numbers1_def by (metis length_map)
+           moreover have "filter even [0..<llen] ! j = 2 * j" using
+            filter_even_nth Suc(2)  ass numbers1_def numbers1_even llen_def l1_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+              "map ((!) numbers) (filter even [0..<llen]) ! j * \<omega> ^ (n div 2 ^ l * i * j) =
+                        numbers ! (2 * j) * \<omega> ^ (n div llen * i * (2 * j))" 
+             by (metis (mono_tags, lifting) mult.assoc mult.left_commute)
+         qed
+         done
+        have 007:"\<dots> = (\<Sum>j=0..<l1. (numbers ! (2*j)) * \<omega>^((n div llen)*(2^l + i)*(2*j))) "
+         apply (rule sum_rules(2))
+         subgoal for j 
+           using Suc(2) Suc(3) omega_div_exp_min1[of l] llen_def l1_def numbers1_def
+           apply(smt (verit, del_insts) add.commute minus_power_mult_self mult_2 mult_minus1_right power_add power_mult)
+           done
+         done
+       moreover have 008: "(fntt2!i) * (\<omega>^((n div llen) * i)) =
+                      (\<Sum>j=0..<l2. (numbers2 ! j) * \<omega>^((n div (2^l))*i*j+ (n div llen) * i))" 
+         apply(rule trans[where s = "(\<Sum>j = 0..<l2. numbers2 ! j * \<omega> ^ (n div 2 ^ l * i * j) * \<omega> ^ (n div llen * i))"])
+         subgoal 
+           using fntt2_by_index[of i] that sum_in comm_semiring_1_class.semiring_normalization_rules(26)[of \<omega>]
+           unfolding ntt_gen_def
+           using sum_rules l2_def apply presburger
+         done
+         apply (rule sum_rules(2))
+       subgoal for j
+         using fntt2_by_index[of i] that sum_in comm_semiring_1_class.semiring_normalization_rules(26)[of \<omega>]
+         unfolding ntt_gen_def
+         apply auto
+         done
+       done
+     have 009: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<omega>^((n div llen)*i*(2*j+1))))"
+      apply (rule sum_rules(2))
+       subgoal for j unfolding numbers2_def 
+         apply(subst llen_def[symmetric])
+           proof-
+           assume ass: "j < l2 "
+           hence "map ((!) numbers) (filter odd [0..<llen]) ! j = numbers ! (filter odd [0..<llen] ! j)"
+             using  nth_map llen_def l2_def numbers2_def by (metis length_map)
+           moreover have "filter odd [0..<llen] ! j = 2 * j +1" using
+            filter_odd_nth Suc(2)  ass numbers2_def numbers2_even llen_def l2_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+             "map ((!) numbers) (filter odd [0..<llen]) ! j * \<omega> ^ (n div 2 ^ l * i * j + n div llen * i)
+                 = numbers ! (2 * j + 1) * \<omega> ^ (n div llen * i * (2 * j + 1))" 
+             by (smt (z3) Groups.mult_ac(2) distrib_left mult.right_neutral mult_2 mult_cancel_left)
+         qed
+         done
+       have 010: " (fntt2!i) * (\<omega>^((n div llen) * i)) = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<omega>^((n div llen)*i*(2*j+1)))) "
+         using 008 009 by presburger
+       have 011: " - (fntt2!i) * (\<omega>^((n div llen) * i)) =
+                  (\<Sum>j=0..<l2. - (numbers ! (2*j+1) * \<omega>^((n div llen)*i*(2*j+1)))) "
+         apply(rule neg_cong)
+         apply(rule trans[of _ "fntt2 ! i * \<omega> ^ (n div llen * i)"])
+         subgoal by simp
+         apply(rule trans[where s="(\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<omega>^((n div llen)*i*(2*j+1))))"])
+          subgoal using 008 009 by simp 
+         apply(rule sym)
+         using sum_neg_in[of _ "l2"] 
+         apply simp
+         done
+       have 012: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<omega>^((n div llen)*(2^l+i)*(2*j+1))))"
+         apply(rule sum_rules(2))
+         subgoal for j
+           using Suc(2) Suc(3) omega_div_exp_min1[of l] llen_def l2_def
+           apply (smt (z3) add.commute exp_rule mult.assoc mult_minus1_right plus_1_eq_Suc power_add power_minus1_odd power_mult)
+           done
+         done
+       have 013:"fntt1 ! i = (\<Sum>j = 0..<2 ^ l. numbers!(2*j) * \<omega> ^ (n div llen * (2^l + i) * (2*j)))"
+         using 005 006 007 numbers1_even llen_def  l1_def by auto
+       have 014: "(\<Sum>j = 0..<2 ^ l. numbers ! (2*j + 1) * \<omega> ^ (n div llen* (2^l + i) * (2*j + 1))) =
+                    - fntt2 ! i * \<omega> ^ (n div llen * i)"
+      using  trans[OF l2_def numbers2_even]  sym[OF 012] sym[OF 011] by simp
+      have "ntt_gen numbers llen (2 ^ l + i) = (fntt1!i) - (fntt2!i) * (\<omega>^((n div llen) * i))"
+        unfolding ntt_gen_def apply(subst Suc(2))
+        using  sum_splice[of "\<lambda> d.  numbers ! d  * \<omega> ^ (n div llen * (2^l+i) * d)" "2^l"] sym[OF 013]  014 Suc(2) by simp
+       thus ?thesis using 000 sym[OF 001] "004" sum2_def by simp
+     qed    
+     then show ?thesis 
+       by (metis "00" "01" list_eq_iff_nth_eq)
+   qed
+   obtain x y xs where xyxs: "numbers = x#y#xs" using Suc(2) 
+     by (metis FNTT.cases add.left_neutral even_Suc even_add length_Cons list.size(3) mult_2 power_Suc power_eq_0_iff zero_neq_numeral)
+   show ?case 
+    apply(subst xyxs)
+    apply(subst FNTT.simps(3))
+    apply(subst xyxs[symmetric])+
+     unfolding Let_def      
+     using map_append[of "ntt_gen numbers llen" " [0..<llen div 2]" "[llen div 2..<llen]"] before_half after_half 
+     unfolding llen_def sum1_def sum2_def fntt1_def fntt2_def NTT_gen_def
+    apply (metis (no_types, lifting) Suc.prems(1) numbers1_def length_odd_filter mult_2 numbers2_def numbers2_even power_Suc upt_add_eq_append zero_le_numeral zero_le_power)
+   done
+qed
+
+text \<open>\noindent \textbf{Major Correctness Theorem for Butterfly Algorithm}.\\
+ 
+We have already shown:
+\begin{itemize}
+\item Generalized $NTT$ with degree annotation $2^N$ equals usual $NTT$.
+\item Generalized $NTT$ tracks all levels of recursion in $FNTT$.
+\end{itemize}
+Thus, $FNTT$ equals $NTT$.
+\<close>
+
+theorem FNTT_correct:
+  assumes "length numbers = n"
+  shows "FNTT numbers = NTT numbers"
+  using FNTT_NTT_gen_eq NTT_gen_NTT_full_length assms n_two_pot by force
+
+subsection \<open>Inverse Transform in Butterfly Scheme\<close>
+
+text \<open>We also formalized the inverse transform by using the butterfly scheme.
+Proofs are obtained by adaption of arguments for $FNTT$.\<close>
+
+
+lemmas [simp] = FNTT_termination_aux
+
+fun IFNTT where
+"IFNTT [] = []"|
+"IFNTT [a] = [a]"|
+"IFNTT nums = (let nn = length nums;
+                  nums1 = [nums!i .  i <- (filter even [0..<nn])];
+                  nums2 = [nums!i .  i <- (filter odd [0..<nn])];
+                  ifntt1 = IFNTT nums1;
+                  ifntt2 = IFNTT nums2;
+                  sum1 = map2 (+) ifntt1 (map2 ( \<lambda> x k.  x*(\<mu>^( (n div nn) * k))) ifntt2 [0..<(nn div 2)]);
+                  sum2 = map2 (-) ifntt1 (map2 ( \<lambda> x k.  x*(\<mu>^( (n div nn) * k))) ifntt2 [0..<(nn div 2)])
+                   in sum1@sum2)"
+
+lemmas [simp del] = FNTT_termination_aux
+
+
+definition "intt_gen numbers degr i = (\<Sum>j=0..<(length numbers). (numbers ! j) * \<mu> ^((n div degr)*i*j)) "
+
+definition "INTT_gen degr numbers = map (intt_gen numbers (degr)) [0..< length numbers]"
+
+lemma INTT_gen_INTT_full_length: 
+  assumes "length numbers =n"
+  shows "INTT_gen n numbers = INTT numbers"
+  unfolding INTT_gen_def intt_gen_def INTT_def intt_def 
+  using assms by simp
+
+lemma my_div_exp_min1:
+  assumes "2^(Suc l) \<le> n"
+  shows "(\<mu> ^(n div 2^(Suc l)))^(2^l) = -1" 
+  by (metis assms divide_minus1 mult_zero_right mu_properties(1) nonzero_mult_div_cancel_right omega_div_exp_min1 power_one_over zero_neq_one)
+
+lemma my_n_2_min1:  "\<mu>^(n div 2) = -1" 
+  by (metis divide_minus1 mult_zero_right mu_properties(1) nonzero_mult_div_cancel_right omg_n_2_min1 power_one_over zero_neq_one)
+
+text \<open>Correctness proof by common induction technique. Same strategies as for $FNTT$.\<close>
+
+theorem IFNTT_INTT_gen_eq: 
+ "length numbers = 2^l \<Longrightarrow> 2^l \<le> n \<Longrightarrow> IFNTT numbers = INTT_gen (length numbers) numbers"
+proof(induction l arbitrary: numbers)
+  case 0
+  hence "local.IFNTT numbers = [numbers ! 0]" 
+    by (metis IFNTT.simps(2) One_nat_def Suc_length_conv length_0_conv nth_Cons_0 power_0)
+  then show ?case unfolding INTT_gen_def intt_gen_def 
+    using 0 by simp
+next
+  case (Suc l)
+  text \<open>We define some lists that are used during the recursive call.\<close>
+  define numbers1 where "numbers1 = [numbers!i .  i <- (filter even [0..<length numbers])]" 
+  define numbers2 where "numbers2 = [numbers!i .  i <- (filter odd [0..<length numbers])]" 
+  define ifntt1 where "ifntt1 = IFNTT numbers1"
+  define ifntt2 where "ifntt2 = IFNTT numbers2" 
+  define sum1 where 
+    "sum1 = map2 (+) ifntt1 (map2 ( \<lambda> x k.  x*(\<mu>^( (n div (length numbers)) * k))) 
+                   ifntt2 [0..<((length numbers) div 2)])" 
+  define sum2 where  
+    "sum2 = map2 (-) ifntt1 (map2 ( \<lambda> x k.  x*(\<mu>^( (n div (length numbers)) * k))) 
+                   ifntt2 [0..<((length numbers) div 2)])" 
+  define l1 where "l1 = length numbers1"
+  define l2 where "l2 = length numbers2"
+  define llen where "llen = length numbers"
+
+  text \<open>Properties of those lists\<close>
+  have numbers1_even: "length numbers1 = 2^l" 
+     using numbers1_def length_even_filter Suc by simp
+   have numbers2_even: "length numbers2 = 2^l"
+     using numbers2_def length_odd_filter Suc by simp
+  have numbers1_ifntt: "ifntt1 = INTT_gen (2^l) numbers1" 
+    using ifntt1_def Suc.IH[of numbers1] numbers1_even Suc(3) by simp
+  hence ifntt1_by_index: "ifntt1 ! i = intt_gen numbers1 (2^l) i" if "i < 2^l" for i
+    unfolding INTT_gen_def by (simp add: numbers1_even that)
+  have numbers2_ifntt: "ifntt2 = INTT_gen (2^l) numbers2" 
+    using ifntt2_def Suc.IH[of numbers2] numbers2_even Suc(3) by simp
+  hence ifntt2_by_index: "ifntt2 ! i = intt_gen numbers2 (2^l) i" if "i < 2^l" for i
+    unfolding INTT_gen_def by (simp add: numbers2_even that)
+  have ifntt1_length: "length ifntt1 = 2^l" unfolding numbers1_ifntt INTT_gen_def numbers1_def
+    using numbers1_def numbers1_even by force
+   have ifntt2_length: "length ifntt2 = 2^l" unfolding numbers2_ifntt INTT_gen_def numbers2_def
+     using numbers2_def numbers2_even by force
+
+   text \<open>Same proof structure as for the  \textit{FNTT} proof.
+         $\omega$s are just replaced by $\mu$s.\<close>
+   have before_half: "map (intt_gen numbers llen) [0..<(llen div 2)] = sum1"
+   proof-
+ 
+     text \<open>Length is important, since we want to use list lemmas later on.\<close>
+     have 00:"length (map (intt_gen numbers llen) [0..<(llen div 2)]) =  length sum1"
+       unfolding sum1_def llen_def
+       using Suc(2) map2_length[of _ ifntt2 "[0..<length numbers div 2]"]
+       map2_length[of "(+)" ifntt1 "(map2 (\<lambda>x y. x * \<mu> ^ (n div length numbers * y)) ifntt2 [0..<length numbers div 2])"]
+       ifntt1_length ifntt2_length by (simp add: mult_2)
+     have 01:"length sum1 = 2^l" unfolding sum1_def 
+       using "00" Suc.prems(1) sum1_def unfolding llen_def by auto
+
+     text \<open>We show equality by extensionality on indices.\<close>
+     have 02:"(map (intt_gen numbers llen) [0..<(llen div 2)]) ! i = sum1 ! i" 
+       if "i < 2^l" for i
+     proof-
+       text \<open>First simplify this term.\<close>
+       have 000:"(map (intt_gen numbers llen) [0..<(llen div 2)]) ! i =  intt_gen numbers llen i" 
+         using "00" "01" that by auto
+
+       text \<open>Expand the definition of $sum1$ and massage the result.\<close>
+       moreover have 001:"sum1 ! i = (ifntt1!i) + (ifntt2!i) * (\<mu>^((n div llen) * i))"
+         unfolding sum1_def using map2_index
+         "00" "01" INTT_gen_def add.left_neutral diff_zero ifntt1_length length_map length_upt map2_map_map map_nth nth_upt numbers2_even numbers2_ifntt that llen_def by force
+       moreover have 002:"(ifntt1!i) = (\<Sum>j=0..<l1. (numbers1 ! j) * \<mu>^((n div (2^l))*i*j))"
+         unfolding l1_def
+         using ifntt1_by_index[of i] that unfolding intt_gen_def by simp
+       have 003:"... = (\<Sum>j=0..<l1. (numbers ! (2*j)) * \<mu>^((n div llen)*i*(2*j)))"
+         apply (rule sum_rules(2))
+         subgoal for j unfolding numbers1_def 
+           apply(subst llen_def[symmetric])
+         proof-
+           assume ass: "j < l1 "
+           hence "map ((!) numbers) (filter even [0..<length numbers]) ! j = numbers ! (filter even [0..<length numbers] ! j)"
+             using  nth_map[of j "filter even [0..<length numbers]" "(!) numbers" ] 
+             unfolding l1_def numbers1_def
+             by (metis length_map)
+           moreover have "filter even [0..<llen] ! j = 2 * j" using
+            filter_even_nth[of j "llen" "2^l"] Suc(2)  ass numbers1_def numbers1_even 
+             unfolding llen_def l1_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show "map ((!) numbers) (filter even [0..<llen]) ! j * \<mu> ^ (n div 2 ^ l * i * j) =
+                   numbers ! (2 * j) * \<mu> ^ (n div llen * i * (2 * j))" 
+             unfolding llen_def l1_def l2_def by (metis (mono_tags, lifting) mult.assoc mult.left_commute)
+         qed
+         done
+       moreover have 004:
+          "(ifntt2!i) * (\<mu>^((n div llen) * i)) = 
+               (\<Sum>j=0..<l2.(numbers2 ! j) * \<mu>^((n div (2^l))*i*j+ (n div llen) * i))"
+          apply(rule trans[where s = "(\<Sum>j = 0..<l2. numbers2 ! j * \<mu> ^ (n div 2 ^ l * i * j) * \<mu> ^ (n div llen * i))"])
+         subgoal 
+            unfolding l2_def llen_def
+            using ifntt2_by_index[of i] that sum_in[of _ "(\<mu>^((n div llen) * i))" "l2"] comm_semiring_1_class.semiring_normalization_rules(26)[of \<mu>]
+            unfolding intt_gen_def
+            using sum_rules apply presburger
+            done
+          apply (rule sum_rules(2))
+          subgoal for j
+             using ifntt2_by_index[of i] that sum_in[of _ "(\<mu>^((n div llen) * i))" "l2"] comm_semiring_1_class.semiring_normalization_rules(26)[of \<mu>]
+            unfolding intt_gen_def
+            apply auto
+            done
+          done
+     have 005: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<mu>^((n div llen)*i*(2*j+1))))"
+      apply (rule sum_rules(2))
+       subgoal for j unfolding numbers2_def 
+         apply(subst llen_def[symmetric])
+           proof-
+           assume ass: "j < l2 "
+           hence "map ((!) numbers) (filter odd [0..<llen]) ! j = numbers ! (filter odd [0..<llen] ! j)"
+             using  nth_map unfolding l2_def numbers2_def llen_def by (metis length_map)
+           moreover have "filter odd [0..<llen] ! j = 2 * j +1" using
+            filter_odd_nth[of j "length numbers" "2^l"] Suc(2)  ass numbers2_def numbers2_even
+             unfolding l2_def numbers2_def llen_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+            " map ((!) numbers) (filter odd [0..<llen]) ! j * \<mu> ^ (n div 2 ^ l * i * j + n div llen * i) 
+                = numbers ! (2 * j + 1) * \<mu> ^ (n div llen * i * (2 * j + 1))" unfolding llen_def
+             by (smt (z3) Groups.mult_ac(2) distrib_left mult.right_neutral mult_2 mult_cancel_left)
+         qed
+         done
+       then show ?thesis 
+         using 000 001 002 003 004 005 
+         unfolding sum1_def llen_def l1_def l2_def
+         using sum_splice_other_way_round[of "\<lambda> d.  numbers ! d  * \<mu> ^ (n div length numbers * i * d)" "2^l"] Suc(2)
+         unfolding intt_gen_def 
+         by (smt (z3) Groups.mult_ac(2) numbers1_even numbers2_even power_Suc2)
+     qed
+     then show ?thesis 
+       by  (metis "00" "01" nth_equalityI)
+   qed
+
+   text \<open>We show index-wise equality for the second halves\<close>
+   have after_half: "map (intt_gen numbers llen) [(llen div 2)..<llen] = sum2"
+   proof-
+     have 00:"length (map (intt_gen numbers llen) [(llen div 2)..<llen]) =  length sum2"
+       unfolding sum2_def llen_def 
+       using Suc(2) map2_length map2_length ifntt1_length ifntt2_length by (simp add: mult_2)
+     have 01:"length sum2 = 2^l" unfolding sum1_def 
+       using "00" Suc.prems(1) sum1_def llen_def  by auto
+
+     text \<open>Equality for every index\<close>
+     have 02:"(map (intt_gen numbers llen)  [(llen div 2)..<llen]) ! i = sum2 ! i" 
+       if "i < 2^l" for i
+     proof-
+       have 000:"(map (intt_gen numbers llen)  [(llen div 2)..<llen]) ! i =  intt_gen numbers llen (2^l+i)"
+         unfolding llen_def by (simp add: Suc.prems(1) that)
+       have 001:" (map2 (\<lambda>x y. x * \<mu> ^ (n div llen * y)) ifntt2 [0..<llen div 2]) ! i =
+                  ifntt2 ! i * \<mu> ^ (n div llen * i)"
+         using  Suc(2) that by (simp add:  ifntt2_length  llen_def)
+       have 003: "- ifntt2 ! i * \<mu> ^ (n div llen * i) = ifntt2 ! i * \<mu> ^ (n div llen * (i+ llen div 2))" 
+         using Suc(2) my_div_exp_min1[of l] unfolding llen_def
+         by (smt (z3) Suc.prems(2) mult.commute mult.left_commute mult_1s_ring_1(2) neq0_conv nonzero_mult_div_cancel_left numeral_One pos2 power_Suc power_add power_mult)
+       hence 004:"sum2 ! i = (ifntt1!i) - (ifntt2!i) * (\<mu>^((n div llen) * i))"
+         unfolding sum2_def llen_def 
+         by (simp add: Suc.prems(1) ifntt1_length ifntt2_length that)
+       have 005:"(ifntt1!i) = 
+                     (\<Sum>j=0..<l1. (numbers1 ! j) * \<mu>^((n div (2^l))*i*j))"
+        using ifntt1_by_index that unfolding intt_gen_def l1_def by simp
+      have 006:"\<dots> =(\<Sum>j=0..<l1. (numbers ! (2*j)) * \<mu>^((n div llen)*i*(2*j)))"
+         apply (rule sum_rules(2))
+         subgoal for j unfolding numbers1_def 
+          apply(subst llen_def[symmetric])
+         proof-
+           assume ass: "j < l1 "
+           hence "map ((!) numbers) (filter even [0..<llen]) ! j = numbers ! (filter even [0..<llen] ! j)"
+             using  nth_map unfolding llen_def l1_def numbers1_def by (metis length_map)
+           moreover have "filter even [0..<llen] ! j = 2 * j" using
+            filter_even_nth Suc(2)  ass numbers1_def numbers1_even llen_def l1_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+              "map ((!) numbers) (filter even [0..<llen]) ! j * \<mu> ^ (n div 2 ^ l * i * j) =
+                        numbers ! (2 * j) * \<mu> ^ (n div llen * i * (2 * j))" 
+             by (metis (mono_tags, lifting) mult.assoc mult.left_commute)
+         qed
+         done
+        have 007:"\<dots> = (\<Sum>j=0..<l1. (numbers ! (2*j)) * \<mu> ^((n div llen)*(2^l + i)*(2*j))) "
+         apply (rule sum_rules(2))
+         subgoal for j 
+           using Suc(2) Suc(3) my_div_exp_min1[of l] llen_def l1_def numbers1_def
+           apply(smt (verit, del_insts) add.commute minus_power_mult_self mult_2 mult_minus1_right power_add power_mult)
+           done
+         done
+       moreover have 008: "(ifntt2!i) * (\<mu>^((n div llen) * i)) =
+                      (\<Sum>j=0..<l2. (numbers2 ! j) * \<mu>^((n div (2^l))*i*j+ (n div llen) * i))"
+         apply(rule trans[where s = "(\<Sum>j = 0..<l2. numbers2 ! j * \<mu> ^ (n div 2 ^ l * i * j) * \<mu> ^ (n div llen * i))"])
+         subgoal 
+          using ifntt2_by_index[of i] that sum_in comm_semiring_1_class.semiring_normalization_rules(26)[of \<mu>]
+          unfolding intt_gen_def
+          using sum_rules l2_def apply presburger
+         done
+         apply (rule sum_rules(2))
+       subgoal for j
+         using ifntt2_by_index[of i] that sum_in comm_semiring_1_class.semiring_normalization_rules(26)[of \<mu>]
+         unfolding intt_gen_def
+         apply auto 
+         done
+       done
+     have 009: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<mu>^((n div llen)*i*(2*j+1))))"
+      apply (rule sum_rules(2))
+       subgoal for j unfolding numbers2_def 
+         apply(subst llen_def[symmetric])
+           proof-
+           assume ass: "j < l2 "
+           hence "map ((!) numbers) (filter odd [0..<llen]) ! j = numbers ! (filter odd [0..<llen] ! j)"
+             using  nth_map llen_def l2_def numbers2_def by (metis length_map)
+           moreover have "filter odd [0..<llen] ! j = 2 * j +1" using
+            filter_odd_nth Suc(2)  ass numbers2_def numbers2_even llen_def l2_def by fastforce
+           moreover have "n div llen * (2 * j) = ((n div (2 ^ l))  * j)"
+             using Suc(2) two_powrs_div[of l N] n_two_pot two_powr_div Suc(3) llen_def
+             by (metis One_nat_def div_if mult.assoc nat_less_le not_less_eq numeral_2_eq_2 power_eq_0_iff power_inject_exp zero_neq_numeral)
+           ultimately show 
+             "map ((!) numbers) (filter odd [0..<llen]) ! j * \<mu> ^ (n div 2 ^ l * i * j + n div llen * i)
+                 = numbers ! (2 * j + 1) * \<mu> ^ (n div llen * i * (2 * j + 1))" 
+             by (smt (z3) Groups.mult_ac(2) distrib_left mult.right_neutral mult_2 mult_cancel_left)
+         qed
+         done
+       have 010: " (ifntt2!i) * (\<mu>^((n div llen) * i)) = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<mu>^((n div llen)*i*(2*j+1)))) "
+         using 008 009 by presburger
+       have 011: " - (ifntt2!i) * (\<mu>^((n div llen) * i)) =
+                  (\<Sum>j=0..<l2. - (numbers ! (2*j+1) * \<mu>^((n div llen)*i*(2*j+1)))) "
+         apply(rule neg_cong)
+         apply(rule trans[where s="(\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<mu>^((n div llen)*i*(2*j+1))))"])
+         subgoal using 008 009 by simp
+         apply(rule sym)
+         using sum_neg_in[of _ "l2"] 
+         apply simp
+         done
+       have 012: "\<dots> = (\<Sum>j=0..<l2. (numbers ! (2*j+1) * \<mu>^((n div llen)*(2^l+i)*(2*j+1))))"
+         apply(rule sum_rules(2))
+         subgoal for j
+           using Suc(2) Suc(3) my_div_exp_min1[of l] llen_def l2_def
+           apply (smt (z3) add.commute exp_rule mult.assoc mult_minus1_right plus_1_eq_Suc power_add power_minus1_odd power_mult)
+           done
+         done
+       have 013:"ifntt1 ! i = (\<Sum>j = 0..<2 ^ l. numbers!(2*j) * \<mu> ^ (n div llen * (2^l + i) * (2*j)))"
+         using 005 006 007 numbers1_even llen_def  l1_def by auto
+       have 014: "(\<Sum>j = 0..<2 ^ l. numbers ! (2*j + 1) * \<mu> ^ (n div llen* (2^l + i) * (2*j + 1))) =
+                    - ifntt2 ! i * \<mu> ^ (n div llen * i)"
+      using  trans[OF l2_def numbers2_even]  sym[OF 012] sym[OF 011] by simp
+      have "intt_gen numbers llen (2 ^ l + i) = (ifntt1!i) - (ifntt2!i) * (\<mu>^((n div llen) * i))"
+        unfolding intt_gen_def 
+        apply(subst Suc(2))
+        using  sum_splice[of "\<lambda> d.  numbers ! d  * \<mu> ^ (n div llen * (2^l+i) * d)" "2^l"] sym[OF 013]  014 Suc(2) by simp
+       thus ?thesis using 000 sym[OF 001] "004" sum2_def by simp
+     qed    
+     then show ?thesis 
+       by (metis "00" "01" list_eq_iff_nth_eq)
+   qed
+   obtain x y xs where xyxs: "numbers = x#y#xs" using Suc(2) 
+     by (metis FNTT.cases add.left_neutral even_Suc even_add length_Cons list.size(3) mult_2 power_Suc power_eq_0_iff zero_neq_numeral)
+   show ?case 
+    apply(subst xyxs)
+    apply(subst IFNTT.simps(3))
+    apply(subst xyxs[symmetric])+
+     unfolding Let_def      
+     using map_append[of "intt_gen numbers llen" " [0..<llen div 2]" "[llen div 2..<llen]"] before_half after_half 
+     unfolding llen_def sum1_def sum2_def ifntt1_def ifntt2_def INTT_gen_def
+    apply (metis (no_types, lifting) Suc.prems(1) numbers1_def length_odd_filter mult_2 numbers2_def numbers2_even power_Suc upt_add_eq_append zero_le_numeral zero_le_power)
+   done
+qed
+
+text \<open>Correctness of the butterfly scheme for the inverse \textit{INTT}.\<close>
+
+theorem IFNTT_correct:
+  assumes "length numbers = n"
+  shows "IFNTT numbers = INTT numbers"
+  using IFNTT_INTT_gen_eq INTT_gen_INTT_full_length assms n_two_pot by force
+
+text \<open>Also $FNTT$ and $IFNTT$ are mutually inverse\<close>
+
+theorem IFNTT_inv_FNTT:  
+  assumes "length numbers = n"
+  shows "IFNTT (FNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers"
+  by (simp add: FNTT_correct IFNTT_correct assms length_NTT ntt_correct)
+
+text \<open>The other way round:\<close>
+
+theorem FNTT_inv_IFNTT:  
+  assumes "length numbers = n"
+  shows "FNTT (IFNTT numbers) = map ((*) (of_int_mod_ring (int n))) numbers"
+by (simp add: FNTT_correct IFNTT_correct assms inv_ntt_correct length_INTT)
+
+subsection \<open>An Optimization\<close>
+text \<open>Currently, we extract elements on even and odd positions respectively by a list comprehension 
+     over even and odd indices. 
+Due to the definition in Isabelle, an index access has linear time complexity. 
+This results in quadratic running time complexity for every level
+in the recursion tree of the \textit{FNTT}. 
+In order to reach the $\mathcal{O}(n \log n)$ time bound, 
+we have find a better way of splitting the elements at even or odd indices respectively.
+\<close>
+
+text \<open>A core of this optimization is the $evens\text{-}odds$ function,
+ which splits the vectors in linear time.\<close>
+
+fun evens_odds::"bool \<Rightarrow>'b list \<Rightarrow> 'b list" where
+"evens_odds _ [] = []"|
+"evens_odds True (x#xs)= (x# evens_odds False xs)"|
+"evens_odds False (x#xs) = evens_odds True xs"
+
+lemma map_filter_shift: " map f (filter even [0..<Suc g]) = 
+        f 0 #  map (\<lambda> x. f (x+1)) (filter odd [0..<g])"
+  by (induction g) auto
+
+lemma map_filter_shift': " map f (filter odd [0..<Suc g]) = 
+          map (\<lambda> x. f (x+1)) (filter even [0..<g])"
+  by (induction g) auto
+
+text \<open>A splitting by the $evens\text{-}odds$ function is 
+equivalent to the more textbook-like list comprehension.\<close>
+
+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 "
+  apply(induction xs)
+   apply simp
+  subgoal for x xs
+    apply rule
+    subgoal 
+      apply(subst evens_odds.simps)
+      apply(rule trans[of _ "map ((!) (x # xs)) (filter even [0..<Suc (length xs)])"])
+      subgoal by simp
+      apply(rule trans[OF  map_filter_shift[of "(!) (x # xs)" "length xs"]])
+      apply simp
+      done
+
+      apply(subst evens_odds.simps)
+      apply(rule trans[of _ "map ((!) (x # xs)) (filter odd [0..<Suc (length xs)])"])
+      subgoal by simp
+      apply(rule trans[OF  map_filter_shift'[of "(!) (x # xs)" "length xs"]])
+      apply simp
+    done
+  done
+
+text \<open>For automated termination proof.\<close>
+
+lemma [simp]: "length (evens_odds True vc) < Suc (length vc)" 
+              "length (evens_odds False vc) < Suc (length vc)"
+  by (metis filter_compehension_evens_odds le_imp_less_Suc length_filter_le length_map map_nth)+
+
+
+text \<open>The $FNTT$ definition from above was suitable for matters of proof conduction.
+   However, the naive decomposition into elements at odd and even indices induces a complexity of $n^2$ in every recursive step.
+As mentioned, the $evens\text{-}odds$ function filters for elements on even or odd positions respectively.
+The list has to be traversed only once which gives \textit{linear} complexity for every recursive step. \<close>
+
+fun FNTT' where
+"FNTT' [] = []"|
+"FNTT' [a] = [a]"|
+"FNTT' nums = (let nn = length nums;
+                  nums1 = evens_odds  True nums;
+                  nums2 = evens_odds False nums;
+                  fntt1 = FNTT' nums1;
+                  fntt2 = FNTT' nums2;
+                  fntt2_omg =  (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)]);
+                  sum1 = map2 (+) fntt1 fntt2_omg;
+                  sum2 = map2 (-) fntt1 fntt2_omg
+                   in sum1@sum2)"
+
+text \<open>The optimized \textit{FNTT} is equivalent to the naive \textit{NTT}.\<close>
+
+lemma FNTT'_FNTT: "FNTT' xs = FNTT xs"
+  apply(induction xs rule: FNTT'.induct)
+  subgoal by simp
+  subgoal by simp
+  apply(subst FNTT'.simps(3))
+  apply(subst FNTT.simps(3))
+  subgoal for a b xs
+    unfolding Let_def
+    apply (metis filter_compehension_evens_odds)
+    done
+  done
+
+text \<open>It is quite surprising that some inaccuracies in the interpretation of informal textbook definitions 
+- even when just considering such a simple algorithm - can indeed affect time complexity.\<close>
+
+subsection \<open>Arguments on Running Time\<close>
+
+text \<open> $FFT$ is especially known for its $\mathcal{O}(n \log n)$ running time. 
+Unfortunately, Isabelle does not provide a built-in time formalization. 
+Nonetheless we can reason about running time after defining some "reasonable" consumption functions by hand.
+Our approach loosely follows a general pattern by Nipkow et al.~\parencite{funalgs}.
+First, we give running times and lemmas for the auxiliary functions used during FNTT.\\
+General ideas behind the $\mathcal{O}(n \log n)$ are:
+\begin{itemize}
+\item By recursively halving the problem size, we obtain a tree of depth  $\mathcal{O}(\log n)$.
+\item For every level of that tree, we have to process all elements which gives  $\mathcal{O}(n)$ time.
+\end{itemize}
+
+\<close>
+
+text \<open>Time for splitting the list according to even and odd indices.\<close>
+
+fun T_\<^sub>e\<^sub>o::"bool \<Rightarrow> 'c list \<Rightarrow> nat" where
+" T_\<^sub>e\<^sub>o _ [] = 1"|
+" T_\<^sub>e\<^sub>o True (x#xs)= (1+  T_\<^sub>e\<^sub>o False xs)"|
+" T_\<^sub>e\<^sub>o  False (x#xs) = (1+  T_\<^sub>e\<^sub>o True xs)"
+
+lemma T_eo_linear:  "T_\<^sub>e\<^sub>o b xs = length xs + 1"
+  by (induction b xs rule: T_\<^sub>e\<^sub>o.induct) auto
+
+text \<open>Time for length.\<close>
+
+fun T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h where
+"T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h [] = 1 "|
+"T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x#xs) = 1+ T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h xs"
+
+lemma T_length_linear: "T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h xs = length xs +1"
+  by (induction xs) auto
+
+text \<open>Time for index access.\<close>
+
+fun T\<^sub>n\<^sub>t\<^sub>h where
+"T\<^sub>n\<^sub>t\<^sub>h [] i = 1 "|
+"T\<^sub>n\<^sub>t\<^sub>h (x#xs) 0 = 1"|
+"T\<^sub>n\<^sub>t\<^sub>h (x#xs) (Suc i) = 1 + T\<^sub>n\<^sub>t\<^sub>h xs i"
+
+lemma T_nth_linear: "T\<^sub>n\<^sub>t\<^sub>h xs i \<le> length xs +1"
+  by (induction xs i rule: T\<^sub>n\<^sub>t\<^sub>h.induct) auto
+
+text \<open>Time for mapping two lists into one result.\<close>
+
+fun  T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 where
+ "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t [] _ = 1"|
+ "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t  _ [] = 1"|
+ "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t (x#xs) (y#ys) = (t x y + 1 + T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 t xs ys)"
+
+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"
+  apply(induction t xs ys rule: T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.induct)
+  subgoal by simp
+  subgoal by simp
+  subgoal for t x xs y ys
+    apply(subst  T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.simps, subst length_Cons, subst length_Cons)
+    using min_add_distrib_right[of 1]
+    by (smt (z3) Suc_eq_plus1 add.assoc add.commute add_le_mono le_numeral_extra(4) min_def mult.commute mult_Suc_right)
+  done
+
+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"
+ by(induction t xs ys rule: T\<^sub>m\<^sub>a\<^sub>p\<^sub>2.induct) simp+
+  
+
+text \<open>Time for append.\<close>
+
+fun T\<^sub>a\<^sub>p\<^sub>p where
+ " T\<^sub>a\<^sub>p\<^sub>p  [] _ = 1"|
+ " T\<^sub>a\<^sub>p\<^sub>p  (x#xs) ys = 1 +  T\<^sub>a\<^sub>p\<^sub>p  xs ys"
+
+lemma T_app_linear: " T\<^sub>a\<^sub>p\<^sub>p xs ys = length xs +1"
+  by(induction xs) auto
+
+
+text \<open>Running Time of (optimized) $FNTT$.\<close>
+
+fun T\<^sub>F\<^sub>N\<^sub>T\<^sub>T::"('a mod_ring) list \<Rightarrow> nat" where
+"T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = 1"|
+"T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = 1"|
+"T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums = (1 +T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h nums+ 3+
+                 
+                 (let nn = length nums;
+                  nums1 = evens_odds True nums;
+                  nums2 = evens_odds False nums
+                  in 
+                  T_\<^sub>e\<^sub>o True nums + T_\<^sub>e\<^sub>o False nums + 2 +
+                 (let
+                  fntt1 = FNTT nums1;
+                  fntt2 = FNTT nums2
+                  in 
+                  (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1) + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2) +
+                 (let 
+                  sum1 = map2 (+) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)]);
+                  sum2 = map2 (-) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)])
+                   in 
+                    2* T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda> x y. 1) fntt2 [0..<(nn div 2)] +
+                      2* T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda> x y. 1) fntt1 (map2 ( \<lambda> x k.  x*(\<omega>^( (n div nn) * k))) fntt2 [0..<(nn div 2)]) +
+                    T\<^sub>a\<^sub>p\<^sub>p sum1 sum2))))"
+
+lemma mono:  "((f x)::nat) \<le> f y \<Longrightarrow> f y \<le> fz \<Longrightarrow> f x \<le> fz" by simp
+
+lemma evens_odds_length:
+      "length (evens_odds True xs) = (length xs+1) div 2 \<and>
+       length (evens_odds False xs) = (length xs) div 2"
+ by(induction xs) simp+
+
+text \<open>Length preservation during $FNTT$.\<close>
+
+lemma FNTT_length: "length numbers = 2^l \<Longrightarrow> length (FNTT numbers) = length numbers" 
+proof(induction l arbitrary: numbers)
+  case (Suc l)
+  define numbers1 where "numbers1 = [numbers!i .  i <- (filter even [0..<length numbers])]" 
+  define numbers2 where "numbers2 = [numbers!i .  i <- (filter odd [0..<length numbers])]" 
+  define fntt1 where "fntt1 = FNTT numbers1"
+  define fntt2 where "fntt2 = FNTT numbers2" 
+  define presum where 
+    "presum = (map2 ( \<lambda> x k.  x*(\<omega>^( (n div (length numbers)) * k))) 
+                   fntt2 [0..<((length numbers) div 2)])" 
+  define sum1 where 
+    "sum1 = map2 (+) fntt1 presum" 
+   define sum2 where  
+    "sum2 = map2 (-) fntt1 presum" 
+  have "length numbers1  = 2^l" 
+    by (metis Suc.prems numbers1_def diff_add_inverse2 length_even_filter mult_2 nonzero_mult_div_cancel_left power_Suc zero_neq_numeral)
+  hence "length fntt1 = 2^l" 
+    by (simp add: Suc.IH fntt1_def)
+  hence "length presum = 2^l" unfolding presum_def 
+    using map2_length Suc.IH Suc.prems fntt2_def length_odd_filter numbers2_def by force
+   hence "length sum1 = 2^l" 
+    by (simp add: \<open>length fntt1 = 2 ^ l\<close> sum1_def)
+   have "length numbers2 = 2^l"
+    by (metis Suc.prems numbers2_def length_odd_filter nonzero_mult_div_cancel_left power_Suc zero_neq_numeral)
+  hence "length fntt2 = 2^l"
+    by (simp add: Suc.IH fntt2_def)
+  hence "length sum2 = 2^l" unfolding sum2_def  
+    using \<open>length sum1 = 2 ^ l\<close> sum1_def by force
+  hence final:"length (sum1@sum2) = 2^(Suc l)" 
+    by (simp add: \<open>length sum1 = 2 ^ l\<close>)
+  obtain x y xs where xyxs_Def: "numbers = x#y#xs"
+    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)
+  show ?case 
+    apply(subst xyxs_Def, subst FNTT.simps(3), subst xyxs_Def[symmetric])
+    unfolding Let_def
+    using final 
+    unfolding sum1_def sum2_def presum_def fntt1_def fntt2_def numbers1_def numbers2_def
+    using Suc by (metis xyxs_Def)
+qed (metis FNTT.simps(2) Suc_length_conv length_0_conv nat_power_eq_Suc_0_iff)
+   
+lemma add_cong: "(a1::nat) + a2+a3 +a4= b \<Longrightarrow> a1 +a2+ c + a3+a4= c +b"
+  by simp
+
+lemma add_mono:"a \<le> (b::nat) \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b +d" by simp
+
+lemma xyz: " Suc (Suc (length xs)) = 2 ^ l \<Longrightarrow> length (x # evens_odds True xs) = 2 ^ (l - 1)"
+  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)
+
+lemma zyx:" Suc (Suc (length xs)) = 2 ^ l  \<Longrightarrow> length (y # evens_odds False xs) = 2 ^ (l - 1)"
+  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)
+
+text \<open>When $length \; xs = 2^l$, then $length \; (evens\text{-}odds \; xs) = 2^{l-1}$.\<close>
+
+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-
+  have "Suc(length (evens_odds b xs)) = length (evens_odds b (x#y#xs))" 
+    by (metis (full_types)  evens_odds.simps(2) evens_odds.simps(3) length_Cons)
+  have "length (x#y#xs) = 2^l" using assms by simp
+  have "length (evens_odds b (x#y#xs))  = 2^(l-1)" 
+    apply (cases b)
+    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)
+    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)
+   then show ?thesis 
+    by (metis \<open>Suc (length (evens_odds b xs)) = length (evens_odds b (x # y # xs))\<close>)
+qed
+
+text \<open> \noindent \textbf{Major Lemma:} We rewrite the Running time of $FNTT$ in this proof and collect constraints for the time bound.
+Using this, bounds are chosen in a way such that the induction goes through properly.
+\paragraph \noindent We define:
+
+\begin{equation*}
+T(2^0) = 1
+\end{equation*}
+
+\begin{equation*}
+T(2^l) = 
+(2^l - 1)\cdot 14 apply+ 15 \cdot l \cdot 2^{l-1} + 2^l
+\end{equation*}
+
+\paragraph \noindent We want to show:
+
+\begin{equation*}
+T_{FNTT}(2^l) = T(2^l)
+\end{equation*}
+
+(Note that by abuse of types, the $2^l$ denotes a list of length $2^l$.)
+
+\paragraph \noindent First, let's informally check that $T$ is indeed an accurate description of the running time:
+
+\begin{align*}
+T_{FNTT}(2^l) & \; =  14 + 15 \cdot  2 ^ {l-1} + 2 \cdot T_{FNTT}(2^{l-1}) \hspace{1cm} \text{by analyzing the running time function}\\
+&\overset{I.H.}{=}  14 + 15 \cdot  2 ^ {l-1} + 2 \cdot  ((2^{l-1} - 1) \cdot 14 + (l - 1) \cdot 15 \cdot 2^{l-2} + 2^{l-1})\\
+& \;= 14 \cdot 2^l - 14 + 15 \cdot  2 ^ {l-1} + 15\cdot l \cdot 2^{l-1} -  15 \cdot 2^{l-1} + 2^l\\
+&\; = (2^l - 1)\cdot 14 + 15 \cdot l \cdot 2^{l-1} + 2^l\\
+&\overset{def.}{=} T(2^l)
+\end{align*}
+
+The base case is trivially true.
+\<close>
+
+theorem tight_bound: 
+  assumes T_def: "\<And> numbers l. length numbers = 2^l \<Longrightarrow> l > 0 \<Longrightarrow>
+                               T numbers  = (2^l - 1) * 14 + l *15*2^(l-1) + 2^l"
+                 "\<And> numbers l. l =0 \<Longrightarrow> length numbers = 2^l \<Longrightarrow> T numbers = 1"
+  shows " length numbers = 2^l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers =  T numbers"
+proof(induction numbers arbitrary: l rule: T\<^sub>F\<^sub>N\<^sub>T\<^sub>T.induct)
+  case (3 x y numbers)
+
+  text \<open>Some definitions for making term rewriting simpler.\<close>
+
+  define  nn where "nn = length (x # y # numbers)" 
+  define  nums1 where "nums1 = evens_odds True (x # y # numbers)" 
+  define  nums2 where "nums2 = evens_odds False (x # y # numbers)"
+  define fntt1  where "fntt1 = local.FNTT nums1"
+  define fntt2 where "fntt2 = local.FNTT nums2"
+  define sum1 where "sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])"
+  define sum2 where "sum2 = map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])"
+
+  text \<open>Unfolding the running time function and combining it with the definitions above.\<close>
+
+  have TFNNT_simp: " T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) =
+                    1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 +  
+                    T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 +
+                    local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 +
+                    2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] +
+                    2 *
+                    T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) +
+                    T\<^sub>a\<^sub>p\<^sub>p sum1 sum2" 
+    apply(subst  T\<^sub>F\<^sub>N\<^sub>T\<^sub>T.simps(3))
+    unfolding Let_def unfolding sum2_def sum1_def fntt1_def fntt2_def nums1_def nums2_def nn_def
+    apply simp
+    done
+
+  text \<open>Application of lemmas related to running times of auxiliary functions.\<close>
+
+  have length_nums1: "length nums1 = (2::nat)^(l-1)"
+    unfolding nums1_def
+    using evens_odds_length[of "x # y # numbers"] 3(3) xyz by fastforce
+ have length_nums2: "length nums2 = (2::nat)^(l-1)"
+    unfolding nums2_def
+    using evens_odds_length[of "x # y # numbers"] 3(3) 
+    by (metis One_nat_def le_0_eq length_Cons lessI list.size(4) neq0_conv not_add_less2 not_less_eq_eq pos2 power_Suc0_right power_diff_power_eq power_eq_if)
+  have length_simp: "T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = (2::nat) ^l +1"
+    using T_length_linear[of "x#y#numbers"]  3(3)  by simp
+  have even_odd_simp: " T_\<^sub>e\<^sub>o b (x # y # numbers) = (2::nat)^l + 1" for b
+    by (metis "3.prems" T_eo_linear)+
+  have 02: "(length fntt2) =  (length [0..<nn div 2])" unfolding fntt2_def 
+    apply(subst FNTT_length[of _ "l-1"])
+    unfolding nums2_def
+    using length_nums2 nums2_def apply fastforce 
+    by (simp add: evens_odds_length nn_def)
+  have 03: "(length fntt1) =  (length [0..<nn div 2])" unfolding fntt1_def 
+    apply(subst FNTT_length[of _ "l-1"])
+    unfolding nums1_def
+    using length_nums1 nums1_def apply fastforce
+    by (metis "02" FNTT_length fntt2_def length_nums1 length_nums2 nums1_def)
+  have map21_simp: "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] = (2::nat)^l + 1"
+    apply(subst T_map_2_linear'[of 1])
+    subgoal by simp subgoal by simp 
+    by (smt (z3) "02" "3"(3) FNTT_length div_less evens_odds_length fntt2_def length_nums2 lessI less_numeral_extra(3) min.idem mult.commute nat_1_add_1 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_power2)
+  have map22_simp: "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) =
+        (2::nat)^l + 1"
+    apply(subst T_map_2_linear'[of 1])
+    subgoal by simp subgoal by simp apply simp
+    unfolding fntt1_def fntt2_def unfolding nn_def
+    apply(subst FNTT_length[of _ "l-1"], (rule length_nums1)?, (rule length_nums2)?,
+                 (subst length_nums1)?,  (subst length_nums2)?,  (subst 3(3))?)+
+    apply (metis (no_types, lifting) "3"(3) div_less evens_odds_length length_nums2 lessI min_def mult_2 nat_1_add_1 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_neq_numeral)
+    done
+  have sum1_simp: "length sum1 = 2^(l-1)"
+    unfolding sum1_def
+    apply(subst map2_length)+
+    apply(subst 02, subst 03) 
+    unfolding nn_def using 3(3)
+    by (metis "02" FNTT_length fntt2_def length_nums2 min.idem nn_def)
+  have app_simp: "T\<^sub>a\<^sub>p\<^sub>p sum1 sum2 = (2::nat)^(l-1) + 1"
+    by(subst T_app_linear, subst sum1_simp, simp)
+  let ?T1 = "(2^(l-1) - 1) * 14 + (l-1) *15*2^(l-1 -1) + 2^(l-1)"
+
+  text \<open>Induction hypotheses\<close>
+
+  have IH_pluged1: "local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 = ?T1"
+     apply(subst "3.IH"(1)[of nn nums1 nums2 fntt1 fntt2 "l-1", 
+                            OF nn_def nums1_def nums2_def fntt1_def fntt2_def length_nums1])
+     apply(cases "l \<le> 1")
+    subgoal
+      apply(subst T_def(2)[of "l-1"])
+      subgoal by simp
+       apply(rule length_nums1)
+      apply simp
+      done      
+     apply(subst T_def(1)[OF length_nums1])
+    subgoal by simp
+    subgoal by simp
+    done
+
+    have IH_pluged2: "local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 = ?T1"
+     apply(subst "3.IH"(2)[of nn nums1 _ fntt1 fntt2 "l-1", OF nn_def nums1_def nums2_def fntt1_def
+                           fntt2_def length_nums2 ])
+     apply(cases "l \<le> 1")
+    subgoal
+      apply(subst T_def(2)[of "l-1"])
+      subgoal by simp
+       apply(rule length_nums2)
+      apply simp
+      done      
+     apply(subst T_def(1)[OF length_nums2])
+    subgoal by simp
+    subgoal by simp
+    done
+    
+  have " T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) =    
+        14 + (3 * 2 ^ l + (local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 +
+        (local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2^(l-1) + 4 * (2 ^ l div 2)))))"
+    apply(subst TFNNT_simp, subst map21_simp, subst map22_simp, subst  length_simp,
+          subst app_simp, subst even_odd_simp, subst even_odd_simp)
+    apply(auto simp add: algebra_simps power_eq_if[of 2 l])
+    done
+
+  text \<open>Proof that the term $T\text{-}def$ indeed fulfills the recursive properties, i.e.
+          $t(2^l) = 2 \cdot t(2^{l-1}) + s$\<close>
+
+  also have "\<dots> = 14 + (3 * 2 ^ l + (?T1 + (?T1 + (5 * 2^(l-1) + 4 * (2 ^ l div 2)))))" 
+    apply(subst IH_pluged1, subst IH_pluged2) 
+    by simp
+  also have "\<dots> =  14 + (6 * 2 ^ (l-1) +
+          2*((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) +
+       (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))"
+    by (smt (verit) "3"(3) add.assoc div_less evens_odds_length left_add_twice length_nums2 lessI mult.assoc mult_2_right nat_1_add_1 numeral_Bit0 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_neq_numeral)
+  also have "\<dots> =  14 +  15 * 2 ^ (l-1) +
+     2*((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1))" 
+    by (smt (z3) "3"(3) add.assoc add.commute calculation diff_diff_left distrib_left div2_Suc_Suc evens_odds_length left_add_twice length_Cons length_nums2 mult.assoc mult.commute mult_2 mult_2_right numeral_Bit0 numeral_Bit1 numeral_plus_numeral nums2_def one_add_one)
+  also have "... = 14 + 15 * 2 ^ (l-1) +
+                    (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l"
+    apply(cases "l > 1")
+    apply (smt (verit, del_insts) add.assoc diff_is_0_eq distrib_left_numeral left_diff_distrib' less_imp_le_nat mult.assoc mult_2 mult_2_right nat_1_add_1 not_le not_one_le_zero power_eq_if)
+    by (smt (z3) "3"(3) add.commute add.right_neutral cancel_comm_monoid_add_class.diff_cancel diff_add_inverse2 diff_is_0_eq div_less_dividend evens_odds_length length_nums2 mult_2 mult_eq_0_iff nat_1_add_1 not_le nums2_def power_eq_if)
+  also have "\<dots> =  15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l"
+    by (smt (z3) "3"(3) One_nat_def add.commute combine_common_factor diff_add_inverse2 diff_diff_left list.size(4) nat_1_add_1 nat_mult_1)
+  also have "\<dots> = (2^l - 1) * 14 + l *15*2^(l-1) + 2^l" 
+    apply(cases "l > 0")
+    subgoal using group_cancel.add1 group_cancel.add2 less_numeral_extra(3) mult.assoc mult_eq_if by auto[1]
+    using "3"(3) by fastforce
+
+  text \<open>By the previous proposition, we can conclude that $T$ is indeed a suitable term for describing the running time\<close>
+
+  finally have "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)"
+    using T_def(1)[of "x#y#numbers" l] 
+    by (metis "3.prems" bits_1_div_2 diff_is_0_eq' evens_odds_length length_nums2 neq0_conv nums2_def power_0 zero_le_one zero_neq_one)
+  thus ?case by simp
+qed (auto simp add: assms)
+
+text \<open>We can finally state that $FNTT$ has $\mathcal{O}(n \log n)$ time complexity.\<close>
+
+theorem log_lin_time:
+  assumes "length numbers = 2^l"
+  shows "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers \<le> 30 * l * length numbers + 1"
+proof-
+  have 00: "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers  = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l"
+    using tight_bound[of "\<lambda> xs. (length xs - 1) * 14 + (Discrete.log (length xs)) * 15 * 
+                            2 ^ ( (Discrete.log (length xs)) - 1) + length xs" numbers l] 
+          assms by simp
+  have " l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers" using assms by simp
+  moreover have "(2 ^ l - 1) * 14  + 2^l\<le> 15 * length numbers " 
+    using assms by linarith
+  moreover hence "(2 ^ l - 1) * 14 + 2^l \<le> 15 * l * length numbers +1"  using assms 
+    apply(cases l)
+    subgoal by simp 
+    by (metis (no_types) add.commute le_add1 mult.assoc mult.commute
+          mult_le_mono nat_mult_1 plus_1_eq_Suc trans_le_add2)
+  ultimately have " (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le>  30 * l * length numbers +1"
+    by linarith
+  then show  ?thesis using 00 by simp
+qed
+
+theorem log_lin_time_explicitly:
+  assumes "length numbers = 2^l"
+  shows "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers \<le> 30 * Discrete.log (length numbers) * length numbers + 1"
+  using log_lin_time[of numbers l] assms by simp
+
+end
+end
diff --git a/thys/Number_Theoretic_Transform/NTT.thy b/thys/Number_Theoretic_Transform/NTT.thy
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/NTT.thy
@@ -0,0 +1,472 @@
+(*
+Title: Number Theoretic Transform
+Author: Thomas Ammer
+*)
+
+theory NTT
+  imports Preliminary_Lemmas
+begin
+
+section \<open>Number Theoretic Transform and Inverse Transform\<close>
+text \<open>\label{NTT}\<close>
+
+locale ntt = preliminary "TYPE ('a ::prime_card)" +
+fixes \<omega> :: "('a::prime_card mod_ring)"
+fixes \<mu> :: "('a mod_ring)"
+assumes omega_properties: "\<omega>^n = 1" "\<omega> \<noteq> 1" "(\<forall> m. \<omega>^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n)"
+assumes mu_properties: "\<mu> * \<omega> = 1"
+begin
+
+lemma mu_properties': "\<mu> \<noteq> 1"
+  using omega_properties mu_properties by auto
+
+subsection \<open>Definition of $NTT$ and $INTT$\<close>
+text \<open>\label{NTTdef}\<close>
+
+text \<open>
+Now we can state an analogue to the $DFT$ on finite fields, 
+namely the \textit{Number Theoretic Transform}.
+First, let us look at an informal definition of $\mathsf{NTT}$~\parencite{ntt_intro}:
+\begin{equation*}
+\mathsf{NTT}(\vec{x}) = 
+\begin{pmatrix}
+ 1 &     1  &        1 &     1    &  \cdots&           1 \\
+ 1 & \omega   & \omega^2 & \omega^3 & \cdots & \omega^{n-1} \\
+ 1 & \omega^2 & \omega^4 & \omega^6 & \cdots & \omega^{2\cdot(n-1)} \\
+ 1 & \omega^3 & \omega^6 & \omega^9 & \cdots & \omega^{3\cdot(n-1)} \\
+\vdots &  \vdots &  \vdots &  \vdots  &        &      \vdots          \\
+ 1 & \omega^{n-1} & \omega^{2\cdot(n-1)} & \omega^{3\cdot(n-1)} & \cdots & \omega^{(n-1)\cdot(n-1)} 
+\end{pmatrix} \cdot \vec{x}
+\end{equation*}
+
+Or for single vector entries:
+\begin{equation*}
+\mathsf{NTT}(\vec{x})_i = \sum _{j = 0} ^{n-1} x_j \cdot \omega ^{i\cdot j} 
+\end{equation*}
+
+\<close>
+
+text \<open>Formally:\<close>
+
+definition ntt::"(('a ::prime_card) mod_ring) list \<Rightarrow> nat \<Rightarrow> 'a mod_ring" where
+"ntt numbers i = (\<Sum>j=0..<n. (numbers ! j) * \<omega>^(i*j)) "
+
+definition "NTT numbers = map (ntt numbers) [0..<n]"
+
+
+text \<open>\label{INTTdef}
+We define the inverse transform $\mathsf{INTT}$ by matrices:
+\begin{equation*}
+ \mathsf{INTT}(\vec{y}) = 
+\begin{pmatrix}
+ 1 &     1  &        1 &     1    &  \cdots&           1 \\
+ 1 & \mu   & \mu^2 & \mu^3 & \cdots & \mu^{n-1} \\
+ 1 & \mu^2 & \mu^4 & \mu^6 & \cdots & \mu^{2\cdot(n-1)} \\
+ 1 & \mu^3 & \mu^6 & \mu^9 & \cdots & \mu^{3\cdot(n-1)} \\
+\vdots &  \vdots &  \vdots &  \vdots  &        &      \vdots          \\
+ 1 & \mu^{n-1} & \mu^{2\cdot(n-1)} & \mu^{3\cdot(n-1)} & \cdots & \mu^{(n-1)\cdot(n-1)} 
+\end{pmatrix} \cdot \vec{y}
+\end{equation*}
+Per component: 
+\begin{equation*}
+%
+\mathsf{INTT}(\vec{y})_i = \sum _{j = 0} ^{n-1} y_j \cdot \mu ^{i\cdot j} 
+%
+\end{equation*}
+
+\<close>
+
+definition "intt xs i = (\<Sum>j=0..<n. (xs ! j) * \<mu>^(i*j)) "
+
+definition "INTT xs = map (intt xs) [0..<n]"
+
+text \<open>Vector length is preserved.\<close>
+
+lemma length_NTT:
+  assumes n_def: "length numbers = n"
+  shows "length (NTT numbers) = n"
+  unfolding NTT_def ntt_def using n_def length_map[of _ "[0..<n]"]
+  by simp
+
+lemma length_INTT:
+  assumes n_def: "length numbers = n"
+  shows "length (INTT numbers) = n"
+  unfolding INTT_def intt_def using n_def length_map[of _ "[0..<n]"]
+  by simp
+
+subsection \<open>Correctness Proof of $NTT$ and $INTT$\<close>
+text \<open>\label{NTTcorr}\<close>
+text \<open>
+We prove $\mathsf{NTT}$ and $\mathsf{INTT}$ correct:
+By taking $\mathsf{INTT}(\mathsf{NTT} (x))$ we obtain $x$ scaled by $n$.
+Analogue to $DFT$, one can get rid of the factor $n$ by a simple rescaling.
+First, consider an informal proof sketch using the matrix form:
+\begin{equation*}
+\begin{split}
+\mathsf{INTT}(\mathsf{NTT}(\vec{x})) = \hspace{11cm}\\
+%
+\begin{pmatrix}
+ 1 &     1  &            1    &  \cdots&           1 \\
+ 1 & \mu   & \mu^2 &  \cdots & \mu^{n-1} \\
+ 1 & \mu^2 & \mu^4 &  \cdots & \mu^{2\cdot(n-1)} \\
+\vdots &  \vdots &    \vdots  &        &      \vdots          \\
+ 1 & \mu^{n-1} & \mu^{2\cdot(n-1)}& \cdots & \mu^{(n-1)\cdot(n-1)} 
+\end{pmatrix}
+%
+\cdot
+%
+\begin{pmatrix}
+ 1 &     1  &        1 &  \cdots&           1 \\
+ 1 & \omega   & \omega^2 & \cdots & \omega^{n-1} \\
+ 1 & \omega^2 & \omega^4  & \cdots & \omega^{2\cdot(n-1)} \\
+\vdots &  \vdots &  \vdots  &        &      \vdots          \\
+ 1 & \omega^{n-1} & \omega^{2\cdot(n-1)} & \cdots & \omega^{(n-1)\cdot(n-1)} 
+\end{pmatrix} 
+\cdot
+%
+\vec{x}
+%
+\end{split}
+\end{equation*}
+
+A resulting entry is of the following form:
+
+\begin{equation*}
+%
+\mathsf{INTT}(\mathsf{NTT}(x))_i = \sum _ {j = 0} ^{n-1} (\sum _{k = 0} ^{n-1} \mu^{i\cdot k} \cdot \omega^{j\cdot k}) \cdot x_j
+%
+\end{equation*}
+
+Now, we analyze the interior sum by cases on $i = j$.
+
+\paragraph \noindent Case $i = j$.
+\begin{align*}
+\sum _{k = 0} ^{n-1} \mu^{i\cdot k} \cdot \omega^{j\cdot k}
+&= \sum _{k = 0} ^{n-1} (\mu \cdot \omega)^{i \cdot k} \\
+&= n \cdot (\mu \cdot \omega)^{i \cdot k} \\
+&=  n \cdot 1 ^{i \cdot k} \\ &= n
+\end{align*}
+Note that $\omega$ and $\mu$ are mutually inverse.
+\paragraph \noindent Case $i \neq j$. Wlog assume $i > j$, otherwise replace $\omega$ by $\mu$ and $i -j$ by $j - i$ respectively.
+\begin{align*}
+\sum _{k = 0} ^{n-1} \mu^{i\cdot k} \cdot \omega^{j\cdot k}
+&= \sum _{k = 0} ^{n-1} (\mu \cdot \omega)^{j \cdot k} \cdot \omega^{(i-j) \cdot k} \\
+&= \sum _{k = 0} ^{n-1} \omega^{(i-j) \cdot k} \\
+&=  (1 - \omega ^{(i-j)\cdot n}) \cdot (1 - \omega^{i-j})^{-1} && \text{by lemma on geometric sum}\\
+&=  (1 - 1^n) \cdot (1 - \omega^{i-j})^{-1} \\
+&= 0
+\end{align*}
+
+We conclude that $\sum \limits _ {j = 0} ^{n-1} (\sum \limits _{k = 0} ^{n-1} \mu^{i\cdot k} \cdot \omega^{j\cdot k}) \cdot x_j = n \cdot x_i$.
+
+\<close>
+
+theorem ntt_correct: 
+  assumes n_def: "length numbers = n"
+  shows "INTT (NTT numbers) = map (\<lambda> x. (of_int_mod_ring n) * x ) numbers"
+proof-
+  have 0:"\<And> i. i < n \<Longrightarrow> (INTT (NTT numbers)) ! i = intt (NTT numbers) i " using n_def length_NTT
+    unfolding INTT_def NTT_def intt_def by simp
+
+  text \<open>Major sublemma.\<close>
+
+  have 1:"\<And> i. i < n \<Longrightarrow>intt (NTT numbers) i = (of_int_mod_ring n)*numbers ! i"
+  proof-
+    fix i
+    assume i_assms:"i < n"
+
+    text \<open>First, simplify by some chains of equations.\<close>
+
+    hence 1:"intt (NTT numbers) i  =
+            (\<Sum>l = 0..<n. 
+              (\<Sum>j = 0..<n. numbers ! j * \<omega> ^ (l * j)) * \<mu> ^ (i * l))" 
+      unfolding NTT_def intt_def ntt_def using n_def length_map nth_map by simp
+    also have 2:"\<dots> =
+            (\<Sum>l = 0..<n. 
+              (\<Sum>j = 0..<n. (numbers ! j * \<omega> ^ (l * j)) * \<mu> ^ (i * l)))"
+      using sum_in by (simp add: sum_distrib_right) 
+    also have 3:"\<dots> =
+            (\<Sum>j = 0..<n. 
+              (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))))" using sum_swap by fast
+
+    text \<open>As in the informal proof, we consider three cases. First $j = i$.\<close>
+
+    have iisj:"\<And> j. j = i \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = (numbers ! j)* (of_int_mod_ring n)"
+    proof-
+      fix j
+      assume "j=i"
+      hence "\<And> l. l < n \<Longrightarrow> (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))= (numbers ! j)"
+        by (simp add: left_right_inverse_power mult.commute mu_properties(1))
+      moreover have "\<And> l. l < n  \<Longrightarrow> numbers ! j *  \<omega> ^ (l * j) * \<mu> ^ (i * l) = numbers ! j" 
+        using calculation by blast
+
+      text \<open>$\omega^{il}\cdot \omega^{jl} = 1$. Thus, we sum over $1$ $n$ times, which gives the goal.\<close>
+
+      ultimately show "(\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = 
+        (numbers ! j)* (of_int_mod_ring n)" 
+        using n_def sum_const[of "numbers ! j" n] exp_rule[of \<omega> \<mu>] mu_properties(1) 
+        by (metis (no_types, lifting) atLeastLessThan_iff mult.commute sum.cong) 
+
+    qed
+
+    text \<open>Case $j < i$.\<close>
+
+    have jlsi:"\<And> j. j < i \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = 0"
+    proof-
+      fix j
+      assume j_assms:"j < i"
+      hence 00:"\<And>  (c::('a::prime_card) mod_ring) a b. c * a^j*b^i  = (a*b)^j*(c * b^(i-j))" 
+         using  algebra_simps 
+         by (smt (z3) le_less ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add)
+
+       text \<open>A geometric sum over $\mu^l$ remains.\<close>
+
+      have 01:" (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = 
+                (\<Sum>l = 0..<n. (numbers ! j *  (\<mu>^l)^(i-j)))" 
+           apply(rule sum_eq)
+           using mu_properties(1) 00 algebra_simps(23)
+           by (smt (z3) mult.commute mult.left_neutral power_mult power_one)
+      have 02:"\<dots> = numbers ! j *(\<Sum>l = 0..<n. ((\<mu>^l)^(i-j))) " 
+           using sum_in[of "\<lambda> l. numbers ! j * (\<mu> ^ l) ^ (i - j)" " numbers ! j" n] 
+           by (simp add: mult_hom.hom_sum)
+      moreover have 03:"(\<Sum>l = 0..<n. ((\<mu>^l)^(i-j))) = 
+                     (\<Sum>l = 0..<n. ((\<mu>^(i-j))^l)) "
+        by(rule sum_eq) (metis mult.commute power_mult)
+      have "\<mu>^(i-j) \<noteq> 1" 
+      proof
+        assume "\<mu> ^ (i - j) = 1"
+        hence "ord p (to_int_mod_ring \<mu>) \<le> i-j" 
+          by (simp add: j_assms not_le ord_max)
+        moreover hence "ord p (to_int_mod_ring \<omega>) \<le> i-j" 
+          by (metis \<open>\<mu> ^ (i - j) = 1\<close> diff_is_0_eq exp_rule j_assms leD mult.comm_neutral mult.commute mu_properties(1) ord_max)
+        moreover hence "i-j < n" 
+          using j_assms i_assms p_fact k_bound n_lst2 by linarith
+        moreover have "ord p (to_int_mod_ring \<omega>) = n" using omega_properties n_lst2 unfolding ord_def          
+          by (metis (no_types) \<open>\<mu> ^ (i - j) = 1\<close> calculation(3) diff_is_0_eq j_assms leD left_right_inverse_power mult.comm_neutral mult_cancel_left mu_properties(1) omega_properties(3) zero_neq_one)
+        ultimately show False by simp
+      qed
+
+      text \<open>Application of the lemma for geometric sums.\<close>
+
+      ultimately have "(1-\<mu>^(i-j))*(\<Sum>l = 0..<n. ((\<mu>^(i-j))^l)) = (1-(\<mu>^(i-j))^n)" 
+        using geo_sum[of "\<mu> ^ (i - j)" n] by simp
+      moreover have "(\<mu>^(i-j))^n = 1"
+        by (metis (no_types) left_right_inverse_power mult.commute mult.right_neutral mu_properties(1) omega_properties(1) power_mult power_one)
+
+      text \<open>The sum for the current index is 0.\<close>
+      
+      ultimately have "(\<Sum>l = 0..<n. ((\<mu>^(i-j))^l)) = 0"
+        by (metis \<open>\<mu> ^ (i - j) \<noteq> 1\<close> divisors_zero eq_iff_diff_eq_0)
+      thus "(\<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) = 0" using  01 02 03 by simp
+    qed
+
+    text \<open>Case $i < j$. 
+       We also rewrite the whole summation until the lemma for geometric sums is applicable.
+       From this, we conclude that the term is 0.\<close>
+
+    have ilsj:"\<And> j. i < j \<and> j < n \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = 0"
+    proof-
+      fix j
+      assume ij_Assm: "i < j \<and> j < n"
+      hence 00:"\<And>  (c::('a::prime_card) mod_ring) a b. (a*b)^i*(c * b^(j-i)) = c * a^i*b^j  " 
+        by (auto simp: field_simps simp flip: power_add)
+      have 01:" (\<Sum>l = 0..<n. (numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l))) = 
+                (\<Sum>l = 0..<n. (numbers ! j *  (\<omega>^l)^(j-i))) " 
+           apply(rule sum_eq) subgoal for l
+           using mu_properties(1) 00[of "\<omega>^l" "\<mu>^l" "numbers ! j "] algebra_simps(23) 
+           by (smt (z3) "00" left_right_inverse_power mult.assoc mult.commute mult.right_neutral power_mult)
+         done
+      moreover have 02:"(\<Sum>l = 0..<n. (numbers ! j *   (\<omega>^l)^(j-i)))  = 
+                         numbers ! j *(\<Sum>l = 0..<n. ( (\<omega>^l)^(j-i))) " 
+        by (simp add: mult_hom.hom_sum)
+      moreover have 03:"(\<Sum>l = 0..<n. ( (\<omega>^l)^(j-i))) = 
+                     (\<Sum>l = 0..<n. (( (\<omega>^(j-i))^l))) "
+        by(rule sum_eq) (metis mult.commute power_mult)
+      have "\<omega>^(j-i) \<noteq> 1"
+      proof
+        assume " \<omega> ^ (j - i) = 1"
+        hence "ord p (to_int_mod_ring  \<omega>) \<le> j-i" using ord_max[of "j-i" \<omega>] ij_Assm by simp
+        moreover have "ord p (to_int_mod_ring \<omega>) =p-1" 
+          by (meson \<open>\<omega> ^ (j - i) = 1\<close> diff_is_0_eq diff_le_self ij_Assm leD le_trans omega_properties(3))
+        ultimately show False 
+          by (meson \<open>\<omega> ^ (j - i) = 1\<close> diff_is_0_eq diff_le_self ij_Assm leD le_trans omega_properties(3))
+      qed
+
+      text \<open>Geometric sum.\<close>
+
+      ultimately have "(1-\<omega>^(j-i))* (\<Sum>l = 0..<n. ((\<omega>^(j-i))^l)) = (1-(\<omega>^(j-i))^n)" 
+        using geo_sum[of "\<omega> ^ (j-i)" n] by simp
+      moreover have "(\<omega>^(j-i))^n = 1"
+        by (metis (no_types) mult.commute  omega_properties(1) power_mult power_one)
+      ultimately have "(\<Sum>l = 0..<n. ((\<omega>^(j-i))^l)) = 0"
+        by (metis \<open>\<omega> ^ (j - i) \<noteq> 1\<close> eq_iff_diff_eq_0 no_zero_divisors)
+      thus "(\<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) = 0" using  01 02 03 by simp
+    qed
+
+    text \<open>We compose the cases $j <i$, $j = i$ and $j > i$ to a complete summation over index $j$.\<close>
+
+    have " (\<Sum>j = 0..<i. \<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) = 0" using jlsi by simp
+    moreover have " (\<Sum>j = i..<i+1. \<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) =  numbers ! i * (of_int_mod_ring n)" using iisj by simp
+    moreover have " (\<Sum>j = (i+1)..<n. \<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) = 0" using ilsj by simp
+    ultimately have " (\<Sum>j = 0..<n. \<Sum>l = 0..<n. numbers ! j * \<omega> ^ (l * j) * \<mu> ^ (i * l)) =
+                        numbers ! i * (of_int_mod_ring n)" using i_assms sum_split 
+      by (smt (z3) add.commute add.left_neutral int_ops(2) less_imp_of_nat_less of_nat_add of_nat_eq_iff of_nat_less_imp_less)
+    
+    text \<open>Index-wise equality can be shown.\<close>
+    
+    thus "intt (NTT numbers) i = of_int_mod_ring (int n) * numbers ! i" using 1 2 3
+      by (metis mult.commute)
+  qed
+  have 2: "\<And> i. i < n \<Longrightarrow> (map ((*) (of_int_mod_ring (int n))) numbers ) ! i = (of_int_mod_ring (int n)) * (numbers ! i)"
+    by (simp add: n_def)
+
+  text \<open>We relate index-wise equality to the function definition.\<close>
+
+   show ?thesis
+     apply(rule nth_equalityI)
+     subgoal my_subgoal
+       unfolding INTT_def NTT_def 
+       apply (simp add: n_def)
+       done
+     subgoal for i
+     using 0 1 2 n_def algebra_simps my_subgoal length_map 
+     apply  auto
+     done
+   done
+qed
+
+text \<open>Now we prove the converse to be true:
+$\mathsf{NTT}(\mathsf{INTT}(\vec{x})) = n \cdot \vec{x}$. 
+The proof proceeds analogously with exchanged roles of $\omega$ and $\mu$.
+\<close>
+
+theorem inv_ntt_correct: 
+  assumes n_def: "length numbers = n"
+  shows "NTT (INTT numbers) = map (\<lambda> x. (of_int_mod_ring n) * x ) numbers"
+proof-
+  have 0:"\<And> i. i < n \<Longrightarrow> (NTT (INTT numbers)) ! i = ntt (INTT numbers) i " using n_def length_NTT
+    unfolding INTT_def NTT_def intt_def by simp
+  have 1:"\<And> i. i < n \<Longrightarrow>ntt (INTT numbers) i = (of_int_mod_ring n)*numbers ! i"
+  proof-
+    fix i
+    assume i_assms:"i < n"
+    hence 1:"ntt (INTT numbers) i  =
+            (\<Sum>l = 0..<n. 
+               (\<Sum>j = 0..<n. numbers ! j * \<mu> ^ (l * j)) * \<omega> ^ (i * l))" 
+      unfolding INTT_def ntt_def intt_def using n_def length_map nth_map by simp
+    hence 2:"\<dots> = (\<Sum>l = 0..<n. 
+                     (\<Sum>j = 0..<n. (numbers ! j * \<mu> ^ (l * j)) * \<omega> ^ (i * l)))" using sum_in by simp
+    have 3:" \<dots> =(\<Sum>j = 0..<n. 
+                  (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))))" using sum_swap by fast
+    have iisj:"\<And> j. j = i \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = (numbers ! j)* (of_int_mod_ring n)"
+    proof-
+      fix j
+      assume "j=i"
+      hence "\<And> l. l < n \<Longrightarrow> (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))= (numbers ! j)"
+        by (simp add: left_right_inverse_power mult.commute mu_properties(1))
+      moreover have "\<And> l. l < n  \<Longrightarrow> numbers ! j *  \<mu> ^ (l * j) * \<omega> ^ (i * l) = numbers ! j" 
+        using calculation by blast
+      ultimately show "(\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = (numbers ! j)* (of_int_mod_ring n)" 
+        using n_def sum_const[of "numbers ! j" n] exp_rule[of \<omega> \<mu>] mu_properties(1) 
+        by (metis (no_types, lifting) atLeastLessThan_iff mult.commute sum.cong) 
+    qed
+    have jlsi:"\<And> j. j < i \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = 0"
+    proof-
+      fix j
+      assume j_assms:"j < i"
+      hence 00:"\<And>  (c::('a::prime_card) mod_ring) a b. c * a^j*b^i  = (a*b)^j*(c * b^(i-j))" 
+         using  algebra_simps 
+         by (smt (z3) le_less ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add)
+      have 01:" (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = 
+                (\<Sum>l = 0..<n. (numbers ! j *  (\<omega>^l)^(i-j))) " 
+           apply(rule sum_eq)
+           using mu_properties(1) 00 algebra_simps(23)
+           by (smt (z3) mult.commute mult.left_neutral power_mult power_one)
+      moreover have 02: "\<dots>=  numbers ! j *(\<Sum>l = 0..<n. ((\<omega>^l)^(i-j))) "
+           using sum_in[of "\<lambda> l. numbers ! j * (\<mu> ^ l) ^ (i - j)" " numbers ! j" n] 
+        by (simp add: mult_hom.hom_sum)
+      moreover have 03:"(\<Sum>l = 0..<n. ((\<omega>^l)^(i-j))) = 
+                     (\<Sum>l = 0..<n. ((\<omega>^(i-j))^l)) "
+        by(rule sum_eq) (metis mult.commute power_mult)
+      have "\<omega>^(i-j) \<noteq> 1" 
+      proof
+        assume "\<omega> ^ (i - j) = 1"
+        hence "ord p (to_int_mod_ring \<omega>) \<le> i-j" 
+          by (simp add: j_assms not_le ord_max)
+         moreover have "ord p (to_int_mod_ring \<omega>) = n" using omega_properties n_lst2 unfolding ord_def
+           by (meson \<open>\<omega> ^ (i - j) = 1\<close> diff_is_0_eq diff_le_self i_assms j_assms leD le_trans)
+         ultimately show False 
+           by (metis i_assms leD less_imp_diff_less)
+      qed
+      ultimately have "(1-\<omega>^(i-j))*(\<Sum>l = 0..<n. ((\<omega>^(i-j))^l)) = (1-(\<omega>^(i-j))^n)" 
+        using geo_sum[of "\<omega> ^ (i - j)" n] by simp
+      moreover have "(\<omega>^(i-j))^n = 1"
+        by (metis (no_types)  mult.commute omega_properties(1) power_mult power_one)
+      ultimately have "(\<Sum>l = 0..<n. ((\<omega>^(i-j))^l)) = 0" 
+        by (metis \<open>\<omega> ^ (i - j) \<noteq> 1\<close> divisors_zero eq_iff_diff_eq_0)
+      thus "(\<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) = 0" using  01 02 03 by simp
+    qed
+    have ilsj:"\<And> j. i < j \<and> j < n \<Longrightarrow> (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = 0"
+    proof-
+      fix j
+      assume ij_Assm: "i < j \<and> j < n"
+      hence 00:"\<And>  (c::('a::prime_card) mod_ring) a b. (a*b)^i*(c * b^(j-i)) = c * a^i*b^j  " 
+        by (simp add: field_simps flip: power_add)
+      have 01:" (\<Sum>l = 0..<n. (numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l))) = 
+                (\<Sum>l = 0..<n. (numbers ! j *  (\<mu>^l)^(j-i))) " 
+           apply(rule sum_eq) subgoal for l
+           using mu_properties(1) 00[of "\<omega>^l" "\<mu>^l" "numbers ! j "] algebra_simps(23) 
+           by (smt (z3) "00" left_right_inverse_power mult.assoc mult.commute mult.right_neutral power_mult)
+         done
+      moreover have 02:"(\<Sum>l = 0..<n. (numbers ! j *   (\<mu>^l)^(j-i)))  = 
+            numbers ! j *(\<Sum>l = 0..<n. ( (\<mu>^l)^(j-i))) " 
+        by (simp add: mult_hom.hom_sum)
+      moreover have 03:"(\<Sum>l = 0..<n. ( (\<mu>^l)^(j-i))) = 
+                     (\<Sum>l = 0..<n. (( (\<mu>^(j-i))^l))) "
+        by(rule sum_eq) (metis mult.commute power_mult)
+      have "\<mu>^(j-i) \<noteq> 1"
+       proof
+        assume "\<mu> ^ (j - i) = 1"
+        hence "ord p (to_int_mod_ring \<mu>) \<le> j -i " 
+          by (simp add: ij_Assm not_le ord_max)
+        moreover hence "ord p (to_int_mod_ring \<omega>) \<le> j-i" 
+          by (metis \<open>\<mu> ^ (j - i) = 1\<close> diff_is_0_eq exp_rule ij_Assm leD mult.comm_neutral mult.commute mu_properties(1) ord_max)
+        moreover hence "j-i < n" using ij_Assm i_assms p_fact k_bound n_lst2 by linarith
+        moreover have "ord p (to_int_mod_ring \<omega>) = n" using omega_properties n_lst2 unfolding ord_def
+          by (metis (no_types) \<open>\<mu> ^ (j-i) = 1\<close> calculation(3) diff_is_0_eq ij_Assm leD left_right_inverse_power mult.comm_neutral mult_cancel_left mu_properties(1) omega_properties(3) zero_neq_one)
+        ultimately show False by simp
+      qed
+      ultimately have "(1-\<mu>^(j-i))* (\<Sum>l = 0..<n. ((\<mu>^(j-i))^l)) = (1-(\<mu>^(j-i))^n)" 
+        using geo_sum[of "\<mu> ^ (j-i)" n] by simp
+      moreover have "(\<mu>^(j-i))^n = 1"
+        by (metis (no_types) left_right_inverse_power mult.commute mult.right_neutral mu_properties(1) omega_properties(1) power_mult power_one)
+      ultimately have "(\<Sum>l = 0..<n. ((\<mu>^(j-i))^l)) = 0"
+        by (metis \<open>\<mu> ^ (j - i) \<noteq> 1\<close> eq_iff_diff_eq_0 no_zero_divisors)
+      thus "(\<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) = 0" using  01 02 03 by simp
+    qed
+    have " (\<Sum>j = 0..<i. \<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) = 0" using jlsi by simp
+    moreover have " (\<Sum>j = i..<i+1. \<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) =  numbers ! i * (of_int_mod_ring n)" using iisj by simp
+    moreover have " (\<Sum>j = (i+1)..<n. \<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) = 0" using ilsj by simp
+    ultimately have " (\<Sum>j = 0..<n. \<Sum>l = 0..<n. numbers ! j * \<mu> ^ (l * j) * \<omega> ^ (i * l)) =
+                        numbers ! i * (of_int_mod_ring n)" using i_assms sum_split 
+      by (smt (z3) add.commute add.left_neutral int_ops(2) less_imp_of_nat_less of_nat_add of_nat_eq_iff of_nat_less_imp_less)
+    thus "ntt (INTT numbers) i = of_int_mod_ring (int n) * numbers ! i" using 1 2 3 
+      by (metis mult.commute)
+  qed
+  have 2: "\<And> i. i < n \<Longrightarrow> (map ((*) (of_int_mod_ring (int n))) numbers ) ! i = (of_int_mod_ring (int n)) * (numbers ! i)"
+     by (simp add: n_def)
+   show ?thesis
+     apply(rule nth_equalityI)
+     subgoal my_little_subgoal
+       unfolding INTT_def NTT_def 
+       apply (simp add: n_def)
+       done
+     subgoal for i
+       using 0 1 2 n_def algebra_simps  my_little_subgoal length_map 
+       apply  auto
+     done
+   done
+qed
+
+end
+end
diff --git a/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy b/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy
@@ -0,0 +1,453 @@
+(*
+Title: Preliminary Lemmas for Number Theoretic Transform
+Author: Thomas Ammer
+*)
+
+theory Preliminary_Lemmas
+ imports Berlekamp_Zassenhaus.Finite_Field 
+         "HOL-Number_Theory.Number_Theory"
+begin
+
+section \<open>Preliminary Lemmas\<close>
+
+subsection \<open>A little bit of Modular Arithmetic\<close>
+
+text \<open>An obvious lemma. Just for simplification.\<close>
+
+lemma two_powrs_div:
+  assumes "j < (i::nat) "
+  shows "((2^i) div ((2::nat)^(Suc j)))*2 =  ((2^i) div (2^j))"
+proof-
+  have "((2::nat)^i) div (2^(Suc j)) = 2^(i -1) div(2^ j)" using assms 
+    by (smt (z3) One_nat_def add_le_cancel_left diff_Suc_Suc div_by_Suc_0 div_if less_nat_zero_code plus_1_eq_Suc power_diff_power_eq zero_neq_numeral)
+  thus ?thesis 
+    by (metis Suc_diff_Suc Suc_leI assms less_imp_le_nat mult.commute power_Suc power_diff_power_eq zero_neq_numeral)
+qed
+
+lemma two_powr_div:
+  assumes "j < (i::nat) "
+  shows "((2^i) div ((2::nat)^j)) =  2^(i-j)" 
+  by (simp add: assms less_or_eq_imp_le power_diff)
+
+
+text \<open>
+  The order of an element is the same whether we consider it as an integer or as a natural number.
+\<close>
+(* TODO: Move *)
+lemma ord_int: "ord (int p) (int x) = ord p x"
+proof (cases "coprime p x")
+  case False
+  thus ?thesis
+    by (auto simp: ord_def)
+next
+  case True
+  have "(LEAST d. 0 < d \<and> [int x ^ d = 1] (mod int p)) = ord p x"
+  proof (intro Least_equality conjI)
+    show "[int x ^ ord p x = 1] (mod int p)"
+      using True by (metis cong_int_iff of_nat_1 of_nat_power ord_works)
+    show "ord p x \<le> y" if "0 < y \<and> [int x ^ y = 1] (mod int p)" for y
+      using that by (metis cong_int_iff int_ops(2) linorder_not_less of_nat_power ord_minimal)
+  qed (use True in auto)
+  thus ?thesis
+    by (auto simp: ord_def)
+qed
+
+lemma not_residue_primroot_1:
+  assumes "n > 2"
+  shows   "\<not>residue_primroot n 1"
+  using assms totient_gt_1[of n] by (auto simp: residue_primroot_def)
+
+lemma residue_primroot_not_cong_1:
+  assumes "residue_primroot n g" "n > 2"
+  shows   "[g \<noteq> 1] (mod n)"
+  using residue_primroot_cong not_residue_primroot_1 assms by metis  
+
+
+text \<open>
+We want to show the existence of a generating element of $\mathbb{Z}_p$ where $p$ is prime.
+\label{primroot1} \<close>
+
+text \<open>Non-trivial order of an element $g$ modulo $p$ in a ring  implies $g\neq1$.
+Although this lemma applies to all rings, it's only intended to be used in connection with $nat$s or $int$s
+\<close>
+
+lemma prime_not_2_order_not_1:
+  assumes "prime p"
+          "p > 2 "
+          "ord p g > 2"
+  shows   "g \<noteq> 1"
+proof
+  assume "g = 1"
+  hence "ord p g = 1" unfolding ord_def
+    by (simp add: Least_equality)
+  then show False using assms by auto
+qed
+
+text \<open>The same for modular arithmetic.\<close>
+
+lemma prime_not_2_order_not_1_mod:
+ assumes "prime p "
+         "p > 2 "
+         "ord p g > 2"
+ shows   "[g \<noteq> 1] (mod p)"
+proof
+  assume "[g = 1] (mod p)"
+  hence "ord p g = 1" unfolding ord_def
+    by(split if_split, metis assms(1) assms(2) assms(3) ord_cong prime_not_2_order_not_1)
+  then show False using assms by auto
+qed
+
+text \<open>
+Now we formulate our lemma about generating elements in residue classes:
+There is an element $g \in \mathbb{Z}_p$ such that for any $x \in \mathbb{Z}_p$ 
+there is a natural $i$ such that $g^i \equiv x \; (\mod p)$.\<close>
+
+lemma generator_exists:
+  assumes "prime (p::nat)" "p > 2"
+  shows "\<exists> g. [g \<noteq> 1] (mod p) \<and> (\<forall> x. (0<x \<and> x < p )\<longrightarrow> (\<exists> i. [g^i = x] (mod p)))"
+proof-
+  obtain g where g_prim_root:"residue_primroot p g" 
+    using assms prime_gt_1_nat prime_primitive_root_exists
+    by (metis One_nat_def)
+  have g_not_1: "[g \<noteq> 1] (mod p)"
+    using residue_primroot_not_cong_1 assms g_prim_root by blast
+
+  have "\<exists>i. [g ^ i = x] (mod p)" if x_bounds: "x > 0" "x < p" for x
+  proof -
+    have 1:"coprime p x" 
+      using assms prime_nat_iff'' x_bounds by blast
+    have 2:"ord p g = p-1"
+      by (metis assms(1) g_prim_root residue_primroot_def totient_prime)
+    hence bij: "bij_betw (\<lambda>i. g ^ i mod p) {..<totient p} (totatives p)"
+      using residue_primroot_is_generator[of p g] totatives_def[of p] 
+          1 totient_def[of p] assms g_prim_root prime_gt_1_nat by blast
+    have 3:"x mod p \<in> totatives p" 
+      by (simp add: "1" coprime_commute in_totatives_iff order_le_less x_bounds)
+    have " {..<totient p} \<noteq> {}" 
+      by (metis assms(1) lessThan_empty_iff prime_nat_iff'' totient_0_iff)
+   then obtain i where "g^i mod p = x mod p" 
+      using bij_betw_inv[of "(\<lambda>i. g ^ i mod p)" "{..<totient p}" "(totatives p)"] 
+      3 bij 
+      by (metis (no_types, lifting) bij_betw_iff_bijections)
+   then show ?thesis
+     using cong_def by blast
+  qed
+  thus ?thesis
+    using g_prim_root g_not_1 by auto
+qed
+
+subsection \<open>General Lemmas in a Finite Field\<close>
+
+text \<open>
+\label{primroot2}
+We make certain assumptions:
+From now on, we will calculate in a finite field which is the ring of integers modulo a prime $p$.
+Let $n$ be the length of vectors to be transformed. 
+By Dirichlet's theorem on arithmetic progressions we can
+ assume that there is a natural number $k$ and a prime $p$ with $p = k\cdot n + 1$.
+In order to avoid some special cases and even contradictions, 
+we additionally assume that $p \geq 3$ and $n \geq 2$. 
+\<close>
+
+text \<open>\label{prelim}\<close>
+locale preliminary = 
+  fixes
+       a_type::"('a::prime_card) itself" 
+   and p::nat
+   and n::nat 
+   and k::nat
+ assumes
+       p_def: "p= CARD('a)" and p_lst3: "p > 2"  and p_fact: "p = k*n +1"
+   and n_lst2: "n \<ge> 2" 
+begin
+
+lemma exp_rule: "((c::('a) mod_ring) * d )^e= (c^e) * (d^e)" 
+  by (simp add: power_mult_distrib)
+
+lemma "\<exists> y. x \<noteq> 0 \<longrightarrow> (x::(('a) mod_ring)) *  y = 1" 
+  by (metis dvd_field_iff unit_dvdE)
+
+lemma test: "prime p" 
+  by (simp add: p_def prime_card)
+
+lemma k_bound: "k > 0" 
+  using p_fact prime_nat_iff'' test by force
+
+text \<open>We show some homomorphisms.\<close>
+
+lemma homomorphism_add: "(of_int_mod_ring x)+(of_int_mod_ring y) = 
+              ((of_int_mod_ring  (x+y)) ::(('a::prime_card) mod_ring))"
+  by (metis of_int_hom.hom_add of_int_of_int_mod_ring)
+
+lemma homomorphism_mul_on_ring: "(of_int_mod_ring x)*(of_int_mod_ring y) =  
+              ((of_int_mod_ring  (x*y)) ::(('a::prime_card) mod_ring))"
+  by (metis of_int_mult of_int_of_int_mod_ring)
+
+lemma exp_homo:"(of_int_mod_ring (x^i)) = ((of_int_mod_ring x)^i ::(('a::prime_card) mod_ring))"
+  by (induction i) (metis of_int_of_int_mod_ring of_int_power)+
+
+lemma mod_homo: "((of_int_mod_ring x)::(('a::prime_card) mod_ring)) = of_int_mod_ring (x mod p)"
+  using p_def unfolding of_int_mod_ring_def by simp
+
+lemma int_exp_hom: "int x ^i = int (x^i)" 
+  by simp
+
+lemma coprime_nat_int: "coprime (int p) (to_int_mod_ring pr) \<longleftrightarrow> coprime p (nat(to_int_mod_ring pr))"
+  unfolding coprime_def to_int_mod_ring_def 
+  by (smt (z3) Rep_mod_ring atLeastLessThan_iff dvd_trans int_dvd_int_iff int_nat_eq int_ops(2) prime_divisor_exists prime_nat_int_transfer primes_dvd_imp_eq test to_int_mod_ring.rep_eq to_int_mod_ring_def)
+
+lemma nat_int_mod:"[nat (to_int_mod_ring pr) ^ d = 1] (mod p) = 
+                           [ (to_int_mod_ring pr) ^ d = 1] (mod (int p)) "
+  unfolding to_int_mod_ring_def 
+  by (metis Rep_mod_ring atLeastLessThan_iff cong_int_iff int_exp_hom int_nat_eq int_ops(2) to_int_mod_ring.rep_eq to_int_mod_ring_def)
+
+text \<open>Order of $p$ doesn't change when interpreting it as an integer.\<close>
+
+lemma ord_lift: "ord (int p) (to_int_mod_ring pr) = ord p (nat (to_int_mod_ring pr))"
+proof -
+  have "to_int_mod_ring pr = int (nat (to_int_mod_ring pr))"
+    by (metis Rep_mod_ring atLeastLessThan_iff int_nat_eq to_int_mod_ring.rep_eq)
+  thus ?thesis
+    using ord_int by metis
+qed
+
+text \<open>A primitive root has order $p-1$.\<close>
+
+lemma primroot_ord: "residue_primroot p g \<Longrightarrow> ord p g = p -1" 
+  by (simp add: residue_primroot_def test totient_prime)
+
+text \<open>If $x^l = 1$ in $\mathbb{Z}_p$, then $l$ is an upper bound for the order of $x$ in $\mathbb{Z}_ p$.\<close>
+
+lemma ord_max:
+  assumes "l \<noteq> 0" "(x :: (('a::prime_card) mod_ring))^l = 1"
+  shows " ord p (to_int_mod_ring x) \<le> l"
+proof-
+  have "[(to_int_mod_ring x)^l = 1] (mod p)" 
+    by (metis assms(2) cong_def exp_homo of_int_mod_ring.rep_eq of_int_mod_ring_to_int_mod_ring one_mod_card_int one_mod_ring.rep_eq p_def)
+  thus ?thesis unfolding ord_def using assms 
+    by (smt (z3) Least_le less_imp_le_nat not_gr0)
+qed
+
+subsection \<open>Existence of $n$-th Roots of Unity in the Finite Field\<close>
+
+text \<open>
+\label{primroot3}
+We obtain an element in the finite field such that
+its reinterpretation as a $nat$ will be a primitive root in the residue class modulo $p$.
+The difference between residue classes, their representatives in the Integers and elements 
+of the finite field is notable. When conducting informal proofs, this distinction
+ is usually blurred, but Isabelle enforces the explicit conversion between those structures.
+\<close>
+
+lemma primroot_ex:
+  obtains primroot::"('a::prime_card) mod_ring" where 
+    "primroot^(p-1) = 1"
+    "primroot \<noteq> 1"
+    "residue_primroot p (nat (to_int_mod_ring primroot))"
+proof-
+  obtain g where g_Def: "residue_primroot p g \<and> g \<noteq> 1" 
+    using prime_nat_iff' prime_primitive_root_exists test 
+    by (metis bigger_prime euler_theorem ord_1_right power_one_right prime_nat_iff'' residue_primroot.cases residue_primroot_cong)
+  hence "[g \<noteq> 1] (mod p)" using prime_not_2_order_not_1_mod[of p g]
+    by (metis One_nat_def p_lst3 less_numeral_extra(4) ord_eq_Suc_0_iff residue_primroot.cases totient_gt_1)
+  hence "[g^(p-1) = 1] (mod p)" using g_Def
+    by (metis coprime_commute euler_theorem residue_primroot_def test totient_prime)
+  moreover hence "int (g ^ (p - 1)) mod int p = (1::int)" 
+    by (metis cong_def int_ops(2) mod_less of_nat_mod prime_gt_1_nat test)
+  moreover hence "of_int_mod_ring (int (g ^ (p - 1)) mod int p) = 
+                      ((of_int_mod_ring 1) ::(('a::prime_card) mod_ring))" by simp
+  ultimately have "(of_int_mod_ring (g^(p-1))) = (1 ::(('a::prime_card) mod_ring))" 
+    using mod_homo[of "g^(p-1)"]  by (metis exp_homo power_0)
+  hence "((of_int_mod_ring g)^(p-1) ::(('a::prime_card) mod_ring)) = 1" 
+    using exp_homo[of "int g" "p-1"] by simp
+  moreover 
+  have "((of_int_mod_ring g) ::(('a::prime_card) mod_ring)) \<noteq> 1" 
+  proof
+    assume "((of_int_mod_ring g) ::(('a::prime_card) mod_ring)) = 1"
+    hence "[int g = 1] (mod p)" using p_def unfolding of_int_mod_ring_def 
+      by (metis \<open>of_int_mod_ring (int g) = 1\<close> cong_def of_int_mod_ring.rep_eq one_mod_card_int one_mod_ring.rep_eq)
+    hence "[g=1] (mod p)"
+      by (metis cong_int_iff int_ops(2))
+    thus False 
+      using \<open>[g \<noteq> 1] (mod p)\<close> by auto
+    qed
+    thus ?thesis using that g_Def calculation 
+    by (metis Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign mod_homo nat_int of_nat_0_less_iff of_nat_mod p_def residue_primroot_mod to_int_mod_ring_of_int_mod_ring zero_less_card_finite)
+qed
+
+text \<open>From this, we obtain an $n$-th root of unity $\omega$ in the finite 
+field of characteristic $p$.
+ Note that in this step we will use the assumption $p = k \cdot n +1$ 
+from locale $preliminary$: The $k$-th power of a primitive 
+root $pr$ modulo $p$ will have the property $(pr^k)^n \equiv 1 \mod p$.
+\<close>
+
+lemma omega_properties_ex: 
+  obtains \<omega> ::"(('a::prime_card) mod_ring)" 
+  where  "\<omega>^n = 1" 
+         "\<omega> \<noteq> 1"  
+         "\<forall> m. \<omega>^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n"
+proof-
+  obtain pr::"(('a::prime_card) mod_ring)" where a: "pr^(p-1) = 1 " and b: "pr \<noteq> 1"
+              and c: "residue_primroot p (nat( to_int_mod_ring pr))"
+    using primroot_ex by blast
+  moreover hence "(pr^k)^n =1" 
+    by (simp add: p_fact power_mult)
+  moreover have "pr^k \<noteq> 1"
+  proof
+    assume " pr ^ k = 1"
+    hence "(to_int_mod_ring pr)^k mod p = 1"
+      by (metis exp_homo of_int_mod_ring.rep_eq of_int_mod_ring_to_int_mod_ring one_mod_ring.rep_eq p_def)
+    hence "ord p (to_int_mod_ring pr) \<le> k"
+      by (simp add: \<open>pr ^ k = 1\<close> k_bound ord_max)
+    hence "ord p (nat (to_int_mod_ring pr)) \<le> k" 
+      by (metis ord_lift)
+    also have "ord p (nat (to_int_mod_ring pr)) = p - 1"
+      using c primroot_ord[of "(nat (to_int_mod_ring pr))"] by blast
+    also have "\<dots> = k * n"
+      using p_fact by simp
+    finally have "n \<le> 1"
+      using k_bound by simp
+    thus False
+      using n_lst2 by linarith
+  qed
+  moreover have "\<forall> m. (pr^k)^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n"
+  proof(rule ccontr)
+    assume  "\<not> (\<forall>m. (pr ^ k) ^ m = 1 \<and> m\<noteq>0 \<longrightarrow> n \<le> m) "
+    then obtain m where "(pr^k)^m = 1  \<and> m\<noteq>0 \<and> m < n" by force
+    hence "ord p (to_int_mod_ring pr) \<le> k * m" using ord_max[of "k*m" pr]
+      by (metis calculation(5) mult_is_0 power_mult) 
+    moreover have "ord p (nat (to_int_mod_ring pr)) = p-1" using c primroot_ord ord_lift by simp
+    ultimately show False 
+      by (metis \<open>(pr ^ k) ^ m = 1 \<and> m \<noteq> 0 \<and> m < n\<close> add_diff_cancel_right' nat_0_less_mult_iff nat_mult_le_cancel_disj not_less ord_lift p_def p_fact prime_card prime_gt_1_nat zero_less_diff)
+  qed
+    ultimately show ?thesis
+    using that by simp
+qed
+
+text \<open>We define an $n$-th root of unity $\omega$ for $NTT$.\<close>
+theorem omega_exists: "\<exists> \<omega> ::(('a::prime_card) mod_ring) .
+                              \<omega>^n = 1 \<and> \<omega> \<noteq> 1 \<and> (\<forall> m. \<omega>^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n)"
+  using omega_properties_ex by metis
+
+definition "(omega::(('a::prime_card) mod_ring)) = 
+       (SOME \<omega> . (\<omega>^n = 1 \<and> \<omega> \<noteq> 1\<and> (\<forall> m. \<omega>^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n)))"
+
+lemma omega_properties: "omega^n = 1" "omega \<noteq> 1" 
+  "(\<forall> m. omega^m = 1 \<and> m\<noteq>0 \<longrightarrow> m \<ge> n)"
+  unfolding omega_def using omega_exists 
+  by (smt (verit, best) verit_sko_ex')+
+
+text \<open>We define the multiplicative inverse $\mu$ of $\omega$.\<close>
+
+definition "mu = omega ^ (n - 1)"
+
+lemma mu_properties: "mu * omega = 1" "mu \<noteq> 1" 
+proof -
+  have "omega ^ (n - 1) * omega = omega ^ Suc (n - 1)"
+    by simp
+  also have "Suc (n - 1) = n"
+    using n_lst2 by simp
+  also have "omega ^ n = 1"
+    using omega_properties(1) by auto
+  finally show "mu * omega = 1"
+    by (simp add: mu_def)
+next
+  show "mu \<noteq> 1"
+    using omega_properties n_lst2 by (auto simp: mu_def)
+qed
+
+subsection \<open>Some Lemmas on Sums\<close>
+text \<open>\label{sums}\<close>
+
+text \<open>The following lemmas concern sums over a finite field. 
+ Most of the propositions are intuitive.\<close>
+
+lemma sum_in: "(\<Sum>i=0..<(x::nat). f i * (y ::('a mod_ring))) = (\<Sum>i=0..<x. f i )* (y) "
+  by(induction x) (auto simp add: algebra_simps)
+
+lemma sum_eq: "(\<And> i. i < x \<Longrightarrow> f i = g i)
+                    \<Longrightarrow> (\<Sum>i=0..<(x::nat). f i) = (\<Sum>i=0..<x. g i) " 
+  by(induction x) (auto simp add: algebra_simps)
+
+lemma sum_diff_in: "(\<Sum>i=0..<(x::nat). (f i)::('a mod_ring)) - (\<Sum>i=0..<x. g i) = 
+                    (\<Sum>i=0..<x. f i - g i)"
+ by(induction x) (auto simp add: algebra_simps)
+
+lemma sum_swap: "(\<Sum>i=0..<(x::nat). \<Sum>j=0..<(y::nat). f i j) = 
+                 (\<Sum>j=0..<(y::nat). \<Sum>i=0..<(x::nat). f i j ) "
+  using Groups_Big.comm_monoid_add_class.sum.swap by fast
+
+lemma sum_const: "(\<Sum>i=0..<(x::nat). (c::('a::prime_card) mod_ring)) = (of_int_mod_ring x) * c" 
+  by(induction x, simp add: algebra_simps,  simp add: algebra_simps)
+    (metis distrib_left mult.right_neutral of_int_of_int_mod_ring of_int_of_nat_eq of_nat_Suc)
+
+lemma sum_split: "(r1::nat) < r2 \<Longrightarrow> (\<Sum>l = 0..<r1. ((f l)::(('a::prime_card) mod_ring))) 
+                                         +(\<Sum>l = r1..<r2. f l) = (\<Sum>l = 0..<r2. f l)" 
+  by (meson less_or_eq_imp_le sum.atLeastLessThan_concat zero_le)
+
+lemma sum_index_shift: "(\<Sum>l = (a::nat)..< b. f(l+c)) = (\<Sum>l = (a+c)..< (b+c). f l )"
+  by(induction a arbitrary: b c) (metis sum.shift_bounds_nat_ivl)+
+
+text \<open>One may sum over even and odd indices independently.
+The lemma statement was taken from a formalization of FFT~\parencite{FFT-AFP}. 
+We give an alternative proof adapted to the finite field $\mathbb{Z}_p$. 
+\<close>
+
+lemma sum_splice:
+  "(\<Sum>i::nat = 0..<2*nn. f i) = (\<Sum>i = 0..<nn. f (2*i)) + (\<Sum>i = 0..<nn. f (2*i+1))"
+proof(induction nn)
+  case (Suc n)
+  have "(\<Sum>i::nat = 0..<2*(n+1). f i)  = (\<Sum>i::nat = 0..<(2*n). f i) + f(2*n+1) + f (2*n)" 
+    by( simp add: algebra_simps)
+  also have "\<dots> = (\<Sum>i::nat = 0..<n. f (2*i)) + (\<Sum>i::nat = 0..<n. f (2*i+1)) + f(2*n+1) + f (2*n)"
+    using Suc by simp
+  also have "\<dots> = (\<Sum>i::nat = 0..<(Suc n). f (2*i)) + (\<Sum>i::nat = 0..<(Suc n). f (2*i+1))"
+   by( simp add: algebra_simps)
+  finally show ?case by simp
+qed simp
+
+lemma sum_even_odd_split: "even (a::nat) \<Longrightarrow> (\<Sum>j=0..<(a div 2). f (2*j))+ (\<Sum>j=0..<(a div 2). f (2*j+1)) =  (\<Sum>j=0..<a. f j)"
+  by (induction a, simp)(metis even_two_times_div_two sum_splice)
+
+lemma sum_splice_other_way_round: " (\<Sum>j=(0::nat)..<i. f (2*j)) + (\<Sum>j=0..<i. f (2*j+1)) = 
+        (\<Sum>j=(0::nat)..<2*i. f j )"
+by (metis sum_splice)
+
+lemma sum_neg_in: "- (\<Sum>j = 0..<l. (f j)::('a mod_ring)) =  (\<Sum>j = 0..<l. - f j) " 
+  by (simp add: sum_negf)
+
+subsection \<open>Geometric Sums\<close>
+
+text \<open>\label{geosum}\<close>
+
+text \<open>This lemma will be important for proving properties on $\mathsf{NTT}$. At first, an informal proof sketch:
+\begin{align*}
+(1-x) \cdot \sum \limits _{l = 0} ^ {r-1} x^l 
+&= \sum \limits _{l = 0} ^ {r-1} x^l  - x \cdot \sum \limits _{l = 0} ^{r-1} x^l \\ 
+&= \sum \limits _{l = 0} ^ {r-1} x^l  - \sum \limits _{l = 1} ^{r} x^l \\ 
+& = 1 - x^r
+\end{align*}
+
+The same lemma for integers can be found in~\parencite{Dirichlet_Series-AFP}.
+ Our version is adapted to finite fields.
+\<close>
+
+lemma geo_sum: 
+  assumes "x \<noteq> 1"
+  shows "(1-x)*(\<Sum>l = 0..<r. (x::('a mod_ring))^l) = (1-x^r)"
+proof-
+  have 0:"x * (\<Sum>l = 0..<r. x^l) = (\<Sum>l = 0..<r. x^(Suc l))" using sum_in[of "\<lambda> l. x^l" x r] 
+    by(simp add: algebra_simps)
+  have 1:"(\<Sum>l = 0..<r. x^l) - (\<Sum>l = 0..<r. x^(Suc l)) = (\<Sum>l = 0..<r. x^l - x^(Suc l))" 
+    by(rule sum_diff_in)
+  have 2: "(\<Sum>l = 0..<r. x^l - x^(Suc l)) = 1 - x^r"
+    by(induction r) simp+
+  thus ?thesis
+    by (simp add: lessThan_atLeast0 one_diff_power_eq)
+qed 
+
+lemmas sum_rules = sum_in sum_eq sum_diff_in sum_swap sum_const sum_split sum_index_shift
+
+end
+end
diff --git a/thys/Number_Theoretic_Transform/ROOT b/thys/Number_Theoretic_Transform/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/ROOT
@@ -0,0 +1,14 @@
+chapter AFP
+
+session "Number_Theoretic_Transform" (AFP) = "HOL-Number_Theory" +
+  (*descpription "Number Theoretic Tranform, NTT with finite fields"*)
+  options [timeout = 600]
+  sessions
+    Berlekamp_Zassenhaus
+  theories
+   Preliminary_Lemmas
+   NTT
+   Butterfly
+  document_files
+    "root.bib"
+    "root.tex"
diff --git a/thys/Number_Theoretic_Transform/document/root.bib b/thys/Number_Theoretic_Transform/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/document/root.bib
@@ -0,0 +1,86 @@
+@Inbook{Good1997,
+author="Good, I. J.",
+editor="Kotz, Samuel
+and Johnson, Norman L.",
+title="Introduction to Cooley and Tukey (1965) An Algorithm for the Machine Calculation of Complex Fourier Series",
+bookTitle="Breakthroughs in Statistics",
+year="1997",
+publisher="Springer New York",
+address="New York, NY",
+pages="201--216",
+abstract="Fourier (frequency) analysis is important in statistics, mathematics, and all the hard sciences (as in x-ray crystallography), and in signal processing, so Fast Fourier Transforms (FFTs) are widely applicable. For example, Costain (1974) said the FFTs are regarded as an economic breakthrough in geo­physics, especially in seismology.",
+isbn="978-1-4612-0667-5",
+doi="10.1007/978-1-4612-0667-5_9",
+url="https://doi.org/10.1007/978-1-4612-0667-5_9"
+}
+
+
+@book{10.5555/1614191,
+author = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford},
+title = {Introduction to Algorithms, Third Edition},
+year = {2009},
+isbn = {0262033844},
+publisher = {The MIT Press},
+edition = {3rd},
+abstract = {If you had to buy just one text on algorithms, Introduction to Algorithms is a magnificent choice. The book begins by considering the mathematical foundations of the analysis of algorithms and maintains this mathematical rigor throughout the work. The tools developed in these opening sections are then applied to sorting, data structures, graphs, and a variety of selected algorithms including computational geometry, string algorithms, parallel models of computation, fast Fourier transforms (FFTs), and more. This book's strength lies in its encyclopedic range, clear exposition, and powerful analysis. Pseudo-code explanation of the algorithms coupled with proof of their accuracy makes this book is a great resource on the basic tools used to analyze the performance of algorithms.}
+}
+
+@misc{cryptoeprint:2016/504,
+      author = {Patrick Longa and Michael Naehrig},
+      title = {Speeding up the Number Theoretic Transform for Faster Ideal Lattice-Based Cryptography},
+      howpublished = {Cryptology ePrint Archive, Paper 2016/504},
+      year = {2016},
+      note = {\url{https://eprint.iacr.org/2016/504}},
+      url = {https://eprint.iacr.org/2016/504}
+}
+
+@inproceedings{NipkowEH-ATVA20,
+author = {Tobias Nipkow and Manuel Eberl and Maximilian P. L. Haslbeck},
+title = {Verified Textbook Algorithms. {A} Biased Survey},
+booktitle = {ATVA 2020, Automated Technology for Verification and Analysis},
+editor = {Dang Van Hung and Oleg Sokolsky},
+publisher = {Springer},
+series = {LNCS},
+volume = {12302},
+pages = {25-53},
+year =2020,
+note = {Invited paper}
+}
+
+@misc{ntt_intro,
+ author = {Nayuki},
+ title = {Number-theoretic transform (integer DFT)},
+  year = {2022},
+ howpublished = {\url{https://www.nayuki.io/page/number-theoretic-transform-integer-dft}}
+}
+
+@misc{funalgs,
+author ="{Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, Bohua Zhan}",
+title = {Functional Algorithms, Verified!},
+year = 2021,
+howpublished = {\url{https://functional-algorithms-verified.org/}}
+}
+
+@article{FFT-AFP,
+  author  = {Clemens Ballarin},
+  title   = {Fast Fourier Transform},
+  journal = {Archive of Formal Proofs},
+  month   = {October},
+  year    = {2005},
+  note    = {\url{https://isa-afp.org/entries/FFT.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{Dirichlet_Series-AFP,
+  author  = {Manuel Eberl},
+  title   = {Dirichlet Series},
+  journal = {Archive of Formal Proofs},
+  month   = {October},
+  year    = {2017},
+  note    = {\url{https://isa-afp.org/entries/Dirichlet_Series.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+
diff --git a/thys/Number_Theoretic_Transform/document/root.tex b/thys/Number_Theoretic_Transform/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Number_Theoretic_Transform/document/root.tex
@@ -0,0 +1,71 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+%\usepackage{hyperref}
+\usepackage{amsmath, amssymb, wasysym}
+\usepackage[autostyle]{csquotes}
+\usepackage{stmaryrd}
+\usepackage[T1]{fontenc}
+%\usepackage{hyperref}
+%\usepackage[T2A]{fontenc}
+%\usepackage[utf8]{inputenx}
+\usepackage[backend = bibtex,
+url=false,
+  citestyle=numeric,
+  bibstyle = numeric,
+  maxnames=4,
+  minnames=3,
+  maxbibnames=99,
+  giveninits,
+  sorting = none,
+  uniquename=init]{biblatex}
+% this should be the last package used
+\usepackage{pdfsetup}
+
+\addtolength{\hoffset}{-1,5cm}
+\addtolength{\textwidth}{3cm}
+\bibliography{root}
+\begin{document}
+
+\title{Number Theoretic Transform}
+\author{Thomas Ammer and Katharina Kreuzer}
+\maketitle
+
+\begin{abstract}
+\indent  This entry contains an Isabelle formalization of the \textit{Number Theoretic Transform (NTT)} which is the analogue to a \textit{Discrete Fourier Transform (DFT)}, just over a finite field. Roots of unity in the complex numbers are replaced by those in a finite field.\\
+ \indent First, we define both \textit{NTT} and the inverse transform \textit{INTT} in Isabelle and prove them to be mutually inverse. \\
+\indent $DFT$ can be efficiently computed by the recursive \textit{Fast Fourier Transform (FFT)}. In our formalization, this algorithm is adapted to the setting of the $NTT$: We implement a \textit{Fast Number Theoretic Transform (FNTT)} based on the Butterfly scheme by Cooley and Tukey~\parencite{Good1997}. Additionally, we provide an inverse transform \textit{IFNTT} and prove it mutually inverse to \textit{FNTT}.\\
+\indent Afterwards, a recursive formalization of the \textit{FNTT} running time is examined and the famous $\mathcal{O}(n \log n)$ bounds are proven.
+\end{abstract}
+
+\pagebreak
+
+\tableofcontents
+\pagebreak
+%\parindent 0pt\parskip 0.5ex
+\isabellestyle{it}
+% include generated text of all theories
+\section{Introduction}
+\indent \indent The \textit{Discrete Fourier Transform~(DFT)} is used to analyze a periodic signal given by equidistant samples for its frequencies. 
+For an introduction to \textit{DFT} one may have a look at~\parencite{10.5555/1614191}.
+ However, one may generalize the setting and consider any algebraic structure with roots of unity.
+ For finite fields, we call the analogue to \textit{DFT} a \textit{Number Theoretic Transform~(NTT)}. It can be used for fast Integer multiplications and post-quantum lattice-based cryptography~\parencite{cryptoeprint:2016/504}.\\
+\indent Starting our formalization, we provide some initial setup, namely roots of unity by an argument on generating elements in $\mathbb{Z}_p$ (Sections~\ref{primroot1},~\ref{primroot2},~\ref{primroot3}) and lemmas on summation (Section~\ref{sums}), especially geometric sums (Section~\ref{geosum}).\\
+\indent We continue with a mathematical definition of \textit{NTT}~\parencite{ntt_intro} and formalize it in Isabelle (Section~\ref{NTTdef}). Let us consider a definition of \textit{DFT}:
+\begin{equation*}
+\mathsf{DFT}(\vec{x})_k = \sum \limits _{l=0}^{n-1} x_l \cdot e^{- \frac{i2\pi}{n}\cdot k \cdot l} \hspace{1cm} \text{ where } i = \sqrt{-1}
+\end{equation*}
+In this equation, $e^{- \frac{i2\pi}{n}}$ is a root of unity. Let $\omega$ be a $n$-th root of unity in $\mathbb{Z}_p$ and we can state analogously:
+\begin{equation*}
+\mathsf{NTT}(\vec{x})_k = \sum \limits _{l=0}^{n-1} x_l \cdot \omega^{ k l}
+\end{equation*}
+Throughout the paper, we stick to this definition. 
+An inverse tranform \textit{INTT} is obtained by replacing $\omega$ by its field inverse $\mu$ (i.e. $\mu \cdot \omega \equiv 1  \mod p$). We prove \textit{NTT} and \textit{INTT} to be mutually inverse in Section~\ref{NTTcorr}.\\
+\indent For computing \textit{DFT} more efficiently than $\mathcal{O}(n^2)$, a divide and conquer approach can be applied. By a smart rearranging, the sum can  be split into two subproblems of size $\frac{n}{2}$ which gives  an $\mathcal{O}(n \log n)$ algorithm. We call this the \textit{Fast Nuber Theoretic Transform (FNTT)}~\parencite{cryptoeprint:2016/504} and \textit{IFNTT} respectively. The corresponding procedure is treated in Section~\ref{Butterfly}. We prove equality between \textit{(I)NTT} and \textit{(I)FNTT} and can infer that both are mutually inverse by previos results.\\
+\indent \textit{DFT} and similar transforms like \textit{NTT} are especially famous for algorithms with $\mathcal{O}(n \log n)$ running times. Thus, it is appropriate to formalize some related arguments. We loosely follow a generic approach for verifying resource bounds of functional data structures and algorithms in Isabelle~\parencite{funalgs}.\\
+\indent During the formalization, we also present some informal arguments in order to give a better intution of what's going on in the formal proofs.\\
+\indent The present formalization was developed during a practical course on specification and verification at the \href{https://www21.in.tum.de/index.html}{TUM Chair of Logic and Verification}.\\
+
+\input{session}
+\pagebreak
+\printbibliography{}
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,697 +1,698 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DPRM_Theorem
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 IsaNet
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multiset_Ordering_NPC
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
+Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 Package_logic
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sophomores_Dream
 Solidity
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL