# HG changeset patch # User bulwahn # Date 1323693954 -3600 # Node ID 53a697f5454ab3f08e613b6b4b4305cf8de84a9e # Parent bb39fba83e9b331c64b4e6fa3518649eeb031a1c hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory; diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 12 12:03:34 2011 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 12 13:45:54 2011 +0100 @@ -430,8 +430,8 @@ class fast_exhaustive = term_of + fixes fast_exhaustive :: "('a \ unit) \ code_numeral \ unit" -consts throw_Counterexample :: "term list => unit" -consts catch_Counterexample :: "unit => term list option" +axiomatization throw_Counterexample :: "term list => unit" +axiomatization catch_Counterexample :: "unit => term list option" code_const throw_Counterexample (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)") @@ -535,7 +535,16 @@ hide_fact orelse_def no_notation orelse (infixr "orelse" 55) -hide_const (open) orelse unknown mk_map_term check_all_n_lists + +hide_fact + exhaustive'_def + exhaustive_code_numeral'_def + +hide_const (open) + exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral' + throw_Counterexample catch_Counterexample + check_all enum_term_of + orelse unknown mk_map_term check_all_n_lists hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Mon Dec 12 12:03:34 2011 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Mon Dec 12 13:45:54 2011 +0100 @@ -448,7 +448,7 @@ *) hide_type code_int narrowing_type narrowing_term cons property -hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists +hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero hide_const (open) Var Ctr "apply" sum cons hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Rat.thy --- a/src/HOL/Rat.thy Mon Dec 12 12:03:34 2011 +0100 +++ b/src/HOL/Rat.thy Mon Dec 12 13:45:54 2011 +0100 @@ -1158,7 +1158,7 @@ begin definition - "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d" + "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d" instance .. @@ -1168,7 +1168,7 @@ begin definition - "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k. + "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k. f (let j = Code_Numeral.int_of l + 1 in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d" diff -r bb39fba83e9b -r 53a697f5454a src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Mon Dec 12 12:03:34 2011 +0100 +++ b/src/HOL/RealDef.thy Mon Dec 12 13:45:54 2011 +0100 @@ -1729,7 +1729,7 @@ begin definition - "exhaustive f d = exhaustive (%r. f (Ratreal r)) d" + "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d" instance .. @@ -1739,7 +1739,7 @@ begin definition - "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d" + "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d" instance ..