src/HOL/BNF/Examples/Misc_Data.thy
author blanchet
Mon Apr 29 09:10:49 2013 +0200 (2013-04-29)
changeset 51804 be6e703908f4
parent 51744 0468af6546ff
child 52323 a11bbb5fef56
permissions -rw-r--r--
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet@49509
     1
(*  Title:      HOL/BNF/Examples/Misc_Data.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@48975
     7
Miscellaneous datatype declarations.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@48975
    10
header {* Miscellaneous Datatype Declarations *}
blanchet@48975
    11
blanchet@48975
    12
theory Misc_Data
blanchet@49509
    13
imports "../BNF"
blanchet@48975
    14
begin
blanchet@48975
    15
blanchet@51804
    16
datatype_new simple = X1 | X2 | X3 | X4
blanchet@49157
    17
blanchet@51804
    18
datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
blanchet@48975
    19
blanchet@51804
    20
datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
blanchet@48975
    21
blanchet@51804
    22
datatype_new ('b, 'c, 'd, 'e) some_passive =
blanchet@49157
    23
  SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
blanchet@48975
    24
blanchet@51804
    25
datatype_new hfset = HFset "hfset fset"
blanchet@49601
    26
blanchet@51804
    27
datatype_new lambda =
blanchet@49157
    28
  Var string |
blanchet@49157
    29
  App lambda lambda |
blanchet@49157
    30
  Abs string lambda |
blanchet@49157
    31
  Let "(string \<times> lambda) fset" lambda
blanchet@48975
    32
blanchet@51804
    33
datatype_new 'a par_lambda =
blanchet@49157
    34
  PVar 'a |
blanchet@49157
    35
  PApp "'a par_lambda" "'a par_lambda" |
blanchet@49157
    36
  PAbs 'a "'a par_lambda" |
blanchet@49157
    37
  PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda"
blanchet@48975
    38
blanchet@48975
    39
(*
blanchet@48975
    40
  ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
blanchet@48975
    41
  ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
blanchet@48975
    42
*)
blanchet@48975
    43
blanchet@51804
    44
datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
blanchet@51804
    45
and 'a I2 = I21 | I22 "'a I1" "'a I2"
blanchet@48975
    46
blanchet@51804
    47
datatype_new 'a tree = TEmpty | TNode 'a "'a forest"
blanchet@51804
    48
and 'a forest = FNil | FCons "'a tree" "'a forest"
blanchet@48975
    49
blanchet@51804
    50
datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
blanchet@51804
    51
and 'a branch = Branch 'a "'a tree'"
blanchet@48975
    52
blanchet@51804
    53
datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
blanchet@51804
    54
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
blanchet@51804
    55
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
blanchet@48975
    56
blanchet@51804
    57
datatype_new ('a, 'b, 'c) some_killing =
blanchet@49157
    58
  SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
blanchet@51804
    59
and ('a, 'b, 'c) in_here =
blanchet@49157
    60
  IH1 'b 'a | IH2 'c
blanchet@48975
    61
blanchet@51804
    62
datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
blanchet@51804
    63
datatype_new 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
blanchet@51804
    64
datatype_new 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
blanchet@51804
    65
datatype_new 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
blanchet@48975
    66
blanchet@48975
    67
(*
blanchet@51804
    68
datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list"
blanchet@51804
    69
datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b
blanchet@51804
    70
datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail"
blanchet@51804
    71
datatype_new 'b fail = F "'b fail" 'b
blanchet@48975
    72
*)
blanchet@48975
    73
blanchet@51804
    74
datatype_new l1 = L1 "l2 list"
blanchet@51804
    75
and l2 = L21 "l1 fset" | L22 l2
blanchet@48975
    76
blanchet@51804
    77
datatype_new kk1 = KK1 kk2
blanchet@51804
    78
and kk2 = KK2 kk3
blanchet@51804
    79
and kk3 = KK3 "kk1 list"
blanchet@48975
    80
blanchet@51804
    81
datatype_new t1 = T11 t3 | T12 t2
blanchet@51804
    82
and t2 = T2 t1
blanchet@51804
    83
and t3 = T3
blanchet@48975
    84
blanchet@51804
    85
datatype_new t1' = T11' t2' | T12' t3'
blanchet@51804
    86
and t2' = T2' t1'
blanchet@51804
    87
and t3' = T3'
blanchet@48975
    88
blanchet@48975
    89
(*
blanchet@51804
    90
datatype_new fail1 = F1 fail2
blanchet@51804
    91
and fail2 = F2 fail3
blanchet@51804
    92
and fail3 = F3 fail1
blanchet@48975
    93
blanchet@51804
    94
datatype_new fail1 = F1 "fail2 list" fail2
blanchet@51804
    95
and fail2 = F2 "fail2 fset" fail3
blanchet@51804
    96
and fail3 = F3 fail1
blanchet@48975
    97
blanchet@51804
    98
datatype_new fail1 = F1 "fail2 list" fail2
blanchet@51804
    99
and fail2 = F2 "fail1 fset" fail1
blanchet@48975
   100
*)
blanchet@49157
   101
blanchet@49162
   102
(* SLOW
blanchet@51804
   103
datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
blanchet@51804
   104
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
blanchet@51804
   105
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
blanchet@51804
   106
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
blanchet@51804
   107
and ('a, 'c) D5 = A5 "('a, 'c) D6"
blanchet@51804
   108
and ('a, 'c) D6 = A6 "('a, 'c) D7"
blanchet@51804
   109
and ('a, 'c) D7 = A7 "('a, 'c) D8"
blanchet@51804
   110
and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
blanchet@48975
   111
blanchet@48975
   112
(*time comparison*)
blanchet@49157
   113
datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list"
blanchet@49157
   114
     and ('a, 'c) D2' = A2' "('a, 'c) D3'" | B2' "'c list"
blanchet@49157
   115
     and ('a, 'c) D3' = A3' "('a, 'c) D3'" | B3' "('a, 'c) D4'" | C3' "('a, 'c) D4'" "('a, 'c) D5'"
blanchet@49157
   116
     and ('a, 'c) D4' = A4' "('a, 'c) D5'" | B4' "'a list list list"
blanchet@49157
   117
     and ('a, 'c) D5' = A5' "('a, 'c) D6'"
blanchet@49157
   118
     and ('a, 'c) D6' = A6' "('a, 'c) D7'"
blanchet@49157
   119
     and ('a, 'c) D7' = A7' "('a, 'c) D8'"
blanchet@49157
   120
     and ('a, 'c) D8' = A8' "('a, 'c) D1' list"
blanchet@49162
   121
*)
blanchet@48975
   122
blanchet@48975
   123
(* fail:
blanchet@51804
   124
datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
blanchet@51804
   125
and tt2 = TT2
blanchet@51804
   126
and tt3 = TT3 tt4
blanchet@51804
   127
and tt4 = TT4 tt1
blanchet@48975
   128
*)
blanchet@48975
   129
blanchet@51804
   130
datatype_new k1 = K11 k2 k3 | K12 k2 k4
blanchet@51804
   131
and k2 = K2
blanchet@51804
   132
and k3 = K3 k4
blanchet@51804
   133
and k4 = K4
blanchet@48975
   134
blanchet@51804
   135
datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
blanchet@51804
   136
and tt2 = TT2
blanchet@51804
   137
and tt3 = TT3 tt1
blanchet@51804
   138
and tt4 = TT4
blanchet@49157
   139
blanchet@49162
   140
(* SLOW
blanchet@51804
   141
datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
blanchet@51804
   142
and s2 = S21 s7 s5 | S22 s5 s4 s6
blanchet@51804
   143
and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
blanchet@51804
   144
and s4 = S4 s5
blanchet@51804
   145
and s5 = S5
blanchet@51804
   146
and s6 = S61 s6 | S62 s1 s2 | S63 s6
blanchet@51804
   147
and s7 = S71 s8 | S72 s5
blanchet@51804
   148
and s8 = S8 nat
blanchet@49162
   149
*)
blanchet@48975
   150
blanchet@51804
   151
datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
blanchet@51804
   152
datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
traytel@49185
   153
blanchet@51804
   154
datatype_new 'a dead_foo = A
blanchet@51804
   155
datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
traytel@49186
   156
blanchet@51804
   157
datatype_new d1 = D
blanchet@51804
   158
datatype_new d1' = is_D: D
blanchet@51744
   159
blanchet@51804
   160
datatype_new d2 = D nat
blanchet@51804
   161
datatype_new d2' = is_D: D nat
blanchet@51744
   162
blanchet@51804
   163
datatype_new d3 = D | E
blanchet@51804
   164
datatype_new d3' = D | is_E: E
blanchet@51804
   165
datatype_new d3'' = is_D: D | E
blanchet@51804
   166
datatype_new d3''' = is_D: D | is_E: E
blanchet@51744
   167
blanchet@51804
   168
datatype_new d4 = D nat | E
blanchet@51804
   169
datatype_new d4' = D nat | is_E: E
blanchet@51804
   170
datatype_new d4'' = is_D: D nat | E
blanchet@51804
   171
datatype_new d4''' = is_D: D nat | is_E: E
blanchet@51744
   172
blanchet@51804
   173
datatype_new d5 = D nat | E int
blanchet@51804
   174
datatype_new d5' = D nat | is_E: E int
blanchet@51804
   175
datatype_new d5'' = is_D: D nat | E int
blanchet@51804
   176
datatype_new d5''' = is_D: D nat | is_E: E int
blanchet@51744
   177
blanchet@48975
   178
end