src/HOL/Datatype.thy
author wenzelm
Sat Oct 27 00:00:05 2001 +0200 (2001-10-27)
changeset 11954 3d1780208bf3
parent 10212 33fe2d701ddd
child 12029 7df1d840d01d
permissions -rw-r--r--
made new-style theory;
tuned;
berghofe@5181
     1
(*  Title:      HOL/Datatype.thy
berghofe@5181
     2
    ID:         $Id$
wenzelm@11954
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@11954
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@5181
     5
*)
berghofe@5181
     6
wenzelm@11954
     7
header {* Datatype package setup -- final stage *}
wenzelm@11954
     8
wenzelm@11954
     9
theory Datatype = Datatype_Universe:
wenzelm@11954
    10
wenzelm@11954
    11
(*belongs to theory Datatype_Universe; hides popular names *)
wenzelm@11954
    12
hide const Node Atom Leaf Numb Lim Funs Split Case
wenzelm@11954
    13
hide type node item
wenzelm@11954
    14
wenzelm@11954
    15
wenzelm@11954
    16
subsection {* Representing primitive types *}
berghofe@5181
    17
berghofe@5759
    18
rep_datatype bool
wenzelm@11954
    19
  distinct True_not_False False_not_True
wenzelm@11954
    20
  induction bool_induct
wenzelm@11954
    21
wenzelm@11954
    22
declare case_split [cases type: bool]
wenzelm@11954
    23
  -- "prefer plain propositional version"
wenzelm@11954
    24
berghofe@5759
    25
berghofe@5181
    26
rep_datatype sum
wenzelm@11954
    27
  distinct Inl_not_Inr Inr_not_Inl
wenzelm@11954
    28
  inject Inl_eq Inr_eq
wenzelm@11954
    29
  induction sum_induct
wenzelm@11954
    30
wenzelm@11954
    31
rep_datatype unit
wenzelm@11954
    32
  induction unit_induct
berghofe@5181
    33
berghofe@5181
    34
rep_datatype prod
wenzelm@11954
    35
  inject Pair_eq
wenzelm@11954
    36
  induction prod_induct
wenzelm@11954
    37
wenzelm@11954
    38
text {* Further cases/induct rules for 3--7 tuples. *}
wenzelm@11954
    39
wenzelm@11954
    40
lemma prod_cases3 [case_names fields, cases type]:
wenzelm@11954
    41
    "(!!a b c. y = (a, b, c) ==> P) ==> P"
wenzelm@11954
    42
  apply (cases y)
wenzelm@11954
    43
  apply (case_tac b)
wenzelm@11954
    44
  apply blast
wenzelm@11954
    45
  done
wenzelm@11954
    46
wenzelm@11954
    47
lemma prod_induct3 [case_names fields, induct type]:
wenzelm@11954
    48
    "(!!a b c. P (a, b, c)) ==> P x"
wenzelm@11954
    49
  by (cases x) blast
wenzelm@11954
    50
wenzelm@11954
    51
lemma prod_cases4 [case_names fields, cases type]:
wenzelm@11954
    52
    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
wenzelm@11954
    53
  apply (cases y)
wenzelm@11954
    54
  apply (case_tac c)
wenzelm@11954
    55
  apply blast
wenzelm@11954
    56
  done
wenzelm@11954
    57
wenzelm@11954
    58
lemma prod_induct4 [case_names fields, induct type]:
wenzelm@11954
    59
    "(!!a b c d. P (a, b, c, d)) ==> P x"
wenzelm@11954
    60
  by (cases x) blast
berghofe@5181
    61
wenzelm@11954
    62
lemma prod_cases5 [case_names fields, cases type]:
wenzelm@11954
    63
    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
wenzelm@11954
    64
  apply (cases y)
wenzelm@11954
    65
  apply (case_tac d)
wenzelm@11954
    66
  apply blast
wenzelm@11954
    67
  done
wenzelm@11954
    68
wenzelm@11954
    69
lemma prod_induct5 [case_names fields, induct type]:
wenzelm@11954
    70
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
wenzelm@11954
    71
  by (cases x) blast
wenzelm@11954
    72
wenzelm@11954
    73
lemma prod_cases6 [case_names fields, cases type]:
wenzelm@11954
    74
    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
wenzelm@11954
    75
  apply (cases y)
wenzelm@11954
    76
  apply (case_tac e)
wenzelm@11954
    77
  apply blast
wenzelm@11954
    78
  done
wenzelm@11954
    79
wenzelm@11954
    80
lemma prod_induct6 [case_names fields, induct type]:
wenzelm@11954
    81
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
wenzelm@11954
    82
  by (cases x) blast
wenzelm@11954
    83
wenzelm@11954
    84
lemma prod_cases7 [case_names fields, cases type]:
wenzelm@11954
    85
    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
wenzelm@11954
    86
  apply (cases y)
wenzelm@11954
    87
  apply (case_tac f)
wenzelm@11954
    88
  apply blast
wenzelm@11954
    89
  done
wenzelm@11954
    90
wenzelm@11954
    91
lemma prod_induct7 [case_names fields, induct type]:
wenzelm@11954
    92
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
wenzelm@11954
    93
  by (cases x) blast
berghofe@5759
    94
berghofe@5181
    95
end