simplified atomize;
authorwenzelm
Fri Nov 10 19:03:55 2000 +0100 (2000-11-10)
changeset 104346ea4735c3955
parent 10433 6c5659d461dd
child 10435 b100e8d2c355
simplified atomize;
added inductive_rulify2 (to accomodate malformed induction rules);
src/HOL/Inductive.thy
     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