src/HOL/Quickcheck_Narrowing.thy
changeset 65481 b11b7ad22684
parent 65480 5407bc278c9a
child 65482 721feefce9c6
equal deleted inserted replaced
65480:5407bc278c9a 65481:b11b7ad22684
    82 
    82 
    83 subsubsection \<open>Narrowing's basic operations\<close>
    83 subsubsection \<open>Narrowing's basic operations\<close>
    84 
    84 
    85 type_synonym 'a narrowing = "integer => 'a narrowing_cons"
    85 type_synonym 'a narrowing = "integer => 'a narrowing_cons"
    86 
    86 
    87 definition empty :: "'a narrowing"
       
    88 where
       
    89   "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
       
    90   
       
    91 definition cons :: "'a => 'a narrowing"
    87 definition cons :: "'a => 'a narrowing"
    92 where
    88 where
    93   "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
    89   "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
    94 
    90 
    95 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    91 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"