inductive_atomize, inductive_rulify;
authorwenzelm
Mon Nov 06 22:49:16 2000 +0100 (2000-11-06)
changeset 104025e82d6cafb5f
parent 10401 58bb50f69497
child 10403 2955ee2424ce
inductive_atomize, inductive_rulify;
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Mon Nov 06 22:48:42 2000 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Nov 06 22:49:16 2000 +0100
     1.3 @@ -1,21 +1,62 @@
     1.4  (*  Title:      HOL/Inductive.thy
     1.5      ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7  *)
     1.8  
     1.9  theory Inductive = Gfp + Sum_Type + NatDef
    1.10  files
    1.11 -  "Tools/induct_method.ML"
    1.12 -  "Tools/inductive_package.ML"
    1.13 -  "Tools/datatype_aux.ML"
    1.14 -  "Tools/datatype_prop.ML"
    1.15 -  "Tools/datatype_rep_proofs.ML"
    1.16 -  "Tools/datatype_abs_proofs.ML"
    1.17 -  "Tools/datatype_package.ML"
    1.18 -  "Tools/primrec_package.ML":
    1.19 +  ("Tools/induct_method.ML")
    1.20 +  ("Tools/inductive_package.ML")
    1.21 +  ("Tools/datatype_aux.ML")
    1.22 +  ("Tools/datatype_prop.ML")
    1.23 +  ("Tools/datatype_rep_proofs.ML")
    1.24 +  ("Tools/datatype_abs_proofs.ML")
    1.25 +  ("Tools/datatype_package.ML")
    1.26 +  ("Tools/primrec_package.ML"):
    1.27 +
    1.28 +constdefs
    1.29 +  forall :: "('a => bool) => bool"
    1.30 +  "forall P == \<forall>x. P x"
    1.31 +  implies :: "bool => bool => bool"
    1.32 +  "implies A B == A --> B"
    1.33 +
    1.34 +lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
    1.35 +proof
    1.36 +  assume "!!x. P x"
    1.37 +  thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast
    1.38 +next
    1.39 +  fix x
    1.40 +  assume "forall (\<lambda>x. P x)"
    1.41 +  thus "P x" by (unfold forall_def) blast
    1.42 +qed
    1.43  
    1.44 +lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
    1.45 +proof
    1.46 +  assume "A ==> B"
    1.47 +  thus "implies A B" by (unfold implies_def) blast
    1.48 +next
    1.49 +  assume "implies A B" and A
    1.50 +  thus B by (unfold implies_def) blast
    1.51 +qed
    1.52 +
    1.53 +lemmas inductive_atomize = forall_eq implies_eq
    1.54 +lemmas inductive_rulify = inductive_atomize [symmetric, standard]
    1.55 +hide const forall implies
    1.56 +
    1.57 +use "Tools/induct_method.ML"
    1.58  setup InductMethod.setup
    1.59 +
    1.60 +use "Tools/inductive_package.ML"
    1.61  setup InductivePackage.setup
    1.62 +
    1.63 +use "Tools/datatype_aux.ML"
    1.64 +use "Tools/datatype_prop.ML"
    1.65 +use "Tools/datatype_rep_proofs.ML"
    1.66 +use "Tools/datatype_abs_proofs.ML"
    1.67 +use "Tools/datatype_package.ML"
    1.68  setup DatatypePackage.setup
    1.69 +
    1.70 +use "Tools/primrec_package.ML"
    1.71  setup PrimrecPackage.setup
    1.72  
    1.73  theorems basic_monos [mono] =