src/FOL/IFOL.thy
changeset 26580 c3e597a476fd
parent 26286 3ff5d257f175
child 26956 1309a6a0a29f
     1.1 --- a/src/FOL/IFOL.thy	Tue Apr 08 15:47:15 2008 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Tue Apr 08 18:30:40 2008 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    "~~/src/Provers/eqsubst.ML"
     1.5    "~~/src/Provers/quantifier1.ML"
     1.6    "~~/src/Provers/project_rule.ML"
     1.7 +  "~~/src/Tools/atomize_elim.ML"
     1.8    ("fologic.ML")
     1.9    ("hypsubstdata.ML")
    1.10    ("intprover.ML")
    1.11 @@ -738,6 +739,22 @@
    1.12    and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
    1.13  
    1.14  
    1.15 +subsection {* Atomizing elimination rules *}
    1.16 +
    1.17 +setup AtomizeElim.setup
    1.18 +
    1.19 +lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
    1.20 +by rule iprover+
    1.21 +
    1.22 +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
    1.23 +by rule iprover+
    1.24 +
    1.25 +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
    1.26 +by rule iprover+
    1.27 +
    1.28 +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
    1.29 +
    1.30 +
    1.31  subsection {* Calculational rules *}
    1.32  
    1.33  lemma forw_subst: "a = b ==> P(b) ==> P(a)"