hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
authorbulwahn
Mon Dec 12 13:45:54 2011 +0100 (2011-12-12)
changeset 4581853a697f5454a
parent 45817 bb39fba83e9b
child 45819 b85bb803bcf3
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 12:03:34 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Dec 12 13:45:54 2011 +0100
     1.3 @@ -430,8 +430,8 @@
     1.4  class fast_exhaustive = term_of +
     1.5    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
     1.6  
     1.7 -consts throw_Counterexample :: "term list => unit"
     1.8 -consts catch_Counterexample :: "unit => term list option"
     1.9 +axiomatization throw_Counterexample :: "term list => unit"
    1.10 +axiomatization catch_Counterexample :: "unit => term list option"
    1.11  
    1.12  code_const throw_Counterexample
    1.13    (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
    1.14 @@ -535,7 +535,16 @@
    1.15  
    1.16  hide_fact orelse_def
    1.17  no_notation orelse (infixr "orelse" 55)
    1.18 -hide_const (open) orelse unknown mk_map_term check_all_n_lists 
    1.19 +
    1.20 +hide_fact
    1.21 +  exhaustive'_def
    1.22 +  exhaustive_code_numeral'_def
    1.23 +
    1.24 +hide_const (open)
    1.25 +  exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
    1.26 +  throw_Counterexample catch_Counterexample
    1.27 +  check_all enum_term_of
    1.28 +  orelse unknown mk_map_term check_all_n_lists
    1.29  
    1.30  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    1.31  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
     2.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 12:03:34 2011 +0100
     2.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 13:45:54 2011 +0100
     2.3 @@ -448,7 +448,7 @@
     2.4  *)
     2.5  
     2.6  hide_type code_int narrowing_type narrowing_term cons property
     2.7 -hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists 
     2.8 +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
     2.9  hide_const (open) Var Ctr "apply" sum cons
    2.10  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    2.11  
     3.1 --- a/src/HOL/Rat.thy	Mon Dec 12 12:03:34 2011 +0100
     3.2 +++ b/src/HOL/Rat.thy	Mon Dec 12 13:45:54 2011 +0100
     3.3 @@ -1158,7 +1158,7 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
     3.8 +  "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
     3.9  
    3.10  instance ..
    3.11  
    3.12 @@ -1168,7 +1168,7 @@
    3.13  begin
    3.14  
    3.15  definition
    3.16 -  "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
    3.17 +  "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k.
    3.18       f (let j = Code_Numeral.int_of l + 1
    3.19          in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
    3.20  
     4.1 --- a/src/HOL/RealDef.thy	Mon Dec 12 12:03:34 2011 +0100
     4.2 +++ b/src/HOL/RealDef.thy	Mon Dec 12 13:45:54 2011 +0100
     4.3 @@ -1729,7 +1729,7 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
     4.8 +  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
     4.9  
    4.10  instance ..
    4.11  
    4.12 @@ -1739,7 +1739,7 @@
    4.13  begin
    4.14  
    4.15  definition
    4.16 -  "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
    4.17 +  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
    4.18  
    4.19  instance ..
    4.20