--- a/src/HOL/Code_Evaluation.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Sep 03 00:06:24 2014 +0200
@@ -13,7 +13,7 @@
subsubsection {* Terms and class @{text term_of} *}
-datatype "term" = dummy_term
+datatype_new "term" = dummy_term
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
--- a/src/HOL/Enum.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Enum.thy Wed Sep 03 00:06:24 2014 +0200
@@ -493,7 +493,7 @@
text {* We define small finite types for the use in Quickcheck *}
-datatype finite_1 = a\<^sub>1
+datatype_new finite_1 = a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +595,7 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype finite_2 = a\<^sub>1 | a\<^sub>2
+datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -701,7 +701,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -825,7 +825,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -927,7 +927,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
--- a/src/HOL/Groups_List.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Groups_List.thy Wed Sep 03 00:06:24 2014 +0200
@@ -8,7 +8,7 @@
begin
definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
-"listsum xs = foldr plus xs 0"
+ "listsum xs = foldr plus xs 0"
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
--- a/src/HOL/Lazy_Sequence.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy Wed Sep 03 00:06:24 2014 +0200
@@ -9,7 +9,7 @@
subsection {* Type of lazy sequences *}
-datatype 'a lazy_sequence = lazy_sequence_of_list "'a list"
+datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
where
@@ -29,7 +29,7 @@
lemma size_lazy_sequence_eq [code]:
"size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
- "size (xq :: 'a lazy_sequence) = 0"
+ "size xq = Suc (length (list_of_lazy_sequence xq))"
by (cases xq, simp)+
lemma case_lazy_sequence [simp]:
--- a/src/HOL/Main.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Main.thy Wed Sep 03 00:06:24 2014 +0200
@@ -30,10 +30,9 @@
convol ("\<langle>(_,/ _)\<rangle>")
hide_const (open)
- czero cinfinite cfinite csum cone ctwo Csum cprod cexp
- image2 image2p vimage2p Gr Grp collect fsts snds setl setr
- convol pick_middlep fstOp sndOp csquare relImage relInvImage
- Succ Shift shift proj
+ czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
+ fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
+ shift proj
no_syntax (xsymbols)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- a/src/HOL/Nitpick.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Nitpick.thy Wed Sep 03 00:06:24 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype ('a, 'b) pair_box = PairBox 'a 'b
-datatype 'a word = Word "'a set"
+datatype_new (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype_new (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype_new (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit
--- a/src/HOL/Num.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Num.thy Wed Sep 03 00:06:24 2014 +0200
@@ -11,7 +11,7 @@
subsection {* The @{text num} type *}
-datatype num = One | Bit0 num | Bit1 num
+datatype_new num = One | Bit0 num | Bit1 num
text {* Increment function for type @{typ num} *}
--- a/src/HOL/Predicate.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Predicate.thy Wed Sep 03 00:06:24 2014 +0200
@@ -10,7 +10,7 @@
subsection {* The type of predicate enumerations (a monad) *}
-datatype 'a pred = Pred "'a \<Rightarrow> bool"
+datatype_new 'a pred = Pred "'a \<Rightarrow> bool"
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
eval_pred: "eval (Pred f) = f"
@@ -402,7 +402,7 @@
subsection {* Implementation *}
-datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
+datatype_new 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
"pred_of_seq Empty = \<bottom>"
--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Sep 03 00:06:24 2014 +0200
@@ -574,8 +574,8 @@
where
"pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
-datatype 'a unknown = Unknown | Known 'a
-datatype 'a three_valued = Unknown_value | Value 'a | No_value
+datatype_new (dead 'a) unknown = Unknown | Known 'a
+datatype_new (dead 'a) three_valued = Unknown_value | Value 'a | No_value
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Sep 03 00:06:24 2014 +0200
@@ -26,13 +26,19 @@
subsubsection {* Narrowing's deep representation of types and terms *}
-datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
-datatype narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list"
-datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
+datatype_new narrowing_type =
+ Narrowing_sum_of_products "narrowing_type list list"
+
+datatype_new narrowing_term =
+ Narrowing_variable "integer list" narrowing_type
+| Narrowing_constructor integer "narrowing_term list"
+
+datatype_new (dead 'a) narrowing_cons =
+ Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
where
- "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
+ "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f o c) cs)"
subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
@@ -70,7 +76,7 @@
definition cons :: "'a => 'a narrowing"
where
- "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
+ "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
where
@@ -88,7 +94,7 @@
case a (d - 1) of Narrowing_cons ta cas =>
let
shallow = (d > 0 \<and> non_empty ta);
- cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
+ cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
@@ -121,7 +127,7 @@
class narrowing =
fixes narrowing :: "integer => 'a narrowing_cons"
-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
+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
(* FIXME: hard-wired maximal depth of 100 here *)
definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
@@ -149,7 +155,7 @@
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
-datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
+datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
where
@@ -159,7 +165,7 @@
hide_type (open) ffun
hide_const (open) Constant Update eval_ffun
-datatype 'b cfun = Constant 'b
+datatype_new (dead 'b) cfun = Constant 'b
primrec eval_cfun :: "'b cfun => 'a => 'b"
where
@@ -308,4 +314,3 @@
hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
end
-
--- a/src/HOL/Quickcheck_Random.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Quickcheck_Random.thy Wed Sep 03 00:06:24 2014 +0200
@@ -228,4 +228,3 @@
hide_fact (open) collapse_def beyond_def random_fun_lift_def
end
-
--- a/src/HOL/Record.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Record.thy Wed Sep 03 00:06:24 2014 +0200
@@ -79,7 +79,7 @@
subsection {* Operators and lemmas for types isomorphic to tuples *}
-datatype ('a, 'b, 'c) tuple_isomorphism =
+datatype_new (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
primrec
--- a/src/HOL/String.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/String.thy Wed Sep 03 00:06:24 2014 +0200
@@ -8,7 +8,7 @@
subsection {* Characters and strings *}
-datatype nibble =
+datatype_new nibble =
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
@@ -114,7 +114,7 @@
"nibble_of_nat (n mod 16) = nibble_of_nat n"
by (simp add: nibble_of_nat_def)
-datatype char = Char nibble nibble
+datatype_new char = Char nibble nibble
-- "Note: canonical order of character encoding coincides with standard term ordering"
syntax
--- a/src/HOL/Typerep.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Typerep.thy Wed Sep 03 00:06:24 2014 +0200
@@ -6,7 +6,7 @@
imports String
begin
-datatype typerep = Typerep String.literal "typerep list"
+datatype_new typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself \<Rightarrow> typerep"