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