handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 4202451df23535105
parent 42023 1bd4b6d1c482
child 42025 cb5b1e85b32e
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
src/HOL/Library/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/ex/Quickcheck_Narrowing_Examples.thy
     1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -458,16 +458,6 @@
     1.4  
     1.5  declare simp_thms(17,19)[code del]
     1.6  
     1.7 -subsubsection {* Setting up the counterexample generator *}
     1.8 -  
     1.9 -use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
    1.10 -
    1.11 -setup {* Narrowing_Generators.setup *}
    1.12 -
    1.13 -hide_type (open) code_int type "term" cons
    1.14 -hide_const (open) int_of of_int nth error toEnum map_index split_At empty
    1.15 -  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
    1.16 -
    1.17  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    1.18  
    1.19  datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    1.20 @@ -480,5 +470,23 @@
    1.21  hide_type (open) ffun
    1.22  hide_const (open) Constant Update eval_ffun
    1.23  
    1.24 +datatype 'b cfun = Constant 'b
    1.25 +
    1.26 +primrec eval_cfun :: "'b cfun => 'a => 'b"
    1.27 +where
    1.28 +  "eval_cfun (Constant c) y = c"
    1.29 +
    1.30 +hide_type (open) cfun
    1.31 +hide_const (open) Constant eval_cfun
    1.32 +
    1.33 +subsubsection {* Setting up the counterexample generator *}
    1.34 +  
    1.35 +use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
    1.36 +
    1.37 +setup {* Narrowing_Generators.setup *}
    1.38 +
    1.39 +hide_type (open) code_int type "term" cons
    1.40 +hide_const (open) int_of of_int nth error toEnum map_index split_At empty
    1.41 +  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
    1.42  
    1.43  end
    1.44 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.3 @@ -184,9 +184,34 @@
     2.4    fun init _ () = error "Counterexample"
     2.5  )
     2.6  
     2.7 -val put_counterexample =  Counterexample.put
     2.8 +val put_counterexample = Counterexample.put
     2.9  
    2.10 -fun finitize_functions t = t
    2.11 +fun finitize_functions t =
    2.12 +  let
    2.13 +    val ((names, Ts), t') = apfst split_list (strip_abs t)
    2.14 +    fun mk_eval_ffun dT rT =
    2.15 +      Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
    2.16 +        Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
    2.17 +    fun mk_eval_cfun dT rT =
    2.18 +      Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
    2.19 +        Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
    2.20 +    fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
    2.21 +      let
    2.22 +        val (rt', rT') = eval_function rT
    2.23 +      in
    2.24 +        case dT of
    2.25 +          Type (@{type_name fun}, _) =>
    2.26 +            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    2.27 +            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
    2.28 +        | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    2.29 +            Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
    2.30 +      end
    2.31 +      | eval_function T = (I, T)
    2.32 +    val (tt, Ts') = split_list (map eval_function Ts)
    2.33 +    val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t')
    2.34 +  in
    2.35 +    list_abs (names ~~ Ts', t'')
    2.36 +  end
    2.37  
    2.38  fun compile_generator_expr ctxt t size =
    2.39    let
     3.1 --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
     3.2 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
     3.3 @@ -42,13 +42,32 @@
     3.4  declare [[quickcheck_finite_functions]]
     3.5  
     3.6  lemma "map f xs = map g xs"
     3.7 -  quickcheck[tester = narrowing, finite_types = true]
     3.8 +  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
     3.9  oops
    3.10  
    3.11  lemma "map f xs = map f ys ==> xs = ys"
    3.12 -  quickcheck[tester = narrowing, finite_types = true]
    3.13 +  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
    3.14 +oops
    3.15 +
    3.16 +lemma
    3.17 +  "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
    3.18 +  quickcheck[tester = narrowing, expect = counterexample]
    3.19 +oops
    3.20 +
    3.21 +lemma "map f xs = F f xs"
    3.22 +  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
    3.23  oops
    3.24  
    3.25 +lemma "map f xs = F f xs"
    3.26 +  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
    3.27 +oops
    3.28 +
    3.29 +(* requires some work...
    3.30 +lemma "R O S = S O R"
    3.31 +  quickcheck[tester = narrowing, size = 2]
    3.32 +oops
    3.33 +*)
    3.34 +
    3.35  subsection {* AVL Trees *}
    3.36  
    3.37  datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat