# 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