src/HOL/Datatype.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 14981 e73f8140af78
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/Datatype.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 (** legacy ML bindings **)
     7 
     8 structure bool =
     9 struct
    10   val distinct = thms "bool.distinct";
    11   val inject = thms "bool.inject";
    12   val exhaust = thm "bool.exhaust";
    13   val cases = thms "bool.cases";
    14   val split = thm "bool.split";
    15   val split_asm = thm "bool.split_asm";
    16   val induct = thm "bool.induct";
    17   val recs = thms "bool.recs";
    18   val simps = thms "bool.simps";
    19   val size = thms "bool.size";
    20 end;
    21 
    22 structure sum =
    23 struct
    24   val distinct = thms "sum.distinct";
    25   val inject = thms "sum.inject";
    26   val exhaust = thm "sum.exhaust";
    27   val cases = thms "sum.cases";
    28   val split = thm "sum.split";
    29   val split_asm = thm "sum.split_asm";
    30   val induct = thm "sum.induct";
    31   val recs = thms "sum.recs";
    32   val simps = thms "sum.simps";
    33   val size = thms "sum.size";
    34 end;
    35 
    36 structure unit =
    37 struct
    38   val distinct = thms "unit.distinct";
    39   val inject = thms "unit.inject";
    40   val exhaust = thm "unit.exhaust";
    41   val cases = thms "unit.cases";
    42   val split = thm "unit.split";
    43   val split_asm = thm "unit.split_asm";
    44   val induct = thm "unit.induct";
    45   val recs = thms "unit.recs";
    46   val simps = thms "unit.simps";
    47   val size = thms "unit.size";
    48 end;
    49 
    50 structure prod =
    51 struct
    52   val distinct = thms "prod.distinct";
    53   val inject = thms "prod.inject";
    54   val exhaust = thm "prod.exhaust";
    55   val cases = thms "prod.cases";
    56   val split = thm "prod.split";
    57   val split_asm = thm "prod.split_asm";
    58   val induct = thm "prod.induct";
    59   val recs = thms "prod.recs";
    60   val simps = thms "prod.simps";
    61   val size = thms "prod.size";
    62 end;
    63 
    64 structure option =
    65 struct
    66   val distinct = thms "option.distinct";
    67   val inject = thms "option.inject";
    68   val exhaust = thm "option.exhaust";
    69   val cases = thms "option.cases";
    70   val split = thm "option.split";
    71   val split_asm = thm "option.split_asm";
    72   val induct = thm "option.induct";
    73   val recs = thms "option.recs";
    74   val simps = thms "option.simps";
    75   val size = thms "option.size";
    76 end;
    77 
    78 val elem_o2s = thm "elem_o2s";
    79 val not_None_eq = thm "not_None_eq";
    80 val not_Some_eq = thm "not_Some_eq";
    81 val o2s_empty_eq = thm "o2s_empty_eq";
    82 val option_caseE = thm "option_caseE";
    83 val option_map_None = thm "option_map_None";
    84 val option_map_Some = thm "option_map_Some";
    85 val option_map_def = thm "option_map_def";
    86 val option_map_eq_Some = thm "option_map_eq_Some";
    87 val option_map_o_sum_case = thm "option_map_o_sum_case";
    88 val ospec = thm "ospec";
    89 val sum_case_inject = thm "sum_case_inject";
    90 val sum_case_weak_cong = thm "sum_case_weak_cong";
    91 val surjective_sum = thm "surjective_sum";