# HG changeset patch # User wenzelm # Date 973879435 -3600 # Node ID 6ea4735c39552cff28d0baaf289d9ba0669bca61 # Parent 6c5659d461dd9872c434c99bd7fee99bb63316eb simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules); diff -r 6c5659d461dd -r 6ea4735c3955 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Fri Nov 10 19:03:06 2000 +0100 +++ b/src/HOL/Inductive.thy Fri Nov 10 19:03:55 2000 +0100 @@ -19,29 +19,23 @@ "forall P == \x. P x" implies :: "bool => bool => bool" "implies A B == A --> B" + equal :: "'a => 'a => bool" + "equal x y == x = y" lemma forall_eq: "(!!x. P x) == Trueprop (forall (\x. P x))" -proof - assume "!!x. P x" - thus "forall (\x. P x)" by (unfold forall_def) blast -next - fix x - assume "forall (\x. P x)" - thus "P x" by (unfold forall_def) blast -qed + by (simp only: atomize_all forall_def) lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" -proof - assume "A ==> B" - thus "implies A B" by (unfold implies_def) blast -next - assume "implies A B" and A - thus B by (unfold implies_def) blast -qed + by (simp only: atomize_imp implies_def) + +lemma equal_eq: "(x == y) == Trueprop (equal x y)" + by (simp only: atomize_eq equal_def) -lemmas inductive_atomize = forall_eq implies_eq -lemmas inductive_rulify = inductive_atomize [symmetric, standard] -hide const forall implies +hide const forall implies equal + +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 use "Tools/induct_method.ML" setup InductMethod.setup