Theory GCD_Impl

(*
  File: GCD_Impl.thy
  Author: Bohua Zhan
*)

theory GCD_Impl
  imports SepAuto
begin

text ‹A tutorial example for computation of GCD.›

text ‹Turn on auto2's trace›
declare [[print_trace]]

text ‹Property of gcd that justifies the recursive computation. Add as a
  right-to-left rewrite rule.›
setup ‹add_rewrite_rule_back @{thm gcd_red_nat}›

text ‹Functional version of gcd.›
fun gcd_fun :: "nat ⇒ nat ⇒ nat" where
  "gcd_fun a b = (if b = 0 then a else gcd_fun b (a mod b))"

text ‹The fun package automatically generates induction rule upon showing
  termination. This adds the induction rule for the @fun\_induct command.›
setup ‹add_fun_induct_rule (@{term gcd_fun}, @{thm gcd_fun.induct})›

lemma gcd_fun_correct:
  "gcd_fun a b = gcd a b"
@proof
  @fun_induct "gcd_fun a b"
  @unfold "gcd_fun a b"
@qed

text ‹Imperative version of gcd.›
partial_function (heap) gcd_impl :: "nat ⇒ nat ⇒ nat Heap" where
  "gcd_impl a b = (
    if b = 0 then return a
    else do {
      c ← return (a mod b);
      r ← gcd_impl b c;
      return r
    })"

text ‹The program is sufficiently simple that we can prove the Hoare triple
  directly (without going through the functional program).›
theorem gcd_impl_correct:
  "<emp> gcd_impl a b <λr. ↑(r = gcd a b)>"
@proof
  @fun_induct "gcd_fun a b"
@qed

text ‹Turn off trace.›
declare [[print_trace = false]]

end