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;
     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 {* Datatype package setup -- final stage *}
     8 
     9 theory Datatype = Datatype_Universe:
    10 
    11 (*belongs to theory 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 
    26 rep_datatype sum
    27   distinct Inl_not_Inr Inr_not_Inl
    28   inject Inl_eq Inr_eq
    29   induction sum_induct
    30 
    31 rep_datatype unit
    32   induction unit_induct
    33 
    34 rep_datatype prod
    35   inject Pair_eq
    36   induction prod_induct
    37 
    38 text {* Further cases/induct rules for 3--7 tuples. *}
    39 
    40 lemma prod_cases3 [case_names fields, cases type]:
    41     "(!!a b c. y = (a, b, c) ==> P) ==> P"
    42   apply (cases y)
    43   apply (case_tac b)
    44   apply blast
    45   done
    46 
    47 lemma prod_induct3 [case_names fields, induct type]:
    48     "(!!a b c. P (a, b, c)) ==> P x"
    49   by (cases x) blast
    50 
    51 lemma prod_cases4 [case_names fields, cases type]:
    52     "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    53   apply (cases y)
    54   apply (case_tac c)
    55   apply blast
    56   done
    57 
    58 lemma prod_induct4 [case_names fields, induct type]:
    59     "(!!a b c d. P (a, b, c, d)) ==> P x"
    60   by (cases x) blast
    61 
    62 lemma prod_cases5 [case_names fields, cases type]:
    63     "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    64   apply (cases y)
    65   apply (case_tac d)
    66   apply blast
    67   done
    68 
    69 lemma prod_induct5 [case_names fields, induct type]:
    70     "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    71   by (cases x) blast
    72 
    73 lemma prod_cases6 [case_names fields, cases type]:
    74     "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    75   apply (cases y)
    76   apply (case_tac e)
    77   apply blast
    78   done
    79 
    80 lemma prod_induct6 [case_names fields, induct type]:
    81     "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    82   by (cases x) blast
    83 
    84 lemma prod_cases7 [case_names fields, cases type]:
    85     "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    86   apply (cases y)
    87   apply (case_tac f)
    88   apply blast
    89   done
    90 
    91 lemma prod_induct7 [case_names fields, induct type]:
    92     "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    93   by (cases x) blast
    94 
    95 end