--- a/src/Doc/Codegen/Evaluation.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Thu Sep 11 18:54:36 2014 +0200
@@ -205,7 +205,7 @@
An simplistic example:
*}
-datatype %quote form_ord = T | F | Less nat nat
+datatype_new %quote form_ord = T | F | Less nat nat
| And form_ord form_ord | Or form_ord form_ord | Neg form_ord
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
@@ -259,7 +259,7 @@
example:
*}
-datatype %quote form = T | F | And form form | Or form form (*<*)
+datatype_new %quote form = T | F | And form form | Or form form (*<*)
(*>*) ML %quotett {*
fun eval_form @{code T} = true
--- a/src/Doc/Codegen/Introduction.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Codegen/Introduction.thy Thu Sep 11 18:54:36 2014 +0200
@@ -35,7 +35,7 @@
subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
text {*
- In a HOL theory, the @{command_def datatype} and @{command_def
+ In a HOL theory, the @{command_def datatype_new} and @{command_def
definition}/@{command_def primrec}/@{command_def fun} declarations
form the core of a functional programming language. By default
equational theorems stemming from those are used for generated code,
@@ -45,7 +45,7 @@
For example, here a simple \qt{implementation} of amortised queues:
*}
-datatype %quote 'a queue = AQueue "'a list" "'a list"
+datatype_new %quote 'a queue = AQueue "'a list" "'a list"
definition %quote empty :: "'a queue" where
"empty = AQueue [] []"
--- a/src/Doc/Codegen/Refinement.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Codegen/Refinement.thy Thu Sep 11 18:54:36 2014 +0200
@@ -87,7 +87,7 @@
queues:
*}
-datatype %quote 'a queue = Queue "'a list"
+datatype_new %quote 'a queue = Queue "'a list"
definition %quote empty :: "'a queue" where
"empty = Queue []"
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 18:54:36 2014 +0200
@@ -5,7 +5,7 @@
Author: Andrei Popescu, TU Muenchen
Author: Dmitriy Traytel, TU Muenchen
-Tutorial for (co)datatype definitions with the new package.
+Tutorial for (co)datatype definitions.
*)
theory Datatypes
@@ -21,14 +21,9 @@
\label{sec:introduction} *}
text {*
-The 2013 edition of Isabelle introduced a new definitional package for freely
-generated datatypes and codatatypes. The datatype support is similar to that
-provided by the earlier package due to Berghofer and Wenzel
-\cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
-\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
-@{command datatype_new} is often all that is needed to port existing theories to
-use the new package.
-
+The 2013 edition of Isabelle introduced a definitional package for freely
+generated datatypes and codatatypes. This package replaces the earlier
+implementation due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}.
Perhaps the main advantage of the new package is that it supports recursion
through a large class of non-datatypes, such as finite sets:
*}
@@ -51,7 +46,7 @@
generated discriminators, selectors, and relators as well as a wealth of
properties about them.
-In addition to inductive datatypes, the new package supports coinductive
+In addition to inductive datatypes, the package supports coinductive
datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
following command introduces the type of lazy lists, which comprises both finite
and infinite values:
@@ -151,12 +146,8 @@
\newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
in.\allowbreak tum.\allowbreak de}}
-The command @{command datatype_new} is expected to replace \keyw{datatype} in a
-future release. Authors of new theories are encouraged to use the new commands,
-and maintainers of older theories may want to consider upgrading.
-
-Comments and bug reports concerning either the tool or this tutorial should be
-directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
+Comments and bug reports concerning either the package or this tutorial should
+be directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
\authoremailiv, and \authoremailv.
*}
@@ -1036,8 +1027,9 @@
text {*
The command @{command datatype_new} has been designed to be highly compatible
-with the old \keyw{datatype}, to ease migration. There are nonetheless a few
-incompatibilities that may arise when porting to the new package:
+with the old command (which is now called \keyw{old_datatype}), to ease
+migration. There are nonetheless a few incompatibilities that may arise when
+porting:
\begin{itemize}
\setlength{\itemsep}{0pt}
@@ -1065,8 +1057,8 @@
@{text "[unfolded all_mem_range]"} attribute on @{text t.induct}.
\item \emph{The internal constructions are completely different.} Proof texts
-that unfold the definition of constants introduced by \keyw{datatype} will be
-difficult to port.
+that unfold the definition of constants introduced by \keyw{old\_datatype} will
+be difficult to port.
\item \emph{Some constants and theorems have different names.}
For non-mutually recursive datatypes,
@@ -2696,9 +2688,6 @@
% * need for this is rare but may arise if you want e.g. to add destructors to
% a type not introduced by ...
%
-% * also useful for compatibility with old package, e.g. add destructors to
-% old \keyw{datatype}
-%
% * @{command free_constructors}
% * @{text plugins}, @{text discs_sels}
% * hack to have both co and nonco view via locale (cf. ext nats)
--- a/src/Doc/Datatypes/document/root.tex Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Datatypes/document/root.tex Thu Sep 11 18:54:36 2014 +0200
@@ -76,10 +76,9 @@
\begin{abstract}
\noindent
-This tutorial describes the new package for defining datatypes and codatatypes
+This tutorial describes the definitional package for datatypes and codatatypes
in Isabelle/HOL. The package provides four main commands: \keyw{datatype_new},
-\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. The first command is
-expected to eventually replace the old \keyw{datatype} command.
+\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
\end{abstract}
\tableofcontents
--- a/src/Doc/Functions/Functions.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Functions/Functions.thy Thu Sep 11 18:54:36 2014 +0200
@@ -522,7 +522,7 @@
and @{term "X"} for true, false and uncertain propositions, respectively.
*}
-datatype P3 = T | F | X
+datatype_new P3 = T | F | X
text {* \noindent Then the conjunction of such values can be defined as follows: *}
@@ -1122,7 +1122,7 @@
As an example, imagine a datatype of n-ary trees:
*}
-datatype 'a tree =
+datatype_new 'a tree =
Leaf 'a
| Branch "'a tree list"
--- a/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 18:54:36 2014 +0200
@@ -736,7 +736,7 @@
monotonically through the theory hierarchy: forming a new theory,
the union of the simpsets of its imports are taken as starting
point. Also note that definitional packages like @{command
- "datatype"}, @{command "primrec"}, @{command "fun"} routinely
+ "datatype_new"}, @{command "primrec"}, @{command "fun"} routinely
declare Simplifier rules to the target context, while plain
@{command "definition"} is an exception in \emph{not} declaring
anything.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200
@@ -283,11 +283,10 @@
\begin{description}
\item @{command (HOL) "primrec"} defines primitive recursive
- functions over datatypes (see also @{command_ref (HOL) datatype} and
- @{command_ref (HOL) rep_datatype}). The given @{text equations}
- specify reduction rules that are produced by instantiating the
- generic combinator for primitive recursion that is available for
- each datatype.
+ functions over datatypes (see also @{command_ref (HOL) datatype_new}).
+ The given @{text equations} specify reduction rules that are produced
+ by instantiating the generic combinator for primitive recursion that
+ is available for each datatype.
Each equation needs to be of the form:
@@ -379,7 +378,7 @@
boolean expressions, and use @{command primrec} for evaluation
functions that follow the same recursive structure. *}
-datatype 'a aexp =
+datatype_new 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
@@ -450,7 +449,7 @@
text {* Functions on datatypes with nested recursion are also defined
by mutual primitive recursion. *}
-datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
+datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
text {* A substitution function on type @{typ "('a, 'b) term"} can be
defined as follows, by working simultaneously on @{typ "('a, 'b)
@@ -471,7 +470,7 @@
lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
"subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
- by (induct t and ts) simp_all
+ by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
subsubsection {* Example: a map function for infinitely branching trees *}
@@ -480,7 +479,7 @@
primitive recursion is just as easy.
*}
-datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
+datatype_new 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
where
@@ -702,16 +701,16 @@
*}
-section {* Datatypes \label{sec:hol-datatype} *}
+section {* Old-style datatypes \label{sec:hol-datatype} *}
text {*
\begin{matharray}{rcl}
- @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "old_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
\end{matharray}
@{rail \<open>
- @@{command (HOL) datatype} (spec + @'and')
+ @@{command (HOL) old_datatype} (spec + @'and')
;
@@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
;
@@ -723,30 +722,16 @@
\begin{description}
- \item @{command (HOL) "datatype"} defines inductive datatypes in
- HOL.
+ \item @{command (HOL) "old_datatype"} defines old-style inductive
+ datatypes in HOL.
\item @{command (HOL) "rep_datatype"} represents existing types as
- datatypes.
-
- For foundational reasons, some basic types such as @{typ nat}, @{typ
- "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
- introduced by more primitive means using @{command_ref typedef}. To
- recover the rich infrastructure of @{command datatype} (e.g.\ rules
- for @{method cases} and @{method induct} and the primitive recursion
- combinators), such types may be represented as actual datatypes
- later. This is done by specifying the constructors of the desired
- type, and giving a proof of the induction rule, distinctness and
- injectivity of constructors.
-
- For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
- representation of the primitive sum type as fully-featured datatype.
+ old-style datatypes.
\end{description}
- The generated rules for @{method induct} and @{method cases} provide
- case names according to the given constructors, while parameters are
- named after the types (see also \secref{sec:cases-induct}).
+ These commands are mostly obsolete; @{command (HOL) "datatype"}
+ should be used instead.
See \cite{isabelle-HOL} for more details on datatypes, but beware of
the old-style theory syntax being used there! Apart from proper
@@ -764,7 +749,7 @@
names than the existing @{typ "'a list"} that is already in @{theory
Main}: *}
-datatype 'a seq = Empty | Seq 'a "'a seq"
+datatype_new 'a seq = Empty | Seq 'a "'a seq"
text {* We can now prove some simple lemma by structural induction: *}
@@ -1173,9 +1158,9 @@
by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
text {* Note that such trivial constructions are better done with
- derived specification mechanisms such as @{command datatype}: *}
-
-datatype three' = One' | Two' | Three'
+ derived specification mechanisms such as @{command datatype_new}: *}
+
+datatype_new three' = One' | Two' | Three'
text {* This avoids re-doing basic definitions and proofs from the
primitive @{command typedef} above. *}
@@ -2369,7 +2354,7 @@
to reason about inductive types. Rules are selected according to
the declarations by the @{attribute cases} and @{attribute induct}
attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
- datatype} package already takes care of this.
+ datatype_new} package already takes care of this.
These unstructured tactics feature both goal addressing and dynamic
instantiation. Note that named rule cases are \emph{not} provided
--- a/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 18:54:36 2014 +0200
@@ -81,7 +81,7 @@
the formal text. Examples may be seen in Isabelle/HOL sources
itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
@{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
- "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
+ "\"old_datatype\""} @{text ":: thy_decl"} for theory-level declarations
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
--- a/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 18:54:36 2014 +0200
@@ -1068,7 +1068,7 @@
provide suitable derived cases rules.
*}
-datatype foo = Foo | Bar foo
+datatype_new foo = Foo | Bar foo
notepad
begin
--- a/src/Doc/Tutorial/CodeGen/CodeGen.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy Thu Sep 11 18:54:36 2014 +0200
@@ -16,9 +16,9 @@
*}
type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
-datatype ('a,'v)expr = Cex 'v
- | Vex 'a
- | Bex "'v binop" "('a,'v)expr" "('a,'v)expr";
+datatype (dead 'a, 'v) expr = Cex 'v
+ | Vex 'a
+ | Bex "'v binop" "('a,'v)expr" "('a,'v)expr";
text{*\noindent
The three constructors represent constants, variables and the application of
@@ -40,7 +40,7 @@
the result. As for @{text"expr"}, addresses and values are type parameters:
*}
-datatype ('a,'v) instr = Const 'v
+datatype (dead 'a, 'v) instr = Const 'v
| Load 'a
| Apply "'v binop";
--- a/src/Doc/Tutorial/Datatype/Fundata.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Datatype/Fundata.thy Thu Sep 11 18:54:36 2014 +0200
@@ -1,7 +1,7 @@
(*<*)
theory Fundata imports Main begin
(*>*)
-datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
+datatype (dead 'a,'i) bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
text{*\noindent
Parameter @{typ"'a"} is the type of values stored in
--- a/src/Doc/Tutorial/Datatype/Nested.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Datatype/Nested.thy Thu Sep 11 18:54:36 2014 +0200
@@ -67,7 +67,7 @@
lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and>
substs Var ts = (ts::('v,'f)term list)";
-apply(induct_tac t and ts, simp_all);
+apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all);
done
text{*\noindent
@@ -105,7 +105,7 @@
(* Exercise 1: *)
lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and>
substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
-apply (induct_tac t and ts)
+apply (induct_tac t and ts rule: subst.induct substs.induct)
apply (simp_all)
done
@@ -125,7 +125,7 @@
lemma "trev (trev t) = (t::('v,'f)term) \<and>
trevs (trevs ts) = (ts::('v,'f)term list)"
-apply (induct_tac t and ts, simp_all)
+apply (induct_tac t and ts rule: trev.induct trevs.induct, simp_all)
done
(*>*)
--- a/src/Doc/Tutorial/Protocol/Message.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Sep 11 18:54:36 2014 +0200
@@ -334,6 +334,7 @@
txt{*MPair case: blast works out the necessary sum itself!*}
prefer 2 apply auto apply (blast elim!: add_leE)
txt{*Nonce case*}
+apply (rename_tac nat)
apply (rule_tac x = "N + Suc nat" in exI, auto)
done
(*>*)
--- a/src/Doc/Tutorial/Trie/Trie.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Trie/Trie.thy Thu Sep 11 18:54:36 2014 +0200
@@ -208,7 +208,7 @@
(* Exercise 3. Solution by Getrud Bauer *)
-datatype ('a,'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option";
+datatype ('a,dead 'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option";
primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
"valuem (Triem ov m) = ov"
--- a/src/HOL/Auth/Event.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,7 +15,7 @@
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
-datatype
+datatype_new
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/Auth/Guard/Extensions.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Thu Sep 11 18:54:36 2014 +0200
@@ -579,6 +579,7 @@
apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
apply (erule initState_used)
apply (case_tac a, auto)
+apply (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto dest: Says_imp_used intro: used_ConsI)
@@ -592,6 +593,7 @@
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
apply (case_tac a, auto)
+apply (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
--- a/src/HOL/BNF_Examples/Compat.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/BNF_Examples/Compat.thy Thu Sep 11 18:54:36 2014 +0200
@@ -27,7 +27,7 @@
|> tap (check_lens lens);
\<close>
-datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
+old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
@@ -169,11 +169,11 @@
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close>
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close>
-datatype funky = Funky "funky tre" | Funky'
+old_datatype funky = Funky "funky tre" | Funky'
ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close>
-datatype fnky = Fnky "nat tre"
+old_datatype fnky = Fnky "nat tre"
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 18:54:36 2014 +0200
@@ -12,6 +12,7 @@
theory BNF_Least_Fixpoint
imports BNF_Fixpoint_Base
keywords
+ "datatype" :: thy_decl and
"datatype_new" :: thy_decl and
"datatype_compat" :: thy_decl
begin
--- a/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 18:54:36 2014 +0200
@@ -5,13 +5,13 @@
theory Brackin imports Main begin
-datatype T =
+old_datatype T =
X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
X32 | X33 | X34
-datatype ('a, 'b, 'c) TY1 =
+old_datatype ('a, 'b, 'c) TY1 =
NoF
| Fk 'a "('a, 'b, 'c) TY2"
and ('a, 'b, 'c) TY2 =
--- a/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 18:54:36 2014 +0200
@@ -5,158 +5,158 @@
theory Instructions imports Main begin
-datatype Size = Byte | Word | Long
+old_datatype Size = Byte | Word | Long
-datatype DataRegister
- = RegD0
- | RegD1
- | RegD2
- | RegD3
- | RegD4
- | RegD5
- | RegD6
- | RegD7
+old_datatype DataRegister =
+ RegD0
+| RegD1
+| RegD2
+| RegD3
+| RegD4
+| RegD5
+| RegD6
+| RegD7
-datatype AddressRegister
- = RegA0
- | RegA1
- | RegA2
- | RegA3
- | RegA4
- | RegA5
- | RegA6
- | RegA7
+old_datatype AddressRegister =
+ RegA0
+| RegA1
+| RegA2
+| RegA3
+| RegA4
+| RegA5
+| RegA6
+| RegA7
-datatype DataOrAddressRegister
- = data DataRegister
- | address AddressRegister
+old_datatype DataOrAddressRegister =
+ data DataRegister
+| address AddressRegister
-datatype Condition
- = Hi
- | Ls
- | Cc
- | Cs
- | Ne
- | Eq
- | Vc
- | Vs
- | Pl
- | Mi
- | Ge
- | Lt
- | Gt
- | Le
+old_datatype Condition =
+ Hi
+| Ls
+| Cc
+| Cs
+| Ne
+| Eq
+| Vc
+| Vs
+| Pl
+| Mi
+| Ge
+| Lt
+| Gt
+| Le
-datatype AddressingMode
- = immediate nat
- | direct DataOrAddressRegister
- | indirect AddressRegister
- | postinc AddressRegister
- | predec AddressRegister
- | indirectdisp nat AddressRegister
- | indirectindex nat AddressRegister DataOrAddressRegister Size
- | absolute nat
- | pcdisp nat
- | pcindex nat DataOrAddressRegister Size
+old_datatype AddressingMode =
+ immediate nat
+| direct DataOrAddressRegister
+| indirect AddressRegister
+| postinc AddressRegister
+| predec AddressRegister
+| indirectdisp nat AddressRegister
+| indirectindex nat AddressRegister DataOrAddressRegister Size
+| absolute nat
+| pcdisp nat
+| pcindex nat DataOrAddressRegister Size
-datatype M68kInstruction
- = ABCD AddressingMode AddressingMode
- | ADD Size AddressingMode AddressingMode
- | ADDA Size AddressingMode AddressRegister
- | ADDI Size nat AddressingMode
- | ADDQ Size nat AddressingMode
- | ADDX Size AddressingMode AddressingMode
- | AND Size AddressingMode AddressingMode
- | ANDI Size nat AddressingMode
- | ANDItoCCR nat
- | ANDItoSR nat
- | ASL Size AddressingMode DataRegister
- | ASLW AddressingMode
- | ASR Size AddressingMode DataRegister
- | ASRW AddressingMode
- | Bcc Condition Size nat
- | BTST Size AddressingMode AddressingMode
- | BCHG Size AddressingMode AddressingMode
- | BCLR Size AddressingMode AddressingMode
- | BSET Size AddressingMode AddressingMode
- | BRA Size nat
- | BSR Size nat
- | CHK AddressingMode DataRegister
- | CLR Size AddressingMode
- | CMP Size AddressingMode DataRegister
- | CMPA Size AddressingMode AddressRegister
- | CMPI Size nat AddressingMode
- | CMPM Size AddressRegister AddressRegister
- | DBT DataRegister nat
- | DBF DataRegister nat
- | DBcc Condition DataRegister nat
- | DIVS AddressingMode DataRegister
- | DIVU AddressingMode DataRegister
- | EOR Size DataRegister AddressingMode
- | EORI Size nat AddressingMode
- | EORItoCCR nat
- | EORItoSR nat
- | EXG DataOrAddressRegister DataOrAddressRegister
- | EXT Size DataRegister
- | ILLEGAL
- | JMP AddressingMode
- | JSR AddressingMode
- | LEA AddressingMode AddressRegister
- | LINK AddressRegister nat
- | LSL Size AddressingMode DataRegister
- | LSLW AddressingMode
- | LSR Size AddressingMode DataRegister
- | LSRW AddressingMode
- | MOVE Size AddressingMode AddressingMode
- | MOVEtoCCR AddressingMode
- | MOVEtoSR AddressingMode
- | MOVEfromSR AddressingMode
- | MOVEtoUSP AddressingMode
- | MOVEfromUSP AddressingMode
- | MOVEA Size AddressingMode AddressRegister
- | MOVEMto Size AddressingMode "DataOrAddressRegister list"
- | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
- | MOVEP Size AddressingMode AddressingMode
- | MOVEQ nat DataRegister
- | MULS AddressingMode DataRegister
- | MULU AddressingMode DataRegister
- | NBCD AddressingMode
- | NEG Size AddressingMode
- | NEGX Size AddressingMode
- | NOP
- | NOT Size AddressingMode
- | OR Size AddressingMode AddressingMode
- | ORI Size nat AddressingMode
- | ORItoCCR nat
- | ORItoSR nat
- | PEA AddressingMode
- | RESET
- | ROL Size AddressingMode DataRegister
- | ROLW AddressingMode
- | ROR Size AddressingMode DataRegister
- | RORW AddressingMode
- | ROXL Size AddressingMode DataRegister
- | ROXLW AddressingMode
- | ROXR Size AddressingMode DataRegister
- | ROXRW AddressingMode
- | RTE
- | RTR
- | RTS
- | SBCD AddressingMode AddressingMode
- | ST AddressingMode
- | SF AddressingMode
- | Scc Condition AddressingMode
- | STOP nat
- | SUB Size AddressingMode AddressingMode
- | SUBA Size AddressingMode AddressingMode
- | SUBI Size nat AddressingMode
- | SUBQ Size nat AddressingMode
- | SUBX Size AddressingMode AddressingMode
- | SWAP DataRegister
- | TAS AddressingMode
- | TRAP nat
- | TRAPV
- | TST Size AddressingMode
- | UNLK AddressRegister
+old_datatype M68kInstruction =
+ ABCD AddressingMode AddressingMode
+| ADD Size AddressingMode AddressingMode
+| ADDA Size AddressingMode AddressRegister
+| ADDI Size nat AddressingMode
+| ADDQ Size nat AddressingMode
+| ADDX Size AddressingMode AddressingMode
+| AND Size AddressingMode AddressingMode
+| ANDI Size nat AddressingMode
+| ANDItoCCR nat
+| ANDItoSR nat
+| ASL Size AddressingMode DataRegister
+| ASLW AddressingMode
+| ASR Size AddressingMode DataRegister
+| ASRW AddressingMode
+| Bcc Condition Size nat
+| BTST Size AddressingMode AddressingMode
+| BCHG Size AddressingMode AddressingMode
+| BCLR Size AddressingMode AddressingMode
+| BSET Size AddressingMode AddressingMode
+| BRA Size nat
+| BSR Size nat
+| CHK AddressingMode DataRegister
+| CLR Size AddressingMode
+| CMP Size AddressingMode DataRegister
+| CMPA Size AddressingMode AddressRegister
+| CMPI Size nat AddressingMode
+| CMPM Size AddressRegister AddressRegister
+| DBT DataRegister nat
+| DBF DataRegister nat
+| DBcc Condition DataRegister nat
+| DIVS AddressingMode DataRegister
+| DIVU AddressingMode DataRegister
+| EOR Size DataRegister AddressingMode
+| EORI Size nat AddressingMode
+| EORItoCCR nat
+| EORItoSR nat
+| EXG DataOrAddressRegister DataOrAddressRegister
+| EXT Size DataRegister
+| ILLEGAL
+| JMP AddressingMode
+| JSR AddressingMode
+| LEA AddressingMode AddressRegister
+| LINK AddressRegister nat
+| LSL Size AddressingMode DataRegister
+| LSLW AddressingMode
+| LSR Size AddressingMode DataRegister
+| LSRW AddressingMode
+| MOVE Size AddressingMode AddressingMode
+| MOVEtoCCR AddressingMode
+| MOVEtoSR AddressingMode
+| MOVEfromSR AddressingMode
+| MOVEtoUSP AddressingMode
+| MOVEfromUSP AddressingMode
+| MOVEA Size AddressingMode AddressRegister
+| MOVEMto Size AddressingMode "DataOrAddressRegister list"
+| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
+| MOVEP Size AddressingMode AddressingMode
+| MOVEQ nat DataRegister
+| MULS AddressingMode DataRegister
+| MULU AddressingMode DataRegister
+| NBCD AddressingMode
+| NEG Size AddressingMode
+| NEGX Size AddressingMode
+| NOP
+| NOT Size AddressingMode
+| OR Size AddressingMode AddressingMode
+| ORI Size nat AddressingMode
+| ORItoCCR nat
+| ORItoSR nat
+| PEA AddressingMode
+| RESET
+| ROL Size AddressingMode DataRegister
+| ROLW AddressingMode
+| ROR Size AddressingMode DataRegister
+| RORW AddressingMode
+| ROXL Size AddressingMode DataRegister
+| ROXLW AddressingMode
+| ROXR Size AddressingMode DataRegister
+| ROXRW AddressingMode
+| RTE
+| RTR
+| RTS
+| SBCD AddressingMode AddressingMode
+| ST AddressingMode
+| SF AddressingMode
+| Scc Condition AddressingMode
+| STOP nat
+| SUB Size AddressingMode AddressingMode
+| SUBA Size AddressingMode AddressingMode
+| SUBI Size nat AddressingMode
+| SUBQ Size nat AddressingMode
+| SUBX Size AddressingMode AddressingMode
+| SWAP DataRegister
+| TAS AddressingMode
+| TRAP nat
+| TRAPV
+| TST Size AddressingMode
+| UNLK AddressRegister
end
--- a/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200
@@ -97,7 +97,7 @@
method_setup pat_completeness = {*
Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
-*} "prove completeness of datatype patterns"
+*} "prove completeness of (co)datatype patterns"
ML_file "Tools/Function/fun.ML"
ML_file "Tools/Function/induction_schema.ML"
--- a/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 18:54:36 2014 +0200
@@ -25,12 +25,10 @@
typedecl D
-datatype
-
+datatype_new
M = Md D | Mreq ("\<bullet>")
-datatype
-
+datatype_new
State = Sd D | Snil ("\<currency>")
type_synonym
--- a/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,11 +15,11 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype
- 'a com = Basic "'a \<Rightarrow> 'a"
- | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
- | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
- | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+datatype_new 'a com =
+ Basic "'a \<Rightarrow> 'a"
+| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
+| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
abbreviation annskip ("SKIP") where "SKIP == Basic id"
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 18:54:36 2014 +0200
@@ -12,12 +12,12 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype
- 'a com = Basic "'a \<Rightarrow> 'a"
- | Abort
- | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
- | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
- | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+datatype_new 'a com =
+ Basic "'a \<Rightarrow> 'a"
+| Abort
+| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
+| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
abbreviation annskip ("SKIP") where "SKIP == Basic id"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200
@@ -37,7 +37,7 @@
and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-datatype 'a up = bot | Up 'a
+old_datatype 'a up = bot | Up 'a
instantiation up :: (SL_top)SL_top
begin
--- a/src/HOL/IMP/Com.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/IMP/Com.thy Thu Sep 11 18:54:36 2014 +0200
@@ -2,7 +2,7 @@
theory Com imports BExp begin
-datatype
+datatype_new
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
--- a/src/HOL/IMP/Procs.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/IMP/Procs.thy Thu Sep 11 18:54:36 2014 +0200
@@ -6,7 +6,7 @@
type_synonym pname = string
-datatype
+datatype_new
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
--- a/src/HOL/Imperative_HOL/Heap.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Thu Sep 11 18:54:36 2014 +0200
@@ -53,11 +53,8 @@
definition empty :: heap where
"empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
-datatype_new 'a array = Array addr -- "note the phantom type 'a"
-datatype_compat array
-
-datatype_new 'a ref = Ref addr -- "note the phantom type 'a"
-datatype_compat ref
+old_datatype 'a array = Array addr -- "note the phantom type 'a"
+old_datatype 'a ref = Ref addr -- "note the phantom type 'a"
primrec addr_of_array :: "'a array \<Rightarrow> addr" where
"addr_of_array (Array x) = x"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Sep 11 18:54:36 2014 +0200
@@ -11,7 +11,7 @@
section {* Definition of Linked Lists *}
setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
-datatype 'a node = Empty | Node 'a "'a node ref"
+old_datatype 'a node = Empty | Node 'a "'a node ref"
primrec
node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
--- a/src/HOL/Induct/Com.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Induct/Com.thy Thu Sep 11 18:54:36 2014 +0200
@@ -12,7 +12,7 @@
typedecl loc
type_synonym state = "loc => nat"
-datatype
+datatype_new
exp = N nat
| X loc
| Op "nat => nat => nat" exp exp
--- a/src/HOL/Induct/QuoDataType.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 11 18:54:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{*Defining the Free Algebra*}
text{*Messages with encryption and decryption as free constructors.*}
-datatype
+datatype_new
freemsg = NONCE nat
| MPAIR freemsg freemsg
| CRYPT nat freemsg
--- a/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 18:54:36 2014 +0200
@@ -10,11 +10,13 @@
subsection{*Defining the Free Algebra*}
text{*Messages with encryption and decryption as free constructors.*}
-datatype
+datatype_new
freeExp = VAR nat
| PLUS freeExp freeExp
| FNCALL nat "freeExp list"
+datatype_compat freeExp
+
text{*The equivalence relation, which makes PLUS associative.*}
text{*The first rule is the desired equation. The next three rules
@@ -38,7 +40,8 @@
lemma exprel_refl: "X \<sim> X"
and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
- by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+
+ by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct)
+ (blast intro: exprel.intros listrel.intros)+
theorem equiv_exprel: "equiv UNIV exprel"
proof -
@@ -306,7 +309,7 @@
lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
apply (cases Xs rule: eq_Abs_ExpList)
apply (simp add: FnCall)
-apply (induct_tac Us)
+apply (induct_tac Us)
apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
done
@@ -428,7 +431,7 @@
obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
- proof (induct U and Us)
+ proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct)
case (VAR nat)
with V show ?case by (simp add: Var_def)
next
--- a/src/HOL/Induct/SList.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Induct/SList.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,10 +15,10 @@
so that list can serve as a "functor" for defining other recursive types.
-This enables the conservative construction of mutual recursive data-types
+This enables the conservative construction of mutual recursive datatypes
such as
-datatype 'a m = Node 'a * ('a m) list
+datatype 'a m = Node 'a * 'a m list
*)
header {* Extended List Theory (old) *}
--- a/src/HOL/Nominal/Examples/Fsub.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Thu Sep 11 18:54:36 2014 +0200
@@ -30,7 +30,7 @@
there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *}
text{* The constructors for types and terms in System \FSUB{} contain abstractions
- over type-variables and term-variables. The nominal datatype-package uses
+ over type-variables and term-variables. The nominal datatype package uses
@{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *}
nominal_datatype ty =
--- a/src/HOL/Old_Datatype.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Old_Datatype.thy Thu Sep 11 18:54:36 2014 +0200
@@ -7,7 +7,7 @@
theory Old_Datatype
imports Power
-keywords "datatype" :: thy_decl
+keywords "old_datatype" :: thy_decl
begin
subsection {* The datatype universe *}
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 18:54:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{*Defining the Free Algebra*}
-datatype
+datatype_new
freemsg = NONCE nat
| MPAIR freemsg freemsg
| CRYPT nat freemsg
--- a/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,7 +15,7 @@
text{*Message events*}
-datatype
+datatype_new
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 18:54:36 2014 +0200
@@ -52,11 +52,11 @@
text{*Agents. We allow any number of certification authorities, cardholders
merchants, and payment gateways.*}
-datatype
+datatype_new
agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
text{*Messages*}
-datatype
+datatype_new
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
@@ -373,6 +373,7 @@
(*MPair case: blast_tac works out the necessary sum itself!*)
prefer 2 apply (blast elim!: add_leE)
(*Nonce case*)
+apply (rename_tac nat)
apply (rule_tac x = "N + Suc nat" in exI)
apply (auto elim!: add_leE)
done
@@ -382,6 +383,7 @@
apply (induct_tac "msg")
apply (simp_all (no_asm_simp) add: exI parts_insert2)
prefer 2 apply (blast elim!: add_leE)
+apply (rename_tac nat)
apply (rule_tac x = "N + Suc nat" in exI, auto)
done
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 18:54:36 2014 +0200
@@ -1814,6 +1814,10 @@
end;
val _ =
+ Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
+ (parse_co_datatype_cmd Least_FP construct_lfp);
+
+val _ =
Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 11 18:54:36 2014 +0200
@@ -791,7 +791,7 @@
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
- Outer_Syntax.command @{command_spec "datatype"} "define old-style inductive datatypes"
+ Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
(Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
--- a/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 18:54:36 2014 +0200
@@ -17,7 +17,7 @@
often need its structure. Traditionnaly such simplifications are written in ML,
proofs are synthesized.
-An other strategy is to declare an HOL-datatype @{text \<tau>} and an HOL function (the
+An other strategy is to declare an HOL datatype @{text \<tau>} and an HOL function (the
interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
--- a/src/HOL/ex/Refute_Examples.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Thu Sep 11 18:54:36 2014 +0200
@@ -507,10 +507,6 @@
subsubsection {* Inductive datatypes *}
-text {* With @{text quick_and_dirty} set, the datatype package does
- not generate certain axioms for recursion operators. Without these
- axioms, Refute may find spurious countermodels. *}
-
text {* unit *}
lemma "P (x::unit)"