1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Sep 03 00:06:23 2014 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Sep 03 00:06:24 2014 +0200
     1.3 @@ -26,13 +26,19 @@
     1.4  
     1.5  subsubsection {* Narrowing's deep representation of types and terms *}
     1.6  
     1.7 -datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
     1.8 -datatype narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list"
     1.9 -datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
    1.10 +datatype_new narrowing_type =
    1.11 +  Narrowing_sum_of_products "narrowing_type list list"
    1.12 +
    1.13 +datatype_new narrowing_term =
    1.14 +  Narrowing_variable "integer list" narrowing_type
    1.15 +| Narrowing_constructor integer "narrowing_term list"
    1.16 +
    1.17 +datatype_new (dead 'a) narrowing_cons =
    1.18 +  Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
    1.19  
    1.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    1.21  where
    1.22 -  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
    1.23 +  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f o c) cs)"
    1.24  
    1.25  subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
    1.26  
    1.27 @@ -70,7 +76,7 @@
    1.28    
    1.29  definition cons :: "'a => 'a narrowing"
    1.30  where
    1.31 -  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
    1.32 +  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
    1.33  
    1.34  fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    1.35  where
    1.36 @@ -88,7 +94,7 @@
    1.37         case a (d - 1) of Narrowing_cons ta cas =>
    1.38         let
    1.39           shallow = (d > 0 \<and> non_empty ta);
    1.40 -         cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
    1.41 +         cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
    1.42         in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
    1.43  
    1.44  definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
    1.45 @@ -121,7 +127,7 @@
    1.46  class narrowing =
    1.47    fixes narrowing :: "integer => 'a narrowing_cons"
    1.48  
    1.49 -datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.50 +datatype_new property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.51  
    1.52  (* FIXME: hard-wired maximal depth of 100 here *)
    1.53  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
    1.54 @@ -149,7 +155,7 @@
    1.55  
    1.56  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    1.57  
    1.58 -datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    1.59 +datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
    1.60  
    1.61  primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
    1.62  where
    1.63 @@ -159,7 +165,7 @@
    1.64  hide_type (open) ffun
    1.65  hide_const (open) Constant Update eval_ffun
    1.66  
    1.67 -datatype 'b cfun = Constant 'b
    1.68 +datatype_new (dead 'b) cfun = Constant 'b
    1.69  
    1.70  primrec eval_cfun :: "'b cfun => 'a => 'b"
    1.71  where
    1.72 @@ -308,4 +314,3 @@
    1.73  hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.74  
    1.75  end
    1.76 -