# HG changeset patch # User blanchet # Date 1410288696 -7200 # Node ID 180f1b3508ed2ae3f235d1d75ecb99a086136116 # Parent 25af24e1f37bb5f3f7ae05d04a7e8791c1d770ec use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Auth/Message.thy Tue Sep 09 20:51:36 2014 +0200 @@ -35,10 +35,10 @@ definition symKeys :: "key set" where "symKeys == {K. invKey K = K}" -datatype --{*We allow any number of friendly agents*} +datatype_new --{*We allow any number of friendly agents*} agent = Server | Friend nat | Spy -datatype +datatype_new msg = Agent agent --{*Agent names*} | Number nat --{*Ordinary integers, timestamps, ...*} | Nonce nat --{*Unguessable nonces*} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Auth/Public.thy Tue Sep 09 20:51:36 2014 +0200 @@ -16,7 +16,7 @@ subsection{*Asymmetric Keys*} -datatype keymode = Signature | Encryption +datatype_new keymode = Signature | Encryption consts publicKey :: "[keymode,agent] => key" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Auth/Smartcard/EventSC.thy --- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Auth/Smartcard/EventSC.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,10 +9,10 @@ consts (*Initial states of agents -- parameter of the construction*) initState :: "agent => msg set" -datatype card = Card agent +datatype_new card = Card agent text{*Four new events express the traffic between an agent and his card*} -datatype +datatype_new event = Says agent agent msg | Notes agent msg | Gets agent msg diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Auth/TLS.thy Tue Sep 09 20:51:36 2014 +0200 @@ -49,7 +49,7 @@ signature. Therefore, we formalize signature as encryption using the private encryption key.*} -datatype role = ClientRole | ServerRole +datatype_new role = ClientRole | ServerRole consts (*Pseudo-random function of Section 5*) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/BNF_Examples/Process.thy --- a/src/HOL/BNF_Examples/Process.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/BNF_Examples/Process.thy Tue Sep 09 20:51:36 2014 +0200 @@ -79,7 +79,7 @@ subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *} -datatype x_y_ax = x | y | ax +datatype_new x_y_ax = x | y | ax primcorec F :: "x_y_ax \ char list process" where "xyax = x \ isChoice (F xyax)" @@ -106,7 +106,7 @@ hide_const x y ax X Y AX (* Process terms *) -datatype ('a,'pvar) process_term = +datatype_new ('a,'pvar) process_term = VAR 'pvar | PROC "'a process" | ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/AxSem.thy Tue Sep 09 20:51:36 2014 +0200 @@ -378,7 +378,7 @@ \prg=G,cls=C,lcl=L\\dom (locals (store s))\t\A ) \ s\\(G,L))" -datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be +datatype_new 'a triple = triple "('a assn)" "term" "('a assn)" (** should be something like triple = \'a. triple ('a assn) term ('a assn) **) ("{(1_)}/ _>/ {(1_)}" [3,65,3]75) type_synonym 'a triples = "'a triple set" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Basis.thy Tue Sep 09 20:51:36 2014 +0200 @@ -155,7 +155,7 @@ primrec the_Inr :: "'a + 'b \ 'b" where "the_Inr (Inr b) = b" -datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c +datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c primrec the_In1 :: "('a, 'b, 'c) sum3 \ 'a" where "the_In1 (In1 a) = a" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Decl.thy Tue Sep 09 20:51:36 2014 +0200 @@ -42,7 +42,7 @@ subsubsection {* Access modifier *} -datatype acc_modi (* access modifier *) +datatype_new acc_modi (* access modifier *) = Private | Package | Protected | Public text {* @@ -223,9 +223,9 @@ introduce the notion of a member declaration (e.g. useful to define accessiblity ) *} -datatype memberdecl = fdecl fdecl | mdecl mdecl +datatype_new memberdecl = fdecl fdecl | mdecl mdecl -datatype memberid = fid vname | mid sig +datatype_new memberid = fid vname | mid sig class has_memberid = fixes memberid :: "'a \ memberid" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -66,9 +66,9 @@ section "type and expression names" (** unfortunately cannot simply instantiate tnam **) -datatype tnam' = HasFoo' | Base' | Ext' | Main' -datatype vnam' = arr' | vee' | z' | e' -datatype label' = lab1' +datatype_new tnam' = HasFoo' | Base' | Ext' | Main' +datatype_new vnam' = arr' | vee' | z' | e' +datatype_new label' = lab1' axiomatization tnam' :: "tnam' \ tnam" and diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Name.thy --- a/src/HOL/Bali/Name.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Name.thy Tue Sep 09 20:51:36 2014 +0200 @@ -12,11 +12,11 @@ typedecl vname --{* variable or field name *} typedecl label --{* label as destination of break or continue *} -datatype ename --{* expression name *} +datatype_new ename --{* expression name *} = VNam vname | Res --{* special name to model the return value of methods *} -datatype lname --{* names for local variables and the This pointer *} +datatype_new lname --{* names for local variables and the This pointer *} = EName ename | This abbreviation VName :: "vname \ lname" @@ -25,7 +25,7 @@ abbreviation Result :: lname where "Result == EName Res" -datatype xname --{* names of standard exceptions *} +datatype_new xname --{* names of standard exceptions *} = Throwable | NullPointer | OutOfMemory | ClassCast | NegArrSize | IndOutBound | ArrStore @@ -39,7 +39,7 @@ done -datatype tname --{* type names for standard classes and other type names *} +datatype_new tname --{* type names for standard classes and other type names *} = Object' | SXcpt' xname | TName tnam diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/State.thy Tue Sep 09 20:51:36 2014 +0200 @@ -19,7 +19,7 @@ section "objects" -datatype obj_tag = --{* tag for generic object *} +datatype_new obj_tag = --{* tag for generic object *} CInst qtname --{* class instance *} | Arr ty int --{* array with component type and length *} --{* | CStat qtname the tag is irrelevant for a class object, @@ -225,7 +225,7 @@ (type) "heap" <= (type) "(loc , obj) table" (* (type) "locals" <= (type) "(lname, val) table" *) -datatype st = (* pure state, i.e. contents of all variables *) +datatype_new st = (* pure state, i.e. contents of all variables *) st globs locals subsection "access" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Term.thy Tue Sep 09 20:51:36 2014 +0200 @@ -60,20 +60,20 @@ type_synonym locals = "(lname, val) table" --{* local variables *} -datatype jump +datatype_new jump = Break label --{* break *} | Cont label --{* continue *} | Ret --{* return from method *} -datatype xcpt --{* exception *} +datatype_new xcpt --{* exception *} = Loc loc --{* location of allocated execption object *} | Std xname --{* intermediate standard exception, see Eval.thy *} -datatype error +datatype_new error = AccessViolation --{* Access to a member that isn't permitted *} | CrossMethodJump --{* Method exits with a break or continue *} -datatype abrupt --{* abrupt completion *} +datatype_new abrupt --{* abrupt completion *} = Xcpt xcpt --{* exception *} | Jump jump --{* break, continue, return *} | Error error -- {* runtime errors, we wan't to detect and proof absent @@ -90,7 +90,7 @@ translations (type) "locals" <= (type) "(lname, val) table" -datatype inv_mode --{* invocation mode for method calls *} +datatype_new inv_mode --{* invocation mode for method calls *} = Static --{* static *} | SuperM --{* super *} | IntVir --{* interface or virtual *} @@ -104,13 +104,13 @@ (type) "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" --{* function codes for unary operations *} -datatype unop = UPlus -- {*{\tt +} unary plus*} +datatype_new unop = UPlus -- {*{\tt +} unary plus*} | UMinus -- {*{\tt -} unary minus*} | UBitNot -- {*{\tt ~} bitwise NOT*} | UNot -- {*{\tt !} logical complement*} --{* function codes for binary operations *} -datatype binop = Mul -- {*{\tt * } multiplication*} +datatype_new binop = Mul -- {*{\tt * } multiplication*} | Div -- {*{\tt /} division*} | Mod -- {*{\tt \%} remainder*} | Plus -- {*{\tt +} addition*} @@ -140,7 +140,7 @@ {\tt true || e} e is not evaluated; *} -datatype var +datatype_new var = LVar lname --{* local variable (incl. parameters) *} | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90) --{* class field *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Type.thy --- a/src/HOL/Bali/Type.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Type.thy Tue Sep 09 20:51:36 2014 +0200 @@ -14,13 +14,13 @@ \end{itemize} *} -datatype prim_ty --{* primitive type, cf. 4.2 *} +datatype_new prim_ty --{* primitive type, cf. 4.2 *} = Void --{* result type of void methods *} | Boolean | Integer -datatype ref_ty --{* reference type, cf. 4.3 *} +datatype_new ref_ty --{* reference type, cf. 4.3 *} = NullT --{* null type, cf. 4.1 *} | IfaceT qtname --{* interface type *} | ClassT qtname --{* class type *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Bali/Value.thy --- a/src/HOL/Bali/Value.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Bali/Value.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ typedecl loc --{* locations, i.e. abstract references on objects *} -datatype val +datatype_new val = Unit --{* dummy result value of void methods *} | Bool bool --{* Boolean value *} | Intg int --{* integer value *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Codegenerator_Test/Code_Test.thy --- a/src/HOL/Codegenerator_Test/Code_Test.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ subsection {* YXML encoding for @{typ Code_Evaluation.term} *} -datatype yxml_of_term = YXML +datatype_new yxml_of_term = YXML lemma yot_anything: "x = (y :: yxml_of_term)" by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp) @@ -58,7 +58,7 @@ sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}. *} -datatype xml_tree = XML_Tree +datatype_new xml_tree = XML_Tree lemma xml_tree_anything: "x = (y :: xml_tree)" by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Tue Sep 09 20:51:36 2014 +0200 @@ -2037,7 +2037,7 @@ subsection "Define syntax and semantics" -datatype floatarith +datatype_new floatarith = Add floatarith floatarith | Minus floatarith | Mult floatarith floatarith @@ -2456,7 +2456,7 @@ show ?case by (cases "n < length vs", auto) qed -datatype form = Bound floatarith floatarith floatarith form +datatype_new form = Bound floatarith floatarith floatarith form | Assign floatarith floatarith form | Less floatarith floatarith | LessEqual floatarith floatarith diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,12 +11,12 @@ text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *} -datatype 'a pol = +datatype_new 'a pol = Pc 'a | Pinj nat "'a pol" | PX "'a pol" nat "'a pol" -datatype 'a polex = +datatype_new 'a polex = Pol "'a pol" | Add "'a polex" "'a polex" | Sub "'a polex" "'a polex" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num | Mul int num primrec num_size :: "num \ nat" -- {* A size for num to make inductive proofs simpler *} @@ -38,7 +38,7 @@ | "Inum bs (Sub a b) = Inum bs a - Inum bs b" | "Inum bs (Mul c a) = c* Inum bs a" -datatype fm = +datatype_new fm = T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm | Closed nat | NClosed nat diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num | Mul int num (* A size for num to make inductive proofs simpler*) @@ -36,7 +36,7 @@ | "Inum bs (Sub a b) = Inum bs a - Inum bs b" | "Inum bs (Mul c a) = (real c) * Inum bs a" (* FORMULAE *) -datatype fm = +datatype_new fm = T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 20:51:36 2014 +0200 @@ -105,7 +105,7 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num | Mul int num | Floor num| CF int num num (* A size for num to make inductive proofs simpler*) @@ -188,7 +188,7 @@ (* FORMULAE *) -datatype fm = +datatype_new fm = T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ subsection {* Terms *} -datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm +datatype_new tm = CP poly | Bound nat | Add tm tm | Mul poly tm | Neg tm | Sub tm tm | CNP nat poly tm (* A size for poly to make inductive proofs simpler*) @@ -493,7 +493,7 @@ subsection{* Formulae *} -datatype fm = T| F| Le tm | Lt tm | Eq tm | NEq tm| +datatype_new fm = T| F| Le tm | Lt tm | Eq tm | NEq tm| NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ subsection{* Datatype of polynomial expressions *} -datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly +datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/Discrete.thy --- a/src/HOL/HOLCF/Discrete.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/Discrete.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Cont begin -datatype 'a discr = Discr "'a :: type" +datatype_new 'a discr = Discr "'a :: type" subsection {* Discrete cpo class instance *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/ABP/Abschannel.thy --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports IOA Action Lemmas begin -datatype 'a abs_action = S 'a | R 'a +datatype_new 'a abs_action = S 'a | R 'a (********************************************************** diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/ABP/Action.thy --- a/src/HOL/HOLCF/IOA/ABP/Action.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Packet begin -datatype 'm action = +datatype_new 'm action = Next | S_msg 'm | R_msg 'm | S_pkt "'m packet" | R_pkt "'m packet" | S_ack bool | R_ack bool diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports IOA Action begin -datatype 'a abs_action = S 'a | R 'a +datatype_new 'a abs_action = S 'a | R 'a definition ch_asig :: "'a abs_action signature" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/NTP/Action.thy --- a/src/HOL/HOLCF/IOA/NTP/Action.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/NTP/Action.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Packet begin -datatype 'm action = S_msg 'm | R_msg 'm +datatype_new 'm action = S_msg 'm | R_msg 'm | S_pkt "'m packet" | R_pkt "'m packet" | S_ack bool | R_ack bool | C_m_s | C_m_r | C_r_s | C_r_r 'm diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/Storage/Action.thy --- a/src/HOL/HOLCF/IOA/Storage/Action.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Main begin -datatype action = New | Loc nat | Free nat +datatype_new action = New | Loc nat | Free nat lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y" by simp diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Abstraction begin -datatype action = INC +datatype_new action = INC definition C_asig :: "action signature" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports IOA Abstraction begin -datatype action = INC +datatype_new action = INC definition C_asig :: "action signature" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/HOLCF/Up.thy --- a/src/HOL/HOLCF/Up.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/HOLCF/Up.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ subsection {* Definition of new type for lifting *} -datatype 'a u = Ibottom | Iup 'a +datatype_new 'a u = Ibottom | Iup 'a type_notation (xsymbols) u ("(_\<^sub>\)" [1000] 999) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Hoare/Heap.thy --- a/src/HOL/Hoare/Heap.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Hoare/Heap.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ subsection "References" -datatype 'a ref = Null | Ref 'a +datatype_new 'a ref = Null | Ref 'a lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)" by (induct x) auto diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Hoare_Parallel/Graph.thy --- a/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 09 20:51:36 2014 +0200 @@ -4,7 +4,7 @@ theory Graph imports Main begin -datatype node = Black | White +datatype_new node = Black | White type_synonym nodes = "node list" type_synonym edge = "nat \ nat" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Hoare_Parallel/OG_Com.thy --- a/src/HOL/Hoare_Parallel/OG_Com.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy Tue Sep 09 20:51:36 2014 +0200 @@ -14,7 +14,7 @@ datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a com"} for non-annotated commands. *} -datatype 'a ann_com = +datatype_new 'a ann_com = AnnBasic "('a assn)" "('a \ 'a)" | AnnSeq "('a ann_com)" "('a ann_com)" | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Hoare_Parallel/RG_Com.thy --- a/src/HOL/Hoare_Parallel/RG_Com.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy Tue Sep 09 20:51:36 2014 +0200 @@ -12,7 +12,7 @@ type_synonym 'a bexp = "'a set" -datatype 'a com = +datatype_new 'a com = Basic "'a \'a" | Seq "'a com" "'a com" | Cond "'a bexp" "'a com" "'a com" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/ACom.thy --- a/src/HOL/IMP/ACom.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/ACom.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Annotated Commands" -datatype 'a acom = +datatype_new 'a acom = SKIP 'a ("SKIP {_}" 61) | Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/AExp.thy --- a/src/HOL/IMP/AExp.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/AExp.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ type_synonym state = "vname \ val" text_raw{*\snip{AExpaexpdef}{2}{1}{% *} -datatype aexp = N int | V vname | Plus aexp aexp +datatype_new aexp = N int | V vname | Plus aexp aexp text_raw{*}%endsnip*} text_raw{*\snip{AExpavaldef}{1}{2}{% *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/ASM.thy --- a/src/HOL/IMP/ASM.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/ASM.thy Tue Sep 09 20:51:36 2014 +0200 @@ -5,7 +5,7 @@ subsection "Stack Machine" text_raw{*\snip{ASMinstrdef}{0}{1}{% *} -datatype instr = LOADI val | LOAD vname | ADD +datatype_new instr = LOADI val | LOAD vname | ADD text_raw{*}%endsnip*} text_raw{*\snip{ASMstackdef}{1}{2}{% *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int1_const.thy --- a/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Constant Propagation" -datatype const = Const val | Any +datatype_new const = Const val | Any fun \_const where "\_const (Const i) = {i}" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int1_parity.thy --- a/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Parity Analysis" -datatype parity = Even | Odd | Either +datatype_new parity = Even | Odd | Either text{* Instantiation of class @{class order} with type @{typ parity}: *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Constant Propagation" -datatype cval = Const val | Any +datatype_new cval = Const val | Any fun rep_cval where "rep_cval (Const n) = {n}" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Interval Analysis" -datatype ivl = I "int option" "int option" +datatype_new ivl = I "int option" "int option" text{* We assume an important invariant: arithmetic operations are never applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j < diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ text{* A concrete type of state with computable @{text"\"}: *} -datatype 'a astate = FunDom "string \ 'a" "string list" +datatype_new 'a astate = FunDom "string \ 'a" "string list" fun "fun" where "fun (FunDom f _) = f" fun dom where "dom (FunDom _ A) = A" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Annotated Commands" -datatype 'a acom = +datatype_new 'a acom = SKIP 'a ("SKIP {_}" 61) | Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Constant Propagation" -datatype const = Const val | Any +datatype_new const = Const val | Any fun \_const where "\_const (Const n) = {n}" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Parity Analysis" -datatype parity = Even | Odd | Either +datatype_new parity = Even | Odd | Either text{* Instantiation of class @{class preord} with type @{typ parity}: *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection "Interval Analysis" -datatype ivl = I "int option" "int option" +datatype_new ivl = I "int option" "int option" definition "\_ivl i = (case i of I (Some l) (Some h) \ {l..h} | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ text{* A concrete type of state with computable @{text"\"}: *} -datatype 'a st = FunDom "vname \ 'a" "vname list" +datatype_new 'a st = FunDom "vname \ 'a" "vname list" fun "fun" where "fun (FunDom f xs) = f" fun dom where "dom (FunDom f xs) = xs" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/BExp.thy --- a/src/HOL/IMP/BExp.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/BExp.thy Tue Sep 09 20:51:36 2014 +0200 @@ -2,7 +2,7 @@ subsection "Boolean Expressions" -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp text_raw{*\snip{BExpbvaldef}{1}{2}{% *} fun bval :: "bexp \ state \ bool" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/C_like.thy --- a/src/HOL/IMP/C_like.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/C_like.thy Tue Sep 09 20:51:36 2014 +0200 @@ -4,14 +4,14 @@ type_synonym state = "nat \ nat" -datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp +datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp fun aval :: "aexp \ state \ nat" where "aval (N n) s = n" | "aval (!a) s = s(aval a s)" | "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp primrec bval :: "bexp \ state \ bool" where "bval (Bc v) _ = v" | @@ -20,7 +20,7 @@ "bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)" -datatype +datatype_new com = SKIP | Assign aexp aexp ("_ ::= _" [61, 61] 61) | New aexp aexp diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Compiler.thy Tue Sep 09 20:51:36 2014 +0200 @@ -43,7 +43,7 @@ subsection "Instructions and Stack Machine" text_raw{*\snip{instrdef}{0}{1}{% *} -datatype instr = +datatype_new instr = LOADI int | LOAD vname | ADD | STORE vname | JMP int | JMPLESS int | JMPGE int text_raw{*}%endsnip*} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/OO.thy --- a/src/HOL/IMP/OO.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/OO.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,13 +8,13 @@ where "f(x,y := z) == f(x := (f x)(y := z))" type_synonym addr = nat -datatype ref = null | Ref addr +datatype_new ref = null | Ref addr type_synonym obj = "string \ ref" type_synonym venv = "string \ ref" type_synonym store = "addr \ obj" -datatype exp = +datatype_new exp = Null | New | V string | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Poly_Types.thy --- a/src/HOL/IMP/Poly_Types.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Poly_Types.thy Tue Sep 09 20:51:36 2014 +0200 @@ -2,7 +2,7 @@ subsection "Type Variables" -datatype ty = Ity | Rty | TV nat +datatype_new ty = Ity | Rty | TV nat text{* Everything else remains the same. *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/Types.thy --- a/src/HOL/IMP/Types.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Types.thy Tue Sep 09 20:51:36 2014 +0200 @@ -7,13 +7,13 @@ subsection "Arithmetic Expressions" -datatype val = Iv int | Rv real +datatype_new val = Iv int | Rv real type_synonym vname = string type_synonym state = "vname \ val" text_raw{*\snip{aexptDef}{0}{2}{% *} -datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp +datatype_new aexp = Ic int | Rc real | V vname | Plus aexp aexp text_raw{*}%endsnip*} inductive taval :: "aexp \ state \ val \ bool" where @@ -32,7 +32,7 @@ subsection "Boolean Expressions" -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp inductive tbval :: "bexp \ state \ bool \ bool" where "tbval (Bc v) s v" | @@ -44,7 +44,7 @@ subsection "Syntax of Commands" (* a copy of Com.thy - keep in sync! *) -datatype +datatype_new com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;; _" [60, 61] 60) @@ -71,7 +71,7 @@ subsection "The Type System" -datatype ty = Ity | Rty +datatype_new ty = Ity | Rty type_synonym tyenv = "vname \ ty" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMP/VCG.thy --- a/src/HOL/IMP/VCG.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/VCG.thy Tue Sep 09 20:51:36 2014 +0200 @@ -7,7 +7,7 @@ text{* Annotated commands: commands where loops are annotated with invariants. *} -datatype acom = +datatype_new acom = Askip ("SKIP") | Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | Aseq acom acom ("_;;/ _" [60, 61] 60) | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMPP/Com.thy --- a/src/HOL/IMPP/Com.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMPP/Com.thy Tue Sep 09 20:51:36 2014 +0200 @@ -18,10 +18,10 @@ Arg :: loc and Res :: loc -datatype vname = Glb glb | Loc loc +datatype_new vname = Glb glb | Loc loc type_synonym globs = "glb => val" type_synonym locals = "loc => val" -datatype state = st globs locals +datatype_new state = st globs locals (* for the meta theory, the following would be sufficient: typedecl state consts st :: "[globs , locals] => state" @@ -31,7 +31,7 @@ typedecl pname -datatype com +datatype_new com = SKIP | Ass vname aexp ("_:==_" [65, 65 ] 60) | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMPP/Hoare.thy Tue Sep 09 20:51:36 2014 +0200 @@ -28,7 +28,7 @@ peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where "peek_and P p = (%Z s. P Z s & p s)" -datatype 'a triple = +datatype_new 'a triple = triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) definition diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Tue Sep 09 20:51:36 2014 +0200 @@ -53,8 +53,8 @@ definition empty :: heap where "empty = \arrays = (\_ _. []), refs = (\_ _. 0), lim = 0\" -datatype 'a array = Array addr -datatype 'a ref = Ref addr -- "note the phantom type 'a " +datatype_new 'a array = Array addr +datatype_new 'a ref = Ref addr -- "note the phantom type 'a " primrec addr_of_array :: "'a array \ addr" where "addr_of_array (Array x) = x" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 20:51:36 2014 +0200 @@ -16,7 +16,7 @@ text {* Monadic heap actions either produce values and transform the heap, or fail *} -datatype 'a Heap = Heap "heap \ ('a \ heap) option" +datatype_new 'a Heap = Heap "heap \ ('a \ heap) option" lemma [code, code del]: "(Code_Evaluation.term_of :: 'a::typerep Heap \ Code_Evaluation.term) = Code_Evaluation.term_of" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ section {* Definition of Linked Lists *} setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \ 'a\type ref"}) *} -datatype 'a node = Empty | Node 'a "('a node) ref" +datatype_new 'a node = Empty | Node 'a "('a node) ref" primrec node_encode :: "'a\countable node \ nat" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Sep 09 20:51:36 2014 +0200 @@ -20,7 +20,7 @@ text {* This resembles exactly to Isat's Proof Steps *} type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list" -datatype ProofStep = +datatype_new ProofStep = ProofDone bool | Root ClauseId Clause | Conflict ClauseId Resolvants diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/ABexp.thy --- a/src/HOL/Induct/ABexp.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/ABexp.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Main begin -datatype 'a aexp = +datatype_new 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/Comb.thy --- a/src/HOL/Induct/Comb.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/Comb.thy Tue Sep 09 20:51:36 2014 +0200 @@ -20,7 +20,7 @@ text {* Datatype definition of combinators @{text S} and @{text K}. *} -datatype comb = K +datatype_new comb = K | S | Ap comb comb (infixl "##" 90) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 20:51:36 2014 +0200 @@ -218,7 +218,7 @@ before! *} -datatype foo = Foo1 nat | Foo2 bar +datatype_new foo = Foo1 nat | Foo2 bar and bar = Bar1 bool | Bar2 bazar and bazar = Bazar foo diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/Ordinals.thy --- a/src/HOL/Induct/Ordinals.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/Ordinals.thy Tue Sep 09 20:51:36 2014 +0200 @@ -14,7 +14,7 @@ @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}). *} -datatype ordinal = +datatype_new ordinal = Zero | Succ ordinal | Limit "nat => ordinal" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/PropLog.thy --- a/src/HOL/Induct/PropLog.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/PropLog.thy Tue Sep 09 20:51:36 2014 +0200 @@ -20,7 +20,7 @@ subsection {* The datatype of propositions *} -datatype 'a pl = +datatype_new 'a pl = false | var 'a ("#_" [1000]) | imp "'a pl" "'a pl" (infixr "->" 90) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/Term.thy --- a/src/HOL/Induct/Term.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/Term.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Main begin -datatype ('a, 'b) "term" = +datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Induct/Tree.thy --- a/src/HOL/Induct/Tree.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Induct/Tree.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ imports Main begin -datatype 'a tree = +datatype_new 'a tree = Atom 'a | Branch "nat => 'a tree" @@ -34,7 +34,7 @@ subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*} -datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" +datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" text{*Addition of ordinals*} primrec add :: "[brouwer,brouwer] => brouwer" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Isar_Examples/Expr_Compiler.thy --- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Sep 09 20:51:36 2014 +0200 @@ -31,7 +31,7 @@ consisting of variables, constants, and binary operations on expressions. *} -datatype ('adr, 'val) expr = +datatype_new ('adr, 'val) expr = Variable 'adr | Constant 'val | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr" @@ -51,7 +51,7 @@ text {* Next we model a simple stack machine, with three instructions. *} -datatype ('adr, 'val) instr = +datatype_new ('adr, 'val) instr = Const 'val | Load 'adr | Apply "'val binop" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Sep 09 20:51:36 2014 +0200 @@ -21,7 +21,7 @@ type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" -datatype 'a com = +datatype_new 'a com = Basic "'a \ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) | Cond "'a bexp" "'a com" "'a com" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Isar_Examples/Nested_Datatype.thy --- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ subsection {* Terms and substitution *} -datatype ('a, 'b) "term" = +datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Lattice/Orders.thy Tue Sep 09 20:51:36 2014 +0200 @@ -46,7 +46,7 @@ of the original one. *} -datatype 'a dual = dual 'a +datatype_new 'a dual = dual 'a primrec undual :: "'a dual \ 'a" where undual_dual: "undual (dual x) = x" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Extended.thy --- a/src/HOL/Library/Extended.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Extended.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ "~~/src/HOL/Library/Simps_Case_Conv" begin -datatype 'a extended = Fin 'a | Pinf ("\") | Minf ("-\") +datatype_new 'a extended = Fin 'a | Pinf ("\") | Minf ("-\") instantiation extended :: (order)order diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Tue Sep 09 20:51:36 2014 +0200 @@ -20,7 +20,7 @@ subsection {* Definition and basic properties *} -datatype ereal = ereal real | PInfty | MInfty +datatype_new ereal = ereal real | PInfty | MInfty instantiation ereal :: uminus begin diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/IArray.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ lists first. Arrays could be converted back into lists for printing if they were wrapped up in an additional constructor. *} -datatype 'a iarray = IArray "'a list" +datatype_new 'a iarray = IArray "'a list" primrec list_of :: "'a iarray \ 'a list" where "list_of (IArray xs) = xs" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Lattice_Constructions.thy --- a/src/HOL/Library/Lattice_Constructions.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Lattice_Constructions.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ subsection {* Values extended by a bottom element *} -datatype 'a bot = Value 'a | Bot +datatype_new 'a bot = Value 'a | Bot instantiation bot :: (preorder) preorder begin @@ -108,7 +108,7 @@ section {* Values extended by a top element *} -datatype 'a top = Value 'a | Top +datatype_new 'a top = Value 'a | Top instantiation top :: (preorder) preorder begin @@ -207,7 +207,7 @@ subsection {* Values extended by a top and a bottom element *} -datatype 'a flat_complete_lattice = Value 'a | Bot | Top +datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top instantiation flat_complete_lattice :: (type) order begin diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Parallel.thy --- a/src/HOL/Library/Parallel.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Parallel.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ subsection {* Futures *} -datatype 'a future = fork "unit \ 'a" +datatype_new 'a future = fork "unit \ 'a" primrec join :: "'a future \ 'a" where "join (fork f) = f ()" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Phantom_Type.thy --- a/src/HOL/Library/Phantom_Type.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Phantom_Type.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Main begin -datatype ('a, 'b) phantom = phantom 'b +datatype_new ('a, 'b) phantom = phantom 'b primrec of_phantom :: "('a, 'b) phantom \ 'b" where "of_phantom (phantom x) = x" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 09 20:51:36 2014 +0200 @@ -16,8 +16,8 @@ subsection {* Datatype of RB trees *} -datatype color = R | B -datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" +datatype_new color = R | B +datatype_new ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" lemma rbt_cases: obtains (Empty) "t = Empty" @@ -1728,7 +1728,7 @@ where "skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \ l | _ \ t')" -datatype compare = LT | GT | EQ +datatype_new compare = LT | GT | EQ partial_function (tailrec) compare_height :: "('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt \ compare" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Metis_Examples/Binary_Tree.thy --- a/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ declare [[metis_new_skolem]] -datatype 'a bt = +datatype_new 'a bt = Lf | Br 'a "'a bt" "'a bt" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Tue Sep 09 20:51:36 2014 +0200 @@ -34,10 +34,10 @@ definition symKeys :: "key set" where "symKeys == {K. invKey K = K}" -datatype --{*We allow any number of friendly agents*} +datatype_new --{*We allow any number of friendly agents*} agent = Server | Friend nat | Spy -datatype +datatype_new msg = Agent agent --{*Agent names*} | Number nat --{*Ordinary integers, timestamps, ...*} | Nonce nat --{*Unguessable nonces*} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Metis_Examples/Trans_Closure.thy --- a/src/HOL/Metis_Examples/Trans_Closure.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ type_synonym addr = nat -datatype val +datatype_new val = Unit -- "dummy result value of void expressions" | Null -- "null reference" | Bool bool -- "Boolean value" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/DFA/Err.thy --- a/src/HOL/MicroJava/DFA/Err.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/DFA/Err.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ imports Semilat begin -datatype 'a err = Err | OK 'a +datatype_new 'a err = Err | OK 'a type_synonym 'a ebinop = "'a \ 'a \ 'a err" type_synonym 'a esl = "'a set * 'a ord * 'a ebinop" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/J/Example.thy --- a/src/HOL/MicroJava/J/Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/J/Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -36,8 +36,8 @@ \end{verbatim} *} -datatype cnam' = Base' | Ext' -datatype vnam' = vee' | x' | e' +datatype_new cnam' = Base' | Ext' +datatype_new vnam' = vee' | x' | e' text {* @{text cnam'} and @{text vnam'} are intended to be isomorphic diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/J/Term.thy --- a/src/HOL/MicroJava/J/Term.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/J/Term.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,9 +6,9 @@ theory Term imports Value begin -datatype binop = Eq | Add -- "function codes for binary operation" +datatype_new binop = Eq | Add -- "function codes for binary operation" -datatype expr +datatype_new expr = NewC cname -- "class instance creation" | Cast cname expr -- "type cast" | Lit val -- "literal value, also references" @@ -21,7 +21,7 @@ | Call cname expr mname "ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" -datatype stmt +datatype_new stmt = Skip -- "empty statement" | Expr expr -- "expression statement" | Comp stmt stmt ("_;; _" [61,60]60) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/J/Type.thy Tue Sep 09 20:51:36 2014 +0200 @@ -45,14 +45,14 @@ end -- "exceptions" -datatype +datatype_new xcpt = NullPointer | ClassCast | OutOfMemory -- "class names" -datatype cname +datatype_new cname = Object | Xcpt xcpt | Cname cnam @@ -128,23 +128,23 @@ end -- "names for @{text This} pointer and local/field variables" -datatype vname +datatype_new vname = This | VName vnam -- "primitive type, cf. 4.2" -datatype prim_ty +datatype_new prim_ty = Void -- "'result type' of void methods" | Boolean | Integer -- "reference type, cf. 4.3" -datatype ref_ty +datatype_new ref_ty = NullT -- "null type, cf. 4.1" | ClassT cname -- "class type" -- "any type, cf. 4.1" -datatype ty +datatype_new ty = PrimT prim_ty -- "primitive type" | RefT ref_ty -- "reference type" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/J/Value.thy --- a/src/HOL/MicroJava/J/Value.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/J/Value.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,11 +8,11 @@ typedecl loc' -- "locations, i.e. abstract references on objects" -datatype loc +datatype_new loc = XcptRef xcpt -- "special locations for pre-allocated system exceptions" | Loc loc' -- "usual locations (references on objects)" -datatype val +datatype_new val = Unit -- "dummy result value of void methods" | Null -- "null reference" | Bool bool -- "Boolean value" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/JVM/JVMDefensive.thy --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ text {* Extend the state space by one element indicating a type error (or other abnormal termination) *} -datatype 'a type_error = TypeError | Normal 'a +datatype_new 'a type_error = TypeError | Normal 'a abbreviation diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/MicroJava/JVM/JVMInstructions.thy --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ theory JVMInstructions imports JVMState begin -datatype +datatype_new instr = Load nat -- "load from local variable" | Store nat -- "store into local variable" | LitPush val -- "push a literal (constant)" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/NanoJava/Decl.thy --- a/src/HOL/NanoJava/Decl.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/NanoJava/Decl.thy Tue Sep 09 20:51:36 2014 +0200 @@ -7,7 +7,7 @@ theory Decl imports Term begin -datatype ty +datatype_new ty = NT --{* null type *} | Class cname --{* class type *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/NanoJava/State.thy --- a/src/HOL/NanoJava/State.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/NanoJava/State.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ text {* Locations, i.e.\ abstract references to objects *} typedecl loc -datatype val +datatype_new val = Null --{* null reference *} | Addr loc --{* address, i.e. location of object *} diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/NanoJava/Term.thy --- a/src/HOL/NanoJava/Term.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/NanoJava/Term.thy Tue Sep 09 20:51:36 2014 +0200 @@ -23,7 +23,7 @@ Res_neq_This [simp]: "Res \ This" *) -datatype stmt +datatype_new stmt = Skip --{* empty statement *} | Comp stmt stmt ("_;; _" [91,90 ] 90) | Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Sep 09 20:51:36 2014 +0200 @@ -44,7 +44,7 @@ nitpick [card = 17, expect = none] oops -datatype ('a, 'b) pd = Pd "'a \ 'b" +datatype_new ('a, 'b) pd = Pd "'a \ 'b" fun fs where "fs (Pd (a, _)) = a" @@ -76,7 +76,7 @@ nitpick [expect = genuine] oops -datatype ('a, 'b) fn = Fn "'a \ 'b" +datatype_new ('a, 'b) fn = Fn "'a \ 'b" fun app where "app (Fn f) x = f x" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 09 20:51:36 2014 +0200 @@ -206,7 +206,7 @@ nitpick [binary_ints, expect = none] sorry -datatype tree = Null | Node nat tree tree +datatype_new tree = Null | Node nat tree tree primrec labels where "labels Null = {}" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 20:51:36 2014 +0200 @@ -223,7 +223,7 @@ subsection {* 2.10. Boxing *} -datatype tm = Var nat | Lam tm | App tm tm +datatype_new tm = Var nat | Lam tm | App tm tm primrec lift where "lift (Var j) k = Var (if j < k then j else j + 1)" | @@ -306,7 +306,7 @@ subsection {* 3.1. A Context-Free Grammar *} -datatype alphabet = a | b +datatype_new alphabet = a | b inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where "[] \ S\<^sub>1" @@ -381,7 +381,7 @@ subsection {* 3.2. AA Trees *} -datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" +datatype_new 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" primrec data where "data \ = undefined" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 20:51:36 2014 +0200 @@ -617,7 +617,7 @@ text {* Non-recursive datatypes *} -datatype T1 = A | B +datatype_new T1 = A | B lemma "P (x\T1)" nitpick [expect = genuine] @@ -653,7 +653,7 @@ nitpick [expect = genuine] oops -datatype 'a T2 = C T1 | D 'a +datatype_new 'a T2 = C T1 | D 'a lemma "P (x\'a T2)" nitpick [expect = genuine] @@ -685,7 +685,7 @@ nitpick [expect = genuine] oops -datatype ('a, 'b) T3 = E "'a \ 'b" +datatype_new ('a, 'b) T3 = E "'a \ 'b" lemma "P (x\('a, 'b) T3)" nitpick [expect = genuine] @@ -790,7 +790,7 @@ nitpick [expect = genuine] oops -datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList +datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList lemma "P (x\BitList)" nitpick [expect = genuine] @@ -823,7 +823,7 @@ nitpick [expect = genuine] oops -datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree" +datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree" lemma "P (x\'a BinTree)" nitpick [expect = genuine] @@ -857,7 +857,7 @@ text {* Mutually recursive datatypes *} -datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" +datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and 'a bexp = Equal "'a aexp" "'a aexp" lemma "P (x\'a aexp)" @@ -880,17 +880,17 @@ nitpick [expect = genuine] oops -lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x" +lemma "rec_aexp number ite equal (Number x) = number x" nitpick [card = 1-3, expect = none] apply simp done -lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)" +lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)" nitpick [card = 1-3, expect = none] apply simp done -lemma "P (rec_aexp_bexp_1 number ite equal x)" +lemma "P (rec_aexp number ite equal x)" nitpick [expect = genuine] oops @@ -898,7 +898,7 @@ nitpick [expect = genuine] oops -lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)" +lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)" nitpick [card = 1-3, expect = none] apply simp done @@ -911,8 +911,7 @@ nitpick [expect = genuine] oops -datatype X = A | B X | C Y - and Y = D X | E Y | F +datatype_new X = A | B X | C Y and Y = D X | E Y | F lemma "P (x\X)" nitpick [expect = genuine] @@ -958,22 +957,22 @@ nitpick [expect = genuine] oops -lemma "rec_X_Y_1 a b c d e f A = a" +lemma "rec_X a b c d e f A = a" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)" +lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)" +lemma "rec_X a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)" +lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X a b c d e f x)" nitpick [card = 1-5, expect = none] apply simp done @@ -988,7 +987,7 @@ apply simp done -lemma "P (rec_X_Y_1 a b c d e f x)" +lemma "P (rec_X a b c d e f x)" nitpick [expect = genuine] oops @@ -1000,7 +999,7 @@ text {* Indirect recursion is implemented via mutual recursion. *} -datatype XOpt = CX "XOpt option" | DX "bool \ XOpt option" +datatype_new XOpt = CX "XOpt option" | DX "bool \ XOpt option" lemma "P (x\XOpt)" nitpick [expect = genuine] @@ -1014,12 +1013,12 @@ nitpick [expect = genuine] oops -lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" +lemma "rec_X cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" nitpick [card = 1-5, expect = none] apply simp done -lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))" +lemma "rec_X cx dx n1 s1 n2 s2 (DX x) = dx x (\b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))" nitpick [card = 1-3, expect = none] apply simp done @@ -1029,7 +1028,7 @@ apply simp done -lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_X cx dx n1 s1 n2 s2 x)" nitpick [card = 1-4, expect = none] apply simp done @@ -1039,12 +1038,12 @@ apply simp done -lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_X cx dx n1 s1 n2 s2 x)" nitpick [card = 1-4, expect = none] apply simp done -lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" +lemma "P (rec_X cx dx n1 s1 n2 s2 x)" nitpick [expect = genuine] oops @@ -1056,7 +1055,7 @@ nitpick [expect = genuine] oops -datatype 'a YOpt = CY "('a \ 'a YOpt) option" +datatype_new 'a YOpt = CY "('a \ 'a YOpt) option" lemma "P (x\'a YOpt)" nitpick [expect = genuine] @@ -1070,30 +1069,7 @@ nitpick [expect = genuine] oops -lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)" -nitpick [card = 1-2, expect = none] -apply simp -done - -lemma "rec_YOpt_2 cy n s None = n" -nitpick [card = 1-2, expect = none] -apply simp -done - -lemma "rec_YOpt_2 cy n s (Some x) = s x (\a. rec_YOpt_1 cy n s (x a))" -nitpick [card = 1-2, expect = none] -apply simp -done - -lemma "P (rec_YOpt_1 cy n s x)" -nitpick [expect = genuine] -oops - -lemma "P (rec_YOpt_2 cy n s x)" -nitpick [expect = genuine] -oops - -datatype Trie = TR "Trie list" +datatype_new Trie = TR "Trie list" lemma "P (x\Trie)" nitpick [expect = genuine] @@ -1107,30 +1083,7 @@ nitpick [expect = genuine] oops -lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "rec_Trie_2 tr nil cons [] = nil" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)" -nitpick [card = 1-4, expect = none] -apply simp -done - -lemma "P (rec_Trie_1 tr nil cons x)" -nitpick [card = 1, expect = genuine] -oops - -lemma "P (rec_Trie_2 tr nil cons x)" -nitpick [card = 1, expect = genuine] -oops - -datatype InfTree = Leaf | Node "nat \ InfTree" +datatype_new InfTree = Leaf | Node "nat \ InfTree" lemma "P (x\InfTree)" nitpick [expect = genuine] @@ -1158,7 +1111,7 @@ nitpick [expect = genuine] oops -datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \ 'a lambda" +datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \ 'a lambda" lemma "P (x\'a lambda)" nitpick [expect = genuine] @@ -1194,8 +1147,8 @@ text {* Taken from "Inductive datatypes in HOL", p. 8: *} -datatype ('a, 'b) T = C "'a \ bool" | D "'b list" -datatype 'c U = E "('c, 'c U) T" +datatype_new ('a, 'b) T = C "'a \ bool" | D "'b list" +datatype_new 'c U = E "('c, 'c U) T" lemma "P (x\'c U)" nitpick [expect = genuine] @@ -1209,43 +1162,6 @@ nitpick [expect = genuine] oops -lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "rec_U_2 e c d nil cons (C x) = c x" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "rec_U_3 e c d nil cons [] = nil" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)" -nitpick [card = 1-3, expect = none] -apply simp -done - -lemma "P (rec_U_1 e c d nil cons x)" -nitpick [expect = genuine] -oops - -lemma "P (rec_U_2 e c d nil cons x)" -nitpick [card = 1, expect = genuine] -oops - -lemma "P (rec_U_3 e c d nil cons x)" -nitpick [card = 1, expect = genuine] -oops - subsubsection {* Records *} record ('a, 'b) point = diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nominal/Examples/CK_Machine.thy --- a/src/HOL/Nominal/Examples/CK_Machine.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Tue Sep 09 20:51:36 2014 +0200 @@ -81,7 +81,7 @@ section {* Evaluation Contexts *} -datatype ctx = +datatype_new ctx = Hole ("\") | CAPPL "ctx" "lam" | CAPPR "lam" "ctx" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Nominal/Examples/Pattern.thy --- a/src/HOL/Nominal/Examples/Pattern.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Nominal/Examples/Pattern.thy Tue Sep 09 20:51:36 2014 +0200 @@ -38,7 +38,7 @@ where "\x:T. t \ Abs T x t" -datatype pat = +datatype_new pat = PVar name ty | PTuple pat pat ("(1'\\_,/ _'\\)") diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -107,7 +107,7 @@ hide_const Pow -datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr +datatype_new expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr | Minus expr expr | Uminus expr | Pow expr int | Exp expr text {* @@ -197,7 +197,7 @@ section {* Example negation *} -datatype abc = A | B | C +datatype_new abc = A | B | C inductive notB :: "abc => bool" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -24,7 +24,7 @@ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} -datatype alphabet = a | b +datatype_new alphabet = a | b inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where "[] \ S\<^sub>1" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,11 +10,11 @@ text {* a contribution by Aditi Barthwal *} -datatype ('nts,'ts) symbol = NTS 'nts +datatype_new ('nts,'ts) symbol = NTS 'nts | TS 'ts -datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" +datatype_new ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts" @@ -75,7 +75,7 @@ subsection {* Some concrete Context Free Grammars *} -datatype alphabet = a | b +datatype_new alphabet = a | b inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where "[] \ S\<^sub>1" @@ -140,7 +140,7 @@ type_synonym var = nat type_synonym state = "int list" -datatype com = +datatype_new com = Skip | Ass var "state => int" | Seq com com | @@ -164,11 +164,11 @@ subsection {* Lambda *} -datatype type = +datatype_new type = Atom nat | Fun type type (infixr "\" 200) -datatype dB = +datatype_new dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB @@ -237,12 +237,12 @@ type_synonym vvalue = int type_synonym var_assign = "vname \ vvalue" --"variable assignment" -datatype ir_expr = +datatype_new ir_expr = IrConst vvalue | ObjAddr vname | Add ir_expr ir_expr -datatype val = +datatype_new val = IntVal vvalue record configuration = @@ -267,14 +267,14 @@ type_synonym name = nat --"For simplicity in examples" type_synonym state' = "name \ nat" -datatype aexp = N nat | V name | Plus aexp aexp +datatype_new aexp = N nat | V name | Plus aexp aexp fun aval :: "aexp \ state' \ nat" where "aval (N n) _ = n" | "aval (V x) st = st x" | "aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st" -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp +datatype_new bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp primrec bval :: "bexp \ state' \ bool" where "bval (B b) _ = b" | @@ -282,7 +282,7 @@ "bval (And b1 b2) st = (bval b1 st \ bval b2 st)" | "bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)" -datatype +datatype_new com' = SKIP | Assign name aexp ("_ ::= _" [1000, 61] 61) | Semi com' com' ("_; _" [60, 61] 60) @@ -326,7 +326,7 @@ text{* This example formalizes finite CCS processes without communication or recursion. For simplicity, labels are natural numbers. *} -datatype proc = nil | pre nat proc | or proc proc | par proc proc +datatype_new proc = nil | pre nat proc | or proc proc | par proc proc inductive step :: "proc \ nat \ proc \ bool" where "step (pre n p) n p" | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -2,13 +2,13 @@ imports Main begin -datatype guest = Guest0 | Guest1 -datatype key = Key0 | Key1 | Key2 | Key3 -datatype room = Room0 +datatype_new guest = Guest0 | Guest1 +datatype_new key = Key0 | Key1 | Key2 | Key3 +datatype_new room = Room0 type_synonym card = "key * key" -datatype event = +datatype_new event = Check_in guest room card | Enter guest room card | Exit guest room definition initk :: "room \ key" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/IMP_1.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ type_synonym var = unit type_synonym state = bool -datatype com = +datatype_new com = Skip | Ass bool | Seq com com | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/IMP_2.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ type_synonym var = unit type_synonym state = bool -datatype com = +datatype_new com = Skip | Ass bool | Seq com com | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/IMP_3.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ type_synonym var = unit type_synonym state = int -datatype com = +datatype_new com = Skip | Ass var "int" | Seq com com | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/IMP_4.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ type_synonym var = nat type_synonym state = "int list" -datatype com = +datatype_new com = Skip | Ass var "int" | Seq com com | diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -4,11 +4,11 @@ subsection {* Lambda *} -datatype type = +datatype_new type = Atom nat | Fun type type (infixr "\" 200) -datatype dB = +datatype_new dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -53,7 +53,7 @@ section {* Context Free Grammar *} -datatype alphabet = a | b +datatype_new alphabet = a | b inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where "[] \ S\<^sub>1" @@ -179,7 +179,7 @@ type_synonym var = nat type_synonym state = "int list" -datatype com = +datatype_new com = Skip | Ass var "int" | Seq com com | @@ -206,11 +206,11 @@ subsection {* Lambda *} -datatype type = +datatype_new type = Atom nat | Fun type type (infixr "\" 200) -datatype dB = +datatype_new dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Sep 09 20:51:36 2014 +0200 @@ -139,7 +139,7 @@ subsection {* Alternative Rules *} -datatype char = C | D | E | F | G | H +datatype_new char = C | D | E | F | G | H inductive is_C_or_D where @@ -784,7 +784,7 @@ type_synonym var = nat type_synonym state = "int list" -datatype com = +datatype_new com = Skip | Ass var "state => int" | Seq com com | @@ -809,7 +809,7 @@ text{* This example formalizes finite CCS processes without communication or recursion. For simplicity, labels are natural numbers. *} -datatype proc = nil | pre nat proc | or proc proc | par proc proc +datatype_new proc = nil | pre nat proc | or proc proc | par proc proc inductive tupled_step :: "(proc \ nat \ proc) \ bool" where @@ -974,7 +974,7 @@ *) subsection {* AVL Tree *} -datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat +datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat fun height :: "'a tree => nat" where "height ET = 0" | "height (MKT x l r h) = max (height l) (height r) + 1" @@ -1403,7 +1403,7 @@ thm is_error'.equation -datatype ErrorObject = Error String.literal int +datatype_new ErrorObject = Error String.literal int inductive is_error'' :: "ErrorObject \ bool" where @@ -1508,7 +1508,7 @@ text {* The higher-order predicate r is in an output term *} -datatype result = Result bool +datatype_new result = Result bool inductive fixed_relation :: "'a => bool" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ manually slightly adapted. *} -datatype Nat = Zer +datatype_new Nat = Zer | Suc Nat fun sub :: "Nat \ Nat \ Nat" @@ -20,10 +20,10 @@ Zer \ Zer | Suc x' \ sub x' y')" -datatype Sym = N0 +datatype_new Sym = N0 | N1 Sym -datatype RE = Sym Sym +datatype_new RE = Sym Sym | Or RE RE | Seq RE RE | And RE RE diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -107,13 +107,13 @@ "unique [] = True" | "unique (x # xs) = (xs\fst x\\<^sub>? = \ \ unique xs)" -datatype type = +datatype_new type = TVar nat | Top | Fun type type (infixr "\" 200) | TyAll type type ("(3\<:_./ _)" [0, 10] 10) -datatype binding = VarB type | TVarB type +datatype_new binding = VarB type | TVarB type type_synonym env = "binding list" primrec is_TVarB :: "binding \ bool" @@ -131,7 +131,7 @@ "mapB f (VarB T) = VarB (f T)" | "mapB f (TVarB T) = TVarB (f T)" -datatype trm = +datatype_new trm = Var nat | Abs type trm ("(3\:_./ _)" [0, 10] 10) | TAbs type trm ("(3\<:_./ _)" [0, 10] 10) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Sep 09 20:51:36 2014 +0200 @@ -2,7 +2,7 @@ imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" begin -datatype agent = Alice | Bob | Spy +datatype_new agent = Alice | Bob | Spy definition agents :: "agent set" where @@ -12,14 +12,14 @@ where "bad = {Spy}" -datatype key = pubEK agent | priEK agent +datatype_new key = pubEK agent | priEK agent fun invKey where "invKey (pubEK A) = priEK A" | "invKey (priEK A) = pubEK A" -datatype +datatype_new msg = Agent agent | Key key | Nonce nat @@ -73,7 +73,7 @@ | initState_Spy: "initState Spy = (Key ` priEK ` bad) \ (Key ` pubEK ` agents)" -datatype +datatype_new event = Says agent agent msg | Gets agent msg | Notes agent msg diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 09 20:51:36 2014 +0200 @@ -18,7 +18,7 @@ subsection {* The Binary Tree *} -datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip +datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip text {* The boolean flag in the node marks the content of the node as diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/TLA/Inc/Inc.thy --- a/src/HOL/TLA/Inc/Inc.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/TLA/Inc/Inc.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ begin (* program counter as an enumeration type *) -datatype pcount = a | b | g +datatype_new pcount = a | b | g axiomatization (* program variables *) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/TLA/Memory/MemClerkParameters.thy --- a/src/HOL/TLA/Memory/MemClerkParameters.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports RPCParameters begin -datatype mClkState = clkA | clkB +datatype_new mClkState = clkA | clkB (* types sent on the clerk's send and receive channels are argument types of the memory and the RPC, respectively *) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Memory RPC MemClerk begin -datatype histState = histA | histB +datatype_new histState = histA | histB type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/TLA/Memory/MemoryParameters.thy --- a/src/HOL/TLA/Memory/MemoryParameters.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ begin (* the memory operations *) -datatype memOp = read Locs | "write" Locs Vals +datatype_new memOp = read Locs | "write" Locs Vals consts (* memory locations and contents *) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/TLA/Memory/RPCParameters.thy --- a/src/HOL/TLA/Memory/RPCParameters.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/TLA/Memory/RPCParameters.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,8 +13,8 @@ memory implementation. *) -datatype rpcOp = memcall memOp | othercall Vals -datatype rpcState = rpcA | rpcB +datatype_new rpcOp = memcall memOp | othercall Vals +datatype_new rpcState = rpcA | rpcB consts (* some particular return values *) diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/UNITY/Comp/Counter.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ theory Counter imports "../UNITY_Main" begin (* Variables are names *) -datatype name = C | c nat +datatype_new name = C | c nat type_synonym state = "name=>int" primrec sum :: "[nat,state]=>int" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/UNITY/Simple/Network.thy --- a/src/HOL/UNITY/Simple/Network.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/UNITY/Simple/Network.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,9 +11,9 @@ (*The state assigns a number to each process variable*) -datatype pvar = Sent | Rcvd | Idle +datatype_new pvar = Sent | Rcvd | Idle -datatype pname = Aproc | Bproc +datatype_new pname = Aproc | Bproc type_synonym state = "pname * pvar => nat" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/UNITY/Simple/Token.thy --- a/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ subsection{*Definitions*} -datatype pstate = Hungry | Eating | Thinking +datatype_new pstate = Hungry | Eating | Thinking --{*process states*} record state = diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Unix/Nested_Environment.thy --- a/src/HOL/Unix/Nested_Environment.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Unix/Nested_Environment.thy Tue Sep 09 20:51:36 2014 +0200 @@ -19,7 +19,7 @@ position within the structure. *} -datatype ('a, 'b, 'c) env = +datatype_new ('a, 'b, 'c) env = Val 'a | Env 'b "'c \ ('a, 'b, 'c) env option" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Unix/Unix.thy Tue Sep 09 20:51:36 2014 +0200 @@ -73,7 +73,7 @@ \cite{Naraschewski:2001}.} *} -datatype perm = +datatype_new perm = Readable | Writable | Executable -- "(ignored)" @@ -284,7 +284,7 @@ @{text "root \x\ root'"} for the operational semantics. *} -datatype operation = +datatype_new operation = Read uid string path | Write uid string path | Chmod uid perms path diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Adhoc_Overloading_Examples.thy --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -19,7 +19,7 @@ subsection {* Plain Ad Hoc Overloading *} text {*Consider the type of first-order terms.*} -datatype ('a, 'b) "term" = +datatype_new ('a, 'b) "term" = Var 'b | Fun 'a "('a, 'b) term list" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/BT.thy --- a/src/HOL/ex/BT.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/BT.thy Tue Sep 09 20:51:36 2014 +0200 @@ -9,7 +9,7 @@ theory BT imports Main begin -datatype 'a bt = +datatype_new 'a bt = Lf | Br 'a "'a bt" "'a bt" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Chinese.thy --- a/src/HOL/ex/Chinese.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Chinese.thy Tue Sep 09 20:51:36 2014 +0200 @@ -16,7 +16,7 @@ *} -datatype shuzi = +datatype_new shuzi = One ("一") | Two ("二") | Three ("三") diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Eval_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -42,7 +42,7 @@ text {* a fancy datatype *} -datatype ('a, 'b) foo = +datatype_new ('a, 'b) foo = Foo "'a\order" 'b | Bla "('a, 'b) bar" | Dummy nat diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Fundefs.thy Tue Sep 09 20:51:36 2014 +0200 @@ -372,7 +372,7 @@ (* Simple Higher-Order Recursion *) -datatype 'a tree = +datatype_new 'a tree = Leaf 'a | Branch "'a tree list" @@ -423,7 +423,7 @@ (* Many equations (quadratic blowup) *) -datatype DT = +datatype_new DT = A | B | C | D | E | F | G | H | I | J | K | L | M | N | P | Q | R | S | T | U | V diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Hebrew.thy --- a/src/HOL/ex/Hebrew.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Hebrew.thy Tue Sep 09 20:51:36 2014 +0200 @@ -12,7 +12,7 @@ text {* The Hebrew Alef-Bet (א-ב). *} -datatype alef_bet = +datatype_new alef_bet = Alef ("א") | Bet ("ב") | Gimel ("ג") diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Normalization_by_Evaluation.thy --- a/src/HOL/ex/Normalization_by_Evaluation.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization lemma "~((0::nat) < (0::nat))" by normalization -datatype n = Z | S n +datatype_new n = Z | S n primrec add :: "n \ n \ n" where "add Z = id" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Records.thy Tue Sep 09 20:51:36 2014 +0200 @@ -166,7 +166,7 @@ subsection {* Coloured points: record extension *} -datatype colour = Red | Green | Blue +datatype_new colour = Red | Green | Blue record cpoint = point + colour :: colour diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Reflection_Examples.thy --- a/src/HOL/ex/Reflection_Examples.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Reflection_Examples.thy Tue Sep 09 20:51:36 2014 +0200 @@ -46,7 +46,7 @@ text {* Example 1 : Propositional formulae and NNF. *} text {* The type @{text fm} represents simple propositional formulae: *} -datatype form = TrueF | FalseF | Less nat nat +datatype_new form = TrueF | FalseF | Less nat nat | And form form | Or form form | Neg form | ExQ form primrec interp :: "form \ ('a::ord) list \ bool" @@ -66,7 +66,7 @@ apply reify oops -datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat +datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat primrec Ifm :: "fm \ bool list \ bool" where @@ -135,7 +135,7 @@ text {* Example 2: Simple arithmetic formulae *} text {* The type @{text num} reflects linear expressions over natural number *} -datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num +datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num text {* This is just technical to make recursive definitions easier. *} primrec num_size :: "num \ nat" @@ -252,7 +252,7 @@ text {* Let's lift this to formulae and see what happens *} -datatype aform = Lt num num | Eq num num | Ge num num | NEq num num | +datatype_new aform = Lt num num | Eq num num | Ge num num | NEq num num | Conj aform aform | Disj aform aform | NEG aform | T | F primrec linaformsize:: "aform \ nat" @@ -331,7 +331,7 @@ one envornement of different types and show that automatic reification also deals with bindings *} -datatype rb = BC bool | BAnd rb rb | BOr rb rb +datatype_new rb = BC bool | BAnd rb rb | BOr rb rb primrec Irb :: "rb \ bool" where @@ -343,7 +343,7 @@ apply (reify Irb.simps) oops -datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint +datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint primrec Irint :: "rint \ int list \ int" @@ -370,7 +370,7 @@ apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)")) oops -datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist +datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist primrec Irlist :: "rlist \ int list \ int list list \ int list" where @@ -387,7 +387,7 @@ apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs")) oops -datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat +datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist primrec Irnat :: "rnat \ int list \ int list list \ nat list \ nat" @@ -418,7 +418,7 @@ ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)")) oops -datatype rifm = RT | RF | RVar nat +datatype_new rifm = RT | RF | RVar nat | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm @@ -451,7 +451,7 @@ text {* An example for equations containing type variables *} -datatype prod = Zero | One | Var nat | Mul prod prod +datatype_new prod = Zero | One | Var nat | Mul prod prod | Pw prod nat | PNM nat nat prod primrec Iprod :: " prod \ ('a::linordered_idom) list \'a" @@ -463,7 +463,7 @@ | "Iprod (Pw a n) vs = Iprod a vs ^ n" | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs" -datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F +datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F | Or sgn sgn | And sgn sgn primrec Isgn :: "sgn \ ('a::linordered_idom) list \ bool" diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Seq.thy --- a/src/HOL/ex/Seq.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Seq.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ imports Main begin -datatype 'a seq = Empty | Seq 'a "'a seq" +datatype_new 'a seq = Empty | Seq 'a "'a seq" fun conc :: "'a seq \ 'a seq \ 'a seq" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Serbian.thy --- a/src/HOL/ex/Serbian.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Serbian.thy Tue Sep 09 20:51:36 2014 +0200 @@ -11,7 +11,7 @@ begin text{* Serbian cyrillic letters *} -datatype azbuka = +datatype_new azbuka = azbA ("А") | azbB ("Б") | azbV ("В") @@ -47,7 +47,7 @@ thm azbuka.induct text{* Serbian latin letters *} -datatype abeceda = +datatype_new abeceda = abcA ("A") | abcB ("B") | abcC ("C") diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Termination.thy --- a/src/HOL/ex/Termination.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Termination.thy Tue Sep 09 20:51:36 2014 +0200 @@ -118,7 +118,7 @@ subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *} -datatype tree = Node | Branch tree tree +datatype_new tree = Node | Branch tree tree fun g_tree :: "tree * tree \ tree" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Transitive_Closure_Table_Ex.thy --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Tue Sep 09 20:51:36 2014 +0200 @@ -6,7 +6,7 @@ imports "~~/src/HOL/Library/Transitive_Closure_Table" begin -datatype ty = A | B | C +datatype_new ty = A | B | C inductive test :: "ty \ ty \ bool" where diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Tree23.thy --- a/src/HOL/ex/Tree23.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Tree23.thy Tue Sep 09 20:51:36 2014 +0200 @@ -21,16 +21,16 @@ type_synonym key = int -- {*for simplicity, should be a type class*} -datatype ord = LESS | EQUAL | GREATER +datatype_new ord = LESS | EQUAL | GREATER definition "ord i j = (if i" 60)