# HG changeset patch # User blanchet # Date 1409695584 -7200 # Node ID 6fe60a9a5bad9b317e22dfe03a97913dc511feba # Parent 414deb2ef328781f7da4e7a28448b4b23d975863 use 'datatype_new' in 'Main' diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Code_Evaluation.thy --- 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 \ typerep \ term" where "Const _ _ = dummy_term" diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Enum.thy --- 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") diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Groups_List.thy --- 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 \ 'a" where -"listsum xs = foldr plus xs 0" + "listsum xs = foldr plus xs 0" subsubsection {* List summation: @{const listsum} and @{text"\"}*} diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Lazy_Sequence.thy --- 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 \ '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]: diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Main.thy --- 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 ("\(_,/ _)\") 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 \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Nitpick.thy --- 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 \ '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 \ '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 diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Num.thy --- 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} *} diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Predicate.thy --- 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 \ bool" +datatype_new 'a pred = Pred "'a \ bool" primrec eval :: "'a pred \ 'a \ 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 \ 'a pred" where "pred_of_seq Empty = \" diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Quickcheck_Exhaustive.thy --- 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" diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Quickcheck_Narrowing.thy --- 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 \ '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 (\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 [[]]) [(\_. 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 \ non_empty ta); - cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs] + cs = [(\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 - diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Quickcheck_Random.thy --- 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 - diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Record.thy --- 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 \ 'b \ 'c" "'b \ 'c \ 'a" primrec diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/String.thy --- 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 diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Typerep.thy --- 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 \ typerep"