--- a/src/HOL/Inductive.thy Thu Oct 18 20:59:33 2001 +0200
+++ b/src/HOL/Inductive.thy Thu Oct 18 20:59:59 2001 +0200
@@ -17,63 +17,6 @@
("Tools/primrec_package.ML"):
-subsection {* Proof by cases and induction *}
-
-text {* Proper handling of non-atomic rule statements. *}
-
-constdefs
- forall :: "('a => bool) => bool"
- "forall P == \<forall>x. P x"
- implies :: "bool => bool => bool"
- "implies A B == A --> B"
- equal :: "'a => 'a => bool"
- "equal x y == x = y"
- conj :: "bool => bool => bool"
- "conj A B == A & B"
-
-lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
- by (simp only: atomize_all forall_def)
-
-lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
- by (simp only: atomize_imp implies_def)
-
-lemma equal_eq: "(x == y) == Trueprop (equal x y)"
- by (simp only: atomize_eq equal_def)
-
-lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
- by (unfold forall_def conj_def) blast
-
-lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
- by (unfold implies_def conj_def) blast
-
-lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
- by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
-
-lemmas inductive_atomize = forall_eq implies_eq equal_eq
-lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
-lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
-lemmas inductive_conj = forall_conj implies_conj conj_curry
-
-hide const forall implies equal conj
-
-
-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. *}
@@ -124,6 +67,8 @@
subsubsection {* Inductive datatypes and primitive recursion *}
+text {* Package setup. *}
+
use "Tools/datatype_aux.ML"
use "Tools/datatype_prop.ML"
use "Tools/datatype_rep_proofs.ML"