src/HOL/Inductive.thy
author berghofe
Tue May 22 15:10:06 2001 +0200 (2001-05-22)
changeset 11325 a5e0289dd56c
parent 11003 ee0838d89deb
child 11436 3f74b80d979f
permissions -rw-r--r--
Inductive definitions are now introduced earlier in the theory hierarchy.
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Setup packages for inductive sets and types etc.
     7 *)
     8 
     9 theory Inductive = Gfp + Sum_Type + Relation
    10 files
    11   ("Tools/induct_method.ML")
    12   ("Tools/inductive_package.ML")
    13   ("Tools/datatype_aux.ML")
    14   ("Tools/datatype_prop.ML")
    15   ("Tools/datatype_rep_proofs.ML")
    16   ("Tools/datatype_abs_proofs.ML")
    17   ("Tools/datatype_package.ML")
    18   ("Tools/primrec_package.ML"):
    19 
    20 
    21 (* handling of proper rules *)
    22 
    23 constdefs
    24   forall :: "('a => bool) => bool"
    25   "forall P == \<forall>x. P x"
    26   implies :: "bool => bool => bool"
    27   "implies A B == A --> B"
    28   equal :: "'a => 'a => bool"
    29   "equal x y == x = y"
    30   conj :: "bool => bool => bool"
    31   "conj A B == A & B"
    32 
    33 lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
    34   by (simp only: atomize_all forall_def)
    35 
    36 lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
    37   by (simp only: atomize_imp implies_def)
    38 
    39 lemma equal_eq: "(x == y) == Trueprop (equal x y)"
    40   by (simp only: atomize_eq equal_def)
    41 
    42 lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
    43   by (unfold forall_def conj_def) blast
    44 
    45 lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
    46   by (unfold implies_def conj_def) blast
    47 
    48 lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
    49   by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
    50 
    51 lemmas inductive_atomize = forall_eq implies_eq equal_eq
    52 lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
    53 lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
    54 lemmas inductive_conj = forall_conj implies_conj conj_curry
    55 
    56 hide const forall implies equal conj
    57 
    58 
    59 (* setup packages *)
    60 
    61 use "Tools/induct_method.ML"
    62 setup InductMethod.setup
    63 
    64 use "Tools/inductive_package.ML"
    65 setup InductivePackage.setup
    66 
    67 use "Tools/datatype_aux.ML"
    68 use "Tools/datatype_prop.ML"
    69 use "Tools/datatype_rep_proofs.ML"
    70 use "Tools/datatype_abs_proofs.ML"
    71 use "Tools/datatype_package.ML"
    72 setup DatatypePackage.setup
    73 
    74 use "Tools/primrec_package.ML"
    75 setup PrimrecPackage.setup
    76 
    77 theorems basic_monos [mono] =
    78   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    79   Collect_mono in_mono vimage_mono
    80   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    81   not_all not_ex
    82   Ball_def Bex_def
    83   inductive_rulify2
    84 
    85 end