Heap_Monad uses Monad_Syntax
authorkrauss
Tue Jul 13 12:00:11 2010 +0200 (2010-07-13)
changeset 37792ba0bc31b90d7
parent 37791 0d6b64060543
child 37794 46c21c1f8cb0
Heap_Monad uses Monad_Syntax
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Mrec.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:50:22 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:00:11 2010 +0200
     1.3 @@ -407,25 +407,25 @@
     1.4    by (simp add: upd'_def upd_return)
     1.5  
     1.6  lemma [code]:
     1.7 -  "map_entry i f a = (do
     1.8 +  "map_entry i f a = do {
     1.9       x \<leftarrow> nth a i;
    1.10       upd i (f x) a
    1.11 -   done)"
    1.12 +   }"
    1.13    by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
    1.14  
    1.15  lemma [code]:
    1.16 -  "swap i x a = (do
    1.17 +  "swap i x a = do {
    1.18       y \<leftarrow> nth a i;
    1.19       upd i x a;
    1.20       return y
    1.21 -   done)"
    1.22 +   }"
    1.23    by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
    1.24  
    1.25  lemma [code]:
    1.26 -  "freeze a = (do
    1.27 +  "freeze a = do {
    1.28       n \<leftarrow> len a;
    1.29       Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
    1.30 -   done)"
    1.31 +   }"
    1.32  proof (rule Heap_eqI)
    1.33    fix h
    1.34    have *: "List.map
    1.35 @@ -440,15 +440,15 @@
    1.36      apply (simp_all add: nth_def guard_def *)
    1.37      apply (simp add: length_def map_nth)
    1.38      done
    1.39 -  then have "execute (do
    1.40 +  then have "execute (do {
    1.41        n \<leftarrow> len a;
    1.42        Heap_Monad.fold_map (Array.nth a) [0..<n]
    1.43 -    done) h = Some (get_array a h, h)"
    1.44 +    }) h = Some (get_array a h, h)"
    1.45      by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
    1.46 -  then show "execute (freeze a) h = execute (do
    1.47 +  then show "execute (freeze a) h = execute (do {
    1.48        n \<leftarrow> len a;
    1.49        Heap_Monad.fold_map (Array.nth a) [0..<n]
    1.50 -    done) h" by (simp add: execute_simps)
    1.51 +    }) h" by (simp add: execute_simps)
    1.52  qed
    1.53  
    1.54  hide_const (open) new' of_list' make' len' nth' upd'
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 11:50:22 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 12:00:11 2010 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
     2.5  
     2.6  theory Heap_Monad
     2.7 -imports Heap
     2.8 +imports Heap Monad_Syntax
     2.9  begin
    2.10  
    2.11  subsection {* The monad *}
    2.12 @@ -259,12 +259,16 @@
    2.13    obtains "False"
    2.14    using assms by (rule crelE) (simp add: success_def execute_simps)
    2.15  
    2.16 -definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
    2.17 -  [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    2.18 +definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
    2.19 +  [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
    2.20                    Some (x, h') \<Rightarrow> execute (g x) h'
    2.21                  | None \<Rightarrow> None)"
    2.22  
    2.23 -notation bind (infixl "\<guillemotright>=" 54)
    2.24 +setup {*
    2.25 +  Adhoc_Overloading.add_variant 
    2.26 +    @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind}
    2.27 +*}
    2.28 +
    2.29  
    2.30  lemma execute_bind [execute_simps]:
    2.31    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
    2.32 @@ -314,92 +318,6 @@
    2.33  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    2.34    by (rule Heap_eqI) (simp add: execute_simps)
    2.35  
    2.36 -abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
    2.37 -  "f >> g \<equiv> f >>= (\<lambda>_. g)"
    2.38 -
    2.39 -notation chain (infixl "\<guillemotright>" 54)
    2.40 -
    2.41 -
    2.42 -subsubsection {* do-syntax *}
    2.43 -
    2.44 -text {*
    2.45 -  We provide a convenient do-notation for monadic expressions
    2.46 -  well-known from Haskell.  @{const Let} is printed
    2.47 -  specially in do-expressions.
    2.48 -*}
    2.49 -
    2.50 -nonterminals do_expr
    2.51 -
    2.52 -syntax
    2.53 -  "_do" :: "do_expr \<Rightarrow> 'a"
    2.54 -    ("(do (_)//done)" [12] 100)
    2.55 -  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    2.56 -    ("_ <- _;//_" [1000, 13, 12] 12)
    2.57 -  "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    2.58 -    ("_;//_" [13, 12] 12)
    2.59 -  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    2.60 -    ("let _ = _;//_" [1000, 13, 12] 12)
    2.61 -  "_nil" :: "'a \<Rightarrow> do_expr"
    2.62 -    ("_" [12] 12)
    2.63 -
    2.64 -syntax (xsymbols)
    2.65 -  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    2.66 -    ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
    2.67 -
    2.68 -translations
    2.69 -  "_do f" => "f"
    2.70 -  "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
    2.71 -  "_chain f g" => "f \<guillemotright> g"
    2.72 -  "_let x t f" => "CONST Let t (\<lambda>x. f)"
    2.73 -  "_nil f" => "f"
    2.74 -
    2.75 -print_translation {*
    2.76 -let
    2.77 -  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
    2.78 -        let
    2.79 -          val (v, t) = Syntax.variant_abs abs;
    2.80 -        in (Free (v, ty), t) end
    2.81 -    | dest_abs_eta t =
    2.82 -        let
    2.83 -          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    2.84 -        in (Free (v, dummyT), t) end;
    2.85 -  fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
    2.86 -        let
    2.87 -          val (v, g') = dest_abs_eta g;
    2.88 -          val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
    2.89 -          val v_used = fold_aterms
    2.90 -            (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
    2.91 -        in if v_used then
    2.92 -          Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
    2.93 -        else
    2.94 -          Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
    2.95 -        end
    2.96 -    | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
    2.97 -        Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
    2.98 -    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    2.99 -        let
   2.100 -          val (v, g') = dest_abs_eta g;
   2.101 -        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
   2.102 -    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   2.103 -        Const (@{const_syntax return}, dummyT) $ f
   2.104 -    | unfold_monad f = f;
   2.105 -  fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
   2.106 -    | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   2.107 -        contains_bind t;
   2.108 -  fun bind_monad_tr' (f::g::ts) = list_comb
   2.109 -    (Const (@{syntax_const "_do"}, dummyT) $
   2.110 -      unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
   2.111 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   2.112 -    if contains_bind g' then list_comb
   2.113 -      (Const (@{syntax_const "_do"}, dummyT) $
   2.114 -        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   2.115 -    else raise Match;
   2.116 -in
   2.117 - [(@{const_syntax bind}, bind_monad_tr'),
   2.118 -  (@{const_syntax Let}, Let_monad_tr')]
   2.119 -end;
   2.120 -*}
   2.121 -
   2.122  
   2.123  subsection {* Generic combinators *}
   2.124  
   2.125 @@ -451,11 +369,11 @@
   2.126  
   2.127  primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   2.128    "fold_map f [] = return []"
   2.129 -| "fold_map f (x # xs) = do
   2.130 +| "fold_map f (x # xs) = do {
   2.131       y \<leftarrow> f x;
   2.132       ys \<leftarrow> fold_map f xs;
   2.133       return (y # ys)
   2.134 -   done"
   2.135 +   }"
   2.136  
   2.137  lemma fold_map_append:
   2.138    "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   2.139 @@ -611,7 +529,7 @@
   2.140  text {* Monad *}
   2.141  
   2.142  code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   2.143 -code_monad "op \<guillemotright>=" Haskell
   2.144 +code_monad bind Haskell
   2.145  code_const return (Haskell "return")
   2.146  code_const Heap_Monad.raise' (Haskell "error/ _")
   2.147  
     3.1 --- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:50:22 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 12:00:11 2010 +0200
     3.3 @@ -64,13 +64,12 @@
     3.4  
     3.5  lemma MREC_rule:
     3.6    "MREC x = 
     3.7 -  (do y \<leftarrow> f x;
     3.8 +  do { y \<leftarrow> f x;
     3.9                  (case y of 
    3.10                  Inl r \<Rightarrow> return r
    3.11                | Inr s \<Rightarrow> 
    3.12 -                do z \<leftarrow> MREC s ;
    3.13 -                   g x s z
    3.14 -                done) done)"
    3.15 +                do { z \<leftarrow> MREC s ;
    3.16 +                     g x s z })}"
    3.17    unfolding MREC_def
    3.18    unfolding bind_def return_def
    3.19    apply simp
     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:50:22 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 12:00:11 2010 +0200
     4.3 @@ -48,12 +48,12 @@
     4.4    [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
     4.5  
     4.6  definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
     4.7 -  "change f r = (do
     4.8 +  "change f r = do {
     4.9       x \<leftarrow> ! r;
    4.10       let y = f x;
    4.11       r := y;
    4.12       return y
    4.13 -   done)"
    4.14 +   }"
    4.15  
    4.16  
    4.17  subsection {* Properties *}
     5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:50:22 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:00:11 2010 +0200
     5.3 @@ -12,14 +12,14 @@
     5.4  
     5.5  definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
     5.6  where
     5.7 -  "swap arr i j = (
     5.8 -     do
     5.9 +  "swap arr i j =
    5.10 +     do {
    5.11         x \<leftarrow> nth arr i;
    5.12         y \<leftarrow> nth arr j;
    5.13         upd i y arr;
    5.14         upd j x arr;
    5.15         return ()
    5.16 -     done)"
    5.17 +     }"
    5.18  
    5.19  lemma crel_swapI [crel_intros]:
    5.20    assumes "i < Array.length a h" "j < Array.length a h"
    5.21 @@ -40,12 +40,12 @@
    5.22  where
    5.23    "part1 a left right p = (
    5.24       if (right \<le> left) then return right
    5.25 -     else (do
    5.26 +     else do {
    5.27         v \<leftarrow> nth a left;
    5.28         (if (v \<le> p) then (part1 a (left + 1) right p)
    5.29 -                    else (do swap a left right;
    5.30 -  part1 a left (right - 1) p done))
    5.31 -     done))"
    5.32 +                    else (do { swap a left right;
    5.33 +  part1 a left (right - 1) p }))
    5.34 +     })"
    5.35  by pat_completeness auto
    5.36  
    5.37  termination
    5.38 @@ -227,14 +227,14 @@
    5.39  
    5.40  fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    5.41  where
    5.42 -  "partition a left right = (do
    5.43 +  "partition a left right = do {
    5.44       pivot \<leftarrow> nth a right;
    5.45       middle \<leftarrow> part1 a left (right - 1) pivot;
    5.46       v \<leftarrow> nth a middle;
    5.47       m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
    5.48       swap a m right;
    5.49       return m
    5.50 -   done)"
    5.51 +   }"
    5.52  
    5.53  declare partition.simps[simp del]
    5.54  
    5.55 @@ -402,12 +402,12 @@
    5.56  where
    5.57    "quicksort arr left right =
    5.58       (if (right > left)  then
    5.59 -        do
    5.60 +        do {
    5.61            pivotNewIndex \<leftarrow> partition arr left right;
    5.62            pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
    5.63            quicksort arr left (pivotNewIndex - 1);
    5.64            quicksort arr (pivotNewIndex + 1) right
    5.65 -        done
    5.66 +        }
    5.67       else return ())"
    5.68  by pat_completeness auto
    5.69  
    5.70 @@ -645,11 +645,11 @@
    5.71  
    5.72  subsection {* Example *}
    5.73  
    5.74 -definition "qsort a = do
    5.75 +definition "qsort a = do {
    5.76      k \<leftarrow> len a;
    5.77      quicksort a 0 (k - 1);
    5.78      return a
    5.79 -  done"
    5.80 +  }"
    5.81  
    5.82  code_reserved SML upto
    5.83  
     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:50:22 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:00:11 2010 +0200
     6.3 @@ -11,19 +11,19 @@
     6.4  hide_const (open) swap rev
     6.5  
     6.6  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
     6.7 -  "swap a i j = (do
     6.8 +  "swap a i j = do {
     6.9       x \<leftarrow> nth a i;
    6.10       y \<leftarrow> nth a j;
    6.11       upd i y a;
    6.12       upd j x a;
    6.13       return ()
    6.14 -   done)"
    6.15 +   }"
    6.16  
    6.17  fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    6.18 -  "rev a i j = (if (i < j) then (do
    6.19 +  "rev a i j = (if (i < j) then do {
    6.20       swap a i j;
    6.21       rev a (i + 1) (j - 1)
    6.22 -   done)
    6.23 +   }
    6.24     else return ())"
    6.25  
    6.26  notation (output) swap ("swap")
     7.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Jul 13 11:50:22 2010 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Jul 13 12:00:11 2010 +0200
     7.3 @@ -31,10 +31,10 @@
     7.4  primrec make_llist :: "'a\<Colon>heap list \<Rightarrow> 'a node Heap"
     7.5  where 
     7.6    [simp del]: "make_llist []     = return Empty"
     7.7 -            | "make_llist (x#xs) = do tl   \<leftarrow> make_llist xs;
     7.8 -                                      next \<leftarrow> ref tl;
     7.9 -                                      return (Node x next)
    7.10 -                                   done"
    7.11 +            | "make_llist (x#xs) = do { tl \<leftarrow> make_llist xs;
    7.12 +                                        next \<leftarrow> ref tl;
    7.13 +                                        return (Node x next)
    7.14 +                                   }"
    7.15  
    7.16  
    7.17  text {* define traverse using the MREC combinator *}
    7.18 @@ -43,18 +43,18 @@
    7.19    traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
    7.20  where
    7.21  [code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
    7.22 -                                | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
    7.23 -                                                  return (Inr tl) done))
    7.24 +                                | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
    7.25 +                                                  return (Inr tl) })
    7.26                     (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
    7.27                                        | Node x r \<Rightarrow> return (x # xs))"
    7.28  
    7.29  
    7.30  lemma traverse_simps[code, simp]:
    7.31    "traverse Empty      = return []"
    7.32 -  "traverse (Node x r) = do tl \<leftarrow> Ref.lookup r;
    7.33 -                            xs \<leftarrow> traverse tl;
    7.34 -                            return (x#xs)
    7.35 -                         done"
    7.36 +  "traverse (Node x r) = do { tl \<leftarrow> Ref.lookup r;
    7.37 +                              xs \<leftarrow> traverse tl;
    7.38 +                              return (x#xs)
    7.39 +                         }"
    7.40  unfolding traverse_def
    7.41  by (auto simp: traverse_def MREC_rule)
    7.42  
    7.43 @@ -529,25 +529,25 @@
    7.44  subsection {* Definition of in-place reversal *}
    7.45  
    7.46  definition rev' :: "(('a::heap) node ref \<times> 'a node ref) \<Rightarrow> 'a node ref Heap"
    7.47 -where "rev' = MREC (\<lambda>(q, p). do v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
    7.48 -                            | Node x next \<Rightarrow> do
    7.49 +where "rev' = MREC (\<lambda>(q, p). do { v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
    7.50 +                            | Node x next \<Rightarrow> do {
    7.51                                      p := Node x q;
    7.52                                      return (Inr (p, next))
    7.53 -                                  done) done)
    7.54 +                                  })})
    7.55               (\<lambda>x s z. return z)"
    7.56  
    7.57  lemma rev'_simps [code]:
    7.58    "rev' (q, p) =
    7.59 -   do
    7.60 +   do {
    7.61       v \<leftarrow> !p;
    7.62       (case v of
    7.63          Empty \<Rightarrow> return q
    7.64        | Node x next \<Rightarrow>
    7.65 -        do
    7.66 +        do {
    7.67            p := Node x q;
    7.68            rev' (p, next)
    7.69 -        done)
    7.70 -  done"
    7.71 +        })
    7.72 +  }"
    7.73    unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
    7.74  thm arg_cong2
    7.75    by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
    7.76 @@ -555,7 +555,7 @@
    7.77  primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
    7.78  where
    7.79    "rev Empty = return Empty"
    7.80 -| "rev (Node x n) = (do q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v done)"
    7.81 +| "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v }"
    7.82  
    7.83  subsection {* Correctness Proof *}
    7.84  
    7.85 @@ -680,7 +680,7 @@
    7.86  
    7.87  definition merge' :: "(('a::{heap, ord}) node ref * ('a::{heap, ord})) * ('a::{heap, ord}) node ref * ('a::{heap, ord}) node ref \<Rightarrow> ('a::{heap, ord}) node ref Heap"
    7.88  where
    7.89 -"merge' = MREC (\<lambda>(_, p, q). (do v \<leftarrow> !p; w \<leftarrow> !q;
    7.90 +"merge' = MREC (\<lambda>(_, p, q). do { v \<leftarrow> !p; w \<leftarrow> !q;
    7.91    (case v of Empty \<Rightarrow> return (Inl q)
    7.92            | Node valp np \<Rightarrow>
    7.93              (case w of Empty \<Rightarrow> return (Inl p)
    7.94 @@ -688,8 +688,8 @@
    7.95                         if (valp \<le> valq) then
    7.96                           return (Inr ((p, valp), np, q))
    7.97                         else
    7.98 -                         return (Inr ((q, valq), p, nq)))) done))
    7.99 - (\<lambda> _ ((n, v), _, _) r. do n := Node v r; return n done)"
   7.100 +                         return (Inr ((q, valq), p, nq)))) })
   7.101 + (\<lambda> _ ((n, v), _, _) r. do { n := Node v r; return n })"
   7.102  
   7.103  definition merge where "merge p q = merge' (undefined, p, q)"
   7.104  
   7.105 @@ -713,21 +713,21 @@
   7.106  term "Ref.change"
   7.107  lemma merge_simps [code]:
   7.108  shows "merge p q =
   7.109 -do v \<leftarrow> !p;
   7.110 +do { v \<leftarrow> !p;
   7.111     w \<leftarrow> !q;
   7.112     (case v of node.Empty \<Rightarrow> return q
   7.113      | Node valp np \<Rightarrow>
   7.114          case w of node.Empty \<Rightarrow> return p
   7.115          | Node valq nq \<Rightarrow>
   7.116 -            if valp \<le> valq then do r \<leftarrow> merge np q;
   7.117 +            if valp \<le> valq then do { r \<leftarrow> merge np q;
   7.118                                     p := (Node valp r);
   7.119                                     return p
   7.120 -                                done
   7.121 -            else do r \<leftarrow> merge p nq;
   7.122 +                                }
   7.123 +            else do { r \<leftarrow> merge p nq;
   7.124                      q := (Node valq r);
   7.125                      return q
   7.126 -                 done)
   7.127 -done"
   7.128 +                 })
   7.129 +}"
   7.130  proof -
   7.131    {fix v x y
   7.132      have case_return: "(case v of Empty \<Rightarrow> return x | Node v n \<Rightarrow> return (y v n)) = return (case v of Empty \<Rightarrow> x | Node v n \<Rightarrow> y v n)" by (cases v) auto
   7.133 @@ -997,11 +997,11 @@
   7.134  
   7.135  text {* A simple example program *}
   7.136  
   7.137 -definition test_1 where "test_1 = (do ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs done)" 
   7.138 -definition test_2 where "test_2 = (do ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys done)"
   7.139 +definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
   7.140 +definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
   7.141  
   7.142  definition test_3 where "test_3 =
   7.143 -  (do
   7.144 +  (do {
   7.145      ll_xs \<leftarrow> make_llist (filter (%n. n mod 2 = 0) [2..8]);
   7.146      ll_ys \<leftarrow> make_llist (filter (%n. n mod 2 = 1) [5..11]);
   7.147      r \<leftarrow> ref ll_xs;
   7.148 @@ -1010,7 +1010,7 @@
   7.149      ll_zs \<leftarrow> !p;
   7.150      zs \<leftarrow> traverse ll_zs;
   7.151      return zs
   7.152 -  done)"
   7.153 +  })"
   7.154  
   7.155  code_reserved SML upto
   7.156  
     8.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 11:50:22 2010 +0200
     8.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:00:11 2010 +0200
     8.3 @@ -174,15 +174,15 @@
     8.4  primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
     8.5  where
     8.6    "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
     8.7 -| "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
     8.8 +| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })"
     8.9  
    8.10  fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    8.11  where
    8.12    "resolve1 l (x#xs) (y#ys) =
    8.13    (if (x = l) then return (merge xs (y#ys))
    8.14 -  else (if (x < y) then (do v \<leftarrow> resolve1 l xs (y#ys); return (x # v) done)
    8.15 -  else (if (x > y) then (do v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) done)
    8.16 -  else (do v \<leftarrow> resolve1 l xs ys; return (x # v) done))))"
    8.17 +  else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) }
    8.18 +  else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) }
    8.19 +  else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))"
    8.20  | "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''"
    8.21  | "resolve1 l xs [] = res_mem l xs"
    8.22  
    8.23 @@ -190,9 +190,9 @@
    8.24  where
    8.25    "resolve2 l (x#xs) (y#ys) =
    8.26    (if (y = l) then return (merge (x#xs) ys)
    8.27 -  else (if (x < y) then (do v \<leftarrow> resolve2 l xs (y#ys); return (x # v) done)
    8.28 -  else (if (x > y) then (do v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) done) 
    8.29 -  else (do v \<leftarrow> resolve2 l xs ys; return (x # v) done))))"
    8.30 +  else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) }
    8.31 +  else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) }
    8.32 +  else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))"
    8.33    | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
    8.34    | "resolve2 l [] ys = res_mem l ys"
    8.35  
    8.36 @@ -413,10 +413,10 @@
    8.37  definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
    8.38  where
    8.39    "get_clause a i = 
    8.40 -       (do c \<leftarrow> nth a i;
    8.41 +       do { c \<leftarrow> nth a i;
    8.42             (case c of None \<Rightarrow> raise (''Clause not found'')
    8.43                      | Some x \<Rightarrow> return x)
    8.44 -        done)"
    8.45 +       }"
    8.46  
    8.47  
    8.48  primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    8.49 @@ -424,9 +424,9 @@
    8.50    "res_thm2 a (l, j) cli =
    8.51    ( if l = 0 then raise(''Illegal literal'')
    8.52      else
    8.53 -     (do clj \<leftarrow> get_clause a j;
    8.54 +     do { clj \<leftarrow> get_clause a j;
    8.55           res_thm' l cli clj
    8.56 -      done))"
    8.57 +     })"
    8.58  
    8.59  primrec
    8.60    foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
    8.61 @@ -437,27 +437,27 @@
    8.62  fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
    8.63  where
    8.64    "doProofStep2 a (Conflict saveTo (i, rs)) rcs =
    8.65 -  (do
    8.66 +  do {
    8.67       cli \<leftarrow> get_clause a i;
    8.68       result \<leftarrow> foldM (res_thm2 a) rs cli;
    8.69       upd saveTo (Some result) a; 
    8.70       return rcs
    8.71 -   done)"
    8.72 -| "doProofStep2 a (Delete cid) rcs = (do upd cid None a; return rcs done)"
    8.73 -| "doProofStep2 a (Root cid clause) rcs = (do upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
    8.74 +  }"
    8.75 +| "doProofStep2 a (Delete cid) rcs = do { upd cid None a; return rcs }"
    8.76 +| "doProofStep2 a (Root cid clause) rcs = do { upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
    8.77  | "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
    8.78  | "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
    8.79  
    8.80  definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
    8.81  where
    8.82    "checker n p i =
    8.83 -  (do 
    8.84 +  do {
    8.85       a \<leftarrow> Array.new n None;
    8.86       rcs \<leftarrow> foldM (doProofStep2 a) p [];
    8.87       ec \<leftarrow> Array.nth a i;
    8.88       (if ec = Some [] then return rcs 
    8.89                  else raise(''No empty clause''))
    8.90 -   done)"
    8.91 +  }"
    8.92  
    8.93  lemma crel_option_case:
    8.94    assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
    8.95 @@ -651,10 +651,10 @@
    8.96    "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
    8.97       (case (xs ! i) of
    8.98         None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
    8.99 -     | Some cli \<Rightarrow> (do
   8.100 +     | Some cli \<Rightarrow> do {
   8.101                        result \<leftarrow> foldM (lres_thm xs) rs cli ;
   8.102                        return ((xs[saveTo:=Some result]), rcl)
   8.103 -                    done))"
   8.104 +                   })"
   8.105  | "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)"
   8.106  | "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)"
   8.107  | "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   8.108 @@ -663,11 +663,11 @@
   8.109  definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
   8.110  where
   8.111    "lchecker n p i =
   8.112 -  (do 
   8.113 +  do {
   8.114       rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
   8.115       (if (fst rcs ! i) = Some [] then return (snd rcs) 
   8.116                  else raise(''No empty clause''))
   8.117 -   done)"
   8.118 +  }"
   8.119  
   8.120  
   8.121  section {* Functional version with RedBlackTrees *}
   8.122 @@ -684,10 +684,10 @@
   8.123    "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
   8.124       (case (RBT_Impl.lookup t i) of
   8.125         None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
   8.126 -     | Some cli \<Rightarrow> (do
   8.127 +     | Some cli \<Rightarrow> do {
   8.128                        result \<leftarrow> foldM (tres_thm t) rs cli;
   8.129                        return ((RBT_Impl.insert saveTo result t), rcl)
   8.130 -                    done))"
   8.131 +                   })"
   8.132  | "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)"
   8.133  | "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
   8.134  | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   8.135 @@ -696,11 +696,11 @@
   8.136  definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
   8.137  where
   8.138    "tchecker n p i =
   8.139 -  (do 
   8.140 +  do {
   8.141       rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
   8.142       (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) 
   8.143                  else raise(''No empty clause''))
   8.144 -   done)"
   8.145 +  }"
   8.146  
   8.147  section {* Code generation setup *}
   8.148