theory week09A_demo_gcd_sol
imports WhileLoopRule
begin


definition gcd' :: "nat \<Rightarrow> nat \<Rightarrow> ('s,nat) nondet_monad" where
  "gcd' a b \<equiv>
   do {
      (a, b) \<leftarrow> whileLoop (\<lambda>(a, b) b. 0 < a)
                          (\<lambda>(a, b). return (b mod a, a))
                          (a, b);
      return b
   }"

lemma prod_case_valid:
  assumes "\<lbrace>P\<rbrace> f (fst x) (snd x) \<lbrace>Q\<rbrace>"
  shows "\<lbrace>P\<rbrace> case x of (a,b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>"
  using assms
  apply(auto simp: valid_def split: prod.splits)
  done

lemma gcd'_correct: 
  "\<lbrace>\<lambda>_. True\<rbrace> gcd' a b \<lbrace>\<lambda>r s. r = gcd a b\<rbrace>"


end