src/HOL/Inductive.thy
author wenzelm
Fri Nov 10 19:03:55 2000 +0100 (2000-11-10)
changeset 10434 6ea4735c3955
parent 10402 5e82d6cafb5f
child 10727 2ccafccb81c0
permissions -rw-r--r--
simplified atomize;
added inductive_rulify2 (to accomodate malformed induction rules);
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 theory Inductive = Gfp + Sum_Type + NatDef
     7 files
     8   ("Tools/induct_method.ML")
     9   ("Tools/inductive_package.ML")
    10   ("Tools/datatype_aux.ML")
    11   ("Tools/datatype_prop.ML")
    12   ("Tools/datatype_rep_proofs.ML")
    13   ("Tools/datatype_abs_proofs.ML")
    14   ("Tools/datatype_package.ML")
    15   ("Tools/primrec_package.ML"):
    16 
    17 constdefs
    18   forall :: "('a => bool) => bool"
    19   "forall P == \<forall>x. P x"
    20   implies :: "bool => bool => bool"
    21   "implies A B == A --> B"
    22   equal :: "'a => 'a => bool"
    23   "equal x y == x = y"
    24 
    25 lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
    26   by (simp only: atomize_all forall_def)
    27 
    28 lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
    29   by (simp only: atomize_imp implies_def)
    30 
    31 lemma equal_eq: "(x == y) == Trueprop (equal x y)"
    32   by (simp only: atomize_eq equal_def)
    33 
    34 hide const forall implies equal
    35 
    36 lemmas inductive_atomize = forall_eq implies_eq equal_eq
    37 lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
    38 lemmas inductive_rulify2 = forall_def implies_def equal_def
    39 
    40 use "Tools/induct_method.ML"
    41 setup InductMethod.setup
    42 
    43 use "Tools/inductive_package.ML"
    44 setup InductivePackage.setup
    45 
    46 use "Tools/datatype_aux.ML"
    47 use "Tools/datatype_prop.ML"
    48 use "Tools/datatype_rep_proofs.ML"
    49 use "Tools/datatype_abs_proofs.ML"
    50 use "Tools/datatype_package.ML"
    51 setup DatatypePackage.setup
    52 
    53 use "Tools/primrec_package.ML"
    54 setup PrimrecPackage.setup
    55 
    56 theorems basic_monos [mono] =
    57    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
    58    Collect_mono in_mono vimage_mono
    59    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    60    not_all not_ex
    61    Ball_def Bex_def
    62 
    63 (*belongs to theory Transitive_Closure*)
    64 declare rtrancl_induct [induct set: rtrancl]
    65 declare rtranclE [cases set: rtrancl]
    66 declare trancl_induct [induct set: trancl]
    67 declare tranclE [cases set: trancl]
    68 
    69 end