use 'datatype_new' in 'Main'
authorblanchet
Wed Sep 03 00:06:24 2014 +0200 (2014-09-03)
changeset 581526fe60a9a5bad
parent 58151 414deb2ef328
child 58153 ca7ea280e906
use 'datatype_new' in 'Main'
src/HOL/Code_Evaluation.thy
src/HOL/Enum.thy
src/HOL/Groups_List.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Main.thy
src/HOL/Nitpick.thy
src/HOL/Num.thy
src/HOL/Predicate.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Record.thy
src/HOL/String.thy
src/HOL/Typerep.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Wed Sep 03 00:06:23 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Sep 03 00:06:24 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection {* Terms and class @{text term_of} *}
     1.6  
     1.7 -datatype "term" = dummy_term
     1.8 +datatype_new "term" = dummy_term
     1.9  
    1.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.11    "Const _ _ = dummy_term"
     2.1 --- a/src/HOL/Enum.thy	Wed Sep 03 00:06:23 2014 +0200
     2.2 +++ b/src/HOL/Enum.thy	Wed Sep 03 00:06:24 2014 +0200
     2.3 @@ -493,7 +493,7 @@
     2.4  
     2.5  text {* We define small finite types for the use in Quickcheck *}
     2.6  
     2.7 -datatype finite_1 = a\<^sub>1
     2.8 +datatype_new finite_1 = a\<^sub>1
     2.9  
    2.10  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.11  
    2.12 @@ -595,7 +595,7 @@
    2.13  declare [[simproc del: finite_1_eq]]
    2.14  hide_const (open) a\<^sub>1
    2.15  
    2.16 -datatype finite_2 = a\<^sub>1 | a\<^sub>2
    2.17 +datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
    2.18  
    2.19  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.20  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.21 @@ -701,7 +701,7 @@
    2.22  
    2.23  hide_const (open) a\<^sub>1 a\<^sub>2
    2.24  
    2.25 -datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.26 +datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.27  
    2.28  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.29  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.30 @@ -825,7 +825,7 @@
    2.31  
    2.32  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    2.33  
    2.34 -datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.35 +datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.36  
    2.37  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.38  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.39 @@ -927,7 +927,7 @@
    2.40  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    2.41  
    2.42  
    2.43 -datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.44 +datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.45  
    2.46  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.47  notation (output) a\<^sub>2  ("a\<^sub>2")
     3.1 --- a/src/HOL/Groups_List.thy	Wed Sep 03 00:06:23 2014 +0200
     3.2 +++ b/src/HOL/Groups_List.thy	Wed Sep 03 00:06:24 2014 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  begin
     3.5  
     3.6  definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
     3.7 -"listsum xs = foldr plus xs 0"
     3.8 +  "listsum xs = foldr plus xs 0"
     3.9  
    3.10  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    3.11  
     4.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Sep 03 00:06:23 2014 +0200
     4.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Sep 03 00:06:24 2014 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  subsection {* Type of lazy sequences *}
     4.6  
     4.7 -datatype 'a lazy_sequence = lazy_sequence_of_list "'a list"
     4.8 +datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
     4.9  
    4.10  primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    4.11  where
    4.12 @@ -29,7 +29,7 @@
    4.13  
    4.14  lemma size_lazy_sequence_eq [code]:
    4.15    "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    4.16 -  "size (xq :: 'a lazy_sequence) = 0"
    4.17 +  "size xq = Suc (length (list_of_lazy_sequence xq))"
    4.18    by (cases xq, simp)+
    4.19  
    4.20  lemma case_lazy_sequence [simp]:
     5.1 --- a/src/HOL/Main.thy	Wed Sep 03 00:06:23 2014 +0200
     5.2 +++ b/src/HOL/Main.thy	Wed Sep 03 00:06:24 2014 +0200
     5.3 @@ -30,10 +30,9 @@
     5.4    convol ("\<langle>(_,/ _)\<rangle>")
     5.5  
     5.6  hide_const (open)
     5.7 -  czero cinfinite cfinite csum cone ctwo Csum cprod cexp
     5.8 -  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     5.9 -  convol pick_middlep fstOp sndOp csquare relImage relInvImage
    5.10 -  Succ Shift shift proj
    5.11 +  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
    5.12 +  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
    5.13 +  shift proj
    5.14  
    5.15  no_syntax (xsymbols)
    5.16    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
     6.1 --- a/src/HOL/Nitpick.thy	Wed Sep 03 00:06:23 2014 +0200
     6.2 +++ b/src/HOL/Nitpick.thy	Wed Sep 03 00:06:24 2014 +0200
     6.3 @@ -14,9 +14,9 @@
     6.4    "nitpick_params" :: thy_decl
     6.5  begin
     6.6  
     6.7 -datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     6.8 -datatype ('a, 'b) pair_box = PairBox 'a 'b
     6.9 -datatype 'a word = Word "'a set"
    6.10 +datatype_new (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
    6.11 +datatype_new (dead 'a, dead 'b) pair_box = PairBox 'a 'b
    6.12 +datatype_new (dead 'a) word = Word "'a set"
    6.13  
    6.14  typedecl bisim_iterator
    6.15  typedecl unsigned_bit
     7.1 --- a/src/HOL/Num.thy	Wed Sep 03 00:06:23 2014 +0200
     7.2 +++ b/src/HOL/Num.thy	Wed Sep 03 00:06:24 2014 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  
     7.5  subsection {* The @{text num} type *}
     7.6  
     7.7 -datatype num = One | Bit0 num | Bit1 num
     7.8 +datatype_new num = One | Bit0 num | Bit1 num
     7.9  
    7.10  text {* Increment function for type @{typ num} *}
    7.11  
     8.1 --- a/src/HOL/Predicate.thy	Wed Sep 03 00:06:23 2014 +0200
     8.2 +++ b/src/HOL/Predicate.thy	Wed Sep 03 00:06:24 2014 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4  
     8.5  subsection {* The type of predicate enumerations (a monad) *}
     8.6  
     8.7 -datatype 'a pred = Pred "'a \<Rightarrow> bool"
     8.8 +datatype_new 'a pred = Pred "'a \<Rightarrow> bool"
     8.9  
    8.10  primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
    8.11    eval_pred: "eval (Pred f) = f"
    8.12 @@ -402,7 +402,7 @@
    8.13  
    8.14  subsection {* Implementation *}
    8.15  
    8.16 -datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
    8.17 +datatype_new 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
    8.18  
    8.19  primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
    8.20    "pred_of_seq Empty = \<bottom>"
     9.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Sep 03 00:06:23 2014 +0200
     9.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Sep 03 00:06:24 2014 +0200
     9.3 @@ -574,8 +574,8 @@
     9.4  where
     9.5    "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
     9.6  
     9.7 -datatype 'a unknown = Unknown | Known 'a
     9.8 -datatype 'a three_valued = Unknown_value | Value 'a | No_value
     9.9 +datatype_new (dead 'a) unknown = Unknown | Known 'a
    9.10 +datatype_new (dead 'a) three_valued = Unknown_value | Value 'a | No_value
    9.11  
    9.12  type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
    9.13  
    10.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Sep 03 00:06:23 2014 +0200
    10.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Sep 03 00:06:24 2014 +0200
    10.3 @@ -26,13 +26,19 @@
    10.4  
    10.5  subsubsection {* Narrowing's deep representation of types and terms *}
    10.6  
    10.7 -datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
    10.8 -datatype narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list"
    10.9 -datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
   10.10 +datatype_new narrowing_type =
   10.11 +  Narrowing_sum_of_products "narrowing_type list list"
   10.12 +
   10.13 +datatype_new narrowing_term =
   10.14 +  Narrowing_variable "integer list" narrowing_type
   10.15 +| Narrowing_constructor integer "narrowing_term list"
   10.16 +
   10.17 +datatype_new (dead 'a) narrowing_cons =
   10.18 +  Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
   10.19  
   10.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
   10.21  where
   10.22 -  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
   10.23 +  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f o c) cs)"
   10.24  
   10.25  subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
   10.26  
   10.27 @@ -70,7 +76,7 @@
   10.28    
   10.29  definition cons :: "'a => 'a narrowing"
   10.30  where
   10.31 -  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
   10.32 +  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
   10.33  
   10.34  fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
   10.35  where
   10.36 @@ -88,7 +94,7 @@
   10.37         case a (d - 1) of Narrowing_cons ta cas =>
   10.38         let
   10.39           shallow = (d > 0 \<and> non_empty ta);
   10.40 -         cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
   10.41 +         cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
   10.42         in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
   10.43  
   10.44  definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   10.45 @@ -121,7 +127,7 @@
   10.46  class narrowing =
   10.47    fixes narrowing :: "integer => 'a narrowing_cons"
   10.48  
   10.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
   10.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
   10.51  
   10.52  (* FIXME: hard-wired maximal depth of 100 here *)
   10.53  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   10.54 @@ -149,7 +155,7 @@
   10.55  
   10.56  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   10.57  
   10.58 -datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   10.59 +datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   10.60  
   10.61  primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
   10.62  where
   10.63 @@ -159,7 +165,7 @@
   10.64  hide_type (open) ffun
   10.65  hide_const (open) Constant Update eval_ffun
   10.66  
   10.67 -datatype 'b cfun = Constant 'b
   10.68 +datatype_new (dead 'b) cfun = Constant 'b
   10.69  
   10.70  primrec eval_cfun :: "'b cfun => 'a => 'b"
   10.71  where
   10.72 @@ -308,4 +314,3 @@
   10.73  hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
   10.74  
   10.75  end
   10.76 -
    11.1 --- a/src/HOL/Quickcheck_Random.thy	Wed Sep 03 00:06:23 2014 +0200
    11.2 +++ b/src/HOL/Quickcheck_Random.thy	Wed Sep 03 00:06:24 2014 +0200
    11.3 @@ -228,4 +228,3 @@
    11.4  hide_fact (open) collapse_def beyond_def random_fun_lift_def
    11.5  
    11.6  end
    11.7 -
    12.1 --- a/src/HOL/Record.thy	Wed Sep 03 00:06:23 2014 +0200
    12.2 +++ b/src/HOL/Record.thy	Wed Sep 03 00:06:24 2014 +0200
    12.3 @@ -79,7 +79,7 @@
    12.4  
    12.5  subsection {* Operators and lemmas for types isomorphic to tuples *}
    12.6  
    12.7 -datatype ('a, 'b, 'c) tuple_isomorphism =
    12.8 +datatype_new (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
    12.9    Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
   12.10  
   12.11  primrec
    13.1 --- a/src/HOL/String.thy	Wed Sep 03 00:06:23 2014 +0200
    13.2 +++ b/src/HOL/String.thy	Wed Sep 03 00:06:24 2014 +0200
    13.3 @@ -8,7 +8,7 @@
    13.4  
    13.5  subsection {* Characters and strings *}
    13.6  
    13.7 -datatype nibble =
    13.8 +datatype_new nibble =
    13.9      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
   13.10    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
   13.11  
   13.12 @@ -114,7 +114,7 @@
   13.13    "nibble_of_nat (n mod 16) = nibble_of_nat n"
   13.14    by (simp add: nibble_of_nat_def)
   13.15  
   13.16 -datatype char = Char nibble nibble
   13.17 +datatype_new char = Char nibble nibble
   13.18    -- "Note: canonical order of character encoding coincides with standard term ordering"
   13.19  
   13.20  syntax
    14.1 --- a/src/HOL/Typerep.thy	Wed Sep 03 00:06:23 2014 +0200
    14.2 +++ b/src/HOL/Typerep.thy	Wed Sep 03 00:06:24 2014 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  imports String
    14.5  begin
    14.6  
    14.7 -datatype typerep = Typerep String.literal "typerep list"
    14.8 +datatype_new typerep = Typerep String.literal "typerep list"
    14.9  
   14.10  class typerep =
   14.11    fixes typerep :: "'a itself \<Rightarrow> typerep"