src/HOL/Datatype.ML
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 12918 bca45be2d25b
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Datatype.ML
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     4
*)
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     5
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
     6
(** legacy ML bindings **)
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
     7
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
     8
structure bool =
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
     9
struct
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    10
  val distinct = thms "bool.distinct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    11
  val inject = thms "bool.inject";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    12
  val exhaust = thm "bool.exhaust";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    13
  val cases = thms "bool.cases";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    14
  val split = thm "bool.split";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    15
  val split_asm = thm "bool.split_asm";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    16
  val induct = thm "bool.induct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    17
  val recs = thms "bool.recs";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    18
  val simps = thms "bool.simps";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    19
  val size = thms "bool.size";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    20
end;
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    21
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    22
structure sum =
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    23
struct
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    24
  val distinct = thms "sum.distinct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    25
  val inject = thms "sum.inject";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    26
  val exhaust = thm "sum.exhaust";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    27
  val cases = thms "sum.cases";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    28
  val split = thm "sum.split";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    29
  val split_asm = thm "sum.split_asm";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    30
  val induct = thm "sum.induct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    31
  val recs = thms "sum.recs";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    32
  val simps = thms "sum.simps";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    33
  val size = thms "sum.size";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    34
end;
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    35
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    36
structure unit =
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    37
struct
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    38
  val distinct = thms "unit.distinct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    39
  val inject = thms "unit.inject";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    40
  val exhaust = thm "unit.exhaust";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    41
  val cases = thms "unit.cases";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    42
  val split = thm "unit.split";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    43
  val split_asm = thm "unit.split_asm";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    44
  val induct = thm "unit.induct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    45
  val recs = thms "unit.recs";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    46
  val simps = thms "unit.simps";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    47
  val size = thms "unit.size";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    48
end;
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    49
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    50
structure prod =
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    51
struct
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    52
  val distinct = thms "prod.distinct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    53
  val inject = thms "prod.inject";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    54
  val exhaust = thm "prod.exhaust";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    55
  val cases = thms "prod.cases";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    56
  val split = thm "prod.split";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    57
  val split_asm = thm "prod.split_asm";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    58
  val induct = thm "prod.induct";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    59
  val recs = thms "prod.recs";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    60
  val simps = thms "prod.simps";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    61
  val size = thms "prod.size";
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    62
end;
3d1780208bf3 made new-style theory;
wenzelm
parents: 9108
diff changeset
    63
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    64
structure option =
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    65
struct
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    66
  val distinct = thms "option.distinct";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    67
  val inject = thms "option.inject";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    68
  val exhaust = thm "option.exhaust";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    69
  val cases = thms "option.cases";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    70
  val split = thm "option.split";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    71
  val split_asm = thm "option.split_asm";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    72
  val induct = thm "option.induct";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    73
  val recs = thms "option.recs";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    74
  val simps = thms "option.simps";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    75
  val size = thms "option.size";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    76
end;
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    77
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    78
val elem_o2s = thm "elem_o2s";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    79
val not_None_eq = thm "not_None_eq";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    80
val not_Some_eq = thm "not_Some_eq";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    81
val o2s_empty_eq = thm "o2s_empty_eq";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    82
val option_caseE = thm "option_caseE";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    83
val option_map_None = thm "option_map_None";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    84
val option_map_Some = thm "option_map_Some";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    85
val option_map_def = thm "option_map_def";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    86
val option_map_eq_Some = thm "option_map_eq_Some";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    87
val option_map_o_sum_case = thm "option_map_o_sum_case";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    88
val ospec = thm "ospec";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    89
val sum_case_inject = thm "sum_case_inject";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    90
val sum_case_weak_cong = thm "sum_case_weak_cong";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 11954
diff changeset
    91
val surjective_sum = thm "surjective_sum";