src/HOL/Datatype.ML
author wenzelm
Sat Oct 27 00:00:05 2001 +0200 (2001-10-27)
changeset 11954 3d1780208bf3
parent 9108 9fff97d29837
child 12918 bca45be2d25b
permissions -rw-r--r--
made new-style theory;
tuned;
berghofe@7293
     1
(*  Title:      HOL/Datatype.ML
berghofe@7293
     2
    ID:         $Id$
wenzelm@11954
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@11954
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@7293
     5
*)
berghofe@7293
     6
wenzelm@11954
     7
(** legacy ML bindings **)
wenzelm@11954
     8
wenzelm@11954
     9
structure bool =
wenzelm@11954
    10
struct
wenzelm@11954
    11
  val distinct = thms "bool.distinct";
wenzelm@11954
    12
  val inject = thms "bool.inject";
wenzelm@11954
    13
  val exhaust = thm "bool.exhaust";
wenzelm@11954
    14
  val cases = thms "bool.cases";
wenzelm@11954
    15
  val split = thm "bool.split";
wenzelm@11954
    16
  val split_asm = thm "bool.split_asm";
wenzelm@11954
    17
  val induct = thm "bool.induct";
wenzelm@11954
    18
  val recs = thms "bool.recs";
wenzelm@11954
    19
  val simps = thms "bool.simps";
wenzelm@11954
    20
  val size = thms "bool.size";
wenzelm@11954
    21
end;
wenzelm@11954
    22
wenzelm@11954
    23
structure sum =
wenzelm@11954
    24
struct
wenzelm@11954
    25
  val distinct = thms "sum.distinct";
wenzelm@11954
    26
  val inject = thms "sum.inject";
wenzelm@11954
    27
  val exhaust = thm "sum.exhaust";
wenzelm@11954
    28
  val cases = thms "sum.cases";
wenzelm@11954
    29
  val split = thm "sum.split";
wenzelm@11954
    30
  val split_asm = thm "sum.split_asm";
wenzelm@11954
    31
  val induct = thm "sum.induct";
wenzelm@11954
    32
  val recs = thms "sum.recs";
wenzelm@11954
    33
  val simps = thms "sum.simps";
wenzelm@11954
    34
  val size = thms "sum.size";
wenzelm@11954
    35
end;
wenzelm@11954
    36
wenzelm@11954
    37
structure unit =
wenzelm@11954
    38
struct
wenzelm@11954
    39
  val distinct = thms "unit.distinct";
wenzelm@11954
    40
  val inject = thms "unit.inject";
wenzelm@11954
    41
  val exhaust = thm "unit.exhaust";
wenzelm@11954
    42
  val cases = thms "unit.cases";
wenzelm@11954
    43
  val split = thm "unit.split";
wenzelm@11954
    44
  val split_asm = thm "unit.split_asm";
wenzelm@11954
    45
  val induct = thm "unit.induct";
wenzelm@11954
    46
  val recs = thms "unit.recs";
wenzelm@11954
    47
  val simps = thms "unit.simps";
wenzelm@11954
    48
  val size = thms "unit.size";
wenzelm@11954
    49
end;
wenzelm@11954
    50
wenzelm@11954
    51
structure prod =
wenzelm@11954
    52
struct
wenzelm@11954
    53
  val distinct = thms "prod.distinct";
wenzelm@11954
    54
  val inject = thms "prod.inject";
wenzelm@11954
    55
  val exhaust = thm "prod.exhaust";
wenzelm@11954
    56
  val cases = thms "prod.cases";
wenzelm@11954
    57
  val split = thm "prod.split";
wenzelm@11954
    58
  val split_asm = thm "prod.split_asm";
wenzelm@11954
    59
  val induct = thm "prod.induct";
wenzelm@11954
    60
  val recs = thms "prod.recs";
wenzelm@11954
    61
  val simps = thms "prod.simps";
wenzelm@11954
    62
  val size = thms "prod.size";
wenzelm@11954
    63
end;
wenzelm@11954
    64
wenzelm@11954
    65
berghofe@7293
    66
(** sum_case -- the selection operator for sums **)
berghofe@7293
    67
berghofe@7293
    68
(*compatibility*)
berghofe@7293
    69
val [sum_case_Inl, sum_case_Inr] = sum.cases;
wenzelm@9108
    70
bind_thm ("sum_case_Inl", sum_case_Inl);
wenzelm@9108
    71
bind_thm ("sum_case_Inr", sum_case_Inr);
berghofe@7293
    72
berghofe@7293
    73
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
wenzelm@11954
    74
by (EVERY1 [res_inst_tac [("s","s")] sumE,
berghofe@7293
    75
            etac ssubst, rtac sum_case_Inl,
berghofe@7293
    76
            etac ssubst, rtac sum_case_Inr]);
berghofe@7293
    77
qed "surjective_sum";
berghofe@7293
    78
berghofe@7293
    79
(*Prevents simplification of f and g: much faster*)
berghofe@7293
    80
Goal "s=t ==> sum_case f g s = sum_case f g t";
berghofe@7293
    81
by (etac arg_cong 1);
berghofe@7293
    82
qed "sum_case_weak_cong";
berghofe@7293
    83
berghofe@7293
    84
val [p1,p2] = Goal
berghofe@7293
    85
  "[| sum_case f1 f2 = sum_case g1 g2;  \
berghofe@7293
    86
\     [| f1 = g1; f2 = g2 |] ==> P |] \
berghofe@7293
    87
\  ==> P";
berghofe@7293
    88
by (rtac p2 1);
berghofe@7293
    89
by (rtac ext 1);
berghofe@7293
    90
by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
berghofe@7293
    91
by (Asm_full_simp_tac 1);
berghofe@7293
    92
by (rtac ext 1);
berghofe@7293
    93
by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
berghofe@7293
    94
by (Asm_full_simp_tac 1);
berghofe@7293
    95
qed "sum_case_inject";