author wenzelm Fri Nov 10 19:03:55 2000 +0100 (2000-11-10) changeset 10434 6ea4735c3955 parent 10433 6c5659d461dd child 10435 b100e8d2c355
simplified atomize;
added inductive_rulify2 (to accomodate malformed induction rules);
 src/HOL/Inductive.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Inductive.thy	Fri Nov 10 19:03:06 2000 +0100
1.2 +++ b/src/HOL/Inductive.thy	Fri Nov 10 19:03:55 2000 +0100
1.3 @@ -19,29 +19,23 @@
1.4    "forall P == \<forall>x. P x"
1.5    implies :: "bool => bool => bool"
1.6    "implies A B == A --> B"
1.7 +  equal :: "'a => 'a => bool"
1.8 +  "equal x y == x = y"
1.9
1.10  lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
1.11 -proof
1.12 -  assume "!!x. P x"
1.13 -  thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast
1.14 -next
1.15 -  fix x
1.16 -  assume "forall (\<lambda>x. P x)"
1.17 -  thus "P x" by (unfold forall_def) blast
1.18 -qed
1.19 +  by (simp only: atomize_all forall_def)
1.20
1.21  lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
1.22 -proof
1.23 -  assume "A ==> B"
1.24 -  thus "implies A B" by (unfold implies_def) blast
1.25 -next
1.26 -  assume "implies A B" and A
1.27 -  thus B by (unfold implies_def) blast
1.28 -qed
1.29 +  by (simp only: atomize_imp implies_def)
1.30 +
1.31 +lemma equal_eq: "(x == y) == Trueprop (equal x y)"
1.32 +  by (simp only: atomize_eq equal_def)
1.33
1.34 -lemmas inductive_atomize = forall_eq implies_eq
1.35 -lemmas inductive_rulify = inductive_atomize [symmetric, standard]
1.36 -hide const forall implies
1.37 +hide const forall implies equal
1.38 +
1.39 +lemmas inductive_atomize = forall_eq implies_eq equal_eq
1.40 +lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
1.41 +lemmas inductive_rulify2 = forall_def implies_def equal_def
1.42
1.43  use "Tools/induct_method.ML"
1.44  setup InductMethod.setup
```