renamed inductive_XXX to induct_XXX;
authorwenzelm
Wed Oct 31 01:20:42 2001 +0100 (2001-10-31)
changeset 11989d4bcba4e080e
parent 11988 8340fb172607
child 11990 c1daefc08eff
renamed inductive_XXX to induct_XXX;
added induct_impliesI;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 31 01:19:58 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 31 01:20:42 2001 +0100
     1.3 @@ -276,42 +276,45 @@
     1.4  subsubsection {* Generic cases and induction *}
     1.5  
     1.6  constdefs
     1.7 -  inductive_forall :: "('a => bool) => bool"
     1.8 -  "inductive_forall P == \<forall>x. P x"
     1.9 -  inductive_implies :: "bool => bool => bool"
    1.10 -  "inductive_implies A B == A --> B"
    1.11 -  inductive_equal :: "'a => 'a => bool"
    1.12 -  "inductive_equal x y == x = y"
    1.13 -  inductive_conj :: "bool => bool => bool"
    1.14 -  "inductive_conj A B == A & B"
    1.15 +  induct_forall :: "('a => bool) => bool"
    1.16 +  "induct_forall P == \<forall>x. P x"
    1.17 +  induct_implies :: "bool => bool => bool"
    1.18 +  "induct_implies A B == A --> B"
    1.19 +  induct_equal :: "'a => 'a => bool"
    1.20 +  "induct_equal x y == x = y"
    1.21 +  induct_conj :: "bool => bool => bool"
    1.22 +  "induct_conj A B == A & B"
    1.23  
    1.24 -lemma inductive_forall_eq: "(!!x. P x) == Trueprop (inductive_forall (\<lambda>x. P x))"
    1.25 -  by (simp only: atomize_all inductive_forall_def)
    1.26 +lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
    1.27 +  by (simp only: atomize_all induct_forall_def)
    1.28  
    1.29 -lemma inductive_implies_eq: "(A ==> B) == Trueprop (inductive_implies A B)"
    1.30 -  by (simp only: atomize_imp inductive_implies_def)
    1.31 +lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
    1.32 +  by (simp only: atomize_imp induct_implies_def)
    1.33  
    1.34 -lemma inductive_equal_eq: "(x == y) == Trueprop (inductive_equal x y)"
    1.35 -  by (simp only: atomize_eq inductive_equal_def)
    1.36 +lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
    1.37 +  by (simp only: atomize_eq induct_equal_def)
    1.38  
    1.39 -lemma inductive_forall_conj: "inductive_forall (\<lambda>x. inductive_conj (A x) (B x)) =
    1.40 -    inductive_conj (inductive_forall A) (inductive_forall B)"
    1.41 -  by (unfold inductive_forall_def inductive_conj_def) blast
    1.42 +lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
    1.43 +    induct_conj (induct_forall A) (induct_forall B)"
    1.44 +  by (unfold induct_forall_def induct_conj_def) blast
    1.45  
    1.46 -lemma inductive_implies_conj: "inductive_implies C (inductive_conj A B) =
    1.47 -    inductive_conj (inductive_implies C A) (inductive_implies C B)"
    1.48 -  by (unfold inductive_implies_def inductive_conj_def) blast
    1.49 +lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
    1.50 +    induct_conj (induct_implies C A) (induct_implies C B)"
    1.51 +  by (unfold induct_implies_def induct_conj_def) blast
    1.52 +
    1.53 +lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)"
    1.54 +  by (simp only: atomize_imp atomize_eq induct_conj_def) (rule equal_intr_rule, blast+)
    1.55  
    1.56 -lemma inductive_conj_curry: "(inductive_conj A B ==> C) == (A ==> B ==> C)"
    1.57 -  by (simp only: atomize_imp atomize_eq inductive_conj_def) (rule equal_intr_rule, blast+)
    1.58 +lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
    1.59 +  by (simp add: induct_implies_def)
    1.60  
    1.61 -lemmas inductive_atomize = inductive_forall_eq inductive_implies_eq inductive_equal_eq
    1.62 -lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
    1.63 -lemmas inductive_rulify2 =
    1.64 -  inductive_forall_def inductive_implies_def inductive_equal_def inductive_conj_def
    1.65 -lemmas inductive_conj = inductive_forall_conj inductive_implies_conj inductive_conj_curry
    1.66 +lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
    1.67 +lemmas induct_rulify1 = induct_atomize [symmetric, standard]
    1.68 +lemmas induct_rulify2 =
    1.69 +  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.70 +lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
    1.71  
    1.72 -hide const inductive_forall inductive_implies inductive_equal inductive_conj
    1.73 +hide const induct_forall induct_implies induct_equal induct_conj
    1.74  
    1.75  
    1.76  text {* Method setup. *}
    1.77 @@ -321,10 +324,11 @@
    1.78    (struct
    1.79      val dest_concls = HOLogic.dest_concls;
    1.80      val cases_default = thm "case_split";
    1.81 +    val local_impI = thm "induct_impliesI";
    1.82      val conjI = thm "conjI";
    1.83 -    val atomize = thms "inductive_atomize";
    1.84 -    val rulify1 = thms "inductive_rulify1";
    1.85 -    val rulify2 = thms "inductive_rulify2";
    1.86 +    val atomize = thms "induct_atomize";
    1.87 +    val rulify1 = thms "induct_rulify1";
    1.88 +    val rulify2 = thms "induct_rulify2";
    1.89    end);
    1.90  *}
    1.91