theory week09B_demo_gcd_sol 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_valid: assumes "\P\ f (fst x) (snd x) \Q\" shows "\P\ case x of (a,b) \ f a b \Q\" using assms apply(auto simp: valid_def split: prod.splits) done lemma gcd'_correct: "\\_. True\ gcd' a b \\r s. r = gcd a b\" unfolding gcd'_def apply (rule bind_wp) apply (rule prod_case_valid) apply (rule return_wp) apply (rule hoare_weaken_pre) apply (rule_tac I="\(x,y) s. gcd x y = gcd a b" in whileLoop_wp) apply (rule prod_case_valid) apply (rule hoare_weaken_pre, rule return_wp) apply clarsimp find_theorems gcd "_ mod _" find_theorems "gcd ?a ?b = gcd ?b ?a" apply (simp add: gcd.commute flip: gcd_red_nat) apply clarsimp apply clarsimp done end