theory week09B_demo_gcd
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:
  "\<lbrace>P\<rbrace> f (fst x) (snd x) \<lbrace>Q\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> case x of (a,b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>"
  sorry

thm gcdI

lemma gcd'_correct: 
  "\<lbrace>\<lambda>_. True\<rbrace> gcd' a b \<lbrace>\<lambda>r s. r = gcd a b\<rbrace>"
  apply (unfold gcd'_def)
  sorry

end