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 :: "'a::semiring_0 mat ⇒ 'a mat ⇒ 'a mat"
  where "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)"
  by (auto simp add: basic_mat_mult_def)

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] by (simp add: basic_mat_mult_def)

end