# HG changeset patch # User blanchet # Date 1367219449 -7200 # Node ID be6e703908f4c6d8c62415cb6a83d7662814e05e # Parent 71260347b7e4c123dd6e3e928b287288be8217f4 renamed BNF "(co)data" commands to names that are closer to their final names diff -r 71260347b7e4 -r be6e703908f4 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Apr 29 06:13:36 2013 +0200 +++ b/etc/isar-keywords.el Mon Apr 29 09:10:49 2013 +0200 @@ -46,7 +46,7 @@ "class_deps" "classes" "classrel" - "codata" + "codatatype" "code_abort" "code_class" "code_const" @@ -68,8 +68,8 @@ "context" "corollary" "cpodef" - "data" "datatype" + "datatype_new" "declaration" "declare" "def" @@ -482,7 +482,7 @@ "class" "classes" "classrel" - "codata" + "codatatype" "code_abort" "code_class" "code_const" @@ -498,8 +498,8 @@ "coinductive_set" "consts" "context" - "data" "datatype" + "datatype_new" "declaration" "declare" "default_sort" diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Mon Apr 29 09:10:49 2013 +0200 @@ -10,7 +10,7 @@ theory BNF_GFP imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Sublist" keywords - "codata" :: thy_decl + "codatatype" :: thy_decl begin lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Mon Apr 29 09:10:49 2013 +0200 @@ -10,7 +10,7 @@ theory BNF_LFP imports BNF_FP keywords - "data" :: thy_decl + "datatype_new" :: thy_decl begin lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy --- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Mon Apr 29 09:10:49 2013 +0200 @@ -16,7 +16,7 @@ typedecl N typedecl T -codata dtree = NNode (root: N) (ccont: "(T + dtree) fset") +codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Lambda_Term.thy --- a/src/HOL/BNF/Examples/Lambda_Term.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Lambda_Term.thy Mon Apr 29 09:10:49 2013 +0200 @@ -15,7 +15,7 @@ section {* Datatype definition *} -data 'a trm = +datatype_new 'a trm = Var 'a | App "'a trm" "'a trm" | Lam 'a "'a trm" | diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/ListF.thy --- a/src/HOL/BNF/Examples/ListF.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/ListF.thy Mon Apr 29 09:10:49 2013 +0200 @@ -12,7 +12,7 @@ imports "../BNF" begin -data (rep_compat) 'a listF = NilF | Conss 'a "'a listF" +datatype_new (rep_compat) 'a listF = NilF | Conss 'a "'a listF" lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Misc_Codata.thy --- a/src/HOL/BNF/Examples/Misc_Codata.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Codata.thy Mon Apr 29 09:10:49 2013 +0200 @@ -12,24 +12,24 @@ imports "../BNF" begin -codata simple = X1 | X2 | X3 | X4 +codatatype simple = X1 | X2 | X3 | X4 -codata simple' = X1' unit | X2' unit | X3' unit | X4' unit +codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit -codata 'a stream = Stream 'a "'a stream" +codatatype 'a stream = Stream 'a "'a stream" -codata 'a mylist = MyNil | MyCons 'a "'a mylist" +codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" -codata ('b, 'c, 'd, 'e) some_passive = +codatatype ('b, 'c, 'd, 'e) some_passive = SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e -codata lambda = +codatatype lambda = Var string | App lambda lambda | Abs string lambda | Let "(string \ lambda) fset" lambda -codata 'a par_lambda = +codatatype 'a par_lambda = PVar 'a | PApp "'a par_lambda" "'a par_lambda" | PAbs 'a "'a par_lambda" | @@ -40,75 +40,75 @@ ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -codata 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" - and 'a J2 = J21 | J22 "'a J1" "'a J2" +codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" +and 'a J2 = J21 | J22 "'a J1" "'a J2" -codata 'a tree = TEmpty | TNode 'a "'a forest" - and 'a forest = FNil | FCons "'a tree" "'a forest" +codatatype 'a tree = TEmpty | TNode 'a "'a forest" +and 'a forest = FNil | FCons "'a tree" "'a forest" -codata 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" - and 'a branch = Branch 'a "'a tree'" +codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" +and 'a branch = Branch 'a "'a tree'" -codata ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" - and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" - and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" +codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" +and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" +and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" -codata ('a, 'b, 'c) some_killing = +codatatype ('a, 'b, 'c) some_killing = SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" - and ('a, 'b, 'c) in_here = +and ('a, 'b, 'c) in_here = IH1 'b 'a | IH2 'c -codata ('a, 'b, 'c) some_killing' = +codatatype ('a, 'b, 'c) some_killing' = SK' "'a \ 'b \ ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'" - and ('a, 'b, 'c) in_here' = +and ('a, 'b, 'c) in_here' = IH1' 'b | IH2' 'c -codata ('a, 'b, 'c) some_killing'' = +codatatype ('a, 'b, 'c) some_killing'' = SK'' "'a \ ('a, 'b, 'c) in_here''" - and ('a, 'b, 'c) in_here'' = +and ('a, 'b, 'c) in_here'' = IH1'' 'b 'a | IH2'' 'c -codata ('b, 'c) less_killing = LK "'b \ 'c" +codatatype ('b, 'c) less_killing = LK "'b \ 'c" -codata 'b cps = CPS1 'b | CPS2 "'b \ 'b cps" +codatatype 'b cps = CPS1 'b | CPS2 "'b \ 'b cps" -codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = +codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = FR "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs" -codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, +codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, 'b18, 'b19, 'b20) fun_rhs' = FR' "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ 'b11 \ 'b12 \ 'b13 \ 'b14 \ 'b15 \ 'b16 \ 'b17 \ 'b18 \ 'b19 \ 'b20 \ ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, 'b18, 'b19, 'b20) fun_rhs'" -codata ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" - and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" - and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" +codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" +and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" +and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" -codata ('c, 'e, 'g) coind_wit1 = +codatatype ('c, 'e, 'g) coind_wit1 = CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2" - and ('c, 'e, 'g) coind_wit2 = +and ('c, 'e, 'g) coind_wit2 = CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g - and ('c, 'e, 'g) ind_wit = +and ('c, 'e, 'g) ind_wit = IW1 | IW2 'c -codata ('b, 'a) bar = BAR "'a \ 'b" -codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" +codatatype ('b, 'a) bar = BAR "'a \ 'b" +codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" -codata 'a dead_foo = A -codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" +codatatype 'a dead_foo = A +codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" (* SLOW, MEMORY-HUNGRY -codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" - and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" - and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" - and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" - and ('a, 'c) D5 = A5 "('a, 'c) D6" - and ('a, 'c) D6 = A6 "('a, 'c) D7" - and ('a, 'c) D7 = A7 "('a, 'c) D8" - and ('a, 'c) D8 = A8 "('a, 'c) D1 list" +codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" +and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" +and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" +and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" +and ('a, 'c) D5 = A5 "('a, 'c) D6" +and ('a, 'c) D6 = A6 "('a, 'c) D7" +and ('a, 'c) D7 = A7 "('a, 'c) D8" +and ('a, 'c) D8 = A8 "('a, 'c) D1 list" *) end diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Misc_Data.thy --- a/src/HOL/BNF/Examples/Misc_Data.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Data.thy Mon Apr 29 09:10:49 2013 +0200 @@ -13,24 +13,24 @@ imports "../BNF" begin -data simple = X1 | X2 | X3 | X4 +datatype_new simple = X1 | X2 | X3 | X4 -data simple' = X1' unit | X2' unit | X3' unit | X4' unit +datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit -data 'a mylist = MyNil | MyCons 'a "'a mylist" +datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist" -data ('b, 'c, 'd, 'e) some_passive = +datatype_new ('b, 'c, 'd, 'e) some_passive = SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e -data hfset = HFset "hfset fset" +datatype_new hfset = HFset "hfset fset" -data lambda = +datatype_new lambda = Var string | App lambda lambda | Abs string lambda | Let "(string \ lambda) fset" lambda -data 'a par_lambda = +datatype_new 'a par_lambda = PVar 'a | PApp "'a par_lambda" "'a par_lambda" | PAbs 'a "'a par_lambda" | @@ -41,73 +41,73 @@ ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -data 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" - and 'a I2 = I21 | I22 "'a I1" "'a I2" +datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" +and 'a I2 = I21 | I22 "'a I1" "'a I2" -data 'a tree = TEmpty | TNode 'a "'a forest" - and 'a forest = FNil | FCons "'a tree" "'a forest" +datatype_new 'a tree = TEmpty | TNode 'a "'a forest" +and 'a forest = FNil | FCons "'a tree" "'a forest" -data 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" - and 'a branch = Branch 'a "'a tree'" +datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" +and 'a branch = Branch 'a "'a tree'" -data ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" - and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" - and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" +datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" +and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" +and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" -data ('a, 'b, 'c) some_killing = +datatype_new ('a, 'b, 'c) some_killing = SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" - and ('a, 'b, 'c) in_here = +and ('a, 'b, 'c) in_here = IH1 'b 'a | IH2 'c -data 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b -data 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" -data 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" -data 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ 'b) fset) list" +datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b +datatype_new 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" +datatype_new 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" +datatype_new 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ 'b) fset) list" (* -data 'b fail = F "'b fail" 'b "'b fail" "'b list" -data 'b fail = F "'b fail" 'b "'b fail" 'b -data 'b fail = F1 "'b fail" 'b | F2 "'b fail" -data 'b fail = F "'b fail" 'b +datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list" +datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b +datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail" +datatype_new 'b fail = F "'b fail" 'b *) -data l1 = L1 "l2 list" - and l2 = L21 "l1 fset" | L22 l2 +datatype_new l1 = L1 "l2 list" +and l2 = L21 "l1 fset" | L22 l2 -data kk1 = KK1 kk2 - and kk2 = KK2 kk3 - and kk3 = KK3 "kk1 list" +datatype_new kk1 = KK1 kk2 +and kk2 = KK2 kk3 +and kk3 = KK3 "kk1 list" -data t1 = T11 t3 | T12 t2 - and t2 = T2 t1 - and t3 = T3 +datatype_new t1 = T11 t3 | T12 t2 +and t2 = T2 t1 +and t3 = T3 -data t1' = T11' t2' | T12' t3' - and t2' = T2' t1' - and t3' = T3' +datatype_new t1' = T11' t2' | T12' t3' +and t2' = T2' t1' +and t3' = T3' (* -data fail1 = F1 fail2 - and fail2 = F2 fail3 - and fail3 = F3 fail1 +datatype_new fail1 = F1 fail2 +and fail2 = F2 fail3 +and fail3 = F3 fail1 -data fail1 = F1 "fail2 list" fail2 - and fail2 = F2 "fail2 fset" fail3 - and fail3 = F3 fail1 +datatype_new fail1 = F1 "fail2 list" fail2 +and fail2 = F2 "fail2 fset" fail3 +and fail3 = F3 fail1 -data fail1 = F1 "fail2 list" fail2 - and fail2 = F2 "fail1 fset" fail1 +datatype_new fail1 = F1 "fail2 list" fail2 +and fail2 = F2 "fail1 fset" fail1 *) (* SLOW -data ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" - and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" - and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" - and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" - and ('a, 'c) D5 = A5 "('a, 'c) D6" - and ('a, 'c) D6 = A6 "('a, 'c) D7" - and ('a, 'c) D7 = A7 "('a, 'c) D8" - and ('a, 'c) D8 = A8 "('a, 'c) D1 list" +datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" +and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" +and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" +and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" +and ('a, 'c) D5 = A5 "('a, 'c) D6" +and ('a, 'c) D6 = A6 "('a, 'c) D7" +and ('a, 'c) D7 = A7 "('a, 'c) D8" +and ('a, 'c) D8 = A8 "('a, 'c) D1 list" (*time comparison*) datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list" @@ -121,58 +121,58 @@ *) (* fail: -data tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 - and tt2 = TT2 - and tt3 = TT3 tt4 - and tt4 = TT4 tt1 +datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 +and tt2 = TT2 +and tt3 = TT3 tt4 +and tt4 = TT4 tt1 *) -data k1 = K11 k2 k3 | K12 k2 k4 - and k2 = K2 - and k3 = K3 k4 - and k4 = K4 +datatype_new k1 = K11 k2 k3 | K12 k2 k4 +and k2 = K2 +and k3 = K3 k4 +and k4 = K4 -data tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 - and tt2 = TT2 - and tt3 = TT3 tt1 - and tt4 = TT4 +datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 +and tt2 = TT2 +and tt3 = TT3 tt1 +and tt4 = TT4 (* SLOW -data s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 - and s2 = S21 s7 s5 | S22 s5 s4 s6 - and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 - and s4 = S4 s5 - and s5 = S5 - and s6 = S61 s6 | S62 s1 s2 | S63 s6 - and s7 = S71 s8 | S72 s5 - and s8 = S8 nat +datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 +and s2 = S21 s7 s5 | S22 s5 s4 s6 +and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 +and s4 = S4 s5 +and s5 = S5 +and s6 = S61 s6 | S62 s1 s2 | S63 s6 +and s7 = S71 s8 | S72 s5 +and s8 = S8 nat *) -data ('a, 'b) bar = Bar "'b \ 'a" -data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" +datatype_new ('a, 'b) bar = Bar "'b \ 'a" +datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" -data 'a dead_foo = A -data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" +datatype_new 'a dead_foo = A +datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" -data d1 = D -data d1' = is_D: D +datatype_new d1 = D +datatype_new d1' = is_D: D -data d2 = D nat -data d2' = is_D: D nat +datatype_new d2 = D nat +datatype_new d2' = is_D: D nat -data d3 = D | E -data d3' = D | is_E: E -data d3'' = is_D: D | E -data d3''' = is_D: D | is_E: E +datatype_new d3 = D | E +datatype_new d3' = D | is_E: E +datatype_new d3'' = is_D: D | E +datatype_new d3''' = is_D: D | is_E: E -data d4 = D nat | E -data d4' = D nat | is_E: E -data d4'' = is_D: D nat | E -data d4''' = is_D: D nat | is_E: E +datatype_new d4 = D nat | E +datatype_new d4' = D nat | is_E: E +datatype_new d4'' = is_D: D nat | E +datatype_new d4''' = is_D: D nat | is_E: E -data d5 = D nat | E int -data d5' = D nat | is_E: E int -data d5'' = is_D: D nat | E int -data d5''' = is_D: D nat | is_E: E int +datatype_new d5 = D nat | E int +datatype_new d5' = D nat | is_E: E int +datatype_new d5'' = is_D: D nat | E int +datatype_new d5''' = is_D: D nat | is_E: E int end diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Process.thy --- a/src/HOL/BNF/Examples/Process.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Process.thy Mon Apr 29 09:10:49 2013 +0200 @@ -13,7 +13,7 @@ hide_fact (open) Quotient_Product.prod_rel_def -codata 'a process = +codatatype 'a process = isAction: Action (prefOf: 'a) (contOf: "'a process") | isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Mon Apr 29 09:10:49 2013 +0200 @@ -12,8 +12,8 @@ imports "../BNF" begin -codata (sset: 'a) stream (map: smap rel: stream_all2) = - Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) +codatatype (sset: 'a) stream (map: smap rel: stream_all2) = + Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) declaration {* Nitpick_HOL.register_codatatype diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/TreeFI.thy --- a/src/HOL/BNF/Examples/TreeFI.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFI.thy Mon Apr 29 09:10:49 2013 +0200 @@ -12,7 +12,7 @@ imports ListF begin -codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF") +codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF") lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Examples/TreeFsetI.thy --- a/src/HOL/BNF/Examples/TreeFsetI.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy Mon Apr 29 09:10:49 2013 +0200 @@ -14,7 +14,7 @@ hide_fact (open) Quotient_Product.prod_rel_def -codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset") +codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset") definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 09:10:49 2013 +0200 @@ -159,7 +159,6 @@ (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 = let (* TODO: sanity checks on arguments *) - (* TODO: integration with function package ("size") *) val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes" else (); diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Apr 29 09:10:49 2013 +0200 @@ -3036,7 +3036,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes" + Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes" (parse_datatype_cmd false construct_gfp); end; diff -r 71260347b7e4 -r be6e703908f4 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 09:10:49 2013 +0200 @@ -1860,7 +1860,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes" + Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" (parse_datatype_cmd true construct_lfp); end;