Theory Strassen_Algorithm_Code

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Strassen's Algorithm as Code Equation›

text ‹We replace the code-equations for matrix-multiplication 
  by Strassen's algorithm. Note that this will strengthen the class-constraint
  for matrix multiplication from semirings to rings!›

theory Strassen_Algorithm_Code
imports 
  Strassen_Algorithm
begin

text ‹The aim is to replace the implementation of @{thm times_mat_def} by @{const strassen_mat_mult}.›

text ‹We first need a copy of standard matrix multiplication to execute the base case.›

definition "basic_mat_mult = (*)"
lemma basic_mat_mult_code[code]: "basic_mat_mult A B = mat (dim_row A) (dim_col B) (λ (i,j). row A i ∙ col B j)"
  unfolding basic_mat_mult_def by auto

text ‹Next use this new matrix multiplication code within Strassen's algorithm.›
lemmas strassen_mat_mult_code[code] = strassen_mat_mult.simps[folded basic_mat_mult_def]

text ‹And finally use Strassen's algorithm for implementing matrix-multiplication.›

lemma mat_mult_code[code]: "A * B = (if dim_col A = dim_row B then strassen_mat_mult A B else basic_mat_mult A B)"
  using strassen_mat_mult[of A B] unfolding basic_mat_mult_def by auto

end