src/HOL/Quickcheck_Narrowing.thy
changeset 48891 c0eafbd55de3
parent 48565 7c497a239007
child 48901 5e0455e29339
equal deleted inserted replaced
48890:d72ca5742f80 48891:c0eafbd55de3
     3 header {* Counterexample generator performing narrowing-based testing *}
     3 header {* Counterexample generator performing narrowing-based testing *}
     4 
     4 
     5 theory Quickcheck_Narrowing
     5 theory Quickcheck_Narrowing
     6 imports Quickcheck_Exhaustive
     6 imports Quickcheck_Exhaustive
     7 keywords "find_unused_assms" :: diag
     7 keywords "find_unused_assms" :: diag
     8 uses
     8 uses  (* FIXME session files *)
     9   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     9   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    10   ("Tools/Quickcheck/Narrowing_Engine.hs")
    10   ("Tools/Quickcheck/Narrowing_Engine.hs")
    11   ("Tools/Quickcheck/narrowing_generators.ML")
       
    12   ("Tools/Quickcheck/find_unused_assms.ML")
       
    13 begin
    11 begin
    14 
    12 
    15 subsection {* Counterexample generator *}
    13 subsection {* Counterexample generator *}
    16 
    14 
    17 text {* We create a new target for the necessary code generation setup. *}
    15 text {* We create a new target for the necessary code generation setup. *}
   338 hide_type (open) cfun
   336 hide_type (open) cfun
   339 hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun
   337 hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun
   340 
   338 
   341 subsubsection {* Setting up the counterexample generator *}
   339 subsubsection {* Setting up the counterexample generator *}
   342 
   340 
   343 use "Tools/Quickcheck/narrowing_generators.ML"
   341 ML_file "Tools/Quickcheck/narrowing_generators.ML"
   344 
   342 
   345 setup {* Narrowing_Generators.setup *}
   343 setup {* Narrowing_Generators.setup *}
   346 
   344 
   347 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
   345 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
   348 where
   346 where
   445 
   443 
   446 *)
   444 *)
   447 
   445 
   448 subsection {* The @{text find_unused_assms} command *}
   446 subsection {* The @{text find_unused_assms} command *}
   449 
   447 
   450 use "Tools/Quickcheck/find_unused_assms.ML"
   448 ML_file "Tools/Quickcheck/find_unused_assms.ML"
   451 
   449 
   452 subsection {* Closing up *}
   450 subsection {* Closing up *}
   453 
   451 
   454 hide_type code_int narrowing_type narrowing_term narrowing_cons property
   452 hide_type code_int narrowing_type narrowing_term narrowing_cons property
   455 hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
   453 hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero