# HG changeset patch
# User haftmann
# Date 1279015520 -7200
# Node ID 96551d6b1414ffa238ff86921b5629d40e4e0c2c
# Parent  46c21c1f8cb0415648bbc15f7873994bc109969a# Parent  08bd610b25839e8b8666f4d0f8c2338a653248a3
merged

diff -r 08bd610b2583 -r 96551d6b1414 Admin/isatest/settings/afp-mac-poly-M4
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/afp-mac-poly-M4	Tue Jul 13 12:05:20 2010 +0200
@@ -0,0 +1,28 @@
+# -*- shell-script -*- :mode=shellscript:
+
+  POLYML_HOME="/home/polyml/polyml-5.3.0"
+  ML_SYSTEM="polyml-5.3.0"
+  ML_PLATFORM="x86-darwin"
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="--mutable 400 --immutable 400"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
+
+init_component "$HOME/contrib_devel/kodkodi"
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Extraction/Higman.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -350,15 +350,14 @@
 end
 
 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word_aux k = (do
+  "mk_word_aux k = (do {
      i \<leftarrow> Random.range 10;
      (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
-     else do
+     else do {
        let l = (if i mod 2 = 0 then A else B);
        ls \<leftarrow> mk_word_aux (Suc k);
        return (l # ls)
-     done)
-   done)"
+     })})"
 by pat_completeness auto
 termination by (relation "measure ((op -) 1001)") auto
 
@@ -367,10 +366,10 @@
 
 primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word_s 0 = mk_word"
-  | "mk_word_s (Suc n) = (do
+  | "mk_word_s (Suc n) = (do {
        _ \<leftarrow> mk_word;
        mk_word_s n
-     done)"
+     })"
 
 definition g1 :: "nat \<Rightarrow> letter list" where
   "g1 s = fst (mk_word_s s (20000, 1))"
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -35,8 +35,9 @@
   length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
   "length a h = List.length (get_array a h)"
   
-definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
-  "update a i x h = set_array a ((get_array a h)[i:=x]) h"
+definition (*FIXME update*)
+  change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
 
 definition (*FIXME noteq*)
   noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
@@ -63,15 +64,15 @@
 
 definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
   [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
-    (\<lambda>h. (a, update a i x h))"
+    (\<lambda>h. (a, change a i x h))"
 
 definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
   [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
-    (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
+    (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))"
 
 definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
   [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
-    (\<lambda>h. (get_array a h ! i, update a i x h))"
+    (\<lambda>h. (get_array a h ! i, change a i x h))"
 
 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
   [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
@@ -108,27 +109,27 @@
   "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
   by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
 
-lemma get_array_update_eq [simp]:
-  "get_array a (update a i v h) = (get_array a h) [i := v]"
-  by (simp add: update_def)
+lemma get_array_change_eq [simp]:
+  "get_array a (change a i v h) = (get_array a h) [i := v]"
+  by (simp add: change_def)
 
-lemma nth_update_array_neq_array [simp]:
-  "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
-  by (simp add: update_def noteq_arrs_def)
+lemma nth_change_array_neq_array [simp]:
+  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
+  by (simp add: change_def noteq_arrs_def)
 
-lemma get_arry_array_update_elem_neqIndex [simp]:
-  "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
+lemma get_arry_array_change_elem_neqIndex [simp]:
+  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
   by simp
 
-lemma length_update [simp]: 
-  "length a (update b i v h) = length a h"
-  by (simp add: update_def length_def set_array_def get_array_def)
+lemma length_change [simp]: 
+  "length a (change b i v h) = length a h"
+  by (simp add: change_def length_def set_array_def get_array_def)
 
-lemma update_swap_neqArray:
+lemma change_swap_neqArray:
   "a =!!= a' \<Longrightarrow> 
-  update a i v (update a' i' v' h) 
-  = update a' i' v' (update a i v h)"
-apply (unfold update_def)
+  change a i v (change a' i' v' h) 
+  = change a' i' v' (change a i v h)"
+apply (unfold change_def)
 apply simp
 apply (subst array_set_set_swap, assumption)
 apply (subst array_get_set_neq)
@@ -136,9 +137,9 @@
 apply (simp)
 done
 
-lemma update_swap_neqIndex:
-  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
-  by (auto simp add: update_def array_set_set_swap list_update_swap)
+lemma change_swap_neqIndex:
+  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
+  by (auto simp add: change_def array_set_set_swap list_update_swap)
 
 lemma get_array_init_array_list:
   "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
@@ -150,9 +151,9 @@
        = snd (array new_ls h)"
   by (simp add: Let_def split_def array_def)
 
-lemma array_present_update [simp]: 
-  "array_present a (update b i v h) = array_present a h"
-  by (simp add: update_def array_present_def set_array_def get_array_def)
+lemma array_present_change [simp]: 
+  "array_present a (change b i v h) = array_present a h"
+  by (simp add: change_def array_present_def set_array_def get_array_def)
 
 lemma array_present_array [simp]:
   "array_present (fst (array xs h)) (snd (array xs h))"
@@ -263,7 +264,7 @@
 
 lemma execute_upd [execute_simps]:
   "i < length a h \<Longrightarrow>
-    execute (upd i x a) h = Some (a, update a i x h)"
+    execute (upd i x a) h = Some (a, change a i x h)"
   "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   by (simp_all add: upd_def execute_simps)
 
@@ -272,20 +273,20 @@
   by (auto intro: success_intros simp add: upd_def)
 
 lemma crel_updI [crel_intros]:
-  assumes "i < length a h" "h' = update a i v h"
+  assumes "i < length a h" "h' = change a i v h"
   shows "crel (upd i v a) h h' a"
   by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_updE [crel_elims]:
   assumes "crel (upd i v a) h h' r"
-  obtains "r = a" "h' = update a i v h" "i < length a h"
+  obtains "r = a" "h' = change a i v h" "i < length a h"
   using assms by (rule crelE)
     (erule successE, cases "i < length a h", simp_all add: execute_simps)
 
 lemma execute_map_entry [execute_simps]:
   "i < length a h \<Longrightarrow>
    execute (map_entry i f a) h =
-      Some (a, update a i (f (get_array a h ! i)) h)"
+      Some (a, change a i (f (get_array a h ! i)) h)"
   "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   by (simp_all add: map_entry_def execute_simps)
 
@@ -294,20 +295,20 @@
   by (auto intro: success_intros simp add: map_entry_def)
 
 lemma crel_map_entryI [crel_intros]:
-  assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
+  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
   shows "crel (map_entry i f a) h h' r"
   by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_map_entryE [crel_elims]:
   assumes "crel (map_entry i f a) h h' r"
-  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h"
+  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
   using assms by (rule crelE)
     (erule successE, cases "i < length a h", simp_all add: execute_simps)
 
 lemma execute_swap [execute_simps]:
   "i < length a h \<Longrightarrow>
    execute (swap i x a) h =
-      Some (get_array a h ! i, update a i x h)"
+      Some (get_array a h ! i, change a i x h)"
   "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   by (simp_all add: swap_def execute_simps)
 
@@ -316,13 +317,13 @@
   by (auto intro: success_intros simp add: swap_def)
 
 lemma crel_swapI [crel_intros]:
-  assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
+  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
   shows "crel (swap i x a) h h' r"
   by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_swapE [crel_elims]:
   assumes "crel (swap i x a) h h' r"
-  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
+  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
   using assms by (rule crelE)
     (erule successE, cases "i < length a h", simp_all add: execute_simps)
 
@@ -356,7 +357,7 @@
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   by (rule Heap_eqI) (simp add: map_nth execute_simps)
 
-hide_const (open) update new of_list make len nth upd map_entry swap freeze
+hide_const (open) new
 
 
 subsection {* Code generator setup *}
@@ -406,25 +407,25 @@
   by (simp add: upd'_def upd_return)
 
 lemma [code]:
-  "Array.map_entry i f a = (do
-     x \<leftarrow> Array.nth a i;
-     Array.upd i (f x) a
-   done)"
+  "map_entry i f a = do {
+     x \<leftarrow> nth a i;
+     upd i (f x) a
+   }"
   by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
 
 lemma [code]:
-  "Array.swap i x a = (do
-     y \<leftarrow> Array.nth a i;
-     Array.upd i x a;
+  "swap i x a = do {
+     y \<leftarrow> nth a i;
+     upd i x a;
      return y
-   done)"
+   }"
   by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
 
 lemma [code]:
-  "Array.freeze a = (do
-     n \<leftarrow> Array.len a;
-     Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n]
-   done)"
+  "freeze a = do {
+     n \<leftarrow> len a;
+     Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
+   }"
 proof (rule Heap_eqI)
   fix h
   have *: "List.map
@@ -439,15 +440,15 @@
     apply (simp_all add: nth_def guard_def *)
     apply (simp add: length_def map_nth)
     done
-  then have "execute (do
-      n \<leftarrow> Array.len a;
+  then have "execute (do {
+      n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
-    done) h = Some (get_array a h, h)"
+    }) h = Some (get_array a h, h)"
     by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
-  then show "execute (Array.freeze a) h = execute (do
-      n \<leftarrow> Array.len a;
+  then show "execute (freeze a) h = execute (do {
+      n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
-    done) h" by (simp add: execute_simps)
+    }) h" by (simp add: execute_simps)
 qed
 
 hide_const (open) new' of_list' make' len' nth' upd'
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -5,7 +5,7 @@
 header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
 
 theory Heap_Monad
-imports Heap
+imports Heap Monad_Syntax
 begin
 
 subsection {* The monad *}
@@ -259,12 +259,16 @@
   obtains "False"
   using assms by (rule crelE) (simp add: success_def execute_simps)
 
-definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
-  [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
+definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
+  [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
                   Some (x, h') \<Rightarrow> execute (g x) h'
                 | None \<Rightarrow> None)"
 
-notation bind (infixl "\<guillemotright>=" 54)
+setup {*
+  Adhoc_Overloading.add_variant 
+    @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind}
+*}
+
 
 lemma execute_bind [execute_simps]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
@@ -314,92 +318,6 @@
 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   by (rule Heap_eqI) (simp add: execute_simps)
 
-abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
-  "f >> g \<equiv> f >>= (\<lambda>_. g)"
-
-notation chain (infixl "\<guillemotright>" 54)
-
-
-subsubsection {* do-syntax *}
-
-text {*
-  We provide a convenient do-notation for monadic expressions
-  well-known from Haskell.  @{const Let} is printed
-  specially in do-expressions.
-*}
-
-nonterminals do_expr
-
-syntax
-  "_do" :: "do_expr \<Rightarrow> 'a"
-    ("(do (_)//done)" [12] 100)
-  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ <- _;//_" [1000, 13, 12] 12)
-  "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_;//_" [13, 12] 12)
-  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("let _ = _;//_" [1000, 13, 12] 12)
-  "_nil" :: "'a \<Rightarrow> do_expr"
-    ("_" [12] 12)
-
-syntax (xsymbols)
-  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
-
-translations
-  "_do f" => "f"
-  "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
-  "_chain f g" => "f \<guillemotright> g"
-  "_let x t f" => "CONST Let t (\<lambda>x. f)"
-  "_nil f" => "f"
-
-print_translation {*
-let
-  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
-        let
-          val (v, t) = Syntax.variant_abs abs;
-        in (Free (v, ty), t) end
-    | dest_abs_eta t =
-        let
-          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
-        in (Free (v, dummyT), t) end;
-  fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-          val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
-          val v_used = fold_aterms
-            (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
-        in if v_used then
-          Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
-        else
-          Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
-        end
-    | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
-        Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
-    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
-    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
-        Const (@{const_syntax return}, dummyT) $ f
-    | unfold_monad f = f;
-  fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
-    | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
-        contains_bind t;
-  fun bind_monad_tr' (f::g::ts) = list_comb
-    (Const (@{syntax_const "_do"}, dummyT) $
-      unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
-  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
-    if contains_bind g' then list_comb
-      (Const (@{syntax_const "_do"}, dummyT) $
-        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
-    else raise Match;
-in
- [(@{const_syntax bind}, bind_monad_tr'),
-  (@{const_syntax Let}, Let_monad_tr')]
-end;
-*}
-
 
 subsection {* Generic combinators *}
 
@@ -451,11 +369,11 @@
 
 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   "fold_map f [] = return []"
-| "fold_map f (x # xs) = do
+| "fold_map f (x # xs) = do {
      y \<leftarrow> f x;
      ys \<leftarrow> fold_map f xs;
      return (y # ys)
-   done"
+   }"
 
 lemma fold_map_append:
   "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
@@ -611,7 +529,7 @@
 text {* Monad *}
 
 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
-code_monad "op \<guillemotright>=" Haskell
+code_monad bind Haskell
 code_const return (Haskell "return")
 code_const Heap_Monad.raise' (Haskell "error/ _")
 
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/Mrec.thy
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -64,13 +64,12 @@
 
 lemma MREC_rule:
   "MREC x = 
-  (do y \<leftarrow> f x;
+  do { y \<leftarrow> f x;
                 (case y of 
                 Inl r \<Rightarrow> return r
               | Inr s \<Rightarrow> 
-                do z \<leftarrow> MREC s ;
-                   g x s z
-                done) done)"
+                do { z \<leftarrow> MREC s ;
+                     g x s z })}"
   unfolding MREC_def
   unfolding bind_def return_def
   apply simp
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -48,12 +48,12 @@
   [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
 
 definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
-  "change f r = (do
+  "change f r = do {
      x \<leftarrow> ! r;
      let y = f x;
      r := y;
      return y
-   done)"
+   }"
 
 
 subsection {* Properties *}
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -12,19 +12,19 @@
 
 definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
 where
-  "swap arr i j = (
-     do
-       x \<leftarrow> Array.nth arr i;
-       y \<leftarrow> Array.nth arr j;
-       Array.upd i y arr;
-       Array.upd j x arr;
+  "swap arr i j =
+     do {
+       x \<leftarrow> nth arr i;
+       y \<leftarrow> nth arr j;
+       upd i y arr;
+       upd j x arr;
        return ()
-     done)"
+     }"
 
 lemma crel_swapI [crel_intros]:
   assumes "i < Array.length a h" "j < Array.length a h"
     "x = get_array a h ! i" "y = get_array a h ! j"
-    "h' = Array.update a j x (Array.update a i y h)"
+    "h' = Array.change a j x (Array.change a i y h)"
   shows "crel (swap a i j) h h' r"
   unfolding swap_def using assms by (auto intro!: crel_intros)
 
@@ -40,12 +40,12 @@
 where
   "part1 a left right p = (
      if (right \<le> left) then return right
-     else (do
-       v \<leftarrow> Array.nth a left;
+     else do {
+       v \<leftarrow> nth a left;
        (if (v \<le> p) then (part1 a (left + 1) right p)
-                    else (do swap a left right;
-  part1 a left (right - 1) p done))
-     done))"
+                    else (do { swap a left right;
+  part1 a left (right - 1) p }))
+     })"
 by pat_completeness auto
 
 termination
@@ -227,14 +227,14 @@
 
 fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
-  "partition a left right = (do
-     pivot \<leftarrow> Array.nth a right;
+  "partition a left right = do {
+     pivot \<leftarrow> nth a right;
      middle \<leftarrow> part1 a left (right - 1) pivot;
-     v \<leftarrow> Array.nth a middle;
+     v \<leftarrow> nth a middle;
      m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
      swap a m right;
      return m
-   done)"
+   }"
 
 declare partition.simps[simp del]
 
@@ -294,8 +294,8 @@
          else middle)"
     unfolding partition.simps
     by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
-  from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
-    (Array.update a rs (get_array a h1 ! r) h1)"
+  from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
+    (Array.change a rs (get_array a h1 ! r) h1)"
     unfolding swap_def
     by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
@@ -326,7 +326,7 @@
       with part_partitions[OF part] right_remains True
       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
       with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
-        unfolding Array.update_def Array.length_def by simp
+        unfolding Array.change_def Array.length_def by simp
     }
     moreover
     {
@@ -352,7 +352,7 @@
           by fastsimp
         with i_is True rs_equals right_remains h'_def
         show ?thesis using in_bounds
-          unfolding Array.update_def Array.length_def
+          unfolding Array.change_def Array.length_def
           by auto
       qed
     }
@@ -368,7 +368,7 @@
       from part_partitions[OF part] rs_equals right_remains i_is_left
       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
       with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
-        unfolding Array.update_def by simp
+        unfolding Array.change_def by simp
     }
     moreover
     {
@@ -388,7 +388,7 @@
         assume i_is: "i = r"
         from i_is False rs_equals right_remains h'_def
         show ?thesis using in_bounds
-          unfolding Array.update_def Array.length_def
+          unfolding Array.change_def Array.length_def
           by auto
       qed
     }
@@ -402,12 +402,12 @@
 where
   "quicksort arr left right =
      (if (right > left)  then
-        do
+        do {
           pivotNewIndex \<leftarrow> partition arr left right;
           pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
           quicksort arr left (pivotNewIndex - 1);
           quicksort arr (pivotNewIndex + 1) right
-        done
+        }
      else return ())"
 by pat_completeness auto
 
@@ -645,11 +645,11 @@
 
 subsection {* Example *}
 
-definition "qsort a = do
-    k \<leftarrow> Array.len a;
+definition "qsort a = do {
+    k \<leftarrow> len a;
     quicksort a 0 (k - 1);
     return a
-  done"
+  }"
 
 code_reserved SML upto
 
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -8,20 +8,22 @@
 imports Imperative_HOL Subarray
 begin
 
+hide_const (open) swap rev
+
 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
-  "swap a i j = (do
-     x \<leftarrow> Array.nth a i;
-     y \<leftarrow> Array.nth a j;
-     Array.upd i y a;
-     Array.upd j x a;
+  "swap a i j = do {
+     x \<leftarrow> nth a i;
+     y \<leftarrow> nth a j;
+     upd i y a;
+     upd j x a;
      return ()
-   done)"
+   }"
 
 fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
-  "rev a i j = (if (i < j) then (do
+  "rev a i j = (if (i < j) then do {
      swap a i j;
      rev a (i + 1) (j - 1)
-   done)
+   }
    else return ())"
 
 notation (output) swap ("swap")
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -31,10 +31,10 @@
 primrec make_llist :: "'a\<Colon>heap list \<Rightarrow> 'a node Heap"
 where 
   [simp del]: "make_llist []     = return Empty"
-            | "make_llist (x#xs) = do tl   \<leftarrow> make_llist xs;
-                                      next \<leftarrow> ref tl;
-                                      return (Node x next)
-                                   done"
+            | "make_llist (x#xs) = do { tl \<leftarrow> make_llist xs;
+                                        next \<leftarrow> ref tl;
+                                        return (Node x next)
+                                   }"
 
 
 text {* define traverse using the MREC combinator *}
@@ -43,18 +43,18 @@
   traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
 where
 [code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
-                                | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
-                                                  return (Inr tl) done))
+                                | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
+                                                  return (Inr tl) })
                    (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
                                       | Node x r \<Rightarrow> return (x # xs))"
 
 
 lemma traverse_simps[code, simp]:
   "traverse Empty      = return []"
-  "traverse (Node x r) = do tl \<leftarrow> Ref.lookup r;
-                            xs \<leftarrow> traverse tl;
-                            return (x#xs)
-                         done"
+  "traverse (Node x r) = do { tl \<leftarrow> Ref.lookup r;
+                              xs \<leftarrow> traverse tl;
+                              return (x#xs)
+                         }"
 unfolding traverse_def
 by (auto simp: traverse_def MREC_rule)
 
@@ -529,25 +529,25 @@
 subsection {* Definition of in-place reversal *}
 
 definition rev' :: "(('a::heap) node ref \<times> 'a node ref) \<Rightarrow> 'a node ref Heap"
-where "rev' = MREC (\<lambda>(q, p). do v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
-                            | Node x next \<Rightarrow> do
+where "rev' = MREC (\<lambda>(q, p). do { v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
+                            | Node x next \<Rightarrow> do {
                                     p := Node x q;
                                     return (Inr (p, next))
-                                  done) done)
+                                  })})
              (\<lambda>x s z. return z)"
 
 lemma rev'_simps [code]:
   "rev' (q, p) =
-   do
+   do {
      v \<leftarrow> !p;
      (case v of
         Empty \<Rightarrow> return q
       | Node x next \<Rightarrow>
-        do
+        do {
           p := Node x q;
           rev' (p, next)
-        done)
-  done"
+        })
+  }"
   unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
 thm arg_cong2
   by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
@@ -555,7 +555,7 @@
 primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
 where
   "rev Empty = return Empty"
-| "rev (Node x n) = (do q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v done)"
+| "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v }"
 
 subsection {* Correctness Proof *}
 
@@ -680,7 +680,7 @@
 
 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"
 where
-"merge' = MREC (\<lambda>(_, p, q). (do v \<leftarrow> !p; w \<leftarrow> !q;
+"merge' = MREC (\<lambda>(_, p, q). do { v \<leftarrow> !p; w \<leftarrow> !q;
   (case v of Empty \<Rightarrow> return (Inl q)
           | Node valp np \<Rightarrow>
             (case w of Empty \<Rightarrow> return (Inl p)
@@ -688,8 +688,8 @@
                        if (valp \<le> valq) then
                          return (Inr ((p, valp), np, q))
                        else
-                         return (Inr ((q, valq), p, nq)))) done))
- (\<lambda> _ ((n, v), _, _) r. do n := Node v r; return n done)"
+                         return (Inr ((q, valq), p, nq)))) })
+ (\<lambda> _ ((n, v), _, _) r. do { n := Node v r; return n })"
 
 definition merge where "merge p q = merge' (undefined, p, q)"
 
@@ -713,21 +713,21 @@
 term "Ref.change"
 lemma merge_simps [code]:
 shows "merge p q =
-do v \<leftarrow> !p;
+do { v \<leftarrow> !p;
    w \<leftarrow> !q;
    (case v of node.Empty \<Rightarrow> return q
     | Node valp np \<Rightarrow>
         case w of node.Empty \<Rightarrow> return p
         | Node valq nq \<Rightarrow>
-            if valp \<le> valq then do r \<leftarrow> merge np q;
+            if valp \<le> valq then do { r \<leftarrow> merge np q;
                                    p := (Node valp r);
                                    return p
-                                done
-            else do r \<leftarrow> merge p nq;
+                                }
+            else do { r \<leftarrow> merge p nq;
                     q := (Node valq r);
                     return q
-                 done)
-done"
+                 })
+}"
 proof -
   {fix v x y
     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
@@ -997,11 +997,11 @@
 
 text {* A simple example program *}
 
-definition test_1 where "test_1 = (do ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs done)" 
-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)"
+definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
+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 })"
 
 definition test_3 where "test_3 =
-  (do
+  (do {
     ll_xs \<leftarrow> make_llist (filter (%n. n mod 2 = 0) [2..8]);
     ll_ys \<leftarrow> make_llist (filter (%n. n mod 2 = 1) [5..11]);
     r \<leftarrow> ref ll_xs;
@@ -1010,7 +1010,7 @@
     ll_zs \<leftarrow> !p;
     zs \<leftarrow> traverse ll_zs;
     return zs
-  done)"
+  })"
 
 code_reserved SML upto
 
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -127,21 +127,21 @@
 unfolding array_ran_def Array.length_def by simp
 
 lemma array_ran_upd_array_Some:
-  assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
+  assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
   shows "cl \<in> array_ran a h \<or> cl = b"
 proof -
   have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
   with assms show ?thesis 
-    unfolding array_ran_def Array.update_def by fastsimp
+    unfolding array_ran_def Array.change_def by fastsimp
 qed
 
 lemma array_ran_upd_array_None:
-  assumes "cl \<in> array_ran a (Array.update a i None h)"
+  assumes "cl \<in> array_ran a (Array.change a i None h)"
   shows "cl \<in> array_ran a h"
 proof -
   have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
   with assms show ?thesis
-    unfolding array_ran_def Array.update_def by auto
+    unfolding array_ran_def Array.change_def by auto
 qed
 
 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
@@ -152,7 +152,7 @@
 lemma correctArray_update:
   assumes "correctArray rcs a h"
   assumes "correctClause rcs c" "sorted c" "distinct c"
-  shows "correctArray rcs a (Array.update a i (Some c) h)"
+  shows "correctArray rcs a (Array.change a i (Some c) h)"
   using assms
   unfolding correctArray_def
   by (auto dest:array_ran_upd_array_Some)
@@ -174,15 +174,15 @@
 primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
   "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
-| "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
+| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })"
 
 fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
   "resolve1 l (x#xs) (y#ys) =
   (if (x = l) then return (merge xs (y#ys))
-  else (if (x < y) then (do v \<leftarrow> resolve1 l xs (y#ys); return (x # v) done)
-  else (if (x > y) then (do v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) done)
-  else (do v \<leftarrow> resolve1 l xs ys; return (x # v) done))))"
+  else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) }
+  else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) }
+  else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))"
 | "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''"
 | "resolve1 l xs [] = res_mem l xs"
 
@@ -190,9 +190,9 @@
 where
   "resolve2 l (x#xs) (y#ys) =
   (if (y = l) then return (merge (x#xs) ys)
-  else (if (x < y) then (do v \<leftarrow> resolve2 l xs (y#ys); return (x # v) done)
-  else (if (x > y) then (do v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) done) 
-  else (do v \<leftarrow> resolve2 l xs ys; return (x # v) done))))"
+  else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) }
+  else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) }
+  else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))"
   | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
   | "resolve2 l [] ys = res_mem l ys"
 
@@ -413,10 +413,10 @@
 definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
 where
   "get_clause a i = 
-       (do c \<leftarrow> Array.nth a i;
+       do { c \<leftarrow> nth a i;
            (case c of None \<Rightarrow> raise (''Clause not found'')
                     | Some x \<Rightarrow> return x)
-        done)"
+       }"
 
 
 primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
@@ -424,9 +424,9 @@
   "res_thm2 a (l, j) cli =
   ( if l = 0 then raise(''Illegal literal'')
     else
-     (do clj \<leftarrow> get_clause a j;
+     do { clj \<leftarrow> get_clause a j;
          res_thm' l cli clj
-      done))"
+     })"
 
 primrec
   foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
@@ -437,27 +437,27 @@
 fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
 where
   "doProofStep2 a (Conflict saveTo (i, rs)) rcs =
-  (do
+  do {
      cli \<leftarrow> get_clause a i;
      result \<leftarrow> foldM (res_thm2 a) rs cli;
-     Array.upd saveTo (Some result) a; 
+     upd saveTo (Some result) a; 
      return rcs
-   done)"
-| "doProofStep2 a (Delete cid) rcs = (do Array.upd cid None a; return rcs done)"
-| "doProofStep2 a (Root cid clause) rcs = (do Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
+  }"
+| "doProofStep2 a (Delete cid) rcs = do { upd cid None a; return rcs }"
+| "doProofStep2 a (Root cid clause) rcs = do { upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
 | "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
 | "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
 
 definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
 where
   "checker n p i =
-  (do 
+  do {
      a \<leftarrow> Array.new n None;
      rcs \<leftarrow> foldM (doProofStep2 a) p [];
      ec \<leftarrow> Array.nth a i;
      (if ec = Some [] then return rcs 
                 else raise(''No empty clause''))
-   done)"
+  }"
 
 lemma crel_option_case:
   assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
@@ -651,10 +651,10 @@
   "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
      (case (xs ! i) of
        None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
-     | Some cli \<Rightarrow> (do
+     | Some cli \<Rightarrow> do {
                       result \<leftarrow> foldM (lres_thm xs) rs cli ;
                       return ((xs[saveTo:=Some result]), rcl)
-                    done))"
+                   })"
 | "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)"
 | "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)"
 | "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
@@ -663,11 +663,11 @@
 definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
 where
   "lchecker n p i =
-  (do 
+  do {
      rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
      (if (fst rcs ! i) = Some [] then return (snd rcs) 
                 else raise(''No empty clause''))
-   done)"
+  }"
 
 
 section {* Functional version with RedBlackTrees *}
@@ -684,10 +684,10 @@
   "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
      (case (RBT_Impl.lookup t i) of
        None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
-     | Some cli \<Rightarrow> (do
+     | Some cli \<Rightarrow> do {
                       result \<leftarrow> foldM (tres_thm t) rs cli;
                       return ((RBT_Impl.insert saveTo result t), rcl)
-                    done))"
+                   })"
 | "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)"
 | "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
 | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
@@ -696,11 +696,11 @@
 definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
 where
   "tchecker n p i =
-  (do 
+  do {
      rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
      (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) 
                 else raise(''No empty clause''))
-   done)"
+  }"
 
 section {* Code generation setup *}
 
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 13 12:05:20 2010 +0200
@@ -397,7 +397,7 @@
 
 $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
   $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
-  Library/Abstract_Rat.thy Library/AssocList.thy			\
+  Library/Abstract_Rat.thy Library/Adhoc_Overloading.thy Library/AssocList.thy	\
   Library/BigO.thy Library/Binomial.thy Library/Bit.thy			\
   Library/Boolean_Algebra.thy Library/Cardinality.thy			\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
@@ -414,8 +414,8 @@
   Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
   Library/Lattice_Syntax.thy Library/Library.thy			\
   Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
-  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
-  Library/Nat_Bijection.thy Library/Nat_Infinity.thy			\
+  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
+  Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy	\
   Library/Nested_Environment.thy Library/Numeral_Type.thy		\
   Library/OptionalSugar.thy Library/Order_Relation.thy			\
   Library/Permutation.thy Library/Permutations.thy			\
@@ -434,8 +434,8 @@
   Library/Sum_Of_Squares/sum_of_squares.ML				\
   Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
   Library/While_Combinator.thy Library/Zorn.thy				\
-  Library/positivstellensatz.ML Library/reflection.ML			\
-  Library/reify_data.ML							\
+  Library/adhoc_overloading.ML Library/positivstellensatz.ML		\
+  Library/reflection.ML Library/reify_data.ML				\
   Library/document/root.bib Library/document/root.tex
 	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
 
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Library/Adhoc_Overloading.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Adhoc_Overloading.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -0,0 +1,14 @@
+(* Author: Alexander Krauss, TU Muenchen
+   Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Ad-hoc overloading of constants based on their types *}
+
+theory Adhoc_Overloading
+imports Main
+uses "adhoc_overloading.ML"
+begin
+
+setup Adhoc_Overloading.setup
+
+end
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -2,6 +2,7 @@
 theory Library
 imports
   Abstract_Rat
+  Adhoc_Overloading
   AssocList
   BigO
   Binomial
@@ -31,6 +32,7 @@
   ListVector
   Kleene_Algebra
   Mapping
+  Monad_Syntax
   More_List
   Multiset
   Nat_Infinity
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Library/Monad_Syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -0,0 +1,66 @@
+(* Author: Alexander Krauss, TU Muenchen
+   Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Monad notation for arbitrary types *}
+
+theory Monad_Syntax
+imports Adhoc_Overloading
+begin
+
+text {*
+  We provide a convenient do-notation for monadic expressions
+  well-known from Haskell.  @{const Let} is printed
+  specially in do-expressions.
+*}
+
+consts
+  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+
+notation (xsymbols)
+  bindM (infixr "\<guillemotright>=" 54)
+
+abbreviation (do_notation)
+  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+where
+  "bindM_do \<equiv> bindM"
+
+notation (output)
+  bindM_do (infixr ">>=" 54)
+
+notation (xsymbols output)
+  bindM_do (infixr "\<guillemotright>=" 54)
+
+nonterminals
+  do_binds do_bind
+
+syntax
+  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
+  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
+  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
+  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
+  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
+
+syntax (xsymbols)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
+
+translations
+  "_do_block (_do_cons (_do_then t) (_do_final e))"
+    == "CONST bindM_do t (\<lambda>_. e)"
+  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
+    == "CONST bindM_do t (\<lambda>p. e)"
+  "_do_block (_do_cons (_do_let p t) bs)"
+    == "let p = t in _do_block bs"
+  "_do_block (_do_cons b (_do_cons c cs))"
+    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
+  "_do_cons (_do_let p t) (_do_final s)"
+    == "_do_final (let p = t in s)"
+  "_do_block (_do_final e)" => "e"
+  "(m >> n)" => "(m >>= (\<lambda>_. n))"
+
+setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
+
+end
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Tue Jul 13 12:01:34 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Tue Jul 13 12:05:20 2010 +0200
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Main
+imports Monad_Syntax
 begin
 
 subsection {* Motivation *}
@@ -112,86 +112,8 @@
 
 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
 
-
-subsection {* Syntax *}
-
-text {*
-  We provide a convenient do-notation for monadic expressions
-  well-known from Haskell.  @{const Let} is printed
-  specially in do-expressions.
-*}
-
-nonterminals do_expr
-
-syntax
-  "_do" :: "do_expr \<Rightarrow> 'a"
-    ("do _ done" [12] 12)
-  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ <- _;// _" [1000, 13, 12] 12)
-  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_;// _" [13, 12] 12)
-  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("let _ = _;// _" [1000, 13, 12] 12)
-  "_done" :: "'a \<Rightarrow> do_expr"
-    ("_" [12] 12)
-
-syntax (xsymbols)
-  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
-
-translations
-  "_do f" => "f"
-  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
-  "_fcomp f g" => "f \<circ>> g"
-  "_let x t f" => "CONST Let t (\<lambda>x. f)"
-  "_done f" => "f"
-
-print_translation {*
-let
-  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
-        let
-          val (v, t) = Syntax.variant_abs abs;
-        in (Free (v, ty), t) end
-    | dest_abs_eta t =
-        let
-          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
-        in (Free (v, dummyT), t) end;
-  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
-    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
-        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
-    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
-    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
-        Const (@{const_syntax "return"}, dummyT) $ f
-    | unfold_monad f = f;
-  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
-    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
-        contains_scomp t
-    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
-        contains_scomp t;
-  fun scomp_monad_tr' (f::g::ts) = list_comb
-    (Const (@{syntax_const "_do"}, dummyT) $
-      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
-  fun fcomp_monad_tr' (f::g::ts) =
-    if contains_scomp g then list_comb
-      (Const (@{syntax_const "_do"}, dummyT) $
-        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
-    else raise Match;
-  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
-    if contains_scomp g' then list_comb
-      (Const (@{syntax_const "_do"}, dummyT) $
-        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
-    else raise Match;
-in
- [(@{const_syntax scomp}, scomp_monad_tr'),
-  (@{const_syntax fcomp}, fcomp_monad_tr'),
-  (@{const_syntax Let}, Let_monad_tr')]
-end;
+setup {*
+  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
 *}
 
 text {*
diff -r 08bd610b2583 -r 96551d6b1414 src/HOL/Library/adhoc_overloading.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/adhoc_overloading.ML	Tue Jul 13 12:05:20 2010 +0200
@@ -0,0 +1,140 @@
+(* Author: Alexander Krauss, TU Muenchen
+   Author: Christian Sternagel, University of Innsbruck
+
+Ad-hoc overloading of constants based on their types.
+*)
+
+signature ADHOC_OVERLOADING =
+sig
+
+  val add_overloaded: string -> theory -> theory
+  val add_variant: string -> string -> theory -> theory
+
+  val show_variants: bool Unsynchronized.ref
+  val setup: theory -> theory
+
+end
+
+
+structure Adhoc_Overloading: ADHOC_OVERLOADING =
+struct
+
+val show_variants = Unsynchronized.ref false;
+
+
+(* errors *)
+
+fun duplicate_variant_err int_name ext_name =
+  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
+
+fun not_overloaded_err name =
+  error ("Constant " ^ quote name ^ " is not declared as overloaded");
+
+fun already_overloaded_err name =
+  error ("Constant " ^ quote name ^ " is already declared as overloaded");
+
+fun unresolved_err ctxt (c, T) t reason =
+  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
+    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
+    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+
+
+(* theory data *)
+
+structure Overload_Data = Theory_Data
+(
+  type T =
+    { internalize : (string * typ) list Symtab.table,
+      externalize : string Symtab.table };
+  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+  val extend = I;
+
+  fun merge_ext int_name (ext_name1, ext_name2) =
+    if ext_name1 = ext_name2 then ext_name1
+    else duplicate_variant_err int_name ext_name1;
+
+  fun merge ({internalize=int1, externalize=ext1},
+      {internalize=int2, externalize=ext2}) =
+    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
+     externalize=Symtab.join merge_ext (ext1, ext2)};
+);
+
+fun map_tables f g =
+  Overload_Data.map (fn {internalize=int, externalize=ext} =>
+    {internalize=f int, externalize=g ext});
+
+val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
+val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
+val get_external = Symtab.lookup o #externalize o Overload_Data.get;
+
+fun add_overloaded ext_name thy =
+  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
+  in map_tables (Symtab.update (ext_name, [])) I thy end;
+
+fun add_variant ext_name name thy =
+  let
+    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
+    val _ = case get_external thy name of
+              NONE => ()
+            | SOME gen' => duplicate_variant_err name gen';
+    val T = Sign.the_const_type thy name;
+  in
+    map_tables (Symtab.cons_list (ext_name, (name, T)))
+      (Symtab.update (name, ext_name)) thy    
+  end
+
+
+(* check / uncheck *)
+
+fun unifiable_with ctxt T1 (c, T2) =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val maxidx1 = Term.maxidx_of_typ T1;
+    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
+    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
+  in
+    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
+    handle Type.TUNIFY => NONE
+  end;
+
+fun insert_internal_same ctxt t (Const (c, T)) =
+  (case map_filter (unifiable_with ctxt T) 
+     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
+      [] => unresolved_err ctxt (c, T) t "no instances"
+    | [c'] => Const (c', dummyT)
+    | _ => raise Same.SAME)
+  | insert_internal_same _ _ _ = raise Same.SAME;
+
+fun insert_external_same ctxt _ (Const (c, T)) =
+    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
+  | insert_external_same _ _ _ = raise Same.SAME;
+
+fun gen_check_uncheck replace ts ctxt =
+  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
+  |> Option.map (rpair ctxt);
+
+val check = gen_check_uncheck insert_internal_same;
+fun uncheck ts ctxt = 
+  if !show_variants then NONE
+  else gen_check_uncheck insert_external_same ts ctxt;
+
+fun reject_unresolved ts ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    fun check_unresolved t =
+      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
+          [] => ()
+        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
+
+    val _ = map check_unresolved ts;
+  in NONE end;
+
+
+(* setup *)
+
+val setup = Context.theory_map 
+  (Syntax.add_term_check 0 "adhoc_overloading" check
+   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
+
+end