added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;

--- a/src/HOL/ROOT	Thu May 30 17:52:38 2013 +0200
+++ b/src/HOL/ROOT	Thu May 30 20:09:49 2013 +0200
@@ -740,6 +740,10 @@
   options [document = false]
   theories WordExamples
 
+session "HOL-Spec_Check" in Spec_Check = HOL +
+  theories
+    Examples
+
 session "HOL-Statespace" in Statespace = HOL +
   theories [skip_proofs = false]
     StateSpaceEx

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/Examples.thy	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,73 @@
+theory Examples
+imports Spec_Check
+begin
+
+section {* List examples *}
+
+ML {*
+check_property @{context} "ALL xs. rev xs = xs";
+*}
+
+ML {*
+check_property @{context} "ALL xs. rev (rev xs) = xs";
+*}
+
+
+section {* AList Specification *}
+
+ML {*
+(* map_entry applies the function to the element *)
+check_property @{context} "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
+
+(* update always results in an entry *)
+check_property @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
+
+(* update always writes the value *)
+check_property @{context} "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
+
+(* default always results in an entry *)
+check_property @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
+
+(* delete always removes the entry *)
+check_property @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
+
+(* default writes the entry iff it didn't exist *)
+check_property @{context} "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
+*}
+
+section {* Examples on Types and Terms *}
+
+ML {*
+check_property @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
+*}
+
+ML {*
+check_property @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
+*}
+
+text {* One would think this holds: *}
+
+ML {*
+check_property @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
+*}
+
+text {* But it only holds with this precondition: *}
+
+ML {*
+check_property @{context} "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
+*}
+
+section {* Some surprises *}
+
+ML {*
+check_property @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
+*}
+
+
+
+ML {* val thy = @{theory}; *}
+ML {*
+  check_property @{context} "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
+*}
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/README	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,47 @@
+This is a Quickcheck tool for Isabelle's ML environment.
+
+Authors
+
+  Lukas Bulwahn
+  Nicolai Schaffroth
+
+Quick Usage
+
+  - Import Spec_Check.thy in your development
+  - Look at examples in Examples.thy
+  - write specifications with the ML function
+      Spec_Check.check_property @{context} "ALL x. P x"
+
+Notes
+
+Our specification-based testing tool originated from Christopher League's
+QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
+provides a rich and uniform ML platform (called Isabelle/ML), this
+testing tools is very different than the one for a typical ML developer.
+
+1. Isabelle/ML provides common data structures, which we can use in the
+tool's implementation for storing data and printing output.
+
+2. The implementation in Isabelle that will be checked with this tool
+commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
+but they do not use other integer types in ML, such as ML's Int.int,
+Word.word and others.
+
+3. As Isabelle can run heavily in parallel, we avoid reference types.
+
+4. Isabelle has special naming conventions and documentation of source
+code is only minimal to avoid parroting.
+
+Next steps:
+  - Remove all references and store the neccessary random seed in the
+    Isabelle's context.
+  - Simplify some existing random generators.
+    The original ones from Christopher League are so complicated to
+    support many integer types uniformly.
+
+License
+
+  The source code originated from Christopher League's QCheck, which is
+  licensed under the 2-clause BSD license. The current source code is
+  licensed under the compatible 3-clause BSD license of Isabelle.
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/Spec_Check.thy	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,15 @@
+theory Spec_Check
+imports Main
+begin
+
+ML_file "random.ML"
+ML_file "property.ML"
+ML_file "base_generator.ML"
+ML_file "generator.ML"
+ML_file "gen_construction.ML"
+ML_file "spec_check.ML"
+ML_file "output_style.ML"
+
+setup {* Perl_Style.setup #> CMStyle.setup *}
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/base_generator.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,201 @@
+(*  Title:      HOL/Spec_Check/base_generator.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Basic random generators.
+*)
+
+signature BASE_GENERATOR =
+sig
+
+type rand
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+val new : unit -> rand
+val range : int * int -> rand -> int * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+val lift : 'a -> 'a gen
+val select : 'a vector -> 'a gen
+val choose : 'a gen vector -> 'a gen
+val choose' : (int * 'a gen) vector -> 'a gen
+val selectL : 'a list -> 'a gen
+val chooseL : 'a gen list -> 'a gen
+val chooseL' : (int * 'a gen) list -> 'a gen
+val filter : ('a -> bool) -> 'a gen -> 'a gen
+
+val zip : ('a gen * 'b gen) -> ('a * 'b) gen
+val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
+val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
+val map : ('a -> 'b) -> 'a gen -> 'b gen
+val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
+val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
+val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
+
+val flip : bool gen
+val flip' : int * int -> bool gen
+
+val list : bool gen -> 'a gen -> 'a list gen
+val option : bool gen -> 'a gen -> 'a option gen
+val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
+
+val variant : (int, 'b) co
+val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
+val cobool : (bool, 'b) co
+val colist : ('a, 'b) co -> ('a list, 'b) co
+val coopt : ('a, 'b) co -> ('a option, 'b) co
+
+type stream
+val start : rand -> stream
+val limit : int -> 'a gen -> ('a, stream) reader
+
+end
+
+structure Base_Generator : BASE_GENERATOR =
+struct
+
+(* random number engine *)
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+  let
+    val t = a * seed
+  in
+    t - m * real (floor (t / m))
+  end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+  if min > max then raise Domain (* TODO: raise its own error *)
+  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
+
+fun split r =
+  let
+    val r = r / a
+    val r0 = real (floor r)
+    val r1 = r - r0
+  in
+    (nextrand r0, nextrand r1)
+  end
+
+(* generators *)
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+fun lift obj r = (obj, r)
+
+local open Vector (* Isabelle does not use vectors? *)
+      fun explode ((freq, gen), acc) =
+          List.tabulate (freq, fn _ => gen) @ acc
+in fun choose v r =
+       let val (i, r) = range(0, length v - 1) r
+        in sub (v, i) r
+       end
+   fun choose' v = choose (fromList (foldr explode nil v))
+   fun select v = choose (map lift v)
+end
+
+fun chooseL l = choose (Vector.fromList l)
+fun chooseL' l = choose' (Vector.fromList l)
+fun selectL l = select (Vector.fromList l)
+
+fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
+
+fun zip3 (g1, g2, g3) =
+  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
+
+fun zip4 (g1, g2, g3, g4) =
+  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
+
+fun map f g = apfst f o g
+
+fun map2 f = map f o zip
+fun map3 f = map f o zip3
+fun map4 f = map f o zip4
+
+fun filter p gen r =
+  let
+    fun loop (x, r) = if p x then (x, r) else loop (gen r)
+  in
+    loop (gen r)
+  end
+
+val flip = selectL [true, false]
+fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
+
+fun list flip g r =
+  case flip r of
+      (true, r) => (nil, r)
+    | (false, r) =>
+      let
+        val (x,r) = g r
+        val (xs,r) = list flip g r
+      in (x::xs, r) end
+
+fun option flip g r =
+  case flip r of
+    (true, r) => (NONE, r)
+  | (false, r) => map SOME g r
+
+fun vector tabulate (int, elem) r =
+  let
+    val (n, r) = int r
+    val p = Unsynchronized.ref r
+    fun g _ =
+      let
+        val (x,r) = elem(!p)
+      in x before p := r end
+  in
+    (tabulate(n, g), !p)
+  end
+
+type stream = rand Unsynchronized.ref * int
+
+fun start r = (Unsynchronized.ref r, 0)
+
+fun limit max gen =
+  let
+    fun next (p, i) =
+      if i >= max then NONE
+      else
+        let val (x, r) = gen(!p)
+        in SOME(x, (p, i+1)) before p := r end
+  in
+    next
+  end
+
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+fun variant v g r =
+  let
+    fun nth (i, r) =
+      let val (r1, r2) = split r
+      in if i = 0 then r1 else nth (i-1, r2) end
+  in
+    g (nth (v, r))
+  end
+
+fun arrow (cogen, gen) r =
+  let
+    val (r1, r2) = split r
+    fun g x = fst (cogen x gen r1)
+  in (g, r2) end
+
+fun cobool false = variant 0
+  | cobool true = variant 1
+
+fun colist _ [] = variant 0
+  | colist co (x::xs) = variant 1 o co x o colist co xs
+
+fun coopt _ NONE = variant 0
+  | coopt co (SOME x) = variant 1 o co x
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,171 @@
+(*  Title:      HOL/Spec_Check/gen_construction.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Constructing generators and pretty printing function for complex types.
+*)
+
+signature GEN_CONSTRUCTION =
+sig
+  val register : string * (string * string) -> theory -> theory
+  type mltype
+  val parse_pred : string -> string * mltype;
+  val build_check : theory -> string -> mltype * string -> string
+  (*val safe_check : string -> mltype * string -> string*)
+  val string_of_bool : bool -> string
+  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
+end;
+
+structure Gen_Construction : GEN_CONSTRUCTION =
+struct
+
+(* Parsing ML types *)
+
+datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
+
+(*Split string into tokens for parsing*)
+fun split s =
+  let
+    fun split_symbol #"(" = "( "
+      | split_symbol #")" = " )"
+      | split_symbol #"," = " ,"
+      | split_symbol #":" = " :"
+      | split_symbol c = Char.toString c
+    fun is_space c = c = #" "
+  in String.tokens is_space (String.translate split_symbol s) end;
+
+(*Accept anything that is not a recognized symbol*)
+val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
+
+(*Turn a type list into a nested Con*)
+fun make_con nil = raise Empty
+  | make_con [c] = c
+  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
+
+(*Parse a type*)
+fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
+
+and parse_type_arg s = (parse_tuple || parse_type_single) s
+
+and parse_type_single s = (parse_con || parse_type_basic) s
+
+and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
+
+and parse_list s =
+  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
+
+and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
+
+and parse_con s = ((parse_con_nest
+  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
+  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
+  >> (make_con o rev)) s
+
+and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, nil)))) s
+
+and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
+
+and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
+  >> (fn (t, tl) => Tuple (t :: tl))) s;
+
+(*Parses entire type + name*)
+fun parse_function s =
+  let
+    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
+    val (name, ty) = p (split s)
+    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+    val (typ, _) = Scan.finite stop parse_type ty
+  in (name, typ) end;
+
+(*Creates desired output*)
+fun parse_pred s =
+  let
+    val (name, Con ("->", t :: _)) = parse_function s
+  in (name, t) end;
+
+(* Construct Generators and Pretty Printers *)
+
+(*copied from smt_config.ML *)
+fun string_of_bool b = if b then "true" else "false"
+
+fun string_of_ref f r = f (!r) ^ " ref";
+
+val initial_content = Symtab.make
+  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
+  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
+  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
+  ("unit", ("gen_unit", "fn () => \"()\"")),
+  ("int", ("Generator.int", "string_of_int")),
+  ("real", ("Generator.real", "string_of_real")),
+  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
+  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
+  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
+  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
+  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
+
+structure Data = Theory_Data
+(
+  type T = (string * string) Symtab.table
+  val empty = initial_content
+  val extend = I
+  fun merge data : T = Symtab.merge (K true) data
+)
+
+fun data_of thy tycon = case Symtab.lookup (Data.get thy) tycon of SOME data => data
+  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)
+
+val generator_of = fst oo data_of
+val printer_of = snd oo data_of
+
+fun register (ty, data) = Data.map (Symtab.update (ty, data))
+
+(*
+fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
+*)
+
+fun combine dict [] = dict
+  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
+
+fun compose_generator _ Var = "Generator.int"
+  | compose_generator thy (Con (s, types)) =
+      combine (generator_of thy s) (map (compose_generator thy) types)
+  | compose_generator thy (Tuple t) =
+    let
+      fun tuple_body t = space_implode ""
+        (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
+        compose_generator thy ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
+      fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+    in "fn r0 => let " ^ tuple_body t ^
+      "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" end;
+
+fun compose_printer _ Var = "Int.toString"
+  | compose_printer thy (Con (s, types)) =
+      combine (printer_of thy s) (map (compose_printer thy) types)
+  | compose_printer thy (Tuple t) =
+    let
+      fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+      fun tuple_body t = space_implode " ^ \", \" ^ "
+        (map (fn (ty, n) => "(" ^ compose_printer thy ty ^ ") x" ^ string_of_int n)
+        (t ~~ (1 upto (length t))))
+    in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
+
+(*produces compilable string*)
+fun build_check thy name (ty, spec) = "Spec_Check.checkGen (ML_Context.the_generic_context ()) ("
+  ^ compose_generator thy ty ^ ", SOME (" ^ compose_printer thy ty ^ ")) (\""
+  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
+
+(*produces compilable string - non-eqtype functions*)
+(*
+fun safe_check name (ty, spec) =
+  let
+    val default = case AList.lookup (op =) (!gen_table) "->"
+      of NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+      | SOME entry => entry
+  in (gen_table := AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\""))
+   (!gen_table);
+    build_check name (ty, spec) before
+    gen_table := AList.update (op =) ("->", default) (!gen_table)) end;
+*)
+
+end;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/generator.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,231 @@
+(*  Title:      HOL/Spec_Check/generator.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random generators for Isabelle/ML's types.
+*)
+
+signature GENERATOR = sig
+  include BASE_GENERATOR
+  (* text generators *)
+  val char : char gen
+  val charRange : char * char -> char gen
+  val charFrom : string -> char gen
+  val charByType : (char -> bool) -> char gen
+  val string : (int gen * char gen) -> string gen
+  val substring : string gen -> substring gen
+  val cochar : (char, 'b) co
+  val costring : (string, 'b) co
+  val cosubstring : (substring, 'b) co
+  (* integer generators *)
+  val int : int gen
+  val int_pos : int gen
+  val int_neg : int gen
+  val int_nonpos : int gen
+  val int_nonneg : int gen
+  val coint : (int, 'b) co
+  (* real generators *)
+  val real : real gen
+  val real_frac : real gen
+  val real_pos : real gen
+  val real_neg : real gen
+  val real_nonpos : real gen
+  val real_nonneg : real gen
+  val real_finite : real gen
+  (* function generators *)
+  val function_const : 'c * 'b gen -> ('a -> 'b) gen
+  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
+  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
+  val unit : unit gen
+  val ref' : 'a gen -> 'a Unsynchronized.ref gen
+  (* more generators *)
+  val term : int -> term gen
+  val typ : int -> typ gen
+
+  val stream : stream
+end
+
+structure Generator : GENERATOR =
+struct
+
+open Base_Generator
+
+val stream = start (new())
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+(* text *)
+
+open Text
+type char = Char.char
+type string = String.string
+type substring = Substring.substring
+
+
+val char = map Char.chr (range (0, Char.maxOrd))
+fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
+
+fun charFrom s =
+  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
+
+fun charByType p = filter p char
+
+val string = vector CharVector.tabulate
+
+fun substring gen r =
+    let val (s, r') = gen r
+        val (i, r'') = range (0, String.size s) r'
+        val (j, r''') = range (0, String.size s - i) r''
+    in
+      (Substring.substring (s, i, j), r''')
+    end
+
+fun cochar c =
+  if Char.ord c = 0 then variant 0
+  else variant 1 o cochar (Char.chr (Char.ord c div 2))
+
+fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
+
+fun costring s = cosubstring (Substring.full s)
+
+(* integers *)
+val digit = charRange (#"0", #"9")
+val nonzero = string (lift 1, charRange (#"1", #"9"))
+fun digits' n = string (range (0, n-1), digit)
+fun digits n = map2 op^ (nonzero, digits' n)
+
+val maxDigits = 64
+val ratio = 49
+
+fun pos_or_neg f r =
+  let
+    val (s, r') = digits maxDigits r
+  in (f (the (Int.fromString s)), r') end
+
+val int_pos = pos_or_neg I
+val int_neg = pos_or_neg Int.~
+val zero = lift 0
+
+val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
+val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
+val int = chooseL [int_nonneg, int_nonpos]
+
+fun coint n =
+  if n = 0 then variant 0
+  else if n < 0 then variant 1 o coint (~ n)
+  else variant 2 o coint (n div 2)
+
+(* reals *)
+val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
+
+fun real_frac r =
+  let val (s, r') = digits r
+  in (the (Real.fromString s), r') end
+
+val {exp=minExp,...} = Real.toManExp Real.minPos
+val {exp=maxExp,...} = Real.toManExp Real.posInf
+
+val ratio = 99
+
+fun mk r =
+  let
+    val (a, r') = digits r
+    val (b, r'') = digits r'
+    val (e, r''') = range (minExp div 4, maxExp div 4) r''
+    val x = String.concat [a, ".", b, "E", Int.toString e]
+  in
+    (the (Real.fromString x), r''')
+  end
+
+val real_pos = chooseL' (List.map ((pair 1) o lift)
+    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
+
+val real_neg = map Real.~ real_pos
+
+val real_zero = Real.fromInt 0
+val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
+val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
+
+val real = chooseL [real_nonneg, real_nonpos]
+
+val real_finite = filter Real.isFinite real
+
+(*alternate list generator - uses an integer generator to determine list length*)
+fun list' int gen = vector List.tabulate (int, gen);
+
+(* more function generators *)
+
+fun function_const (_, gen2) r =
+  let
+    val (v, r') = gen2 r
+  in (fn _ => v, r') end;
+
+fun function_strict size (gen1, gen2) r =
+  let
+    val (def, r') = gen2 r
+    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
+  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
+
+fun function_lazy (gen1, gen2) r =
+  let
+    val (initial1, r') = gen1 r
+    val (initial2, internal) = gen2 r'
+    val seed = Unsynchronized.ref internal
+    val table = Unsynchronized.ref [(initial1, initial2)]
+    fun new_entry k =
+      let
+        val (new_val, new_seed) = gen2 (!seed)
+        val _ =  seed := new_seed
+        val _ = table := AList.update (op =) (k, new_val) (!table)
+      in new_val end
+  in (fn v1 => case AList.lookup (op =) (!table) v1 of
+    NONE => new_entry v1 | SOME v2 => v2, r') end;
+
+(* unit *)
+
+fun unit r = ((), r);
+
+(* references *)
+
+fun ref' gen r =
+  let val (value, r') = gen r
+  in (Unsynchronized.ref value, r') end;
+
+(* types and terms *)
+
+val sort_string = selectL ["sort1", "sort2", "sort3"];
+val type_string = selectL ["TCon1", "TCon2", "TCon3"];
+val tvar_string = selectL ["a", "b", "c"];
+
+val const_string = selectL ["c1", "c2", "c3"];
+val var_string = selectL ["x", "y", "z"];
+val index = selectL [0, 1, 2, 3];
+val bound_index = selectL [0, 1, 2, 3];
+
+val sort = list (flip' (1, 2)) sort_string;
+
+fun typ n =
+  let
+    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
+    val tfree = map TFree (zip (tvar_string, sort))
+    val tvar = map TVar (zip (zip (tvar_string, index), sort))
+  in
+    if n = 0 then chooseL [tfree, tvar]
+    else chooseL [type' (n div 2), tfree, tvar]
+  end;
+
+fun term n =
+  let
+    val const = map Const (zip (const_string, typ 10))
+    val free = map Free (zip (var_string, typ 10))
+    val var = map Var (zip (zip (var_string, index), typ 10))
+    val bound = map Bound bound_index
+    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
+    fun app m = map (op $) (zip (term m, term m))
+  in
+    if n = 0 then chooseL [const, free, var, bound]
+    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
+  end;
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,117 @@
+(*  Title:      HOL/Spec_Check/output_style.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Output styles for presenting Spec_Check's results.
+*)
+
+structure Perl_Style =
+struct
+
+local
+
+open StringCvt
+
+fun new ctxt tag =
+  let
+    val target = Config.get_generic ctxt Spec_Check.gen_target
+    val namew = Config.get_generic ctxt Spec_Check.column_width
+    val sort_examples = Config.get_generic ctxt Spec_Check.sort_examples
+    val show_stats = Config.get_generic ctxt Spec_Check.show_stats
+    val limit = Config.get_generic ctxt Spec_Check.examples
+
+    val resultw = 8
+    val countw = 20
+    val allw = namew + resultw + countw + 2
+
+    val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
+
+    fun result ({count=0,...}, _) _ = "dubious"
+      | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
+      | result ({count,tags,...}, badobjs) true = if not (null badobjs) then "FAILED"
+          else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" else "ok"
+
+    fun ratio (0, _) = "(0/0 passed)"
+      | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
+      | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
+
+    fun update (stats, badobjs) donep =
+      "\r" ^ (padRight #"." namew tag) ^ "." ^ (padRight #" " resultw (result (stats, badobjs) donep))
+      ^ (padRight #" " countw (ratio (#count stats, length badobjs)))
+
+    fun status (_, result, (stats, badobjs)) =
+      if Property.failure result then Output.writeln (update (stats, badobjs) false) else ()
+
+    fun prtag count (tag, n) first =
+      if String.isPrefix "__" tag then ("", first)
+      else
+         let
+           val ratio = round ((real n / real count) * 100.0)
+         in
+           (((if first then "" else padRight #" " allw "\n") ^
+             padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
+           false)
+         end
+
+    fun prtags ({count, tags, ...} : Property.stats) =
+      if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
+
+    fun err badobjs =
+      let
+        fun iter [] _ = ()
+          | iter (e :: es) k =
+              (Output.writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
+                ^ padRight #" " resultw (if k > 0 then "" else ":") ^ e);
+              iter es (k + 1))
+      in
+        iter (maybe_sort (take limit (map_filter I badobjs))) 0
+      end
+
+    fun finish (stats, badobjs) =
+      if null badobjs then Output.writeln (update (stats, badobjs) true ^ prtags stats)
+      else (Output.writeln (update (stats, badobjs) true); err badobjs)
+  in
+    {status=status, finish=finish}
+  end
+
+in
+  val setup = Spec_Check.register_style ("Perl", new)
+end
+
+end
+
+(* CM style: meshes with CM output; highlighted in sml-mode *)
+
+structure CMStyle =
+struct
+
+local
+
+fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
+
+fun new ctxt tag =
+  let
+    val gen_target = Config.get_generic ctxt Spec_Check.gen_target
+    val _ = Output.writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
+    fun finish ({count, ...}, badobjs) = case (count, badobjs) of
+        (0, []) => Output.writeln ("no valid cases generated]")
+      | (n, []) => Output.writeln (
+            if n >= gen_target then "ok]"
+            else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
+      | (_, es) =>
+        let
+          val wd = size (string_of_int (length es))
+          fun each (NONE, _) = ()
+            | each (SOME e, i) = Output.writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+         in
+           (Output.writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+         end
+  in
+    {status = K (), finish = finish}
+  end
+
+in
+  val setup = Spec_Check.register_style ("CM", new)
+end
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/property.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,73 @@
+(*  Title:      HOL/Spec_Check/property.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Conditional properties that can track argument distribution.
+*)
+
+signature PROPERTY =
+sig
+
+type 'a pred = 'a -> bool
+type 'a prop
+val pred : 'a pred -> 'a prop
+val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
+val implies : 'a pred * 'a prop -> 'a prop
+val ==> : 'a pred * 'a pred -> 'a prop
+val trivial : 'a pred -> 'a prop -> 'a prop
+val classify : 'a pred -> string -> 'a prop -> 'a prop
+val classify' : ('a -> string option) -> 'a prop -> 'a prop
+
+(*Results*)
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+val test : 'a prop -> 'a * stats -> result * stats
+val stats : stats
+val success : result pred
+val failure : result pred
+
+end
+
+structure Property : PROPERTY =
+struct
+
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+type 'a pred = 'a -> bool
+type 'a prop = 'a * stats -> result * stats
+
+fun success (SOME true) = true
+  | success _ = false
+
+fun failure (SOME false) = true
+  | failure _ = false
+
+fun apply f x = SOME (f x) handle _ => SOME false (* TODO: do not catch all exceptions! *)
+fun pred f (x,s) = (apply f x, s)
+fun pred2 f z = pred (fn x => f (x, z))
+
+fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
+
+fun ==> (p1, p2) = implies (p1, pred p2)
+
+fun wrap trans p (x,s) =
+  let val (result,s) = p (x,s)
+  in (result, trans (x, result, s)) end
+
+fun classify' f =
+  wrap (fn (x, result, {tags, count}) =>
+    { tags = if is_some result then
+        case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags
+      else tags, count = count })
+
+fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
+
+fun trivial cond = classify cond "trivial"
+
+fun test p =
+  wrap (fn (_, result, {tags, count}) =>
+    { tags = tags, count = if is_some result then count + 1 else count }) p
+
+val stats = { tags = [], count = 0 }
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/random.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,46 @@
+(*  Title:      HOL/Spec_Check/random.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random number engine.
+*)
+
+signature RANDOM =
+sig
+  type rand
+  val new : unit -> rand
+  val range : int * int -> rand -> int * rand
+  val split : rand -> rand * rand
+end
+
+structure Random : RANDOM  =
+struct
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+  let
+    val t = a * seed
+  in
+    t - m * real(floor(t/m))
+  end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+  if min > max then raise Domain (* TODO: raise its own error *)
+  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
+
+fun split r =
+  let
+    val r = r / a
+    val r0 = real(floor r)
+    val r1 = r - r0
+  in
+    (nextrand r0, nextrand r1)
+  end
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:09:49 2013 +0200
@@ -0,0 +1,190 @@
+(*  Title:      HOL/Spec_Check/spec_check.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Specification-based testing of ML programs with random values.
+*)
+
+signature SPEC_CHECK =
+sig
+
+  val gen_target : int Config.T
+  val gen_max : int Config.T
+  val examples : int Config.T
+  val sort_examples : bool Config.T
+  val show_stats : bool Config.T
+  val column_width : int Config.T
+  val style : string Config.T
+
+  type output_style = Context.generic -> string ->
+    {status : string option * Property.result * (Property.stats  * string option list) -> unit, finish: Property.stats * string option list -> unit}
+
+  val register_style : (string * output_style) -> theory -> theory
+
+  val checkGen : Context.generic -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
+
+  val check_property : Proof.context -> string -> unit
+end;
+
+structure Spec_Check : SPEC_CHECK =
+struct
+
+(* configurations *)
+
+val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
+val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
+val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
+
+val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
+val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
+val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
+val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
+
+open Property
+
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+type 'a rep = ('a -> string) option
+
+type output_style = Context.generic -> string ->
+  {status: string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit}
+
+fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen
+
+structure Style = Theory_Data
+(
+  type T = output_style Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge data : T = Symtab.merge (K true) data
+)
+
+fun get_style ctxt =
+  let val name = Config.get_generic ctxt style
+  in case Symtab.lookup (Style.get (Context.theory_of ctxt)) name of
+      SOME style => style ctxt
+    | NONE => error ("No style called " ^ quote name ^ " found")
+  end
+
+fun register_style (name, style) = Style.map (Symtab.update (name, style))
+
+(* testing functions *)
+
+fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
+  let
+    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
+
+    val {status, finish} = get_style ctxt tag
+    fun status' (obj, result, (stats, badobjs)) =
+      let
+        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
+        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
+      in badobjs' end
+
+    fun try_shrink (obj, result, stats') (stats, badobjs) =
+      let
+        fun is_failure s =
+          let val (result, stats') = Property.test prop (s, stats)
+          in if Property.failure result then SOME (s, result, stats') else NONE end
+      in
+        case get_first is_failure (shrink obj) of
+          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
+        | NONE => status' (obj, result, (stats', badobjs))
+      end
+
+    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
+      | iter (SOME (obj, stream), (stats, badobjs)) =
+        if #count stats >= Config.get_generic ctxt gen_target then
+          finish (stats, map apply_show badobjs)
+        else
+          let
+            val (result, stats') = Property.test prop (obj, stats)
+            val badobjs' = if Property.failure result then
+                try_shrink (obj, result, stats') (stats, badobjs)
+              else
+                status' (obj, result, (stats', badobjs))
+          in iter (next stream, (stats', badobjs')) end
+  in
+    fn stream => iter (next stream, (s0, []))
+  end
+
+fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
+fun check ctxt = check' ctxt Property.stats
+fun checks ctxt = cpsCheck ctxt Property.stats
+
+fun checkGen ctxt (gen, show) (tag, prop) =
+    check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
+    cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
+           (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkOne ctxt show (tag, prop) obj = check ctxt (List.getItem, show) (tag, prop) [obj]
+
+(*calls the compiler and passes resulting type string to the parser*)
+fun determine_type context s =
+  let
+    val ret = Unsynchronized.ref "return"
+    val ctx : use_context = {
+      tune_source = ML_Parse.fix_ints,
+      name_space = ML_Env.name_space,
+      str_of_pos = Position.here oo Position.line_file,
+      print = fn r => ret := r,
+      error = error
+      }
+    val _ = context |> Context.proof_map
+      (ML_Context.exec (fn () => Secure.use_text ctx (0, "generated code") true s))
+  in
+    Gen_Construction.parse_pred (!ret)
+  end;
+
+(*calls the compiler and runs the test*)
+fun run_test context s =
+  let
+    val _ = Context.proof_map
+        (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
+        true s)) context
+  in () end;
+
+(*split input into tokens*)
+fun input_split s =
+  let
+    fun dot c = c = #"."
+    fun space c = c = #" "
+    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
+  in (String.tokens space (Substring.string head),
+    Substring.string (Substring.dropl dot code)) end;
+
+(*create the function from the input*)
+fun make_fun s =
+  let
+    val scan_param = Scan.one (fn s => s <> ";")
+    fun parameters s = Scan.repeat1 scan_param s
+    val p = $$ "ALL" |-- parameters
+    val (split, code) = input_split s
+    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+    val (params, _) = Scan.finite stop p split
+  in "fn (" ^ commas params ^ ") => " ^ code end;
+
+(*reads input and performs the test*)
+fun gen_check_property check context s =
+  let
+    val func = make_fun s
+    val (_, ty) = determine_type context func
+  in run_test context (check (Proof_Context.theory_of context) "Check" (ty, func)) end;
+
+val check_property = gen_check_property Gen_Construction.build_check
+(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
+
+(*performs test for specification function*)
+fun gen_check_property_f check context s =
+  let
+    val (name, ty) = determine_type context s
+  in run_test context (check (Proof_Context.theory_of context) name (ty, s)) end;
+
+val check_property_f = gen_check_property_f Gen_Construction.build_check
+(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
+
+end;
+
+val check_property = Spec_Check.check_property;
+