src/HOL/BNF/Examples/Misc_Datatype.thy
author blanchet
Wed, 21 Aug 2013 09:25:40 +0200
changeset 53123 00d922eba913
parent 53122 bc87b7af4767
child 53134 4f8e156d2f19
permissions -rw-r--r--
avoid constructor name clash
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52844
diff changeset
     1
(*  Title:      HOL/BNF/Examples/Misc_Datatype.thy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
     5
    Copyright   2012, 2013
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52844
diff changeset
     7
Miscellaneous datatype definitions.
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52844
diff changeset
    10
header {* Miscellaneous Datatype Definitions *}
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52844
diff changeset
    12
theory Misc_Datatype
49509
163914705f8d renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents: 49463
diff changeset
    13
imports "../BNF"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    14
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    15
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    16
datatype_new simple = X1 | X2 | X3 | X4
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    17
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    18
datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    19
52323
a11bbb5fef56 fixed failure in coinduction rule tactic
blanchet
parents: 51804
diff changeset
    20
datatype_new simple'' = X1'' nat int | X2''
a11bbb5fef56 fixed failure in coinduction rule tactic
blanchet
parents: 51804
diff changeset
    21
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    22
datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    23
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    24
datatype_new ('b, 'c, 'd, 'e) some_passive =
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    25
  SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    26
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    27
datatype_new hfset = HFset "hfset fset"
49601
ba31032887db modernized examples;
blanchet
parents: 49510
diff changeset
    28
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    29
datatype_new lambda =
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    30
  Var string |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    31
  App lambda lambda |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    32
  Abs string lambda |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    33
  Let "(string \<times> lambda) fset" lambda
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    34
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    35
datatype_new 'a par_lambda =
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    36
  PVar 'a |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    37
  PApp "'a par_lambda" "'a par_lambda" |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    38
  PAbs 'a "'a par_lambda" |
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    39
  PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    40
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    41
(*
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    42
  ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    43
  ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    44
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    45
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    46
datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    47
and 'a I2 = I21 | I22 "'a I1" "'a I2"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    48
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    49
datatype_new 'a tree = TEmpty | TNode 'a "'a forest"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    50
and 'a forest = FNil | FCons "'a tree" "'a forest"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    51
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    52
datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    53
and 'a branch = Branch 'a "'a tree'"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    54
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    55
datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    56
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    57
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    58
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    59
datatype_new ('a, 'b, 'c) some_killing =
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    60
  SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    61
and ('a, 'b, 'c) in_here =
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
    62
  IH1 'b 'a | IH2 'c
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    63
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    64
datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    65
datatype_new 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    66
datatype_new 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    67
datatype_new 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    68
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    69
(*
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    70
datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    71
datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    72
datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    73
datatype_new 'b fail = F "'b fail" 'b
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    74
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    75
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    76
datatype_new l1 = L1 "l2 list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    77
and l2 = L21 "l1 fset" | L22 l2
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    78
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    79
datatype_new kk1 = KK1 kk2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    80
and kk2 = KK2 kk3
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    81
and kk3 = KK3 "kk1 list"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    82
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    83
datatype_new t1 = T11 t3 | T12 t2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    84
and t2 = T2 t1
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    85
and t3 = T3
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    86
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    87
datatype_new t1' = T11' t2' | T12' t3'
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    88
and t2' = T2' t1'
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    89
and t3' = T3'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    91
(*
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    92
datatype_new fail1 = F1 fail2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    93
and fail2 = F2 fail3
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    94
and fail3 = F3 fail1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    95
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    96
datatype_new fail1 = F1 "fail2 list" fail2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    97
and fail2 = F2 "fail2 fset" fail3
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
    98
and fail3 = F3 fail1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    99
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   100
datatype_new fail1 = F1 "fail2 list" fail2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   101
and fail2 = F2 "fail1 fset" fail1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   102
*)
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   103
49162
bd6a18a1a5af commented out slow examples again
blanchet
parents: 49158
diff changeset
   104
(* SLOW
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   105
datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   106
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   107
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   108
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   109
and ('a, 'c) D5 = A5 "('a, 'c) D6"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   110
and ('a, 'c) D6 = A6 "('a, 'c) D7"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   111
and ('a, 'c) D7 = A7 "('a, 'c) D8"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   112
and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   113
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   114
(*time comparison*)
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   115
datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   116
     and ('a, 'c) D2' = A2' "('a, 'c) D3'" | B2' "'c list"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   117
     and ('a, 'c) D3' = A3' "('a, 'c) D3'" | B3' "('a, 'c) D4'" | C3' "('a, 'c) D4'" "('a, 'c) D5'"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   118
     and ('a, 'c) D4' = A4' "('a, 'c) D5'" | B4' "'a list list list"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   119
     and ('a, 'c) D5' = A5' "('a, 'c) D6'"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   120
     and ('a, 'c) D6' = A6' "('a, 'c) D7'"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   121
     and ('a, 'c) D7' = A7' "('a, 'c) D8'"
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   122
     and ('a, 'c) D8' = A8' "('a, 'c) D1' list"
49162
bd6a18a1a5af commented out slow examples again
blanchet
parents: 49158
diff changeset
   123
*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   124
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   125
(* fail:
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   126
datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   127
and tt2 = TT2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   128
and tt3 = TT3 tt4
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   129
and tt4 = TT4 tt1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   130
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   132
datatype_new k1 = K11 k2 k3 | K12 k2 k4
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   133
and k2 = K2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   134
and k3 = K3 k4
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   135
and k4 = K4
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   136
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   137
datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   138
and tt2 = TT2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   139
and tt3 = TT3 tt1
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   140
and tt4 = TT4
49157
6407346b74c7 ported "Misc_Data" to new syntax
blanchet
parents: 49115
diff changeset
   141
49162
bd6a18a1a5af commented out slow examples again
blanchet
parents: 49158
diff changeset
   142
(* SLOW
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   143
datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   144
and s2 = S21 s7 s5 | S22 s5 s4 s6
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   145
and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   146
and s4 = S4 s5
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   147
and s5 = S5
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   148
and s6 = S61 s6 | S62 s1 s2 | S63 s6
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   149
and s7 = S71 s8 | S72 s5
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   150
and s8 = S8 nat
49162
bd6a18a1a5af commented out slow examples again
blanchet
parents: 49158
diff changeset
   151
*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   152
52813
963297a24206 more robust tactic
traytel
parents: 52323
diff changeset
   153
datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
963297a24206 more robust tactic
traytel
parents: 52323
diff changeset
   154
datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   155
datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   156
datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
53123
00d922eba913 avoid constructor name clash
blanchet
parents: 53122
diff changeset
   157
datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
49185
073d7d1b7488 respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents: 49166
diff changeset
   158
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   159
datatype_new 'a dead_foo = A
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   160
datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
49186
4b5fa9d5e330 handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents: 49185
diff changeset
   161
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   162
datatype_new d1 = D
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   163
datatype_new d1' = is_D: D
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
   164
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   165
datatype_new d2 = D nat
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   166
datatype_new d2' = is_D: D nat
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
   167
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   168
datatype_new d3 = D | E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   169
datatype_new d3' = D | is_E: E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   170
datatype_new d3'' = is_D: D | E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   171
datatype_new d3''' = is_D: D | is_E: E
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
   172
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   173
datatype_new d4 = D nat | E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   174
datatype_new d4' = D nat | is_E: E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   175
datatype_new d4'' = is_D: D nat | E
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   176
datatype_new d4''' = is_D: D nat | is_E: E
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
   177
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   178
datatype_new d5 = D nat | E int
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   179
datatype_new d5' = D nat | is_E: E int
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   180
datatype_new d5'' = is_D: D nat | E int
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51744
diff changeset
   181
datatype_new d5''' = is_D: D nat | is_E: E int
51744
0468af6546ff more examples
blanchet
parents: 49601
diff changeset
   182
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   183
end