src/HOL/Datatype_Examples/Misc_Datatype.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58455 126c353540fc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
blanchet@58309
     1
(*  Title:      HOL/Datatype_Examples/Misc_Datatype.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@51744
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@51744
     5
    Copyright   2012, 2013
blanchet@48975
     6
blanchet@53122
     7
Miscellaneous datatype definitions.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@53122
    10
header {* Miscellaneous Datatype Definitions *}
blanchet@48975
    11
blanchet@53122
    12
theory Misc_Datatype
blanchet@58163
    13
imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
blanchet@48975
    14
begin
blanchet@48975
    15
blanchet@58310
    16
datatype (discs_sels) simple = X1 | X2 | X3 | X4
blanchet@49157
    17
blanchet@58310
    18
datatype (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
blanchet@48975
    19
blanchet@58310
    20
datatype (discs_sels) simple'' = X1'' nat int | X2''
blanchet@52323
    21
blanchet@58310
    22
datatype (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
blanchet@48975
    23
blanchet@58310
    24
datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
blanchet@49157
    25
  SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
blanchet@48975
    26
desharna@58417
    27
datatype (discs_sels) 'a multi_live_direct1 = MultiLiveDirect1 'a
desharna@58417
    28
datatype (discs_sels) 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
desharna@58417
    29
datatype (discs_sels) 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
desharna@58417
    30
datatype (discs_sels) 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
desharna@58417
    31
datatype (discs_sels) 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
desharna@58417
    32
datatype (discs_sels) 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
desharna@58417
    33
datatype (discs_sels) 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    34
datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    35
datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    36
desharna@58455
    37
datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a"
desharna@58455
    38
blanchet@58310
    39
datatype (discs_sels) hfset = HFset "hfset fset"
blanchet@49601
    40
blanchet@58310
    41
datatype (discs_sels) lambda =
blanchet@49157
    42
  Var string |
blanchet@49157
    43
  App lambda lambda |
blanchet@49157
    44
  Abs string lambda |
blanchet@49157
    45
  Let "(string \<times> lambda) fset" lambda
blanchet@48975
    46
blanchet@58310
    47
datatype (discs_sels) 'a par_lambda =
blanchet@49157
    48
  PVar 'a |
blanchet@49157
    49
  PApp "'a par_lambda" "'a par_lambda" |
blanchet@49157
    50
  PAbs 'a "'a par_lambda" |
blanchet@49157
    51
  PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda"
blanchet@48975
    52
blanchet@48975
    53
(*
blanchet@48975
    54
  ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
blanchet@48975
    55
  ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
blanchet@48975
    56
*)
blanchet@48975
    57
blanchet@58310
    58
datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
blanchet@51804
    59
and 'a I2 = I21 | I22 "'a I1" "'a I2"
blanchet@48975
    60
blanchet@58310
    61
datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
blanchet@51804
    62
and 'a forest = FNil | FCons "'a tree" "'a forest"
blanchet@48975
    63
blanchet@58310
    64
datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
blanchet@51804
    65
and 'a branch = Branch 'a "'a tree'"
blanchet@48975
    66
blanchet@58310
    67
datatype (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
blanchet@55484
    68
blanchet@58310
    69
datatype (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
blanchet@51804
    70
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
blanchet@51804
    71
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
blanchet@48975
    72
blanchet@58310
    73
datatype (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
blanchet@53134
    74
blanchet@58310
    75
datatype (discs_sels) ('a, 'b, 'c) some_killing =
blanchet@49157
    76
  SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
blanchet@51804
    77
and ('a, 'b, 'c) in_here =
blanchet@49157
    78
  IH1 'b 'a | IH2 'c
blanchet@48975
    79
blanchet@58310
    80
datatype (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
blanchet@58310
    81
datatype (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
blanchet@58310
    82
datatype (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
blanchet@58310
    83
datatype (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
blanchet@48975
    84
blanchet@48975
    85
(*
blanchet@58310
    86
datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
blanchet@58310
    87
datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
blanchet@58310
    88
datatype (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
blanchet@58310
    89
datatype (discs_sels) 'b fail = F "'b fail" 'b
blanchet@48975
    90
*)
blanchet@48975
    91
blanchet@58310
    92
datatype (discs_sels) l1 = L1 "l2 list"
blanchet@51804
    93
and l2 = L21 "l1 fset" | L22 l2
blanchet@48975
    94
blanchet@58310
    95
datatype (discs_sels) kk1 = KK1 kk2
blanchet@51804
    96
and kk2 = KK2 kk3
blanchet@51804
    97
and kk3 = KK3 "kk1 list"
blanchet@48975
    98
blanchet@58310
    99
datatype (discs_sels) t1 = T11 t3 | T12 t2
blanchet@51804
   100
and t2 = T2 t1
blanchet@51804
   101
and t3 = T3
blanchet@48975
   102
blanchet@58310
   103
datatype (discs_sels) t1' = T11' t2' | T12' t3'
blanchet@51804
   104
and t2' = T2' t1'
blanchet@51804
   105
and t3' = T3'
blanchet@48975
   106
blanchet@48975
   107
(*
blanchet@58310
   108
datatype (discs_sels) fail1 = F1 fail2
blanchet@51804
   109
and fail2 = F2 fail3
blanchet@51804
   110
and fail3 = F3 fail1
blanchet@48975
   111
blanchet@58310
   112
datatype (discs_sels) fail1 = F1 "fail2 list" fail2
blanchet@51804
   113
and fail2 = F2 "fail2 fset" fail3
blanchet@51804
   114
and fail3 = F3 fail1
blanchet@48975
   115
blanchet@58310
   116
datatype (discs_sels) fail1 = F1 "fail2 list" fail2
blanchet@51804
   117
and fail2 = F2 "fail1 fset" fail1
blanchet@48975
   118
*)
blanchet@49157
   119
blanchet@49162
   120
(* SLOW
blanchet@58310
   121
datatype (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
blanchet@51804
   122
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
blanchet@51804
   123
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
blanchet@51804
   124
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
blanchet@51804
   125
and ('a, 'c) D5 = A5 "('a, 'c) D6"
blanchet@51804
   126
and ('a, 'c) D6 = A6 "('a, 'c) D7"
blanchet@51804
   127
and ('a, 'c) D7 = A7 "('a, 'c) D8"
blanchet@51804
   128
and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
blanchet@49162
   129
*)
blanchet@48975
   130
blanchet@48975
   131
(* fail:
blanchet@58310
   132
datatype (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
blanchet@51804
   133
and tt2 = TT2
blanchet@51804
   134
and tt3 = TT3 tt4
blanchet@51804
   135
and tt4 = TT4 tt1
blanchet@48975
   136
*)
blanchet@48975
   137
blanchet@58310
   138
datatype (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
blanchet@51804
   139
and k2 = K2
blanchet@51804
   140
and k3 = K3 k4
blanchet@51804
   141
and k4 = K4
blanchet@48975
   142
blanchet@58310
   143
datatype (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
blanchet@51804
   144
and tt2 = TT2
blanchet@51804
   145
and tt3 = TT3 tt1
blanchet@51804
   146
and tt4 = TT4
blanchet@49157
   147
blanchet@49162
   148
(* SLOW
blanchet@58310
   149
datatype (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
blanchet@51804
   150
and s2 = S21 s7 s5 | S22 s5 s4 s6
blanchet@51804
   151
and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
blanchet@51804
   152
and s4 = S4 s5
blanchet@51804
   153
and s5 = S5
blanchet@51804
   154
and s6 = S61 s6 | S62 s1 s2 | S63 s6
blanchet@51804
   155
and s7 = S71 s8 | S72 s5
blanchet@51804
   156
and s8 = S8 nat
blanchet@49162
   157
*)
blanchet@48975
   158
blanchet@58310
   159
datatype (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
blanchet@58310
   160
datatype (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
blanchet@58310
   161
datatype (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
blanchet@58310
   162
datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
blanchet@58310
   163
datatype (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
traytel@49185
   164
blanchet@58332
   165
datatype (discs_sels) (dead 'a) dead_foo = A
blanchet@58332
   166
datatype (discs_sels) ('a, 'b) use_dead_foo = Y 'a "'b dead_foo"
blanchet@58332
   167
blanchet@58332
   168
datatype (discs_sels) 'a phantom = A
blanchet@58332
   169
datatype (discs_sels) 'a use_phantom = Y 'a "'a use_phantom phantom"
traytel@49186
   170
desharna@58327
   171
datatype ('t, 'id) dead_sum_fun = Dead_sum_fun "('t list \<Rightarrow> 't) + 't" | Bar (bar: 'id)
desharna@58327
   172
blanchet@58310
   173
datatype (discs_sels) d1 = D
blanchet@58310
   174
datatype (discs_sels) d1' = is_D: D
blanchet@51744
   175
blanchet@58310
   176
datatype (discs_sels) d2 = D nat
blanchet@58310
   177
datatype (discs_sels) d2' = is_D: D nat
blanchet@51744
   178
blanchet@58310
   179
datatype (discs_sels) d3 = D | E
blanchet@58310
   180
datatype (discs_sels) d3' = D | is_E: E
blanchet@58310
   181
datatype (discs_sels) d3'' = is_D: D | E
blanchet@58310
   182
datatype (discs_sels) d3''' = is_D: D | is_E: E
blanchet@51744
   183
blanchet@58310
   184
datatype (discs_sels) d4 = D nat | E
blanchet@58310
   185
datatype (discs_sels) d4' = D nat | is_E: E
blanchet@58310
   186
datatype (discs_sels) d4'' = is_D: D nat | E
blanchet@58310
   187
datatype (discs_sels) d4''' = is_D: D nat | is_E: E
blanchet@51744
   188
blanchet@58310
   189
datatype (discs_sels) d5 = D nat | E int
blanchet@58310
   190
datatype (discs_sels) d5' = D nat | is_E: E int
blanchet@58310
   191
datatype (discs_sels) d5'' = is_D: D nat | E int
blanchet@58310
   192
datatype (discs_sels) d5''' = is_D: D nat | is_E: E int
blanchet@51744
   193
blanchet@58163
   194
instance simple :: countable
blanchet@58163
   195
  by countable_datatype
blanchet@58163
   196
blanchet@58163
   197
instance simple'' :: countable
blanchet@58163
   198
  by countable_datatype
blanchet@58163
   199
blanchet@58163
   200
instance mylist :: (countable) countable
blanchet@58163
   201
  by countable_datatype
blanchet@58163
   202
blanchet@58232
   203
instance some_passive :: (countable, "{countable,ord}", countable, countable) countable
blanchet@58163
   204
  by countable_datatype
blanchet@58163
   205
blanchet@58163
   206
(* TODO: Enable once "fset" is registered as countable:
blanchet@58163
   207
blanchet@58163
   208
instance hfset :: countable
blanchet@58163
   209
  by countable_datatype
blanchet@58163
   210
blanchet@58163
   211
instance lambda :: countable
blanchet@58163
   212
  by countable_datatype
blanchet@58163
   213
blanchet@58163
   214
instance par_lambda :: (countable) countable
blanchet@58163
   215
  by countable_datatype
blanchet@58163
   216
*)
blanchet@58163
   217
blanchet@58163
   218
instance I1 and I2 :: (countable) countable
blanchet@58163
   219
  by countable_datatype
blanchet@58163
   220
blanchet@58163
   221
instance tree and forest :: (countable) countable
blanchet@58163
   222
  by countable_datatype
blanchet@58163
   223
blanchet@58163
   224
instance tree' and branch :: (countable) countable
blanchet@58163
   225
  by countable_datatype
blanchet@58163
   226
blanchet@58163
   227
instance bin_rose_tree :: (countable) countable
blanchet@58163
   228
  by countable_datatype
blanchet@58163
   229
blanchet@58163
   230
instance exp and trm and factor :: (countable, countable) countable
blanchet@58163
   231
  by countable_datatype
blanchet@58163
   232
blanchet@58163
   233
instance nofail1 :: (countable) countable
blanchet@58163
   234
  by countable_datatype
blanchet@58163
   235
blanchet@58163
   236
instance nofail2 :: (countable) countable
blanchet@58163
   237
  by countable_datatype
blanchet@58163
   238
blanchet@58163
   239
(* TODO: Enable once "fset" is registered as countable:
blanchet@58163
   240
blanchet@58163
   241
instance nofail3 :: (countable) countable
blanchet@58163
   242
  by countable_datatype
blanchet@58163
   243
blanchet@58163
   244
instance nofail4 :: (countable) countable
blanchet@58163
   245
  by countable_datatype
blanchet@58163
   246
blanchet@58163
   247
instance l1 and l2 :: countable
blanchet@58173
   248
  by countable_datatype
blanchet@58163
   249
*)
blanchet@58163
   250
blanchet@58163
   251
instance kk1 and kk2 :: countable
blanchet@58163
   252
  by countable_datatype
blanchet@58163
   253
blanchet@58163
   254
instance t1 and t2 and t3 :: countable
blanchet@58163
   255
  by countable_datatype
blanchet@58163
   256
blanchet@58163
   257
instance t1' and t2' and t3' :: countable
blanchet@58163
   258
  by countable_datatype
blanchet@58163
   259
blanchet@58163
   260
instance k1 and k2 and k3 and k4 :: countable
blanchet@58163
   261
  by countable_datatype
blanchet@58163
   262
blanchet@58163
   263
instance tt1 and tt2 and tt3 and tt4 :: countable
blanchet@58163
   264
  by countable_datatype
blanchet@58163
   265
blanchet@58163
   266
instance d1 :: countable
blanchet@58163
   267
  by countable_datatype
blanchet@58163
   268
blanchet@58163
   269
instance d1' :: countable
blanchet@58163
   270
  by countable_datatype
blanchet@58163
   271
blanchet@58163
   272
instance d2 :: countable
blanchet@58163
   273
  by countable_datatype
blanchet@58163
   274
blanchet@58163
   275
instance d2' :: countable
blanchet@58163
   276
  by countable_datatype
blanchet@58163
   277
blanchet@58163
   278
instance d3 :: countable
blanchet@58163
   279
  by countable_datatype
blanchet@58163
   280
blanchet@58163
   281
instance d3' :: countable
blanchet@58163
   282
  by countable_datatype
blanchet@58163
   283
blanchet@58163
   284
instance d3'' :: countable
blanchet@58163
   285
  by countable_datatype
blanchet@58163
   286
blanchet@58163
   287
instance d3''' :: countable
blanchet@58163
   288
  by countable_datatype
blanchet@58163
   289
blanchet@58163
   290
instance d4 :: countable
blanchet@58163
   291
  by countable_datatype
blanchet@58163
   292
blanchet@58163
   293
instance d4' :: countable
blanchet@58163
   294
  by countable_datatype
blanchet@58163
   295
blanchet@58163
   296
instance d4'' :: countable
blanchet@58163
   297
  by countable_datatype
blanchet@58163
   298
blanchet@58163
   299
instance d4''' :: countable
blanchet@58163
   300
  by countable_datatype
blanchet@58163
   301
blanchet@58163
   302
instance d5 :: countable
blanchet@58163
   303
  by countable_datatype
blanchet@58163
   304
blanchet@58163
   305
instance d5' :: countable
blanchet@58163
   306
  by countable_datatype
blanchet@58163
   307
blanchet@58163
   308
instance d5'' :: countable
blanchet@58163
   309
  by countable_datatype
blanchet@58163
   310
blanchet@58163
   311
instance d5''' :: countable
blanchet@58163
   312
  by countable_datatype
blanchet@58163
   313
blanchet@57795
   314
datatype_compat simple
blanchet@57795
   315
datatype_compat simple'
blanchet@57795
   316
datatype_compat simple''
blanchet@57795
   317
datatype_compat mylist
blanchet@57795
   318
datatype_compat some_passive
blanchet@57795
   319
datatype_compat I1 I2
blanchet@57795
   320
datatype_compat tree forest
blanchet@57795
   321
datatype_compat tree' branch
blanchet@57795
   322
datatype_compat bin_rose_tree
blanchet@57795
   323
datatype_compat exp trm factor
blanchet@57795
   324
datatype_compat ftree
blanchet@57795
   325
datatype_compat nofail1
blanchet@57795
   326
datatype_compat kk1 kk2 kk3
blanchet@57795
   327
datatype_compat t1 t2 t3
blanchet@57795
   328
datatype_compat t1' t2' t3'
blanchet@57795
   329
datatype_compat k1 k2 k3 k4
blanchet@57795
   330
datatype_compat tt1 tt2 tt3 tt4
blanchet@57795
   331
datatype_compat deadbar
blanchet@57795
   332
datatype_compat deadbar_option
blanchet@57795
   333
datatype_compat bar
blanchet@57795
   334
datatype_compat foo
blanchet@57795
   335
datatype_compat deadfoo
blanchet@57795
   336
datatype_compat dead_foo
blanchet@57795
   337
datatype_compat use_dead_foo
blanchet@57795
   338
datatype_compat d1
blanchet@57795
   339
datatype_compat d1'
blanchet@57795
   340
datatype_compat d2
blanchet@57795
   341
datatype_compat d2'
blanchet@57795
   342
datatype_compat d3
blanchet@57795
   343
datatype_compat d3'
blanchet@57795
   344
datatype_compat d3''
blanchet@57795
   345
datatype_compat d3'''
blanchet@57795
   346
datatype_compat d4
blanchet@57795
   347
datatype_compat d4'
blanchet@57795
   348
datatype_compat d4''
blanchet@57795
   349
datatype_compat d4'''
blanchet@57795
   350
datatype_compat d5
blanchet@57795
   351
datatype_compat d5'
blanchet@57795
   352
datatype_compat d5''
blanchet@57795
   353
datatype_compat d5'''
blanchet@57795
   354
blanchet@48975
   355
end