src/HOL/Datatype.thy
changeset 11954 3d1780208bf3
parent 10212 33fe2d701ddd
child 12029 7df1d840d01d
     1.1 --- a/src/HOL/Datatype.thy	Fri Oct 26 23:59:13 2001 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sat Oct 27 00:00:05 2001 +0200
     1.3 @@ -1,25 +1,95 @@
     1.4  (*  Title:      HOL/Datatype.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer
     1.7 -    Copyright   1998  TU Muenchen
     1.8 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  *)
    1.11  
    1.12 -Datatype = Datatype_Universe +
    1.13 +header {* Datatype package setup -- final stage *}
    1.14 +
    1.15 +theory Datatype = Datatype_Universe:
    1.16 +
    1.17 +(*belongs to theory Datatype_Universe; hides popular names *)
    1.18 +hide const Node Atom Leaf Numb Lim Funs Split Case
    1.19 +hide type node item
    1.20 +
    1.21 +
    1.22 +subsection {* Representing primitive types *}
    1.23  
    1.24  rep_datatype bool
    1.25 -  distinct True_not_False, False_not_True
    1.26 -  induct   bool_induct
    1.27 +  distinct True_not_False False_not_True
    1.28 +  induction bool_induct
    1.29 +
    1.30 +declare case_split [cases type: bool]
    1.31 +  -- "prefer plain propositional version"
    1.32 +
    1.33  
    1.34  rep_datatype sum
    1.35 -  distinct Inl_not_Inr, Inr_not_Inl
    1.36 -  inject   Inl_eq, Inr_eq
    1.37 -  induct   sum_induct
    1.38 +  distinct Inl_not_Inr Inr_not_Inl
    1.39 +  inject Inl_eq Inr_eq
    1.40 +  induction sum_induct
    1.41 +
    1.42 +rep_datatype unit
    1.43 +  induction unit_induct
    1.44  
    1.45  rep_datatype prod
    1.46 -  inject   Pair_eq
    1.47 -  induct   prod_induct
    1.48 +  inject Pair_eq
    1.49 +  induction prod_induct
    1.50 +
    1.51 +text {* Further cases/induct rules for 3--7 tuples. *}
    1.52 +
    1.53 +lemma prod_cases3 [case_names fields, cases type]:
    1.54 +    "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.55 +  apply (cases y)
    1.56 +  apply (case_tac b)
    1.57 +  apply blast
    1.58 +  done
    1.59 +
    1.60 +lemma prod_induct3 [case_names fields, induct type]:
    1.61 +    "(!!a b c. P (a, b, c)) ==> P x"
    1.62 +  by (cases x) blast
    1.63 +
    1.64 +lemma prod_cases4 [case_names fields, cases type]:
    1.65 +    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.66 +  apply (cases y)
    1.67 +  apply (case_tac c)
    1.68 +  apply blast
    1.69 +  done
    1.70 +
    1.71 +lemma prod_induct4 [case_names fields, induct type]:
    1.72 +    "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.73 +  by (cases x) blast
    1.74  
    1.75 -rep_datatype unit
    1.76 -  induct   unit_induct
    1.77 +lemma prod_cases5 [case_names fields, cases type]:
    1.78 +    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.79 +  apply (cases y)
    1.80 +  apply (case_tac d)
    1.81 +  apply blast
    1.82 +  done
    1.83 +
    1.84 +lemma prod_induct5 [case_names fields, induct type]:
    1.85 +    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.86 +  by (cases x) blast
    1.87 +
    1.88 +lemma prod_cases6 [case_names fields, cases type]:
    1.89 +    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.90 +  apply (cases y)
    1.91 +  apply (case_tac e)
    1.92 +  apply blast
    1.93 +  done
    1.94 +
    1.95 +lemma prod_induct6 [case_names fields, induct type]:
    1.96 +    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.97 +  by (cases x) blast
    1.98 +
    1.99 +lemma prod_cases7 [case_names fields, cases type]:
   1.100 +    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
   1.101 +  apply (cases y)
   1.102 +  apply (case_tac f)
   1.103 +  apply blast
   1.104 +  done
   1.105 +
   1.106 +lemma prod_induct7 [case_names fields, induct type]:
   1.107 +    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.108 +  by (cases x) blast
   1.109  
   1.110  end