# HG changeset patch
# User haftmann
# Date 1256655922 -3600
# Node ID b207d84b64ad26cec5c8ada6283fe5aca75ff7b1
# Parent  f9ff11344ec4a351b8c51d90d67abc86d4ac7c8d# Parent  aac547760e1672e83f2d7be917d84f2b04476ad6
merged

diff -r f9ff11344ec4 -r b207d84b64ad src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy	Tue Oct 27 16:05:22 2009 +0100
@@ -35,4 +35,28 @@
 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
 
+
+definition implode :: "string \<Rightarrow> String.literal" where
+  "implode = STR"
+
+primrec explode :: "String.literal \<Rightarrow> string" where
+  "explode (STR s) = s"
+
+lemma [code]:
+  "literal_case f s = f (explode s)"
+  "literal_rec f s = f (explode s)"
+  by (cases s, simp)+
+
+code_reserved SML String
+
+code_const implode
+  (SML "String.implode")
+  (OCaml "failwith/ \"implode\"")
+  (Haskell "_")
+
+code_const explode
+  (SML "String.explode")
+  (OCaml "failwith/ \"explode\"")
+  (Haskell "_")
+
 end
diff -r f9ff11344ec4 -r b207d84b64ad src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Nitpick.thy	Tue Oct 27 16:05:22 2009 +0100
@@ -28,7 +28,6 @@
 
 typedecl bisim_iterator
 
-(* FIXME: use axiomatization (here and elsewhere) *)
 axiomatization unknown :: 'a
            and undefined_fast_The :: 'a
            and undefined_fast_Eps :: 'a
diff -r f9ff11344ec4 -r b207d84b64ad src/HOL/Random.thy
--- a/src/HOL/Random.thy	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Random.thy	Tue Oct 27 16:05:22 2009 +0100
@@ -12,15 +12,15 @@
 
 subsection {* Auxiliary functions *}
 
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
+
 definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "inc_shift v k = (if v = k then 1 else k + 1)"
 
 definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "minus_shift r k l = (if k < l then r + k - l else k - l)"
 
-fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
-  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
-
 
 subsection {* Random seeds *}
 
@@ -29,28 +29,19 @@
 primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
   "next (v, w) = (let
      k =  v div 53668;
-     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
+     v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211);
      l =  w div 52774;
-     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
+     w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791);
      z =  minus_shift 2147483562 v' (w' + 1) + 1
    in (z, (v', w')))"
 
-lemma next_not_0:
-  "fst (next s) \<noteq> 0"
-  by (cases s) (auto simp add: minus_shift_def Let_def)
-
-primrec seed_invariant :: "seed \<Rightarrow> bool" where
-  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
-
 definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
   "split_seed s = (let
      (v, w) = s;
      (v', w') = snd (next s);
      v'' = inc_shift 2147483562 v;
-     s'' = (v'', w');
-     w'' = inc_shift 2147483398 w;
-     s''' = (v', w'')
-   in (s'', s'''))"
+     w'' = inc_shift 2147483398 w
+   in ((v'', w'), (v', w'')))"
 
 
 subsection {* Base selectors *}
@@ -175,7 +166,7 @@
 *}
 
 hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
+hide (open) const inc_shift minus_shift log "next" split_seed
   iterate range select pick select_weight
 
 no_notation fcomp (infixl "o>" 60)
diff -r f9ff11344ec4 -r b207d84b64ad src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/String.thy	Tue Oct 27 16:05:22 2009 +0100
@@ -155,7 +155,7 @@
 
 datatype literal = STR string
 
-lemmas [code del] = literal.recs literal.cases
+declare literal.cases [code del] literal.recs [code del]
 
 lemma [code]: "size (s\<Colon>literal) = 0"
   by (cases s) simp_all
@@ -168,6 +168,9 @@
 
 use "Tools/string_code.ML"
 
+code_reserved SML string
+code_reserved OCaml string
+
 code_type literal
   (SML "string")
   (OCaml "string")
@@ -185,9 +188,6 @@
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
 
-code_reserved SML string
-code_reserved OCaml string
-
 
 types_code
   "char" ("string")