Theory Babai_Algorithm_Updated

theory Babai_Algorithm_Updated
  imports
    LLL_Basis_Reduction.LLL_Impl
    "HOL.Archimedean_Field"
    "HOL-Analysis.Inner_Product"

begin

fun calculate_c:: "rat vec  rat vec list  nat => int" where
  "calculate_c s L1 n  = round ((s  (L1!((dim_vec s) - n))) / (sq_norm_vec (L1!((dim_vec s) - n))))"

fun update_s:: "rat vec  rat vec list  rat vec list  nat  rat vec" where
  "update_s sn M Mt n = ((rat_of_int (calculate_c sn Mt n)) v M!((dim_vec sn) - n)) "

fun babai_help:: "rat vec  rat vec list  rat vec list  nat  rat vec" where
	"babai_help s M Mt 0 = s" |
	"babai_help s M Mt (Suc n) = (let B = (babai_help s M Mt n) in B - (update_s B M Mt (Suc n)))"

text ‹This assumes an LLL-reduced input and outputs a short vector of the form $v+t$, with $v \in L$ ›
fun babai_of_LLL :: "rat vec  rat vec list  rat vec" where
	"babai_of_LLL s M = babai_help s M (gram_schmidt (dim_vec s) M) (dim_vec s)" 

text ‹This begins with a non-reduced basis and outputs a vector $v$ in $L$ which is close to $t$›
fun full_babai :: "int vec list  rat vec  rat  int vec" 
  where "full_babai fs target α = 
        map_vec int_of_rat
          (babai_of_LLL
            (uminus target)
            (LLL.RAT (LLL_Impl.reduce_basis α fs))
          + target)"

end