author | wenzelm |

Wed Oct 31 01:20:42 2001 +0100 (2001-10-31) | |

changeset 11989 | d4bcba4e080e |

parent 11988 | 8340fb172607 |

child 11990 | c1daefc08eff |

renamed inductive_XXX to induct_XXX;

added induct_impliesI;

added induct_impliesI;

src/HOL/HOL.thy | file | annotate | diff | revisions |

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