src/HOL/Datatype_Examples/Misc_Codatatype.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_Codatatype.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@52323
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@52323
     5
    Copyright   2012, 2013
blanchet@48975
     6
blanchet@53122
     7
Miscellaneous codatatype definitions.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@53122
    10
header {* Miscellaneous Codatatype Definitions *}
blanchet@48975
    11
blanchet@53122
    12
theory Misc_Codatatype
blanchet@55129
    13
imports "~~/src/HOL/Library/FSet"
blanchet@48975
    14
begin
blanchet@48975
    15
blanchet@51804
    16
codatatype simple = X1 | X2 | X3 | X4
blanchet@49158
    17
blanchet@51804
    18
codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit
blanchet@48975
    19
blanchet@52323
    20
codatatype simple'' = X1'' nat int | X2''
blanchet@52323
    21
blanchet@54193
    22
codatatype 'a stream = Stream (shd: 'a) (stl: "'a stream")
blanchet@49158
    23
blanchet@54193
    24
codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
blanchet@49158
    25
blanchet@58228
    26
codatatype ('b, 'c :: ord, 'd, 'e) some_passive =
blanchet@49158
    27
  SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
blanchet@48975
    28
desharna@58417
    29
codatatype 'a multi_live_direct1 = MultiLiveDirect1 'a
desharna@58417
    30
codatatype 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
desharna@58417
    31
codatatype 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
desharna@58417
    32
codatatype 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
desharna@58417
    33
codatatype 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
desharna@58417
    34
codatatype 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
desharna@58417
    35
codatatype 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    36
codatatype 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    37
codatatype 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
desharna@58417
    38
desharna@58455
    39
datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a"
desharna@58455
    40
blanchet@51804
    41
codatatype lambda =
blanchet@49158
    42
  Var string |
blanchet@49158
    43
  App lambda lambda |
blanchet@49158
    44
  Abs string lambda |
blanchet@49158
    45
  Let "(string \<times> lambda) fset" lambda
blanchet@48975
    46
blanchet@51804
    47
codatatype 'a par_lambda =
blanchet@49158
    48
  PVar 'a |
blanchet@49158
    49
  PApp "'a par_lambda" "'a par_lambda" |
blanchet@49158
    50
  PAbs 'a "'a par_lambda" |
blanchet@49158
    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@53591
    58
codatatype 'a p = P "'a + 'a p"
blanchet@53591
    59
blanchet@51804
    60
codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
blanchet@51804
    61
and 'a J2 = J21 | J22 "'a J1" "'a J2"
blanchet@48975
    62
blanchet@51804
    63
codatatype 'a tree = TEmpty | TNode 'a "'a forest"
blanchet@51804
    64
and 'a forest = FNil | FCons "'a tree" "'a forest"
blanchet@48975
    65
blanchet@51804
    66
codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
blanchet@51804
    67
and 'a branch = Branch 'a "'a tree'"
blanchet@48975
    68
blanchet@55484
    69
codatatype 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
blanchet@55484
    70
blanchet@51804
    71
codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
blanchet@51804
    72
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
blanchet@51804
    73
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
blanchet@48975
    74
blanchet@51804
    75
codatatype ('a, 'b, 'c) some_killing =
blanchet@49158
    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@49158
    78
  IH1 'b 'a | IH2 'c
blanchet@48975
    79
blanchet@51804
    80
codatatype ('a, 'b, 'c) some_killing' =
blanchet@49617
    81
  SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'"
blanchet@51804
    82
and ('a, 'b, 'c) in_here' =
blanchet@49617
    83
  IH1' 'b | IH2' 'c
blanchet@48975
    84
blanchet@51804
    85
codatatype ('a, 'b, 'c) some_killing'' =
blanchet@49617
    86
  SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''"
blanchet@51804
    87
and ('a, 'b, 'c) in_here'' =
blanchet@49617
    88
  IH1'' 'b 'a | IH2'' 'c
blanchet@48975
    89
blanchet@51804
    90
codatatype ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
blanchet@48975
    91
traytel@53588
    92
codatatype 'b poly_unit = U "'b \<Rightarrow> 'b poly_unit"
blanchet@51804
    93
codatatype 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
blanchet@49158
    94
blanchet@51804
    95
codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
blanchet@49158
    96
  FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow>
blanchet@49158
    97
      ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs"
traytel@49102
    98
blanchet@51804
    99
codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
blanchet@49158
   100
        'b18, 'b19, 'b20) fun_rhs' =
blanchet@49158
   101
  FR' "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow> 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow>
blanchet@49158
   102
       'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow>
blanchet@49158
   103
       ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
blanchet@49158
   104
        'b18, 'b19, 'b20) fun_rhs'"
blanchet@49158
   105
blanchet@51804
   106
codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2"
blanchet@51804
   107
and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2"
blanchet@51804
   108
and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1"
blanchet@49158
   109
blanchet@51804
   110
codatatype ('c, 'e, 'g) coind_wit1 =
blanchet@49158
   111
       CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2"
blanchet@51804
   112
and ('c, 'e, 'g) coind_wit2 =
blanchet@49158
   113
       CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g
blanchet@51804
   114
and ('c, 'e, 'g) ind_wit =
blanchet@49158
   115
       IW1 | IW2 'c
traytel@49102
   116
blanchet@51804
   117
codatatype ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
blanchet@51804
   118
codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
traytel@49185
   119
blanchet@58332
   120
codatatype (dead 'a) dead_foo = A
blanchet@58332
   121
codatatype ('a, 'b) use_dead_foo = Y 'a "'b dead_foo"
blanchet@58332
   122
blanchet@58332
   123
codatatype 'a phantom = A
blanchet@58332
   124
codatatype 'a use_phantom = Y 'a "'a use_phantom phantom"
traytel@49185
   125
blanchet@48975
   126
(* SLOW, MEMORY-HUNGRY
blanchet@51804
   127
codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
blanchet@51804
   128
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
blanchet@51804
   129
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
blanchet@51804
   130
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
blanchet@51804
   131
and ('a, 'c) D5 = A5 "('a, 'c) D6"
blanchet@51804
   132
and ('a, 'c) D6 = A6 "('a, 'c) D7"
blanchet@51804
   133
and ('a, 'c) D7 = A7 "('a, 'c) D8"
blanchet@51804
   134
and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
blanchet@48975
   135
*)
blanchet@48975
   136
blanchet@48975
   137
end