src/HOL/Datatype.thy
author wenzelm
Sat Nov 03 01:40:28 2001 +0100 (2001-11-03)
changeset 12029 7df1d840d01d
parent 11954 3d1780208bf3
child 12918 bca45be2d25b
permissions -rw-r--r--
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@12029
     7
header {* Final stage of datatype setup *}
wenzelm@11954
     8
wenzelm@11954
     9
theory Datatype = Datatype_Universe:
wenzelm@11954
    10
wenzelm@12029
    11
text {* Belongs to theory @{text 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@5181
    25
rep_datatype sum
wenzelm@11954
    26
  distinct Inl_not_Inr Inr_not_Inl
wenzelm@11954
    27
  inject Inl_eq Inr_eq
wenzelm@11954
    28
  induction sum_induct
wenzelm@11954
    29
wenzelm@11954
    30
rep_datatype unit
wenzelm@11954
    31
  induction unit_induct
berghofe@5181
    32
berghofe@5181
    33
rep_datatype prod
wenzelm@11954
    34
  inject Pair_eq
wenzelm@11954
    35
  induction prod_induct
wenzelm@11954
    36
wenzelm@11954
    37
text {* Further cases/induct rules for 3--7 tuples. *}
wenzelm@11954
    38
wenzelm@11954
    39
lemma prod_cases3 [case_names fields, cases type]:
wenzelm@11954
    40
    "(!!a b c. y = (a, b, c) ==> P) ==> P"
wenzelm@11954
    41
  apply (cases y)
wenzelm@11954
    42
  apply (case_tac b)
wenzelm@11954
    43
  apply blast
wenzelm@11954
    44
  done
wenzelm@11954
    45
wenzelm@11954
    46
lemma prod_induct3 [case_names fields, induct type]:
wenzelm@11954
    47
    "(!!a b c. P (a, b, c)) ==> P x"
wenzelm@11954
    48
  by (cases x) blast
wenzelm@11954
    49
wenzelm@11954
    50
lemma prod_cases4 [case_names fields, cases type]:
wenzelm@11954
    51
    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
wenzelm@11954
    52
  apply (cases y)
wenzelm@11954
    53
  apply (case_tac c)
wenzelm@11954
    54
  apply blast
wenzelm@11954
    55
  done
wenzelm@11954
    56
wenzelm@11954
    57
lemma prod_induct4 [case_names fields, induct type]:
wenzelm@11954
    58
    "(!!a b c d. P (a, b, c, d)) ==> P x"
wenzelm@11954
    59
  by (cases x) blast
berghofe@5181
    60
wenzelm@11954
    61
lemma prod_cases5 [case_names fields, cases type]:
wenzelm@11954
    62
    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
wenzelm@11954
    63
  apply (cases y)
wenzelm@11954
    64
  apply (case_tac d)
wenzelm@11954
    65
  apply blast
wenzelm@11954
    66
  done
wenzelm@11954
    67
wenzelm@11954
    68
lemma prod_induct5 [case_names fields, induct type]:
wenzelm@11954
    69
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
wenzelm@11954
    70
  by (cases x) blast
wenzelm@11954
    71
wenzelm@11954
    72
lemma prod_cases6 [case_names fields, cases type]:
wenzelm@11954
    73
    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
wenzelm@11954
    74
  apply (cases y)
wenzelm@11954
    75
  apply (case_tac e)
wenzelm@11954
    76
  apply blast
wenzelm@11954
    77
  done
wenzelm@11954
    78
wenzelm@11954
    79
lemma prod_induct6 [case_names fields, induct type]:
wenzelm@11954
    80
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
wenzelm@11954
    81
  by (cases x) blast
wenzelm@11954
    82
wenzelm@11954
    83
lemma prod_cases7 [case_names fields, cases type]:
wenzelm@11954
    84
    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
wenzelm@11954
    85
  apply (cases y)
wenzelm@11954
    86
  apply (case_tac f)
wenzelm@11954
    87
  apply blast
wenzelm@11954
    88
  done
wenzelm@11954
    89
wenzelm@11954
    90
lemma prod_induct7 [case_names fields, induct type]:
wenzelm@11954
    91
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
wenzelm@11954
    92
  by (cases x) blast
berghofe@5759
    93
berghofe@5181
    94
end