src/HOL/BNF_Examples/Misc_Codatatype.thy
author blanchet
Fri Jan 24 11:51:45 2014 +0100 (2014-01-24)
changeset 55129 26bd1cba3ab5
parent 55076 1e73e090a514
child 55484 9deb5066508f
permissions -rw-r--r--
killed 'More_BNFs' by moving its various bits where they (now) belong
     1 (*  Title:      HOL/BNF_Examples/Misc_Codatatype.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 codatatype definitions.
     8 *)
     9 
    10 header {* Miscellaneous Codatatype Definitions *}
    11 
    12 theory Misc_Codatatype
    13 imports "~~/src/HOL/Library/FSet"
    14 begin
    15 
    16 codatatype simple = X1 | X2 | X3 | X4
    17 
    18 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit
    19 
    20 codatatype simple'' = X1'' nat int | X2''
    21 
    22 codatatype 'a stream = Stream (shd: 'a) (stl: "'a stream")
    23 
    24 codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
    25 
    26 codatatype ('b, 'c, 'd, 'e) some_passive =
    27   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
    28 
    29 codatatype lambda =
    30   Var string |
    31   App lambda lambda |
    32   Abs string lambda |
    33   Let "(string \<times> lambda) fset" lambda
    34 
    35 codatatype '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 codatatype 'a p = P "'a + 'a p"
    47 
    48 codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
    49 and 'a J2 = J21 | J22 "'a J1" "'a J2"
    50 
    51 codatatype 'a tree = TEmpty | TNode 'a "'a forest"
    52 and 'a forest = FNil | FCons "'a tree" "'a forest"
    53 
    54 codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
    55 and 'a branch = Branch 'a "'a tree'"
    56 
    57 codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
    58 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
    59 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
    60 
    61 codatatype ('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 codatatype ('a, 'b, 'c) some_killing' =
    67   SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'"
    68 and ('a, 'b, 'c) in_here' =
    69   IH1' 'b | IH2' 'c
    70 
    71 codatatype ('a, 'b, 'c) some_killing'' =
    72   SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''"
    73 and ('a, 'b, 'c) in_here'' =
    74   IH1'' 'b 'a | IH2'' 'c
    75 
    76 codatatype ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
    77 
    78 codatatype 'b poly_unit = U "'b \<Rightarrow> 'b poly_unit"
    79 codatatype 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
    80 
    81 codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
    82   FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow>
    83       ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs"
    84 
    85 codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
    86         'b18, 'b19, 'b20) fun_rhs' =
    87   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>
    88        'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow>
    89        ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
    90         'b18, 'b19, 'b20) fun_rhs'"
    91 
    92 codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2"
    93 and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2"
    94 and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1"
    95 
    96 codatatype ('c, 'e, 'g) coind_wit1 =
    97        CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2"
    98 and ('c, 'e, 'g) coind_wit2 =
    99        CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g
   100 and ('c, 'e, 'g) ind_wit =
   101        IW1 | IW2 'c
   102 
   103 codatatype ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
   104 codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
   105 
   106 codatatype 'a dead_foo = A
   107 codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
   108 
   109 (* SLOW, MEMORY-HUNGRY
   110 codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
   111 and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
   112 and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
   113 and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
   114 and ('a, 'c) D5 = A5 "('a, 'c) D6"
   115 and ('a, 'c) D6 = A6 "('a, 'c) D7"
   116 and ('a, 'c) D7 = A7 "('a, 'c) D8"
   117 and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
   118 *)
   119 
   120 end