src/FOL/FOL.thy
changeset 10430 d3f780c3af0c
parent 10383 a092ae7bb2a6
child 11096 bedfd42db838
     1.1 --- a/src/FOL/FOL.thy	Fri Nov 10 19:00:22 2000 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Nov 10 19:00:51 2000 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  use "FOL_lemmas1.ML"
     1.6  
     1.7 -lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
     1.8 +lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
     1.9  proof (rule equal_intr_rule)
    1.10    assume "!!x. P(x)"
    1.11    show "ALL x. P(x)" by (rule allI)
    1.12 @@ -34,7 +34,7 @@
    1.13    thus "!!x. P(x)" by (rule allE)
    1.14  qed
    1.15  
    1.16 -lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
    1.17 +lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
    1.18  proof (rule equal_intr_rule)
    1.19    assume r: "A ==> B"
    1.20    show "A --> B" by (rule impI) (rule r)
    1.21 @@ -43,7 +43,17 @@
    1.22    thus B by (rule mp)
    1.23  qed
    1.24  
    1.25 -lemmas atomize = all_eq imp_eq
    1.26 +lemma atomize_eq: "(x == y) == Trueprop (x = y)"
    1.27 +proof (rule equal_intr_rule)
    1.28 +  assume "x == y"
    1.29 +  show "x = y" by (unfold prems) (rule refl)
    1.30 +next
    1.31 +  assume "x = y"
    1.32 +  thus "x == y" by (rule eq_reflection)
    1.33 +qed
    1.34 +
    1.35 +lemmas atomize = atomize_all atomize_imp
    1.36 +lemmas atomize' = atomize atomize_eq
    1.37  
    1.38  use "cladata.ML"
    1.39  setup Cla.setup