(* File written in class, interactively with students *)

theory Mult
imports AutoCorres

begin

install_C_file "mult.c"

print_theorems
thm mult_global_addresses.mult_body_def

autocorres [ts_rules = nondet] "mult.c"

print_theorems
thm mult.mult'_def

context mult begin

lemma "\<lbrace> \<lambda>s. True \<rbrace> mult' A B  \<lbrace> \<lambda>r s. r=A*B \<rbrace>"
  apply (unfold mult'_def)
  (* using [[show_types]]*)
  thm whileLoop_add_inv
  apply (subst whileLoop_add_inv 
         [where I="\<lambda> (b,tmp) s. tmp+A*b=A*B"]) 
  apply wp
  apply simp_all thm field_simps
   apply (case_tac a, clarsimp simp: field_simps)
  apply (case_tac a, clarsimp simp: field_simps)
  done
 
  
(* VCG version only not created during lecture, just showed solution *)
  
lemma 
  "\<Gamma> \<turnstile> {s. a_' s = a \<and> b_' s = b }
       \<acute>ret__unsigned :== PROC mult(a,b)
       {t.  ret__unsigned_' t = a*b }"
  apply vcg_step
  thm whileAnno_def 
  apply (subst whileAnno_def)
  apply (subst whileAnno_def [symmetric,
        where I= "{s. tmp_' s +a_' s * b_' s = a*b}"])
  apply vcg
    apply simp
   apply clarsimp
   apply (simp add: field_simps) (*find_theorems "_>0" name:word*)
  apply (simp add: word_gt_0)
 done
 
  
  
end


end