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