src/HOL/ex/Quickcheck.thy
changeset 26267 ba710daf77a7
parent 26265 4b63b9e9b10d
child 26275 014d93dc2199
--- a/src/HOL/ex/Quickcheck.thy	Fri Mar 14 08:52:51 2008 +0100
+++ b/src/HOL/ex/Quickcheck.thy	Fri Mar 14 08:52:52 2008 +0100
@@ -13,7 +13,7 @@
 class random = type +
   fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
 
-print_classes
+text {* Type @{typ "'a itself"} *}
 
 instantiation itself :: (type) random
 begin
@@ -25,7 +25,9 @@
 
 end
 
-lemma random_aux_if:
+text {* Datatypes *}
+
+lemma random'_if:
   fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   assumes "random' 0 j = undefined"
     and "\<And>i. random' (Suc_index i) j = rhs2 i"
@@ -34,108 +36,107 @@
 
 setup {*
 let
-  exception REC;
-  fun random_inst tyco thy =
+  exception REC of string;
+  fun mk_collapse thy ty = Sign.mk_const thy
+    (@{const_name collapse}, [@{typ seed}, ty]);
+  fun mk_cons this_ty (c, args) =
     let
-      val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
-      val _ = if length descr > 1 then raise REC else ();
-      val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
+      val tys = map (fst o fst) args;
+      val return = StateMonad.return this_ty @{typ seed}
+        (list_comb (Const (c, tys ---> this_ty),
+           map Bound (length tys - 1 downto 0)));
+      val t = fold_rev (fn ((ty, _), random) => fn t =>
+        StateMonad.mbind ty this_ty @{typ seed} random (Abs ("", ty, t)))
+          args return;
+      val is_rec = exists (snd o fst) args;
+    in (is_rec, StateMonad.run this_ty @{typ seed} t) end;
+  fun mk_conss thy ty [] = NONE
+    | mk_conss thy ty [(_, t)] = SOME t
+    | mk_conss thy ty ts = SOME (mk_collapse thy ty $
+          (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT ty @{typ seed}]) $
+            HOLogic.mk_list (StateMonad.liftT ty @{typ seed}) (map snd ts)));
+  fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
+    let
+      val SOME t_atom = mk_conss thy ty ts_atom;
+    in case mk_conss thy ty ts_rec
+     of SOME t_rec => mk_collapse thy ty $
+          (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT ty @{typ seed}]) $
+             @{term "i\<Colon>index"} $ t_rec $ t_atom)
+      | NONE => t_atom
+    end;
+  fun mk_random_eqs thy tycos =
+    let
+      val (raw_vs, _) = DatatypePackage.the_datatype_spec thy (hd tycos);
       val vs = (map o apsnd)
         (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val typ_of = DatatypeAux.typ_of_dtyp descr vs;
-      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
-      val randomN = NameSpace.base @{const_name random};
-      val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";
-      fun lift_ty ty = StateMonad.liftT ty @{typ seed};
-      val ty_aux = @{typ index} --> @{typ index} --> lift_ty ty;
-      fun random ty =
-        Const (@{const_name random}, @{typ index} --> lift_ty ty);
-      val random_aux = Free (random_aux_name, ty_aux);
-      fun add_cons_arg dty (is_rec, t) =
-        let
-          val ty' = typ_of dty;
-          val rec_call = case try DatatypeAux.dest_DtRec dty
-           of SOME index' => index = index'
-            | NONE => false
-          val random' = if rec_call
-            then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}
-            else random ty' $ @{term "j\<Colon>index"}
-          val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;
-          val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))
-        in (is_rec', t') end;
-      fun mk_cons_t (c, dtys) =
-        let
-          val ty' = map typ_of dtys ---> ty;
-          val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),
-            map Bound (length dtys - 1 downto 0)));
-          val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);
-        in (is_rec, StateMonad.run ty @{typ seed} t') end;
-      fun check_empty [] = NONE
-        | check_empty xs = SOME xs;
-      fun bundle_cons_ts cons_ts =
-        let
-          val ts = map snd cons_ts;
-          val t = HOLogic.mk_list (lift_ty ty) ts;
-          val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) --> lift_ty (lift_ty ty)) $ t;
-          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
-        in t'' end;
-      fun bundle_conss (some_rec_t, nonrec_t) =
+      val this_ty = Type (hd tycos, map TFree vs);
+      val this_ty' = StateMonad.liftT this_ty @{typ seed};
+      val random_name = NameSpace.base @{const_name random};
+      val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
+      fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
+      val random' = Free (random'_name,
+        @{typ index} --> @{typ index} --> this_ty');
+      fun atom ty = ((ty, false), random ty $ @{term "j\<Colon>index"});
+      fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
+      fun rtyp tyco tys = raise REC
+        ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
+      val rhss = DatatypePackage.construction_interpretation thy
+            { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
+        |> (map o apsnd o map) (mk_cons this_ty) 
+        |> (map o apsnd) (List.partition fst)
+        |> map (mk_clauses thy this_ty)
+      val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
+          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, this_ty')),
+          (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
+        ]))) rhss;
+    in eqss end;
+  fun random_inst [tyco] thy =
         let
-          val t = case some_rec_t
-           of SOME rec_t => Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty)
-               $ (Const (@{const_name select_default},
-                   @{typ index} --> lift_ty ty --> lift_ty ty --> lift_ty (lift_ty ty))
-                  $ @{term "i\<Colon>index"} $ rec_t $ nonrec_t)
-            | NONE => nonrec_t
-        in t end;
-      val random_rhs = constrs
-        |> map mk_cons_t 
-        |> List.partition fst
-        |> apfst (Option.map bundle_cons_ts o check_empty)
-        |> apsnd bundle_cons_ts
-        |> bundle_conss;
-      val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
-        (random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))
-      val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
-        (random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);
-      val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},
-        @{typ index} --> lift_ty ty) $ @{term "i\<Colon>index"},
-          random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});
-      val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
-        (fn thm => Context.mapping (Code.del_func thm) I));
-      fun add_code simps lthy =
-        let
-          val thy = ProofContext.theory_of lthy;
-          val thm = @{thm random_aux_if}
-            |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]
-            |> (fn thm => thm OF simps)
-            |> singleton (ProofContext.export lthy (ProofContext.init thy))
+          val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
+          val vs = (map o apsnd)
+            (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
+          val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
+          val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy) tyco;
+          val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+            (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
+               random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
+          val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
+            (fn thm => Context.mapping (Code.del_func thm) I));
+          fun add_code simps lthy =
+            let
+              val thy = ProofContext.theory_of lthy;
+              val thm = @{thm random'_if}
+                |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
+                |> (fn thm => thm OF simps)
+                |> singleton (ProofContext.export lthy (ProofContext.init thy))
+            in
+              lthy
+              |> LocalTheory.theory (PureThy.note Thm.internalK (fst (dest_Free random') ^ "_code", thm)
+                   #-> Code.add_func)
+            end;
         in
-          lthy
-          |> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)
-               #-> Code.add_func)
-        end;
-    in
-      thy
-      |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
-      |> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]
-           [(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]
-      |-> add_code
-      |> `(fn lthy => Syntax.check_term lthy random_eq)
-      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
-      |> snd
-      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-      |> LocalTheory.exit
-      |> ProofContext.theory_of
-    end;
-  fun add_random_inst [tyco] = (fn thy => random_inst tyco thy handle REC =>
-        (warning ("Will not generated random elements for mutual recursive type " ^ quote tyco); thy))
-    | add_random_inst tycos = tap (fn _ => warning
-        ("Will not generated random elements for mutual recursive type(s) " ^ commas (map quote tycos)));
+          thy
+          |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+          |> PrimrecPackage.add_primrec
+               [(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)]
+                 (map (fn eq => (("", [del_func]), eq)) eqs')
+          |-> add_code
+          |> `(fn lthy => Syntax.check_term lthy eq)
+          |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+          |> snd
+          |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+          |> LocalTheory.exit
+          |> ProofContext.theory_of
+        end
+    | random_inst tycos thy = raise REC
+        ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
+  fun add_random_inst tycos thy = random_inst tycos thy
+     handle REC msg => (warning msg; thy);
 in DatatypePackage.interpretation add_random_inst end
 *}
 
+text {* Type @{typ int} *}
+
 instantiation int :: random
 begin
 
@@ -149,6 +150,8 @@
 
 end
 
+text {* Type @{typ "'a set"} *}
+
 instantiation set :: (random) random
 begin
 
@@ -162,7 +165,7 @@
   "random_set' i j s = (if i = 0 then undefined else collapse (select_default (i - 1)
        (do x \<leftarrow> random (i - 1); xs \<leftarrow> random_set' (i - 1) j; return (insert x xs) done)
        (return {})) s)"
-  by (rule random_aux_if random_set'.simps)+
+  by (rule random'_if random_set'.simps)+
 
 definition
   "random i = random_set' i i"
@@ -171,7 +174,63 @@
 
 end
 
-code_reserved SML Quickcheck
+text {* Type @{typ "'a \<Rightarrow> 'b"} *}
+
+ML {*
+structure Random_Engine =
+struct
+
+open Random_Engine;
+
+fun random_fun (eq : 'a -> 'a -> bool)
+    (random : Random_Engine.seed -> 'b * Random_Engine.seed)
+    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
+    (seed : Random_Engine.seed) =
+  let
+    val (seed', seed'') = random_split seed;
+    val state = ref (seed', []);
+    fun random_fun' x =
+      let
+        val (seed, fun_map) = ! state;
+      in case AList.lookup (uncurry eq) fun_map x
+       of SOME y => y
+        | NONE => let
+              val (y, seed') = random seed;
+              val _ = state := (seed', (x, y) :: fun_map);
+            in y end
+      end;
+  in (random_fun', seed'') end;
+
+end
+*}
+
+axiomatization
+  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
+    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
+
+code_const random_fun_aux (SML "Random'_Engine.random'_fun")
+
+instantiation "fun" :: (term_of, term_of) term_of
+begin
+
+instance ..
+
+end
+
+code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
+  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
+
+instantiation "fun" :: (eq, "{type, random}") random
+begin
+
+definition
+  "random n = random_fun_aux (op =) (random n) split_seed"
+
+instance ..
+
+end
+
+code_reserved SML Random_Engine
 
 
 subsection {* Quickcheck generator *}
@@ -220,6 +279,9 @@
 end
 *}
 
+
+subsection {* Examples *}
+
 (*setup {* Quickcheck.VALUE @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
 export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
 use "~~/../../gen_code/quickcheck.ML"
@@ -287,61 +349,6 @@
 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
-subsection {* Incremental function generator *}
-
-ML {*
-structure Quickcheck =
-struct
-
-open Quickcheck;
-
-fun random_fun (eq : 'a -> 'a -> bool)
-    (random : Random_Engine.seed -> 'b * Random_Engine.seed)
-    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
-    (seed : Random_Engine.seed) =
-  let
-    val (seed', seed'') = random_split seed;
-    val state = ref (seed', []);
-    fun random_fun' x =
-      let
-        val (seed, fun_map) = ! state;
-      in case AList.lookup (uncurry eq) fun_map x
-       of SOME y => y
-        | NONE => let
-              val (y, seed') = random seed;
-              val _ = state := (seed', (x, y) :: fun_map);
-            in y end
-      end;
-  in (random_fun', seed'') end;
-
-end
-*}
-
-axiomatization
-  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
-    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
-
-code_const random_fun_aux (SML "Quickcheck.random'_fun")
-
-instantiation "fun" :: (term_of, term_of) term_of
-begin
-
-instance ..
-
-end
-
-code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
-  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
-
-instantiation "fun" :: (eq, "{type, random}") random
-begin
-
-definition
-  "random n = random_fun_aux (op =) (random n) split_seed"
-
-instance ..
-
-end
 
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
@@ -380,4 +387,11 @@
 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
+definition "map2 f xs ys = map (split f) (zip xs ys)"
+
+lemma
+  assumes "\<And>x. f x x = x"
+  shows "map2 f xs xs = xs"
+  by (induct xs) (simp_all add: map2_def assms)
+
 end