1.1 --- a/NEWS	Tue May 29 11:41:37 2012 +0200
     1.2 +++ b/NEWS	Tue May 29 13:46:50 2012 +0200
     1.3 @@ -17,6 +17,13 @@
     1.4  configuration.
     1.5  
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Quickcheck:
    1.10 +
    1.11 +  - added an optimisation for equality premises.
    1.12 +    It is switched on by default, and can be switched off by setting
    1.13 +    the configuration quickcheck_optimise_equality to false.    
    1.14  
    1.15  New in Isabelle2012 (May 2012)
    1.16  ------------------------------

     2.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 29 11:41:37 2012 +0200
     2.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 29 13:46:50 2012 +0200
     2.3 @@ -563,4 +563,43 @@
     2.4  
     2.5  declare [[quickcheck_full_support = true]]
     2.6  
     2.7 +
     2.8 +subsection {* Equality Optimisation *}
     2.9 +
    2.10 +lemma
    2.11 +  "f x = y ==> y = (0 :: nat)"
    2.12 +quickcheck
    2.13 +oops
    2.14 +
    2.15 +lemma
    2.16 +  "y = f x ==> y = (0 :: nat)"
    2.17 +quickcheck
    2.18 +oops
    2.19 +
    2.20 +lemma
    2.21 +  "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []"
    2.22 +quickcheck
    2.23 +oops
    2.24 +
    2.25 +lemma
    2.26 +  "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []"
    2.27 +quickcheck
    2.28 +oops
    2.29 +
    2.30 +lemma
    2.31 +  "x = f x \<Longrightarrow> x = (0 :: nat)"
    2.32 +quickcheck
    2.33 +oops
    2.34 +
    2.35 +lemma
    2.36 +  "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []"
    2.37 +quickcheck
    2.38 +oops
    2.39 +
    2.40 +lemma
    2.41 +  "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v"
    2.42 +quickcheck
    2.43 +oops
    2.44 +
    2.45 +
    2.46  end

     3.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue May 29 11:41:37 2012 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue May 29 13:46:50 2012 +0200
     3.3 @@ -17,6 +17,7 @@
     3.4    val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
     3.5    exception Counterexample of term list
     3.6    val smart_quantifier : bool Config.T
     3.7 +  val optimise_equality : bool Config.T
     3.8    val quickcheck_pretty : bool Config.T
     3.9    val setup_exhaustive_datatype_interpretation : theory -> theory
    3.10    val setup: theory -> theory
    3.11 @@ -36,6 +37,8 @@
    3.12  (** dynamic options **)
    3.13  
    3.14  val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
    3.15 +val optimise_equality = Attrib.setup_config_bool @{binding quickcheck_optimise_equality} (K true)
    3.16 +
    3.17  val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false)
    3.18  val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
    3.19  val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
    3.20 @@ -288,26 +291,72 @@
    3.21  
    3.22  (* building and compiling generator expressions *)
    3.23  
    3.24 +fun mk_let_expr (x, t, e) genuine =
    3.25 +  let
    3.26 +    val (T1, T2) = (fastype_of x, fastype_of (e genuine))
    3.27 +  in  
    3.28 +    Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)
    3.29 +  end
    3.30  
    3.31 -fun mk_test_term lookup mk_closure mk_if none_t return ctxt =
    3.32 +fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt =
    3.33    let
    3.34 +    val cnstrs = flat (maps
    3.35 +      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    3.36 +      (Symtab.dest (Datatype.get_all (Proof_Context.theory_of ctxt))))
    3.37 +    fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
    3.38 +        (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
    3.39 +      | _ => false)
    3.40 +      | is_constrt _ = false
    3.41      fun mk_naive_test_term t =
    3.42        fold_rev mk_closure (map lookup (Term.add_free_names t []))
    3.43          (mk_if (t, none_t, return) true)
    3.44      fun mk_smart_test_term' concl bound_vars assms genuine =
    3.45        let
    3.46          fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
    3.47 +        fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) =
    3.48 +          if member (op =) (Term.add_free_names lhs bound_vars) x then
    3.49 +            c (assm, assms)
    3.50 +          else
    3.51 +            (remove (op =) x (vars_of assm),
    3.52 +              mk_let f (try lookup x) lhs 
    3.53 +                (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
    3.54 +          | mk_equality_term (lhs, t) c (assm, assms) =
    3.55 +            if is_constrt (strip_comb t) then
    3.56 +              let
    3.57 +                val (constr, args) = strip_comb t
    3.58 +                val T = fastype_of t
    3.59 +                val vars = map Free (Variable.variant_frees ctxt (concl :: assms)
    3.60 +                  (map (fn t => ("x", fastype_of t)) args))
    3.61 +                val varnames = map (fst o dest_Free) vars
    3.62 +                val dummy_var = Free (singleton
    3.63 +                  (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
    3.64 +                val new_assms = map HOLogic.mk_eq (vars ~~ args)
    3.65 +                val cont_t = mk_smart_test_term' concl (union (op =) varnames bound_vars)
    3.66 +                  (new_assms @ assms) genuine
    3.67 +              in
    3.68 +                (vars_of lhs, Datatype_Case.make_case ctxt Datatype_Case.Quiet [] lhs
    3.69 +                  [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
    3.70 +              end
    3.71 +            else c (assm, assms)
    3.72 +        fun default (assm, assms) = (vars_of assm,
    3.73 +          mk_if (HOLogic.mk_not assm, none_t, 
    3.74 +          mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
    3.75          val (vars, check) =
    3.76 -          case assms of [] => (vars_of concl, (concl, none_t, return))
    3.77 -            | assm :: assms => (vars_of assm, (HOLogic.mk_not assm, none_t, 
    3.78 -                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms))
    3.79 +          case assms of [] => (vars_of concl, mk_if (concl, none_t, return) genuine)
    3.80 +            | assm :: assms =>
    3.81 +              if Config.get ctxt optimise_equality then
    3.82 +                (case try HOLogic.dest_eq assm of
    3.83 +                  SOME (lhs, rhs) =>
    3.84 +                    mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms)
    3.85 +                | NONE => default (assm, assms))
    3.86 +              else default (assm, assms)
    3.87        in
    3.88 -        fold_rev mk_closure (map lookup vars) (mk_if check genuine)
    3.89 +        fold_rev mk_closure (map lookup vars) check
    3.90        end
    3.91      val mk_smart_test_term =
    3.92        Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
    3.93    in
    3.94 -    if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
    3.95 +    if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
    3.96    end
    3.97  
    3.98  fun mk_fast_generator_expr ctxt (t, eval_terms) =
    3.99 @@ -327,7 +376,8 @@
   3.100          $ lambda free t $ depth
   3.101      val none_t = @{term "()"}
   3.102      fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
   3.103 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt 
   3.104 +    fun mk_let def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   3.105 +    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 
   3.106    in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
   3.107  
   3.108  fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
   3.109 @@ -355,7 +405,8 @@
   3.110          $ lambda free t $ depth
   3.111      val none_t = Const (@{const_name "None"}, resultT)
   3.112      val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
   3.113 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
   3.114 +    fun mk_let def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   3.115 +    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
   3.116    in lambda genuine_only (lambda depth (mk_test_term t)) end
   3.117  
   3.118  fun mk_full_generator_expr ctxt (t, eval_terms) =
   3.119 @@ -384,7 +435,11 @@
   3.120              $ lambda free (lambda term_var t)) $ depth
   3.121      val none_t = Const (@{const_name "None"}, resultT)
   3.122      val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
   3.123 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
   3.124 +    fun mk_let _ (SOME (v, term_var)) t e =
   3.125 +      mk_let_expr (v, t, 
   3.126 +        e #> subst_free [(term_var, absdummy @{typ unit} (HOLogic.mk_term_of (fastype_of t) t))])
   3.127 +      | mk_let v NONE t e = mk_let_expr (v, t, e)
   3.128 +    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
   3.129    in lambda genuine_only (lambda depth (mk_test_term t)) end
   3.130  
   3.131  fun mk_parametric_generator_expr mk_generator_expr =
   3.132 @@ -406,8 +461,9 @@
   3.133        Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
   3.134          $ lambda (Free (s, T)) t $ depth
   3.135      fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
   3.136 +    fun mk_let def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   3.137      val mk_test_term =
   3.138 -      mk_test_term lookup mk_bounded_forall mk_safe_if @{term True} (K @{term False}) ctxt
   3.139 +      mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
   3.140    in lambda depth (mk_test_term t) end
   3.141  
   3.142