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