src/HOL/Datatype.ML
changeset 11954 3d1780208bf3
parent 9108 9fff97d29837
child 12918 bca45be2d25b
equal deleted inserted replaced
11953:f98623fdf6ef 11954:3d1780208bf3
     1 (*  Title:      HOL/Datatype.ML
     1 (*  Title:      HOL/Datatype.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4     Copyright   1999  TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     5 *)
       
     6 
       
     7 (** legacy ML bindings **)
       
     8 
       
     9 structure bool =
       
    10 struct
       
    11   val distinct = thms "bool.distinct";
       
    12   val inject = thms "bool.inject";
       
    13   val exhaust = thm "bool.exhaust";
       
    14   val cases = thms "bool.cases";
       
    15   val split = thm "bool.split";
       
    16   val split_asm = thm "bool.split_asm";
       
    17   val induct = thm "bool.induct";
       
    18   val recs = thms "bool.recs";
       
    19   val simps = thms "bool.simps";
       
    20   val size = thms "bool.size";
       
    21 end;
       
    22 
       
    23 structure sum =
       
    24 struct
       
    25   val distinct = thms "sum.distinct";
       
    26   val inject = thms "sum.inject";
       
    27   val exhaust = thm "sum.exhaust";
       
    28   val cases = thms "sum.cases";
       
    29   val split = thm "sum.split";
       
    30   val split_asm = thm "sum.split_asm";
       
    31   val induct = thm "sum.induct";
       
    32   val recs = thms "sum.recs";
       
    33   val simps = thms "sum.simps";
       
    34   val size = thms "sum.size";
       
    35 end;
       
    36 
       
    37 structure unit =
       
    38 struct
       
    39   val distinct = thms "unit.distinct";
       
    40   val inject = thms "unit.inject";
       
    41   val exhaust = thm "unit.exhaust";
       
    42   val cases = thms "unit.cases";
       
    43   val split = thm "unit.split";
       
    44   val split_asm = thm "unit.split_asm";
       
    45   val induct = thm "unit.induct";
       
    46   val recs = thms "unit.recs";
       
    47   val simps = thms "unit.simps";
       
    48   val size = thms "unit.size";
       
    49 end;
       
    50 
       
    51 structure prod =
       
    52 struct
       
    53   val distinct = thms "prod.distinct";
       
    54   val inject = thms "prod.inject";
       
    55   val exhaust = thm "prod.exhaust";
       
    56   val cases = thms "prod.cases";
       
    57   val split = thm "prod.split";
       
    58   val split_asm = thm "prod.split_asm";
       
    59   val induct = thm "prod.induct";
       
    60   val recs = thms "prod.recs";
       
    61   val simps = thms "prod.simps";
       
    62   val size = thms "prod.size";
       
    63 end;
       
    64 
     6 
    65 
     7 (** sum_case -- the selection operator for sums **)
    66 (** sum_case -- the selection operator for sums **)
     8 
    67 
     9 (*compatibility*)
    68 (*compatibility*)
    10 val [sum_case_Inl, sum_case_Inr] = sum.cases;
    69 val [sum_case_Inl, sum_case_Inr] = sum.cases;
    11 bind_thm ("sum_case_Inl", sum_case_Inl);
    70 bind_thm ("sum_case_Inl", sum_case_Inl);
    12 bind_thm ("sum_case_Inr", sum_case_Inr);
    71 bind_thm ("sum_case_Inr", sum_case_Inr);
    13 
    72 
    14 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    73 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    15 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    74 by (EVERY1 [res_inst_tac [("s","s")] sumE,
    16             etac ssubst, rtac sum_case_Inl,
    75             etac ssubst, rtac sum_case_Inl,
    17             etac ssubst, rtac sum_case_Inr]);
    76             etac ssubst, rtac sum_case_Inr]);
    18 qed "surjective_sum";
    77 qed "surjective_sum";
    19 
    78 
    20 (*Prevents simplification of f and g: much faster*)
    79 (*Prevents simplification of f and g: much faster*)