dropped "run" marker in monad syntax
authorhaftmann
Sat Sep 06 14:02:36 2008 +0200 (2008-09-06)
changeset 28145af3923ed4786
parent 28144 2c27248bf267
child 28146 032cd8a25244
dropped "run" marker in monad syntax
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
src/HOL/Library/Array.thy
src/HOL/Library/Heap_Monad.thy
src/HOL/Library/Relational.thy
src/HOL/Library/State_Monad.thy
src/HOL/ex/ImperativeQuicksort.thy
src/HOL/ex/Quickcheck.thy
src/HOL/ex/Random.thy
src/Tools/code/code_haskell.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Sep 05 11:50:35 2008 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,26 +0,0 @@
     1.4 -structure Nat = 
     1.5 -struct
     1.6 -
     1.7 -datatype nat = Suc of nat | Zero_nat;
     1.8 -
     1.9 -val one_nat : nat = Suc Zero_nat;
    1.10 -
    1.11 -fun nat_case f1 f2 Zero_nat = f1
    1.12 -  | nat_case f1 f2 (Suc nat) = f2 nat;
    1.13 -
    1.14 -fun plus_nat (Suc m) n = plus_nat m (Suc n)
    1.15 -  | plus_nat Zero_nat n = n;
    1.16 -
    1.17 -fun times_nat (Suc m) n = plus_nat n (times_nat m n)
    1.18 -  | times_nat Zero_nat n = Zero_nat;
    1.19 -
    1.20 -end; (*struct Nat*)
    1.21 -
    1.22 -structure Codegen = 
    1.23 -struct
    1.24 -
    1.25 -fun fac n =
    1.26 -  (case n of Nat.Zero_nat => Nat.one_nat
    1.27 -     | Nat.Suc m => Nat.times_nat n (fac m));
    1.28 -
    1.29 -end; (*struct Codegen*)
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Sep 05 11:50:35 2008 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,23 +0,0 @@
     2.4 -structure Nat = 
     2.5 -struct
     2.6 -
     2.7 -datatype nat = Suc of nat | Zero_nat;
     2.8 -
     2.9 -fun less_nat m (Suc n) = less_eq_nat m n
    2.10 -  | less_nat n Zero_nat = false
    2.11 -and less_eq_nat (Suc m) n = less_nat m n
    2.12 -  | less_eq_nat Zero_nat n = true;
    2.13 -
    2.14 -fun minus_nat (Suc m) (Suc n) = minus_nat m n
    2.15 -  | minus_nat Zero_nat n = Zero_nat
    2.16 -  | minus_nat m Zero_nat = m;
    2.17 -
    2.18 -end; (*struct Nat*)
    2.19 -
    2.20 -structure Codegen = 
    2.21 -struct
    2.22 -
    2.23 -fun pick ((k, v) :: xs) n =
    2.24 -  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
    2.25 -
    2.26 -end; (*struct Codegen*)
     3.1 --- a/src/HOL/Library/Array.thy	Fri Sep 05 11:50:35 2008 +0200
     3.2 +++ b/src/HOL/Library/Array.thy	Sat Sep 06 14:02:36 2008 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4    obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
     3.5      by (cases "Heap_Monad.execute (Array.length a) h")
     3.6    then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
     3.7 -    by (auto simp add: upd_def bindM_def run_drop split: sum.split)
     3.8 +    by (auto simp add: upd_def bindM_def split: sum.split)
     3.9  qed
    3.10  
    3.11  
     4.1 --- a/src/HOL/Library/Heap_Monad.thy	Fri Sep 05 11:50:35 2008 +0200
     4.2 +++ b/src/HOL/Library/Heap_Monad.thy	Sat Sep 06 14:02:36 2008 +0200
     4.3 @@ -56,10 +56,6 @@
     4.4    by (simp add: heap_def)
     4.5  
     4.6  definition
     4.7 -  run :: "'a Heap \<Rightarrow> 'a Heap" where
     4.8 -  run_drop [code del]: "run f = f"
     4.9 -
    4.10 -definition
    4.11    bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
    4.12    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    4.13                    (Inl x, h') \<Rightarrow> execute (g x) h'
    4.14 @@ -129,7 +125,7 @@
    4.15    "return" ("\<^raw:{\textsf{return}}>")
    4.16  
    4.17  translations
    4.18 -  "_do f" => "CONST run f"
    4.19 +  "_do f" => "f"
    4.20    "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
    4.21    "_chainM f g" => "f \<guillemotright> g"
    4.22    "_let x t f" => "CONST Let t (\<lambda>x. f)"
    4.23 @@ -140,18 +136,19 @@
    4.24    fun dest_abs_eta (Abs (abs as (_, ty, _))) =
    4.25          let
    4.26            val (v, t) = Syntax.variant_abs abs;
    4.27 -        in ((v, ty), t) end
    4.28 +        in (Free (v, ty), t) end
    4.29      | dest_abs_eta t =
    4.30          let
    4.31            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    4.32 -        in ((v, dummyT), t) end
    4.33 +        in (Free (v, dummyT), t) end;
    4.34    fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
    4.35          let
    4.36 -          val ((v, ty), g') = dest_abs_eta g;
    4.37 +          val (v, g') = dest_abs_eta g;
    4.38 +          val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
    4.39            val v_used = fold_aterms
    4.40 -            (fn Free (w, _) => (fn s => s orelse v = w) | _ => I) g' false;
    4.41 +            (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
    4.42          in if v_used then
    4.43 -          Const ("_bindM", dummyT) $ Free (v, ty) $ f $ unfold_monad g'
    4.44 +          Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
    4.45          else
    4.46            Const ("_chainM", dummyT) $ f $ unfold_monad g'
    4.47          end
    4.48 @@ -159,33 +156,28 @@
    4.49          Const ("_chainM", dummyT) $ f $ unfold_monad g
    4.50      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    4.51          let
    4.52 -          val ((v, ty), g') = dest_abs_eta g;
    4.53 -        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    4.54 +          val (v, g') = dest_abs_eta g;
    4.55 +        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
    4.56      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    4.57 -        Const ("return", dummyT) $ f
    4.58 +        Const (@{const_syntax return}, dummyT) $ f
    4.59      | unfold_monad f = f;
    4.60 -  fun tr' (f::ts) =
    4.61 -    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
    4.62 -in [(@{const_syntax "run"}, tr')] end;
    4.63 +  fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
    4.64 +    | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    4.65 +        contains_bindM t;
    4.66 +  fun bindM_monad_tr' (f::g::ts) = list_comb
    4.67 +    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
    4.68 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
    4.69 +      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    4.70 +    else raise Match;
    4.71 +in [
    4.72 +  (@{const_syntax bindM}, bindM_monad_tr'),
    4.73 +  (@{const_syntax Let}, Let_monad_tr')
    4.74 +] end;
    4.75  *}
    4.76  
    4.77  
    4.78  subsection {* Monad properties *}
    4.79  
    4.80 -subsubsection {* Superfluous runs *}
    4.81 -
    4.82 -text {* @{term run} is just a doodle *}
    4.83 -
    4.84 -lemma run_simp [simp]:
    4.85 -  "\<And>f. run (run f) = run f"
    4.86 -  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
    4.87 -  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
    4.88 -  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
    4.89 -  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
    4.90 -  "\<And>f. f = run g \<longleftrightarrow> f = g"
    4.91 -  "\<And>f. run f = g \<longleftrightarrow> f = g"
    4.92 -  unfolding run_drop by rule+
    4.93 -
    4.94  subsubsection {* Monad laws *}
    4.95  
    4.96  lemma return_bind: "return x \<guillemotright>= f = f x"
    4.97 @@ -293,7 +285,6 @@
    4.98  code_type Heap (SML "unit/ ->/ _")
    4.99  code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
   4.100  code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
   4.101 -code_const run (SML "_")
   4.102  code_const return (SML "!(fn/ ()/ =>/ _)")
   4.103  code_const "Heap_Monad.Fail" (SML "Fail")
   4.104  code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
   4.105 @@ -301,7 +292,6 @@
   4.106  code_type Heap (OCaml "_")
   4.107  code_const Heap (OCaml "failwith/ \"bare Heap\"")
   4.108  code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   4.109 -code_const run (OCaml "_")
   4.110  code_const return (OCaml "!(fun/ ()/ ->/ _)")
   4.111  code_const "Heap_Monad.Fail" (OCaml "Failure")
   4.112  code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
   4.113 @@ -416,7 +406,7 @@
   4.114  
   4.115  code_type Heap (Haskell "ST/ RealWorld/ _")
   4.116  code_const Heap (Haskell "error/ \"bare Heap\"")
   4.117 -code_monad run "op \<guillemotright>=" Haskell
   4.118 +code_monad "op \<guillemotright>=" Haskell
   4.119  code_const return (Haskell "return")
   4.120  code_const "Heap_Monad.Fail" (Haskell "_")
   4.121  code_const "Heap_Monad.raise_exc" (Haskell "error")
     5.1 --- a/src/HOL/Library/Relational.thy	Fri Sep 05 11:50:35 2008 +0200
     5.2 +++ b/src/HOL/Library/Relational.thy	Sat Sep 06 14:02:36 2008 +0200
     5.3 @@ -77,7 +77,7 @@
     5.4    from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
     5.5      and crel_mapM: "crel (mapM f xs) h1 h' ys"
     5.6      and r_def: "r = y#ys"
     5.7 -    unfolding mapM.simps run_drop
     5.8 +    unfolding mapM.simps
     5.9      by (auto elim!: crelE crel_return)
    5.10    from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
    5.11    show ?case by auto
    5.12 @@ -109,14 +109,14 @@
    5.13    assumes "crel (nth a i) h h' r"
    5.14    obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
    5.15    using assms
    5.16 -  unfolding nth_def run_drop
    5.17 +  unfolding nth_def
    5.18    by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
    5.19  
    5.20  lemma crel_upd[consumes 1]:
    5.21    assumes "crel (upd i v a) h h' r"
    5.22    obtains "r = a" "h' = Heap.upd a i v h"
    5.23    using assms
    5.24 -  unfolding upd_def run_drop
    5.25 +  unfolding upd_def
    5.26    by (elim crelE crel_if crel_return crel_raise
    5.27      crel_length crel_heap) auto
    5.28  
    5.29 @@ -132,14 +132,14 @@
    5.30    assumes "crel (Array.map_entry i f a) h h' r"
    5.31    obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
    5.32    using assms
    5.33 -  unfolding Array.map_entry_def run_drop
    5.34 +  unfolding Array.map_entry_def
    5.35    by (elim crelE crel_upd crel_nth) auto
    5.36  
    5.37  lemma crel_swap:
    5.38    assumes "crel (Array.swap i x a) h h' r"
    5.39    obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
    5.40    using assms
    5.41 -  unfolding Array.swap_def run_drop
    5.42 +  unfolding Array.swap_def
    5.43    by (elim crelE crel_upd crel_nth crel_return) auto
    5.44  
    5.45  (* Strong version of the lemma for this operation is missing *)
    5.46 @@ -175,7 +175,7 @@
    5.47    with Suc(2) obtain r where
    5.48      crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
    5.49      and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
    5.50 -    by (auto simp add: run_drop elim!: crelE crel_nth crel_return)
    5.51 +    by (auto elim!: crelE crel_nth crel_return)
    5.52    from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)" 
    5.53      by arith
    5.54    with Suc.hyps[OF crel_mapM] xs_def show ?case
    5.55 @@ -188,7 +188,7 @@
    5.56    obtains "h = h'" "xs = get_array a h"
    5.57  proof 
    5.58    from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
    5.59 -    unfolding freeze_def run_drop
    5.60 +    unfolding freeze_def
    5.61      by (auto elim: crelE crel_length)
    5.62    hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
    5.63      by simp
    5.64 @@ -211,7 +211,7 @@
    5.65      by (simp add: upt_conv_Cons')
    5.66    from Suc(2) this obtain r where
    5.67      crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
    5.68 -    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
    5.69 +    by (auto simp add: elim!: crelE crel_map_entry crel_return)
    5.70    have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
    5.71    from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
    5.72      by simp
    5.73 @@ -236,7 +236,7 @@
    5.74      by (simp add: upt_conv_Cons')
    5.75    from Suc(2) this obtain r where
    5.76      crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
    5.77 -    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
    5.78 +    by (auto simp add: elim!: crelE crel_map_entry crel_return)
    5.79    have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
    5.80    from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
    5.81    from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
    5.82 @@ -264,7 +264,7 @@
    5.83      by (simp add: upt_conv_Cons')
    5.84    from Suc(2) this obtain r where 
    5.85      crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
    5.86 -    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
    5.87 +    by (auto elim!: crelE crel_map_entry crel_return)
    5.88    have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
    5.89    from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
    5.90      by simp
    5.91 @@ -287,10 +287,10 @@
    5.92    obtains "r = a" "get_array a h' = List.map f (get_array a h)"
    5.93  proof
    5.94    from assms crel_mapM_map_entry show  "get_array a h' = List.map f (get_array a h)"
    5.95 -    unfolding Array.map_def run_drop
    5.96 +    unfolding Array.map_def
    5.97      by (fastsimp elim!: crelE crel_length crel_return)
    5.98    from assms show "r = a"
    5.99 -    unfolding Array.map_def run_drop
   5.100 +    unfolding Array.map_def
   5.101      by (elim crelE crel_return)
   5.102  qed
   5.103  
   5.104 @@ -351,7 +351,7 @@
   5.105    assumes "crel (Ref.change f ref) h h' r"
   5.106    obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
   5.107  using assms
   5.108 -unfolding Ref.change_def run_drop Let_def
   5.109 +unfolding Ref.change_def Let_def
   5.110  by (auto elim!: crelE crel_lookup crel_update crel_return)
   5.111  
   5.112  subsection {* Elimination rules for the assert command *}
   5.113 @@ -446,14 +446,14 @@
   5.114    assumes "i < Heap.length a h"
   5.115    shows "crel (nth a i) h h ((get_array a h) ! i)"
   5.116    using assms
   5.117 -  unfolding nth_def run_drop
   5.118 +  unfolding nth_def
   5.119    by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
   5.120  
   5.121  lemma crel_updI:
   5.122    assumes "i < Heap.length a h"
   5.123    shows "crel (upd i v a) h (Heap.upd a i v h) a"
   5.124    using assms
   5.125 -  unfolding upd_def run_drop
   5.126 +  unfolding upd_def
   5.127    by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
   5.128      crel_lengthI crel_heapI')
   5.129  
   5.130 @@ -481,7 +481,7 @@
   5.131  
   5.132  lemma crel_changeI: 
   5.133    shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
   5.134 -unfolding change_def Let_def run_drop by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
   5.135 +unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
   5.136  
   5.137  subsection {* Introduction rules for the assert command *}
   5.138  
   5.139 @@ -562,7 +562,7 @@
   5.140  next
   5.141    case (Cons x xs)
   5.142    thus ?case
   5.143 -    unfolding mapM.simps run_drop
   5.144 +    unfolding mapM.simps
   5.145      by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
   5.146  qed
   5.147  
   5.148 @@ -585,14 +585,14 @@
   5.149    assumes "i < Heap.length a h"
   5.150    shows "noError (Array.upd i v a) h"
   5.151    using assms
   5.152 -  unfolding upd_def run_drop
   5.153 +  unfolding upd_def
   5.154    by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
   5.155  
   5.156  lemma noError_nth:
   5.157  assumes "i < Heap.length a h"
   5.158    shows "noError (Array.nth a i) h"
   5.159    using assms
   5.160 -  unfolding nth_def run_drop
   5.161 +  unfolding nth_def
   5.162    by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
   5.163  
   5.164  lemma noError_of_list:
   5.165 @@ -603,14 +603,14 @@
   5.166    assumes "i < Heap.length a h"
   5.167    shows "noError (map_entry i f a) h"
   5.168    using assms
   5.169 -  unfolding map_entry_def run_drop
   5.170 +  unfolding map_entry_def
   5.171    by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
   5.172  
   5.173  lemma noError_swap:
   5.174    assumes "i < Heap.length a h"
   5.175    shows "noError (swap i x a) h"
   5.176    using assms
   5.177 -  unfolding swap_def run_drop
   5.178 +  unfolding swap_def
   5.179    by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
   5.180  
   5.181  lemma noError_make:
   5.182 @@ -625,7 +625,7 @@
   5.183  
   5.184  lemma noError_freeze:
   5.185    shows "noError (freeze a) h"
   5.186 -unfolding freeze_def run_drop
   5.187 +unfolding freeze_def
   5.188  by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
   5.189    noError_nth crel_nthI elim: crel_length)
   5.190  
   5.191 @@ -641,13 +641,13 @@
   5.192    from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
   5.193      by (simp add: upt_conv_Cons')
   5.194    with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
   5.195 -    by (auto simp add: run_drop intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
   5.196 +    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
   5.197  qed
   5.198  
   5.199  lemma noError_map:
   5.200    shows "noError (Array.map f a) h"
   5.201  using noError_mapM_map_entry[of "Heap.length a h" a h]
   5.202 -unfolding Array.map_def run_drop
   5.203 +unfolding Array.map_def
   5.204  by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
   5.205  
   5.206  subsection {* Introduction rules for the reference commands *}
   5.207 @@ -666,7 +666,7 @@
   5.208  
   5.209  lemma noError_change:
   5.210    shows "noError (Ref.change f ref) h"
   5.211 -  unfolding Ref.change_def run_drop Let_def by (intro noErrorI noError_lookup noError_update noError_return)
   5.212 +  unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
   5.213  
   5.214  subsection {* Introduction rules for the assert command *}
   5.215  
     6.1 --- a/src/HOL/Library/State_Monad.thy	Fri Sep 05 11:50:35 2008 +0200
     6.2 +++ b/src/HOL/Library/State_Monad.thy	Sat Sep 06 14:02:36 2008 +0200
     6.3 @@ -56,31 +56,23 @@
     6.4    we use a set of monad combinators:
     6.5  *}
     6.6  
     6.7 -notation fcomp (infixl ">>" 60)
     6.8 -notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
     6.9 -notation scomp (infixl ">>=" 60)
    6.10 -notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
    6.11 +notation fcomp (infixl "o>" 60)
    6.12 +notation (xsymbols) fcomp (infixl "o>" 60)
    6.13 +notation scomp (infixl "o->" 60)
    6.14 +notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
    6.15  
    6.16  abbreviation (input)
    6.17    "return \<equiv> Pair"
    6.18  
    6.19 -definition
    6.20 -  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    6.21 -  "run f = f"
    6.22 -
    6.23 -print_ast_translation {*
    6.24 -  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    6.25 -*}
    6.26 -
    6.27  text {*
    6.28    Given two transformations @{term f} and @{term g}, they
    6.29 -  may be directly composed using the @{term "op \<guillemotright>"} combinator,
    6.30 -  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
    6.31 +  may be directly composed using the @{term "op o>"} combinator,
    6.32 +  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
    6.33  
    6.34    After any yielding transformation, we bind the side result
    6.35    immediately using a lambda abstraction.  This 
    6.36 -  is the purpose of the @{term "op \<guillemotright>="} combinator:
    6.37 -  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    6.38 +  is the purpose of the @{term "op o\<rightarrow>"} combinator:
    6.39 +  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    6.40  
    6.41    For queries, the existing @{term "Let"} is appropriate.
    6.42  
    6.43 @@ -88,8 +80,6 @@
    6.44    it to the state from the left;  we introduce the
    6.45    suggestive abbreviation @{term return} for this purpose.
    6.46  
    6.47 -  The @{const run} ist just a marker.
    6.48 -
    6.49    The most crucial distinction to Haskell is that we do
    6.50    not need to introduce distinguished type constructors
    6.51    for different kinds of state.  This has two consequences:
    6.52 @@ -107,22 +97,6 @@
    6.53  *}
    6.54  
    6.55  
    6.56 -subsection {* Obsolete runs *}
    6.57 -
    6.58 -text {*
    6.59 -  @{term run} is just a doodle and should not occur nested:
    6.60 -*}
    6.61 -
    6.62 -lemma run_simp [simp]:
    6.63 -  "\<And>f. run (run f) = run f"
    6.64 -  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
    6.65 -  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
    6.66 -  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
    6.67 -  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
    6.68 -  "\<And>f. f = run f \<longleftrightarrow> True"
    6.69 -  "\<And>f. run f = f \<longleftrightarrow> True"
    6.70 -  unfolding run_def by rule+
    6.71 -
    6.72  subsection {* Monad laws *}
    6.73  
    6.74  text {*
    6.75 @@ -130,66 +104,14 @@
    6.76    as normalization rules for monadic expressions:
    6.77  *}
    6.78  
    6.79 -lemma
    6.80 -  return_scomp [simp]: "return x \<guillemotright>= f = f x"
    6.81 -  unfolding scomp_def by (simp add: expand_fun_eq)
    6.82 -
    6.83 -lemma
    6.84 -  scomp_return [simp]: "x \<guillemotright>= return = x"
    6.85 -  unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
    6.86 -
    6.87 -lemma
    6.88 -  id_fcomp [simp]: "id \<guillemotright> f = f"
    6.89 -  unfolding fcomp_def by simp
    6.90 -
    6.91 -lemma
    6.92 -  fcomp_id [simp]: "f \<guillemotright> id = f"
    6.93 -  unfolding fcomp_def by simp
    6.94 -
    6.95 -lemma
    6.96 -  scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    6.97 -  unfolding scomp_def by (simp add: split_def expand_fun_eq)
    6.98 -
    6.99 -lemma
   6.100 -  scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   6.101 -  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
   6.102 -
   6.103 -lemma
   6.104 -  fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   6.105 -  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
   6.106 -
   6.107 -lemma
   6.108 -  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   6.109 -  unfolding fcomp_def o_assoc ..
   6.110 -
   6.111 -lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
   6.112 -  scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
   6.113 +lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
   6.114 +  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
   6.115  
   6.116  text {*
   6.117    Evaluation of monadic expressions by force:
   6.118  *}
   6.119  
   6.120 -lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   6.121 -  scomp_def fcomp_def run_def
   6.122 -
   6.123 -subsection {* ML abstract operations *}
   6.124 -
   6.125 -ML {*
   6.126 -structure StateMonad =
   6.127 -struct
   6.128 -
   6.129 -fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
   6.130 -fun liftT' sT = sT --> sT;
   6.131 -
   6.132 -fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
   6.133 -
   6.134 -fun scomp T1 T2 sT f g = Const (@{const_name scomp},
   6.135 -  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   6.136 -
   6.137 -fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
   6.138 -
   6.139 -end;
   6.140 -*}
   6.141 +lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
   6.142  
   6.143  
   6.144  subsection {* Syntax *}
   6.145 @@ -211,7 +133,7 @@
   6.146      ("_;// _" [13, 12] 12)
   6.147    "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   6.148      ("let _ = _;// _" [1000, 13, 12] 12)
   6.149 -  "_nil" :: "'a \<Rightarrow> do_expr"
   6.150 +  "_done" :: "'a \<Rightarrow> do_expr"
   6.151      ("_" [12] 12)
   6.152  
   6.153  syntax (xsymbols)
   6.154 @@ -219,95 +141,55 @@
   6.155      ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   6.156  
   6.157  translations
   6.158 -  "_do f" => "CONST run f"
   6.159 -  "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   6.160 -  "_fcomp f g" => "f \<guillemotright> g"
   6.161 +  "_do f" => "f"
   6.162 +  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
   6.163 +  "_fcomp f g" => "f o> g"
   6.164    "_let x t f" => "CONST Let t (\<lambda>x. f)"
   6.165 -  "_nil f" => "f"
   6.166 +  "_done f" => "f"
   6.167  
   6.168  print_translation {*
   6.169  let
   6.170    fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   6.171          let
   6.172            val (v, t) = Syntax.variant_abs abs;
   6.173 -        in ((v, ty), t) end
   6.174 +        in (Free (v, ty), t) end
   6.175      | dest_abs_eta t =
   6.176          let
   6.177            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   6.178 -        in ((v, dummyT), t) end
   6.179 +        in (Free (v, dummyT), t) end;
   6.180    fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
   6.181          let
   6.182 -          val ((v, ty), g') = dest_abs_eta g;
   6.183 -        in Const ("_scomp", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   6.184 +          val (v, g') = dest_abs_eta g;
   6.185 +        in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
   6.186      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   6.187          Const ("_fcomp", dummyT) $ f $ unfold_monad g
   6.188      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   6.189          let
   6.190 -          val ((v, ty), g') = dest_abs_eta g;
   6.191 -        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   6.192 +          val (v, g') = dest_abs_eta g;
   6.193 +        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
   6.194      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   6.195          Const ("return", dummyT) $ f
   6.196      | unfold_monad f = f;
   6.197 -  fun tr' (f::ts) =
   6.198 -    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   6.199 -in [(@{const_syntax "run"}, tr')] end;
   6.200 +  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
   6.201 +    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
   6.202 +        contains_scomp t
   6.203 +    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   6.204 +        contains_scomp t;
   6.205 +  fun scomp_monad_tr' (f::g::ts) = list_comb
   6.206 +    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
   6.207 +  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
   6.208 +      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
   6.209 +    else raise Match;
   6.210 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
   6.211 +      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   6.212 +    else raise Match;
   6.213 +in [
   6.214 +  (@{const_syntax scomp}, scomp_monad_tr'),
   6.215 +  (@{const_syntax fcomp}, fcomp_monad_tr'),
   6.216 +  (@{const_syntax Let}, Let_monad_tr')
   6.217 +] end;
   6.218  *}
   6.219  
   6.220 -
   6.221 -subsection {* Combinators *}
   6.222 -
   6.223 -definition
   6.224 -  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
   6.225 -  "lift f x = return (f x)"
   6.226 -
   6.227 -primrec
   6.228 -  list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   6.229 -  "list f [] = id"
   6.230 -| "list f (x#xs) = (do f x; list f xs done)"
   6.231 -
   6.232 -primrec
   6.233 -  list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   6.234 -  "list_yield f [] = return []"
   6.235 -| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
   6.236 -
   6.237 -definition
   6.238 -  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   6.239 -  "collapse f = (do g \<leftarrow> f; g done)"
   6.240 -
   6.241 -text {* combinator properties *}
   6.242 -
   6.243 -lemma list_append [simp]:
   6.244 -  "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
   6.245 -  by (induct xs) (simp_all del: id_apply)
   6.246 -
   6.247 -lemma list_cong [fundef_cong, recdef_cong]:
   6.248 -  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   6.249 -    \<Longrightarrow> list f xs = list g ys"
   6.250 -proof (induct xs arbitrary: ys)
   6.251 -  case Nil then show ?case by simp
   6.252 -next
   6.253 -  case (Cons x xs)
   6.254 -  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   6.255 -  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   6.256 -  with Cons have "list f xs = list g xs" by auto
   6.257 -  with Cons have "list f (x # xs) = list g (x # xs)" by auto
   6.258 -  with Cons show "list f (x # xs) = list g ys" by auto
   6.259 -qed
   6.260 -
   6.261 -lemma list_yield_cong [fundef_cong, recdef_cong]:
   6.262 -  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   6.263 -    \<Longrightarrow> list_yield f xs = list_yield g ys"
   6.264 -proof (induct xs arbitrary: ys)
   6.265 -  case Nil then show ?case by simp
   6.266 -next
   6.267 -  case (Cons x xs)
   6.268 -  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   6.269 -  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   6.270 -  with Cons have "list_yield f xs = list_yield g xs" by auto
   6.271 -  with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
   6.272 -  with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
   6.273 -qed
   6.274 -
   6.275  text {*
   6.276    For an example, see HOL/ex/Random.thy.
   6.277  *}
     7.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Fri Sep 05 11:50:35 2008 +0200
     7.2 +++ b/src/HOL/ex/ImperativeQuicksort.thy	Sat Sep 06 14:02:36 2008 +0200
     7.3 @@ -4,7 +4,6 @@
     7.4  
     7.5  text {* We prove QuickSort correct in the Relational Calculus. *}
     7.6  
     7.7 -
     7.8  definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
     7.9  where
    7.10    "swap arr i j = (
    7.11 @@ -21,7 +20,7 @@
    7.12    shows "multiset_of (get_array a h') 
    7.13    = multiset_of (get_array a h)"
    7.14    using assms
    7.15 -  unfolding swap_def run_drop
    7.16 +  unfolding swap_def
    7.17    by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    7.18  
    7.19  function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    7.20 @@ -49,7 +48,7 @@
    7.21  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    7.22    case (1 a l r p h h' rs)
    7.23    thus ?case
    7.24 -    unfolding part1.simps [of a l r p] run_drop
    7.25 +    unfolding part1.simps [of a l r p]
    7.26      by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    7.27  qed
    7.28  
    7.29 @@ -65,7 +64,7 @@
    7.30    proof (cases "r \<le> l")
    7.31      case True (* Terminating case *)
    7.32      with cr `l \<le> r` show ?thesis
    7.33 -      unfolding part1.simps[of a l r p] run_drop
    7.34 +      unfolding part1.simps[of a l r p]
    7.35        by (elim crelE crel_if crel_return crel_nth) auto
    7.36    next
    7.37      case False (* recursive case *)
    7.38 @@ -76,7 +75,7 @@
    7.39        case True
    7.40        with cr False
    7.41        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    7.42 -        unfolding part1.simps[of a l r p] run_drop
    7.43 +        unfolding part1.simps[of a l r p]
    7.44          by (elim crelE crel_nth crel_if crel_return) auto
    7.45        from rec_condition have "l + 1 \<le> r" by arith
    7.46        from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    7.47 @@ -86,7 +85,7 @@
    7.48        with rec_condition cr
    7.49        obtain h1 where swp: "crel (swap a l r) h h1 ()"
    7.50          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    7.51 -        unfolding part1.simps[of a l r p] run_drop
    7.52 +        unfolding part1.simps[of a l r p]
    7.53          by (elim crelE crel_nth crel_if crel_return) auto
    7.54        from rec_condition have "l \<le> r - 1" by arith
    7.55        from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    7.56 @@ -106,12 +105,12 @@
    7.57    proof (cases "r \<le> l")
    7.58      case True (* Terminating case *)
    7.59      with cr show ?thesis
    7.60 -      unfolding part1.simps[of a l r p] run_drop
    7.61 +      unfolding part1.simps[of a l r p]
    7.62        by (elim crelE crel_if crel_return crel_nth) auto
    7.63    next
    7.64      case False (* recursive case *)
    7.65      with cr 1 show ?thesis
    7.66 -      unfolding part1.simps [of a l r p] swap_def run_drop
    7.67 +      unfolding part1.simps [of a l r p] swap_def
    7.68        by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
    7.69    qed
    7.70  qed
    7.71 @@ -128,7 +127,7 @@
    7.72    proof (cases "r \<le> l")
    7.73      case True (* Terminating case *)
    7.74      with cr show ?thesis
    7.75 -      unfolding part1.simps[of a l r p] run_drop
    7.76 +      unfolding part1.simps[of a l r p]
    7.77        by (elim crelE crel_if crel_return crel_nth) auto
    7.78    next
    7.79      case False (* recursive case *)
    7.80 @@ -139,7 +138,7 @@
    7.81        case True
    7.82        with cr False
    7.83        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    7.84 -        unfolding part1.simps[of a l r p] run_drop
    7.85 +        unfolding part1.simps[of a l r p]
    7.86          by (elim crelE crel_nth crel_if crel_return) auto
    7.87        from 1(1)[OF rec_condition True rec1]
    7.88        show ?thesis by fastsimp
    7.89 @@ -148,11 +147,11 @@
    7.90        with rec_condition cr
    7.91        obtain h1 where swp: "crel (swap a l r) h h1 ()"
    7.92          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    7.93 -        unfolding part1.simps[of a l r p] run_drop
    7.94 +        unfolding part1.simps[of a l r p]
    7.95          by (elim crelE crel_nth crel_if crel_return) auto
    7.96        from swp rec_condition have
    7.97          "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
    7.98 -	unfolding swap_def run_drop
    7.99 +	unfolding swap_def
   7.100  	by (elim crelE crel_nth crel_upd crel_return) auto
   7.101        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   7.102      qed
   7.103 @@ -173,7 +172,7 @@
   7.104    proof (cases "r \<le> l")
   7.105      case True (* Terminating case *)
   7.106      with cr have "rs = r"
   7.107 -      unfolding part1.simps[of a l r p] run_drop
   7.108 +      unfolding part1.simps[of a l r p]
   7.109        by (elim crelE crel_if crel_return crel_nth) auto
   7.110      with True
   7.111      show ?thesis by auto
   7.112 @@ -186,7 +185,7 @@
   7.113        case True
   7.114        with lr cr
   7.115        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   7.116 -        unfolding part1.simps[of a l r p] run_drop
   7.117 +        unfolding part1.simps[of a l r p]
   7.118          by (elim crelE crel_nth crel_if crel_return) auto
   7.119        from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   7.120  	by fastsimp
   7.121 @@ -198,10 +197,10 @@
   7.122        with lr cr
   7.123        obtain h1 where swp: "crel (swap a l r) h h1 ()"
   7.124          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   7.125 -        unfolding part1.simps[of a l r p] run_drop
   7.126 +        unfolding part1.simps[of a l r p]
   7.127          by (elim crelE crel_nth crel_if crel_return) auto
   7.128        from swp False have "get_array a h1 ! r \<ge> p"
   7.129 -	unfolding swap_def run_drop
   7.130 +	unfolding swap_def
   7.131  	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
   7.132        with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   7.133  	by fastsimp
   7.134 @@ -232,7 +231,7 @@
   7.135    = multiset_of (get_array a h)"
   7.136  proof -
   7.137      from assms part_permutes swap_permutes show ?thesis
   7.138 -      unfolding partition.simps run_drop
   7.139 +      unfolding partition.simps
   7.140        by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   7.141  qed
   7.142  
   7.143 @@ -241,7 +240,7 @@
   7.144    shows "Heap.length a h = Heap.length a h'"
   7.145  proof -
   7.146    from assms part_length_remains show ?thesis
   7.147 -    unfolding partition.simps run_drop swap_def
   7.148 +    unfolding partition.simps swap_def
   7.149      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   7.150  qed
   7.151  
   7.152 @@ -251,7 +250,7 @@
   7.153    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   7.154  proof -
   7.155    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   7.156 -    unfolding partition.simps swap_def run_drop
   7.157 +    unfolding partition.simps swap_def
   7.158      by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   7.159  qed
   7.160  
   7.161 @@ -263,7 +262,7 @@
   7.162    from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   7.163      and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   7.164           else middle)"
   7.165 -    unfolding partition.simps run_drop
   7.166 +    unfolding partition.simps
   7.167      by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   7.168    from `l < r` have "l \<le> r - 1" by arith
   7.169    from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   7.170 @@ -280,17 +279,17 @@
   7.171      and swap: "crel (swap a rs r) h1 h' ()"
   7.172      and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   7.173           else middle)"
   7.174 -    unfolding partition.simps run_drop
   7.175 +    unfolding partition.simps
   7.176      by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   7.177    from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
   7.178      (Heap.upd a rs (get_array a h1 ! r) h1)"
   7.179 -    unfolding swap_def run_drop
   7.180 +    unfolding swap_def
   7.181      by (elim crelE crel_return crel_nth crel_upd) simp
   7.182    from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
   7.183 -    unfolding swap_def run_drop
   7.184 +    unfolding swap_def
   7.185      by (elim crelE crel_return crel_nth crel_upd) simp
   7.186    from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
   7.187 -    unfolding swap_def run_drop by (elim crelE crel_return crel_nth crel_upd) auto
   7.188 +    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   7.189    from `l < r` have "l \<le> r - 1" by simp 
   7.190    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   7.191    from part_outer_remains[OF part] `l < r`
   7.192 @@ -298,7 +297,7 @@
   7.193      by fastsimp
   7.194    with swap
   7.195    have right_remains: "get_array a h ! r = get_array a h' ! rs"
   7.196 -    unfolding swap_def run_drop
   7.197 +    unfolding swap_def
   7.198      by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   7.199    from part_partitions [OF part]
   7.200    show ?thesis
   7.201 @@ -414,7 +413,7 @@
   7.202  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   7.203    case (1 a l r h h' rs)
   7.204    with partition_permutes show ?case
   7.205 -    unfolding quicksort.simps [of a l r] run_drop
   7.206 +    unfolding quicksort.simps [of a l r]
   7.207      by (elim crel_if crelE crel_assert crel_return) auto
   7.208  qed
   7.209  
   7.210 @@ -425,7 +424,7 @@
   7.211  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   7.212    case (1 a l r h h' rs)
   7.213    with partition_length_remains show ?case
   7.214 -    unfolding quicksort.simps [of a l r] run_drop
   7.215 +    unfolding quicksort.simps [of a l r]
   7.216      by (elim crel_if crelE crel_assert crel_return) auto
   7.217  qed
   7.218  
   7.219 @@ -463,7 +462,7 @@
   7.220        ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   7.221      }
   7.222      with cr show ?thesis
   7.223 -      unfolding quicksort.simps [of a l r] run_drop
   7.224 +      unfolding quicksort.simps [of a l r]
   7.225        by (elim crel_if crelE crel_assert crel_return) auto
   7.226    qed
   7.227  qed
   7.228 @@ -472,7 +471,7 @@
   7.229    assumes "crel (quicksort a l r) h h' rs"
   7.230    shows "r \<le> l \<longrightarrow> h = h'"
   7.231    using assms
   7.232 -  unfolding quicksort.simps [of a l r] run_drop
   7.233 +  unfolding quicksort.simps [of a l r]
   7.234    by (elim crel_if crel_return) auto
   7.235   
   7.236  lemma quicksort_sorts:
   7.237 @@ -544,7 +543,7 @@
   7.238  	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   7.239      }
   7.240      with True cr show ?thesis
   7.241 -      unfolding quicksort.simps [of a l r] run_drop
   7.242 +      unfolding quicksort.simps [of a l r]
   7.243        by (elim crel_if crel_return crelE crel_assert) auto
   7.244    qed
   7.245  qed
   7.246 @@ -577,7 +576,7 @@
   7.247  proof (induct a l r p arbitrary: h rule: part1.induct)
   7.248    case (1 a l r p)
   7.249    thus ?case
   7.250 -    unfolding part1.simps [of a l r] swap_def run_drop
   7.251 +    unfolding part1.simps [of a l r] swap_def
   7.252      by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
   7.253  qed
   7.254  
   7.255 @@ -585,7 +584,7 @@
   7.256    assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   7.257    shows "noError (partition a l r) h"
   7.258  using assms
   7.259 -unfolding partition.simps swap_def run_drop
   7.260 +unfolding partition.simps swap_def
   7.261  apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
   7.262  apply (frule part_length_remains)
   7.263  apply (frule part_returns_index_in_bounds)
   7.264 @@ -604,7 +603,7 @@
   7.265  proof (induct a l r arbitrary: h rule: quicksort.induct)
   7.266    case (1 a l ri h)
   7.267    thus ?case
   7.268 -    unfolding quicksort.simps [of a l ri] run_drop
   7.269 +    unfolding quicksort.simps [of a l ri]
   7.270      apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
   7.271      apply (frule partition_returns_index_in_bounds)
   7.272      apply auto
   7.273 @@ -614,7 +613,7 @@
   7.274      apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   7.275      apply (erule disjE)
   7.276      apply auto
   7.277 -    unfolding quicksort.simps [of a "Suc ri" ri] run_drop
   7.278 +    unfolding quicksort.simps [of a "Suc ri" ri]
   7.279      apply (auto intro!: noError_if noError_return)
   7.280      done
   7.281  qed
     8.1 --- a/src/HOL/ex/Quickcheck.thy	Fri Sep 05 11:50:35 2008 +0200
     8.2 +++ b/src/HOL/ex/Quickcheck.thy	Sat Sep 06 14:02:36 2008 +0200
     8.3 @@ -27,6 +27,25 @@
     8.4  
     8.5  text {* Datatypes *}
     8.6  
     8.7 +definition
     8.8 +  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
     8.9 +  "collapse f = (do g \<leftarrow> f; g done)"
    8.10 +
    8.11 +ML {*
    8.12 +structure StateMonad =
    8.13 +struct
    8.14 +
    8.15 +fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    8.16 +fun liftT' sT = sT --> sT;
    8.17 +
    8.18 +fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    8.19 +
    8.20 +fun scomp T1 T2 sT f g = Const (@{const_name scomp},
    8.21 +  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    8.22 +
    8.23 +end;
    8.24 +*}
    8.25 +
    8.26  lemma random'_if:
    8.27    fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    8.28    assumes "random' 0 j = undefined"
    8.29 @@ -62,7 +81,7 @@
    8.30          mk_scomp_split thy ty this_ty random)
    8.31            args return;
    8.32        val is_rec = exists (snd o fst) args;
    8.33 -    in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
    8.34 +    in (is_rec, t) end;
    8.35    fun mk_conss thy ty [] = NONE
    8.36      | mk_conss thy ty [(_, t)] = SOME t
    8.37      | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
     9.1 --- a/src/HOL/ex/Random.thy	Fri Sep 05 11:50:35 2008 +0200
     9.2 +++ b/src/HOL/ex/Random.thy	Sat Sep 06 14:02:36 2008 +0200
     9.3 @@ -55,18 +55,6 @@
     9.4    "(if b then f x else f y) = f (if b then x else y)"
     9.5    by (cases b) simp_all
     9.6  
     9.7 -(*lemma seed_invariant:
     9.8 -  assumes "seed_invariant (index_of_nat v, index_of_nat w)"
     9.9 -    and "(index_of_nat z, (index_of_nat v', index_of_nat w')) = next (index_of_nat v, index_of_nat w)"
    9.10 -  shows "seed_invariant (index_of_nat v', index_of_nat w')"
    9.11 -using assms
    9.12 -apply (auto simp add: seed_invariant_def)
    9.13 -apply (auto simp add: minus_shift_def Let_def)
    9.14 -apply (simp_all add: if_same cong del: if_cong)
    9.15 -apply safe
    9.16 -unfolding not_less
    9.17 -oops*)
    9.18 -
    9.19  definition
    9.20    split_seed :: "seed \<Rightarrow> seed \<times> seed"
    9.21  where
    9.22 @@ -109,7 +97,7 @@
    9.23      "range_aux (log 2147483561 k) 1 s = (v, w)"
    9.24      by (cases "range_aux (log 2147483561 k) 1 s")
    9.25    with assms show ?thesis
    9.26 -    by (simp add: range_def run_def scomp_def split_def del: range_aux.simps log.simps)
    9.27 +    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
    9.28  qed
    9.29  
    9.30  definition
    9.31 @@ -130,7 +118,7 @@
    9.32    then have
    9.33      "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
    9.34    then show ?thesis
    9.35 -    by (auto simp add: select_def run_def scomp_def split_def)
    9.36 +    by (auto simp add: monad_collapse select_def)
    9.37  qed
    9.38  
    9.39  definition
    9.40 @@ -143,7 +131,7 @@
    9.41  
    9.42  lemma select_default_zero:
    9.43    "fst (select_default 0 x y s) = y"
    9.44 -  by (simp add: run_def scomp_def split_def select_default_def)
    9.45 +  by (simp add: monad_collapse select_default_def)
    9.46  
    9.47  lemma select_default_code [code]:
    9.48    "select_default k x y = (if k = 0 then do
    9.49 @@ -157,7 +145,7 @@
    9.50    case False then show ?thesis by (simp add: select_default_def)
    9.51  next
    9.52    case True then show ?thesis
    9.53 -    by (simp add: run_def scomp_def split_def select_default_def expand_fun_eq range_def)
    9.54 +    by (simp add: monad_collapse select_default_def range_def)
    9.55  qed
    9.56  
    9.57  
    9.58 @@ -192,3 +180,4 @@
    9.59  *}
    9.60  
    9.61  end
    9.62 +
    10.1 --- a/src/Tools/code/code_haskell.ML	Fri Sep 05 11:50:35 2008 +0200
    10.2 +++ b/src/Tools/code/code_haskell.ML	Sat Sep 06 14:02:36 2008 +0200
    10.3 @@ -425,50 +425,45 @@
    10.4  
    10.5  (** optional monad syntax **)
    10.6  
    10.7 -fun implode_monad c_bind t =
    10.8 -  let
    10.9 -    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   10.10 -          if c = c_bind
   10.11 -            then case Code_Thingol.split_abs t2
   10.12 -             of SOME (((v, pat), ty), t') =>
   10.13 -                  SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   10.14 -              | NONE => NONE
   10.15 -            else NONE
   10.16 -      | dest_monad t = case Code_Thingol.split_let t
   10.17 -           of SOME (((pat, ty), tbind), t') =>
   10.18 -                SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   10.19 -            | NONE => NONE;
   10.20 -  in Code_Thingol.unfoldr dest_monad t end;
   10.21 -
   10.22  fun pretty_haskell_monad c_bind =
   10.23    let
   10.24 -    fun pretty pr thm pat vars fxy [(t, _)] =
   10.25 -      let
   10.26 -        val pr_bind = pr_haskell_bind (K (K pr)) thm;
   10.27 -        fun pr_monad (NONE, t) vars =
   10.28 -              (semicolon [pr vars NOBR t], vars)
   10.29 -          | pr_monad (SOME (bind, true), t) vars = vars
   10.30 -              |> pr_bind NOBR bind
   10.31 -              |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
   10.32 -          | pr_monad (SOME (bind, false), t) vars = vars
   10.33 -              |> pr_bind NOBR bind
   10.34 -              |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   10.35 -        val (binds, t) = implode_monad c_bind t;
   10.36 -        val (ps, vars') = fold_map pr_monad binds vars;
   10.37 -      in (brackify fxy o single o Pretty.enclose "do {" "}") (ps @| pr vars' NOBR t) end;
   10.38 -  in (1, pretty) end;
   10.39 +    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
   10.40 +     of SOME (((v, pat), ty), t') =>
   10.41 +          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   10.42 +      | NONE => NONE;
   10.43 +    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   10.44 +          if c = c_bind then dest_bind t1 t2
   10.45 +          else NONE
   10.46 +      | dest_monad t = case Code_Thingol.split_let t
   10.47 +         of SOME (((pat, ty), tbind), t') =>
   10.48 +              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   10.49 +          | NONE => NONE;
   10.50 +    val implode_monad = Code_Thingol.unfoldr dest_monad;
   10.51 +    fun pr_monad pr_bind pr (NONE, t) vars =
   10.52 +          (semicolon [pr vars NOBR t], vars)
   10.53 +      | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
   10.54 +          |> pr_bind NOBR bind
   10.55 +          |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
   10.56 +      | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   10.57 +          |> pr_bind NOBR bind
   10.58 +          |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   10.59 +    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   10.60 +     of SOME (bind, t') => let
   10.61 +          val (binds, t'') = implode_monad t'
   10.62 +          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
   10.63 +        in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   10.64 +      | NONE => brackify_infix (1, L) fxy
   10.65 +          [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
   10.66 +  in (2, pretty) end;
   10.67  
   10.68 -fun add_monad target' raw_c_run raw_c_bind thy =
   10.69 +fun add_monad target' raw_c_bind thy =
   10.70    let
   10.71 -    val c_run = Code_Unit.read_const thy raw_c_run;
   10.72      val c_bind = Code_Unit.read_const thy raw_c_bind;
   10.73      val c_bind' = Code_Name.const thy c_bind;
   10.74    in if target = target' then
   10.75      thy
   10.76 -    |> Code_Target.add_syntax_const target c_run
   10.77 +    |> Code_Target.add_syntax_const target c_bind
   10.78          (SOME (pretty_haskell_monad c_bind'))
   10.79 -    |> Code_Target.add_syntax_const target c_bind
   10.80 -        (Code_Printer.simple_const_syntax (SOME (Code_Printer.parse_infix fst (L, 1) ">>=")))
   10.81    else error "Only Haskell target allows for monad syntax" end;
   10.82  
   10.83  
   10.84 @@ -482,9 +477,8 @@
   10.85  
   10.86  val _ =
   10.87    OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
   10.88 -    OuterParse.term_group -- OuterParse.term_group -- OuterParse.name
   10.89 -    >> (fn ((raw_run, raw_bind), target) => Toplevel.theory 
   10.90 -          (add_monad target raw_run raw_bind))
   10.91 +    OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
   10.92 +      Toplevel.theory  (add_monad target raw_bind))
   10.93    );
   10.94  
   10.95  val setup =