dropped dead code;
tuned theory text

--- a/src/HOL/Quickcheck.thy	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Quickcheck.thy	Sun Nov 11 19:56:02 2012 +0100
@@ -157,11 +157,11 @@
       (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
 proof (induct i rule: code_numeral.induct)
   case zero
-  show ?case by (subst select_weight_drop_zero[symmetric])
-    (simp add: filter.simps random_aux_set.simps[simplified])
+  show ?case by (subst select_weight_drop_zero [symmetric])
+    (simp add: random_aux_set.simps [simplified])
 next
   case (Suc i)
-  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
+  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
 qed
 
 definition "random_set i = random_aux_set i i"

--- a/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:56:02 2012 +0100
@@ -411,34 +411,6 @@
      Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
 by (rule partial_term_of_anything)+
 
-text {* Defining integers by positive and negative copy of naturals *}
-(*
-datatype simple_int = Positive nat | Negative nat
-
-primrec int_of_simple_int :: "simple_int => int"
-where
-  "int_of_simple_int (Positive n) = int n"
-| "int_of_simple_int (Negative n) = (-1 - int n)"
-
-instantiation int :: narrowing
-begin
-
-definition narrowing_int :: "code_int => int cons"
-where
-  "narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)"
-
-instance ..
-
-end
-
-text {* printing the partial terms *}
-
-lemma [code]:
-  "partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'')
-     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
-by (rule partial_term_of_anything)
-
-*)
 
 subsection {* The @{text find_unused_assms} command *}
 

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Nov 11 19:56:02 2012 +0100
@@ -45,25 +45,6 @@
 val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
 val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
  
-(** general term functions **)
-
-fun mk_measure f =
-  let
-    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
-  in
-    Const (@{const_name Wellfounded.measure},
-      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
-    $ f
-  end
-
-fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
-  let
-    val lt = mk_sumcases rT f TL
-    val rt = mk_sumcases rT f TR
-  in
-    SumTree.mk_sumcase TL TR rT lt rt
-  end
-  | mk_sumcases _ f T = f T
 
 (** abstract syntax **)
 
@@ -80,9 +61,6 @@
     Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
   end
 
-fun mk_unit_let (x, y) =
-  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
-
 fun mk_if (b, t, e) =
   let
     val T = fastype_of t
@@ -100,7 +78,6 @@
 
 val exhaustiveN = "exhaustive";
 val full_exhaustiveN = "full_exhaustive";
-val fast_exhaustiveN = "fast_exhaustive";
 val bounded_forallN = "bounded_forall";
 
 fun fast_exhaustiveT T = (T --> @{typ unit})
@@ -145,20 +122,6 @@
     val bounds = map Bound (((length xs) - 1) downto 0)
     val start_term = test_function simpleT $ list_comb (constr, bounds)
   in fold_rev (fn f => fn t => f t) fns start_term end
-      
-fun mk_fast_equations functerms =
-  let
-    fun test_function T = Free ("f", T --> @{typ "unit"})
-    val mk_call = gen_mk_call (fn T =>
-      Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
-        fast_exhaustiveT T))
-    val mk_aux_call = gen_mk_aux_call functerms
-    val mk_consexpr = gen_mk_consexpr test_function
-    fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
-        $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
-  in
-    mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
-  end
 
 fun mk_equations functerms =
   let
@@ -228,26 +191,6 @@
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
   
-(** foundational definition with the function package **)
-
-val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
-
-fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
-    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
-
-fun mk_termination_measure T =
-  let
-    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
-  in
-    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
-  end
-
-fun termination_tac ctxt = 
-  Function_Relation.relation_tac ctxt mk_termination_measure 1
-  THEN rtac @{thm wf_measure} 1
-  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
-    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
-     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
 
 (** instantiating generator classes **)
   
@@ -278,10 +221,6 @@
  ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
    mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
 
-val instantiate_fast_exhaustive_datatype = instantiate_datatype 
- ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
-   mk_fast_equations, fast_exhaustiveT, ["f", "i"])
-
 val instantiate_exhaustive_datatype = instantiate_datatype  
   ("exhaustive generators", exhaustiveN, @{sort exhaustive},
     mk_equations, exhaustiveT, ["f", "i"])
@@ -479,7 +418,7 @@
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
         $ lambda (Free (s, T)) t $ depth
     fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
-    fun mk_let safe def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
+    fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
     val mk_test_term =
       mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
   in lambda depth (mk_test_term t) end

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Nov 11 19:56:02 2012 +0100
@@ -126,8 +126,6 @@
 fun narrowingT T =
   @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
 
-fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
-
 fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
 
 fun mk_apply (T, t) (U, u) =
@@ -147,7 +145,7 @@
 
 (** deriving narrowing instances **)
 
-fun mk_equations descr vs tycos narrowings (Ts, Us) =
+fun mk_equations descr vs narrowings =
   let
     fun mk_call T =
       (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
@@ -188,7 +186,7 @@
       thy
       |> Class.instantiation (tycos, vs, @{sort narrowing})
       |> Quickcheck_Common.define_functions
-        (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
+        (fn narrowings => mk_equations descr vs narrowings, NONE)
         prfx [] narrowingsN (map narrowingT (Ts @ Us))
       |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
     else
@@ -221,15 +219,13 @@
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
   
-fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
   let
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else Output.urgent_message s
     fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
-    fun excipit () =
-      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     val tmp_prefix = "Quickcheck_Narrowing"
     val ghc_options = Config.get ctxt ghc_options
     val with_tmp_dir =
@@ -262,7 +258,7 @@
           ghc_options ^ " " ^
           (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
           " -o " ^ executable ^ ";"
-        val (result, compilation_time) =
+        val (_, compilation_time) =
           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
         val _ = Quickcheck.add_timing compilation_time current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
@@ -357,7 +353,7 @@
     fun mk_eval_cfun dT rT =
       Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
         Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
-    fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
+    fun eval_function (Type (@{type_name fun}, [dT, rT])) =
       let
         val (rt', rT') = eval_function rT
       in
@@ -433,7 +429,7 @@
 fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
       (t, mk_case_term ctxt (p - 1) qs' c)) cs)
-  | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
+  | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
     if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
 
 val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions
@@ -443,11 +439,11 @@
     val
       ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
     in
-      map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
+      map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
       |> map (apsnd post_process)
     end
   
-fun test_term ctxt catch_code_errors (t, eval_terms) =
+fun test_term ctxt catch_code_errors (t, _) =
   let
     fun dest_result (Quickcheck.Result r) = r 
     val opts =

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Nov 11 19:56:02 2012 +0100
@@ -83,8 +83,6 @@
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
-    fun excipit () =
-      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     val act = if catch_code_errors then try else (fn f => SOME o f) 
     val (test_fun, comp_time) = cpu_time "quickcheck compilation"
         (fn () => act (compile ctxt) [(t, eval_terms)]);
@@ -134,44 +132,6 @@
       in !current_result end
   end;
 
-fun validate_terms ctxt ts =
-  let
-    val _ = map check_test_term ts
-    val size = Config.get ctxt Quickcheck.size
-    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
-      (fn () => Quickcheck.mk_batch_validator ctxt ts) 
-    fun with_size tester k =
-      if k > size then true
-      else if tester k then with_size tester (k + 1) else false
-    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
-        Option.map (map (fn test_fun =>
-          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
-              (fn () => with_size test_fun 1) ()
-             handle TimeLimit.TimeOut => true)) test_funs)
-  in
-    (results, [comp_time, exec_time])
-  end
-  
-fun test_terms ctxt ts =
-  let
-    val _ = map check_test_term ts
-    val size = Config.get ctxt Quickcheck.size
-    val namess = map (fn t => Term.add_free_names t []) ts
-    val (test_funs, comp_time) =
-      cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
-    fun with_size tester k =
-      if k > size then NONE
-      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
-    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
-        Option.map (map (fn test_fun =>
-          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
-              (fn () => with_size test_fun 1) ()
-             handle TimeLimit.TimeOut => NONE)) test_funs)
-  in
-    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
-      [comp_time, exec_time])
-  end
-
 fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
   let
     val genuine_only = Config.get ctxt Quickcheck.genuine_only
@@ -294,7 +254,7 @@
 fun subtype_preprocess ctxt (T, (t, ts)) =
   let
     val preds = Subtype_Predicates.get (Context.Proof ctxt)
-    fun matches (p $ x) = AList.defined Term.could_unify preds p  
+    fun matches (p $ _) = AList.defined Term.could_unify preds p  
     fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
     fun subst_of (tyco, v as Free (x, repT)) =
       let
@@ -330,9 +290,9 @@
           [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
     val error_msg =
       cat_lines
-        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
+        (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
     fun is_wellsorted_term (T, Term t) = SOME (T, t)
-      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
+      | is_wellsorted_term (_, Wellsorted_Error _) = NONE
     val correct_inst_goals =
       case map (map_filter is_wellsorted_term) inst_goals of
         [[]] => error error_msg
@@ -498,7 +458,7 @@
   | make_set T1 ((t1, @{const True}) :: tps) =
     Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
       $ t1 $ (make_set T1 tps)
-  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
+  | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
 
 fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   | make_coset T tps = 

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Nov 11 19:24:01 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Nov 11 19:56:02 2012 +0100
@@ -42,7 +42,7 @@
   let
     val fun_upd = Const (@{const_name fun_upd},
       (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
-    val ((y, t2), seed') = random seed;
+    val ((_, t2), seed') = random seed;
     val (seed'', seed''') = random_split seed';
 
     val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
@@ -62,10 +62,6 @@
     fun term_fun' () = #3 (! state) ();
   in ((random_fun', term_fun'), seed''') end;
 
-fun mk_if (b, t, e) =
-  let
-    val T = fastype_of t
-  in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
   
 (** datatypes **)
 
@@ -77,7 +73,6 @@
 val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg;
 val lhs = eq |> Thm.dest_arg1;
 val pt_random_aux = lhs |> Thm.dest_fun;
-val ct_k = lhs |> Thm.dest_arg;
 val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
 val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
 
@@ -187,14 +182,13 @@
 
 val random_auxN = "random_aux";
 
-fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
+fun mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us) =
   let
     val mk_const = curry (Sign.mk_const thy);
     val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
     val rTs = Ts @ Us;
     fun random_resultT T = @{typ Random.seed}
       --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
-    val pTs = map random_resultT rTs;
     fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T;
     val random_auxT = sizeT o random_resultT;
     val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
@@ -257,7 +251,7 @@
             $ HOLogic.mk_number @{typ code_numeral} l $ size
       | NONE => size;
     val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
-      (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
+      (mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us));
     val random_defs = map_index (fn (k, T) => mk_prop_eq
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
@@ -294,7 +288,7 @@
 
 val target = "Quickcheck";
 
-fun mk_generator_expr ctxt (t, eval_terms) =
+fun mk_generator_expr ctxt (t, _) =
   let  
     val thy = Proof_Context.theory_of ctxt
     val prop = fold_rev absfree (Term.add_frees t []) t
@@ -304,7 +298,7 @@
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
-    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+    val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt
     val genuine_only = Free (genuine_only_name, @{typ bool})
     val none_t = Const (@{const_name "None"}, resultT)
     val check = Quickcheck_Common.mk_safe_if genuine_only none_t (result, none_t,
@@ -327,7 +321,7 @@
       (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   end;
 
-fun mk_reporting_generator_expr ctxt (t, eval_terms) =
+fun mk_reporting_generator_expr ctxt (t, _) =
   let
     val thy = Proof_Context.theory_of ctxt
     val resultT = @{typ "(bool * term list) option * (bool list * bool)"}
@@ -348,7 +342,7 @@
     fun mk_concl_report b =
       HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
         Quickcheck_Common.reflect_bool b)
-    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+    val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt
     val genuine_only = Free (genuine_only_name, @{typ bool})
     val none_t = HOLogic.mk_prod (@{term "None :: (bool * term list) option"}, mk_concl_report true)
     val concl_check = Quickcheck_Common.mk_safe_if genuine_only none_t (concl, none_t,
@@ -422,7 +416,7 @@
           (fn proc => fn g => fn c => fn b => fn s => g c b s
             #>> (apfst o Option.map o apsnd o map) proc) t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
-        fun iterate_and_collect _ (card, size) 0 report = (NONE, report)
+        fun iterate_and_collect _ _ 0 report = (NONE, report)
           | iterate_and_collect genuine_only (card, size) j report =
             let
               val (test_result, single_report) = apsnd Run (single_tester card genuine_only size)
@@ -444,7 +438,7 @@
           (fn proc => fn g => fn c => fn b => fn s => g c b s
             #>> (Option.map o apsnd o map) proc) t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
-        fun iterate _ (card, size) 0 = NONE
+        fun iterate _ _ 0 = NONE
           | iterate genuine_only (card, size) j =
             case single_tester card genuine_only size of
               NONE => iterate genuine_only (card, size) (j - 1)