src/HOL/Quickcheck_Narrowing.thy
changeset 43316 3e274608f06b
parent 43315 893de45ac28d
child 43317 f9283eb3a4bf
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:21 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:22 2011 +0200
     1.3 @@ -26,20 +26,6 @@
     1.4  
     1.5  code_reserved Haskell_Quickcheck Typerep
     1.6  
     1.7 -code_type char
     1.8 -  (Haskell_Quickcheck "Char")
     1.9 -
    1.10 -setup {*
    1.11 -  fold String_Code.add_literal_char ["Haskell_Quickcheck"] 
    1.12 -  #> String_Code.add_literal_list_string "Haskell_Quickcheck"
    1.13 -*}
    1.14 -
    1.15 -code_instance char :: equal
    1.16 -  (Haskell_Quickcheck -)
    1.17 -
    1.18 -code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.19 -  (Haskell_Quickcheck infix 4 "==")
    1.20 -
    1.21  subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
    1.22  
    1.23  typedef (open) code_int = "UNIV \<Colon> int set"
    1.24 @@ -248,10 +234,10 @@
    1.25  
    1.26  code_const toEnum (Haskell_Quickcheck "toEnum")
    1.27  
    1.28 -consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
    1.29 +consts marker :: "char"
    1.30  
    1.31 -consts split_At :: "code_int => 'a list => 'a list * 'a list"
    1.32 - 
    1.33 +code_const marker (Haskell_Quickcheck "''\\0'")
    1.34 +
    1.35  subsubsection {* Narrowing's basic operations *}
    1.36  
    1.37  type_synonym 'a narrowing = "code_int => 'a cons"
    1.38 @@ -266,7 +252,7 @@
    1.39  
    1.40  fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    1.41  where
    1.42 -  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
    1.43 +  "conv cs (Var p _) = error (marker # map toEnum p)"
    1.44  | "conv cs (Ctr i xs) = (nth cs i) xs"
    1.45  
    1.46  fun nonEmpty :: "narrowing_type => bool"
    1.47 @@ -384,7 +370,7 @@
    1.48  setup {* Narrowing_Generators.setup *}
    1.49  
    1.50  hide_type code_int narrowing_type narrowing_term cons property
    1.51 -hide_const int_of of_int nth error toEnum map_index split_At empty
    1.52 +hide_const int_of of_int nth error toEnum marker empty
    1.53    C cons conv nonEmpty "apply" sum ensure_testable all exists 
    1.54  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.55