theory HoareLogicSolutions
imports Main Binomial "~~/src/HOL/Hoare/Hoare_Logic"
begin

(* The minimum of two integers x and y: *)
lemma Min: "VARS (z :: int)
 {True}
 IF x \<le> y THEN z := x ELSE z := y FI
 { z = min x y }"
apply vcg_simp
by auto


(* Iteratively copy an integer variable x to y: *)
lemma Copy: "VARS (a :: int) y
 {0 \<le> x}
 a := x; y := 0;
 WHILE a \<noteq> 0
 INV { a + y = x } 
 DO y := y + 1 ; a := a - 1 OD
 {x = y}"
by vcg_simp


(* Iterative multiplication through addition: *)
lemma Multi: "VARS (a :: int) z
 {0 \<le> y}
 a := 0; z := 0;
 WHILE a \<noteq> y
 INV { z = x * a }
 DO 
   z := z + x ; 
   a := a + 1 
 OD
 {z = x * y}"
apply vcg_simp
by (simp add: algebra_simps)



(* A factorial algorithm: *)
lemma DownFact: "VARS (z :: nat) (y::nat)
 {True}
 z := x; y := 1;
 WHILE z > 0
 INV { y * fact z = fact x }
 DO 
   y := y * z; 
   z := z - 1 
 OD
 {y = fact x}"
apply vcg_simp
by (auto simp add: fact_reduce)


(* Integer division of x by y: *)
lemma Div: "VARS (r :: int) d 
 {y \<noteq> 0}
 r := x; d := 0;
 WHILE y \<le> r
 INV { x = d * y + r }
 DO 
  r := r - y;
  d := d + 1
 OD
 { x = d * y + r \<and> r < y }"
apply vcg_simp
by (simp add: algebra_simps)


end