theory week09B_demo_gcd imports WhileLoopRule begin definition gcd' :: "nat \ nat \ ('s,nat) nondet_monad" where "gcd' a b \ do { (a, b) \ whileLoop (\(a, b) b. 0 < a) (\(a, b). return (b mod a, a)) (a, b); return b }" lemma prod_case_wp: "\P\ f (fst x) (snd x) \Q\ \ \P\ case x of (a,b) \ f a b \Q\" sorry lemma gcd'_correct: "\\_. True\ gcd' x y \\r s. r = gcd x y\" sorry end