# 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