src/HOL/Codatatype/Examples/Misc_Data.thy
author blanchet
Tue Aug 28 17:16:00 2012 +0200 (2012-08-28)
changeset 48975 7f79f94a432c
child 48980 debfa361f648
permissions -rw-r--r--
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet@48975
     1
(*  Title:      Codatatype_Examples/Misc_Data.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Miscellaneous datatype declarations.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
header {* Miscellaneous Datatype Declarations *}
blanchet@48975
    10
blanchet@48975
    11
theory Misc_Data
blanchet@48975
    12
imports "../Codatatype/Codatatype"
blanchet@48975
    13
begin
blanchet@48975
    14
blanchet@48975
    15
ML {* quick_and_dirty := false *}
blanchet@48975
    16
blanchet@48975
    17
ML {* PolyML.fullGC (); *}
blanchet@48975
    18
blanchet@48975
    19
bnf_data simple: 'a = "unit + unit + unit + unit"
blanchet@48975
    20
blanchet@48975
    21
bnf_data mylist: 'list = "unit + 'a \<times> 'list"
blanchet@48975
    22
blanchet@48975
    23
bnf_data some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
blanchet@48975
    24
blanchet@48975
    25
bnf_data lambda:
blanchet@48975
    26
  'trm = "string +
blanchet@48975
    27
          'trm \<times> 'trm +
blanchet@48975
    28
          string \<times> 'trm +
blanchet@48975
    29
          (string \<times> 'trm) fset \<times> 'trm"
blanchet@48975
    30
blanchet@48975
    31
bnf_data par_lambda:
blanchet@48975
    32
  'trm = "'a +
blanchet@48975
    33
          'trm \<times> 'trm +
blanchet@48975
    34
          'a \<times> 'trm +
blanchet@48975
    35
          ('a \<times> 'trm) fset \<times> 'trm"
blanchet@48975
    36
blanchet@48975
    37
(*
blanchet@48975
    38
  ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
blanchet@48975
    39
  ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
blanchet@48975
    40
*)
blanchet@48975
    41
blanchet@48975
    42
bnf_data F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
blanchet@48975
    43
and F2: 'b2 = "unit + 'b1 * 'b2"
blanchet@48975
    44
blanchet@48975
    45
(*
blanchet@48975
    46
  'a tree = Empty | Node of 'a * 'a forest      ('b = unit + 'a * 'c)
blanchet@48975
    47
  'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c)
blanchet@48975
    48
*)
blanchet@48975
    49
blanchet@48975
    50
bnf_data tree: 'tree = "unit + 'a \<times> 'forest"
blanchet@48975
    51
and forest: 'forest = "unit + 'tree \<times> 'forest"
blanchet@48975
    52
blanchet@48975
    53
(*
blanchet@48975
    54
  'a tree = Empty | Node of 'a branch * 'a branch ('b = unit + 'c * 'c)
blanchet@48975
    55
'  a branch = Branch of 'a * 'a tree              ('c = 'a * 'b)
blanchet@48975
    56
*)
blanchet@48975
    57
blanchet@48975
    58
bnf_data tree': 'tree = "unit + 'branch \<times> 'branch"
blanchet@48975
    59
and branch: 'branch = "'a \<times> 'tree"
blanchet@48975
    60
blanchet@48975
    61
(*
blanchet@48975
    62
  exp = Sum of term * exp          ('c = 'd + 'd * 'c)
blanchet@48975
    63
  term = Prod of factor * term     ('d = 'e + 'e * 'd)
blanchet@48975
    64
  factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c)
blanchet@48975
    65
*)
blanchet@48975
    66
blanchet@48975
    67
bnf_data EXPR: 'E = "'T + 'T \<times> 'E"
blanchet@48975
    68
and TERM: 'T = "'F + 'F \<times> 'T"
blanchet@48975
    69
and FACTOR: 'F = "'a + 'b + 'E"
blanchet@48975
    70
blanchet@48975
    71
bnf_data some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
blanchet@48975
    72
and in_here: 'c = "'d \<times> 'b + 'e"
blanchet@48975
    73
blanchet@48975
    74
bnf_data nofail1: 'a = "'a \<times> 'b + 'b"
blanchet@48975
    75
bnf_data nofail2: 'a = "('a \<times> 'b \<times> 'a \<times> 'b) list"
blanchet@48975
    76
bnf_data nofail3: 'a = "'b \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset"
blanchet@48975
    77
bnf_data nofail4: 'a = "('a \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset) list"
blanchet@48975
    78
blanchet@48975
    79
(*
blanchet@48975
    80
bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b list"
blanchet@48975
    81
bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b"
blanchet@48975
    82
bnf_data fail: 'a = "'a \<times> 'b + 'a"
blanchet@48975
    83
bnf_data fail: 'a = "'a \<times> 'b"
blanchet@48975
    84
*)
blanchet@48975
    85
blanchet@48975
    86
bnf_data L1: 'L1 = "'L2 list"
blanchet@48975
    87
and L2: 'L2 = "'L1 fset + 'L2"
blanchet@48975
    88
blanchet@48975
    89
bnf_data K1: 'K1 = "'K2"
blanchet@48975
    90
and K2: 'K2 = "'K3"
blanchet@48975
    91
and K3: 'K3 = "'K1 list"
blanchet@48975
    92
blanchet@48975
    93
bnf_data t1: 't1 = "'t3 + 't2"
blanchet@48975
    94
and t2: 't2 = "'t1"
blanchet@48975
    95
and t3: 't3 = "unit"
blanchet@48975
    96
blanchet@48975
    97
bnf_data t1': 't1 = "'t2 + 't3"
blanchet@48975
    98
and t2': 't2 = "'t1"
blanchet@48975
    99
and t3': 't3 = "unit"
blanchet@48975
   100
blanchet@48975
   101
(*
blanchet@48975
   102
bnf_data fail1: 'L1 = "'L2"
blanchet@48975
   103
and fail2: 'L2 = "'L3"
blanchet@48975
   104
and fail2: 'L3 = "'L1"
blanchet@48975
   105
blanchet@48975
   106
bnf_data fail1: 'L1 = "'L2 list \<times> 'L2"
blanchet@48975
   107
and fail2: 'L2 = "'L2 fset \<times> 'L3"
blanchet@48975
   108
and fail2: 'L3 = "'L1"
blanchet@48975
   109
blanchet@48975
   110
bnf_data fail1: 'L1 = "'L2 list \<times> 'L2"
blanchet@48975
   111
and fail2: 'L2 = "'L1 fset \<times> 'L1"
blanchet@48975
   112
*)
blanchet@48975
   113
(* SLOW
blanchet@48975
   114
bnf_data K1': 'K1 = "'K2 + 'a list"
blanchet@48975
   115
and K2': 'K2 = "'K3 + 'c fset"
blanchet@48975
   116
and K3': 'K3 = "'K3 + 'K4 + 'K4 \<times> 'K5"
blanchet@48975
   117
and K4': 'K4 = "'K5 + 'a list list list"
blanchet@48975
   118
and K5': 'K5 = "'K6"
blanchet@48975
   119
and K6': 'K6 = "'K7"
blanchet@48975
   120
and K7': 'K7 = "'K8"
blanchet@48975
   121
and K8': 'K8 = "'K1 list"
blanchet@48975
   122
blanchet@48975
   123
(*time comparison*)
blanchet@48975
   124
datatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
blanchet@48975
   125
     and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
blanchet@48975
   126
     and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
blanchet@48975
   127
     and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
blanchet@48975
   128
     and ('a, 'c) D5 = A5 "('a, 'c) D6"
blanchet@48975
   129
     and ('a, 'c) D6 = A6 "('a, 'c) D7"
blanchet@48975
   130
     and ('a, 'c) D7 = A7 "('a, 'c) D8"
blanchet@48975
   131
     and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
blanchet@48975
   132
*)
blanchet@48975
   133
blanchet@48975
   134
(* fail:
blanchet@48975
   135
bnf_data t1: 't1 = "'t2 * 't3 + 't2 * 't4"
blanchet@48975
   136
and t2: 't2 = "unit"
blanchet@48975
   137
and t3: 't3 = 't4
blanchet@48975
   138
and t4: 't4 = 't1
blanchet@48975
   139
*)
blanchet@48975
   140
blanchet@48975
   141
bnf_data k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4"
blanchet@48975
   142
and k2: 'k2 = unit
blanchet@48975
   143
and k3: 'k3 = 'k4
blanchet@48975
   144
and k4: 'k4 = unit
blanchet@48975
   145
blanchet@48975
   146
bnf_data tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4"
blanchet@48975
   147
and tt2: 'tt2 = unit
blanchet@48975
   148
and tt3: 'tt3 = 'tt1
blanchet@48975
   149
and tt4: 'tt4 = unit
blanchet@48975
   150
(* SLOW
blanchet@48975
   151
bnf_data s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2"
blanchet@48975
   152
and s2: 's2 = "'s7 * 's5 + 's5 * 's4 * 's6"
blanchet@48975
   153
and s3: 's3 = "'s1 * 's7 * 's2 + 's3 * 's3 + 's4 * 's5"
blanchet@48975
   154
and s4: 's4 = 's5
blanchet@48975
   155
and s5: 's5 = unit
blanchet@48975
   156
and s6: 's6 = "'s6 + 's1 * 's2 + 's6"
blanchet@48975
   157
and s7: 's7 = "'s8 + 's5"
blanchet@48975
   158
and s8: 's8 = nat
blanchet@48975
   159
*)
blanchet@48975
   160
blanchet@48975
   161
end