summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 31 Oct 2001 01:20:42 +0100 | |

changeset 11989 | d4bcba4e080e |

parent 11988 | 8340fb172607 |

child 11990 | c1daefc08eff |

renamed inductive_XXX to induct_XXX;
added induct_impliesI;

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

--- a/src/HOL/HOL.thy Wed Oct 31 01:19:58 2001 +0100 +++ b/src/HOL/HOL.thy Wed Oct 31 01:20:42 2001 +0100 @@ -276,42 +276,45 @@ subsubsection {* Generic cases and induction *} constdefs - inductive_forall :: "('a => bool) => bool" - "inductive_forall P == \<forall>x. P x" - inductive_implies :: "bool => bool => bool" - "inductive_implies A B == A --> B" - inductive_equal :: "'a => 'a => bool" - "inductive_equal x y == x = y" - inductive_conj :: "bool => bool => bool" - "inductive_conj A B == A & B" + induct_forall :: "('a => bool) => bool" + "induct_forall P == \<forall>x. P x" + induct_implies :: "bool => bool => bool" + "induct_implies A B == A --> B" + induct_equal :: "'a => 'a => bool" + "induct_equal x y == x = y" + induct_conj :: "bool => bool => bool" + "induct_conj A B == A & B" -lemma inductive_forall_eq: "(!!x. P x) == Trueprop (inductive_forall (\<lambda>x. P x))" - by (simp only: atomize_all inductive_forall_def) +lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" + by (simp only: atomize_all induct_forall_def) -lemma inductive_implies_eq: "(A ==> B) == Trueprop (inductive_implies A B)" - by (simp only: atomize_imp inductive_implies_def) +lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" + by (simp only: atomize_imp induct_implies_def) -lemma inductive_equal_eq: "(x == y) == Trueprop (inductive_equal x y)" - by (simp only: atomize_eq inductive_equal_def) +lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" + by (simp only: atomize_eq induct_equal_def) -lemma inductive_forall_conj: "inductive_forall (\<lambda>x. inductive_conj (A x) (B x)) = - inductive_conj (inductive_forall A) (inductive_forall B)" - by (unfold inductive_forall_def inductive_conj_def) blast +lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = + induct_conj (induct_forall A) (induct_forall B)" + by (unfold induct_forall_def induct_conj_def) blast -lemma inductive_implies_conj: "inductive_implies C (inductive_conj A B) = - inductive_conj (inductive_implies C A) (inductive_implies C B)" - by (unfold inductive_implies_def inductive_conj_def) blast +lemma induct_implies_conj: "induct_implies C (induct_conj A B) = + induct_conj (induct_implies C A) (induct_implies C B)" + by (unfold induct_implies_def induct_conj_def) blast + +lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)" + by (simp only: atomize_imp atomize_eq induct_conj_def) (rule equal_intr_rule, blast+) -lemma inductive_conj_curry: "(inductive_conj A B ==> C) == (A ==> B ==> C)" - by (simp only: atomize_imp atomize_eq inductive_conj_def) (rule equal_intr_rule, blast+) +lemma induct_impliesI: "(A ==> B) ==> induct_implies A B" + by (simp add: induct_implies_def) -lemmas inductive_atomize = inductive_forall_eq inductive_implies_eq inductive_equal_eq -lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] -lemmas inductive_rulify2 = - inductive_forall_def inductive_implies_def inductive_equal_def inductive_conj_def -lemmas inductive_conj = inductive_forall_conj inductive_implies_conj inductive_conj_curry +lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq +lemmas induct_rulify1 = induct_atomize [symmetric, standard] +lemmas induct_rulify2 = + induct_forall_def induct_implies_def induct_equal_def induct_conj_def +lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry -hide const inductive_forall inductive_implies inductive_equal inductive_conj +hide const induct_forall induct_implies induct_equal induct_conj text {* Method setup. *} @@ -321,10 +324,11 @@ (struct val dest_concls = HOLogic.dest_concls; val cases_default = thm "case_split"; + val local_impI = thm "induct_impliesI"; val conjI = thm "conjI"; - val atomize = thms "inductive_atomize"; - val rulify1 = thms "inductive_rulify1"; - val rulify2 = thms "inductive_rulify2"; + val atomize = thms "induct_atomize"; + val rulify1 = thms "induct_rulify1"; + val rulify2 = thms "induct_rulify2"; end); *}