# HG changeset patch # User haftmann # Date 1279812382 -7200 # Node ID 440114da2488a8110d8f03ac9ef213d3e1e1ab7e # Parent d00a3f47b6072e9e07a6f6da261a4c15b419e6a7 dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607) diff -r d00a3f47b607 -r 440114da2488 src/HOL/Extraction/Higman.thy --- a/src/HOL/Extraction/Higman.thy Thu Jul 22 12:07:30 2010 +0200 +++ b/src/HOL/Extraction/Higman.thy Thu Jul 22 17:26:22 2010 +0200 @@ -350,14 +350,14 @@ end function mk_word_aux :: "nat \ Random.seed \ letter list \ Random.seed" where - "mk_word_aux k = (do { + "mk_word_aux k = exec { i \ Random.range 10; (if i > 7 \ k > 2 \ k > 1000 then return [] - else do { + else exec { let l = (if i mod 2 = 0 then A else B); ls \ mk_word_aux (Suc k); return (l # ls) - })})" + })}" by pat_completeness auto termination by (relation "measure ((op -) 1001)") auto @@ -366,10 +366,10 @@ primrec mk_word_s :: "nat \ Random.seed \ letter list \ Random.seed" where "mk_word_s 0 = mk_word" - | "mk_word_s (Suc n) = (do { + | "mk_word_s (Suc n) = exec { _ \ mk_word; mk_word_s n - })" + }" definition g1 :: "nat \ letter list" where "g1 s = fst (mk_word_s s (20000, 1))"