author wenzelm Mon, 06 Nov 2000 22:49:16 +0100 changeset 10402 5e82d6cafb5f parent 10401 58bb50f69497 child 10403 2955ee2424ce
inductive_atomize, inductive_rulify;
 src/HOL/Inductive.thy file | annotate | diff | comparison | revisions
```--- 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] =```