generic induct_method.ML;
authorwenzelm
Thu Oct 04 15:43:17 2001 +0200 (2001-10-04)
changeset 1168856833637db2a
parent 11687 b0fe6e522559
child 11689 38788d98504f
generic induct_method.ML;
tuned;
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Thu Oct 04 15:42:48 2001 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Oct 04 15:43:17 2001 +0200
     1.3 @@ -2,13 +2,12 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 +*)
     1.8  
     1.9 -Setup packages for inductive sets and types etc.
    1.10 -*)
    1.11 +header {* Support for inductive sets and types *}
    1.12  
    1.13  theory Inductive = Gfp + Sum_Type + Relation
    1.14  files
    1.15 -  ("Tools/induct_method.ML")
    1.16    ("Tools/inductive_package.ML")
    1.17    ("Tools/datatype_aux.ML")
    1.18    ("Tools/datatype_prop.ML")
    1.19 @@ -18,7 +17,9 @@
    1.20    ("Tools/primrec_package.ML"):
    1.21  
    1.22  
    1.23 -(* handling of proper rules *)
    1.24 +subsection {* Proof by cases and induction *}
    1.25 +
    1.26 +text {* Proper handling of non-atomic rule statements. *}
    1.27  
    1.28  constdefs
    1.29    forall :: "('a => bool) => bool"
    1.30 @@ -56,7 +57,26 @@
    1.31  hide const forall implies equal conj
    1.32  
    1.33  
    1.34 -(* inversion of injective functions *)
    1.35 +text {* Method setup. *}
    1.36 +
    1.37 +ML {*
    1.38 +  structure InductMethod = InductMethodFun
    1.39 +  (struct
    1.40 +    val dest_concls = HOLogic.dest_concls;
    1.41 +    val cases_default = thm "case_split";
    1.42 +    val conjI = thm "conjI";
    1.43 +    val atomize = thms "inductive_atomize";
    1.44 +    val rulify1 = thms "inductive_rulify1";
    1.45 +    val rulify2 = thms "inductive_rulify2";
    1.46 +  end);
    1.47 +*}
    1.48 +
    1.49 +setup InductMethod.setup
    1.50 +
    1.51 +
    1.52 +subsection {* Inductive sets *}
    1.53 +
    1.54 +text {* Inversion of injective functions. *}
    1.55  
    1.56  constdefs
    1.57    myinv :: "('a => 'b) => ('b => 'a)"
    1.58 @@ -88,14 +108,22 @@
    1.59  hide const myinv
    1.60  
    1.61  
    1.62 -(* setup packages *)
    1.63 -
    1.64 -use "Tools/induct_method.ML"
    1.65 -setup InductMethod.setup
    1.66 +text {* Package setup. *}
    1.67  
    1.68  use "Tools/inductive_package.ML"
    1.69  setup InductivePackage.setup
    1.70  
    1.71 +theorems basic_monos [mono] =
    1.72 +  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    1.73 +  Collect_mono in_mono vimage_mono
    1.74 +  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.75 +  not_all not_ex
    1.76 +  Ball_def Bex_def
    1.77 +  inductive_rulify2
    1.78 +
    1.79 +
    1.80 +subsubsection {* Inductive datatypes and primitive recursion *}
    1.81 +
    1.82  use "Tools/datatype_aux.ML"
    1.83  use "Tools/datatype_prop.ML"
    1.84  use "Tools/datatype_rep_proofs.ML"
    1.85 @@ -106,12 +134,4 @@
    1.86  use "Tools/primrec_package.ML"
    1.87  setup PrimrecPackage.setup
    1.88  
    1.89 -theorems basic_monos [mono] =
    1.90 -  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    1.91 -  Collect_mono in_mono vimage_mono
    1.92 -  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.93 -  not_all not_ex
    1.94 -  Ball_def Bex_def
    1.95 -  inductive_rulify2
    1.96 -
    1.97  end