src/HOL/Inductive.thy
changeset 11825 ef7d619e2c88
parent 11688 56833637db2a
child 11990 c1daefc08eff
     1.1 --- a/src/HOL/Inductive.thy	Thu Oct 18 20:59:33 2001 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Oct 18 20:59:59 2001 +0200
     1.3 @@ -17,63 +17,6 @@
     1.4    ("Tools/primrec_package.ML"):
     1.5  
     1.6  
     1.7 -subsection {* Proof by cases and induction *}
     1.8 -
     1.9 -text {* Proper handling of non-atomic rule statements. *}
    1.10 -
    1.11 -constdefs
    1.12 -  forall :: "('a => bool) => bool"
    1.13 -  "forall P == \<forall>x. P x"
    1.14 -  implies :: "bool => bool => bool"
    1.15 -  "implies A B == A --> B"
    1.16 -  equal :: "'a => 'a => bool"
    1.17 -  "equal x y == x = y"
    1.18 -  conj :: "bool => bool => bool"
    1.19 -  "conj A B == A & B"
    1.20 -
    1.21 -lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
    1.22 -  by (simp only: atomize_all forall_def)
    1.23 -
    1.24 -lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
    1.25 -  by (simp only: atomize_imp implies_def)
    1.26 -
    1.27 -lemma equal_eq: "(x == y) == Trueprop (equal x y)"
    1.28 -  by (simp only: atomize_eq equal_def)
    1.29 -
    1.30 -lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
    1.31 -  by (unfold forall_def conj_def) blast
    1.32 -
    1.33 -lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
    1.34 -  by (unfold implies_def conj_def) blast
    1.35 -
    1.36 -lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
    1.37 -  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
    1.38 -
    1.39 -lemmas inductive_atomize = forall_eq implies_eq equal_eq
    1.40 -lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
    1.41 -lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
    1.42 -lemmas inductive_conj = forall_conj implies_conj conj_curry
    1.43 -
    1.44 -hide const forall implies equal conj
    1.45 -
    1.46 -
    1.47 -text {* Method setup. *}
    1.48 -
    1.49 -ML {*
    1.50 -  structure InductMethod = InductMethodFun
    1.51 -  (struct
    1.52 -    val dest_concls = HOLogic.dest_concls;
    1.53 -    val cases_default = thm "case_split";
    1.54 -    val conjI = thm "conjI";
    1.55 -    val atomize = thms "inductive_atomize";
    1.56 -    val rulify1 = thms "inductive_rulify1";
    1.57 -    val rulify2 = thms "inductive_rulify2";
    1.58 -  end);
    1.59 -*}
    1.60 -
    1.61 -setup InductMethod.setup
    1.62 -
    1.63 -
    1.64  subsection {* Inductive sets *}
    1.65  
    1.66  text {* Inversion of injective functions. *}
    1.67 @@ -124,6 +67,8 @@
    1.68  
    1.69  subsubsection {* Inductive datatypes and primitive recursion *}
    1.70  
    1.71 +text {* Package setup. *}
    1.72 +
    1.73  use "Tools/datatype_aux.ML"
    1.74  use "Tools/datatype_prop.ML"
    1.75  use "Tools/datatype_rep_proofs.ML"