--- a/src/HOL/Inductive.thy Mon Nov 06 22:48:42 2000 +0100
+++ b/src/HOL/Inductive.thy Mon Nov 06 22:49:16 2000 +0100
@@ -1,21 +1,62 @@
(* Title: HOL/Inductive.thy
ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
*)
theory Inductive = Gfp + Sum_Type + NatDef
files
- "Tools/induct_method.ML"
- "Tools/inductive_package.ML"
- "Tools/datatype_aux.ML"
- "Tools/datatype_prop.ML"
- "Tools/datatype_rep_proofs.ML"
- "Tools/datatype_abs_proofs.ML"
- "Tools/datatype_package.ML"
- "Tools/primrec_package.ML":
+ ("Tools/induct_method.ML")
+ ("Tools/inductive_package.ML")
+ ("Tools/datatype_aux.ML")
+ ("Tools/datatype_prop.ML")
+ ("Tools/datatype_rep_proofs.ML")
+ ("Tools/datatype_abs_proofs.ML")
+ ("Tools/datatype_package.ML")
+ ("Tools/primrec_package.ML"):
+
+constdefs
+ forall :: "('a => bool) => bool"
+ "forall P == \<forall>x. P x"
+ implies :: "bool => bool => bool"
+ "implies A B == A --> B"
+
+lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
+proof
+ assume "!!x. P x"
+ thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast
+next
+ fix x
+ assume "forall (\<lambda>x. P x)"
+ thus "P x" by (unfold forall_def) blast
+qed
+lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
+proof
+ assume "A ==> B"
+ thus "implies A B" by (unfold implies_def) blast
+next
+ assume "implies A B" and A
+ thus B by (unfold implies_def) blast
+qed
+
+lemmas inductive_atomize = forall_eq implies_eq
+lemmas inductive_rulify = inductive_atomize [symmetric, standard]
+hide const forall implies
+
+use "Tools/induct_method.ML"
setup InductMethod.setup
+
+use "Tools/inductive_package.ML"
setup InductivePackage.setup
+
+use "Tools/datatype_aux.ML"
+use "Tools/datatype_prop.ML"
+use "Tools/datatype_rep_proofs.ML"
+use "Tools/datatype_abs_proofs.ML"
+use "Tools/datatype_package.ML"
setup DatatypePackage.setup
+
+use "Tools/primrec_package.ML"
setup PrimrecPackage.setup
theorems basic_monos [mono] =