# HG changeset patch
# User wenzelm
# Date 1002202997 -7200
# Node ID 56833637db2af69870f0d7dfe419aada0a9653fa
# Parent  b0fe6e5225593120d767c76aaeffa5066f5d1051
generic induct_method.ML;
tuned;

diff -r b0fe6e522559 -r 56833637db2a src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Oct 04 15:42:48 2001 +0200
+++ b/src/HOL/Inductive.thy	Thu Oct 04 15:43:17 2001 +0200
@@ -2,13 +2,12 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
 
-Setup packages for inductive sets and types etc.
-*)
+header {* Support for inductive sets and types *}
 
 theory Inductive = Gfp + Sum_Type + Relation
 files
-  ("Tools/induct_method.ML")
   ("Tools/inductive_package.ML")
   ("Tools/datatype_aux.ML")
   ("Tools/datatype_prop.ML")
@@ -18,7 +17,9 @@
   ("Tools/primrec_package.ML"):
 
 
-(* handling of proper rules *)
+subsection {* Proof by cases and induction *}
+
+text {* Proper handling of non-atomic rule statements. *}
 
 constdefs
   forall :: "('a => bool) => bool"
@@ -56,7 +57,26 @@
 hide const forall implies equal conj
 
 
-(* inversion of injective functions *)
+text {* Method setup. *}
+
+ML {*
+  structure InductMethod = InductMethodFun
+  (struct
+    val dest_concls = HOLogic.dest_concls;
+    val cases_default = thm "case_split";
+    val conjI = thm "conjI";
+    val atomize = thms "inductive_atomize";
+    val rulify1 = thms "inductive_rulify1";
+    val rulify2 = thms "inductive_rulify2";
+  end);
+*}
+
+setup InductMethod.setup
+
+
+subsection {* Inductive sets *}
+
+text {* Inversion of injective functions. *}
 
 constdefs
   myinv :: "('a => 'b) => ('b => 'a)"
@@ -88,14 +108,22 @@
 hide const myinv
 
 
-(* setup packages *)
-
-use "Tools/induct_method.ML"
-setup InductMethod.setup
+text {* Package setup. *}
 
 use "Tools/inductive_package.ML"
 setup InductivePackage.setup
 
+theorems basic_monos [mono] =
+  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
+  Collect_mono in_mono vimage_mono
+  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
+  not_all not_ex
+  Ball_def Bex_def
+  inductive_rulify2
+
+
+subsubsection {* Inductive datatypes and primitive recursion *}
+
 use "Tools/datatype_aux.ML"
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"
@@ -106,12 +134,4 @@
 use "Tools/primrec_package.ML"
 setup PrimrecPackage.setup
 
-theorems basic_monos [mono] =
-  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
-  Collect_mono in_mono vimage_mono
-  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-  not_all not_ex
-  Ball_def Bex_def
-  inductive_rulify2
-
 end