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