setup "rules" method;
authorwenzelm
Mon Dec 03 21:03:06 2001 +0100 (2001-12-03)
changeset 1234994e812f9683e
parent 12348 c3f34d7c50f8
child 12350 5fad0e7129c3
setup "rules" method;
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Mon Dec 03 21:02:26 2001 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Mon Dec 03 21:03:06 2001 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  setup Simplifier.setup
     1.5  use "IFOL_lemmas.ML"
     1.6  
     1.7 -declare impE [Pure.elim]  iffD1 [Pure.elim]  iffD2 [Pure.elim]
     1.8 +declare impE [Pure.elim?]  iffD1 [Pure.elim?]  iffD2 [Pure.elim?]
     1.9  
    1.10  use "fologic.ML"
    1.11  use "hypsubstdata.ML"
    1.12 @@ -125,6 +125,37 @@
    1.13  use "intprover.ML"
    1.14  
    1.15  
    1.16 +lemma impE':
    1.17 +  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
    1.18 +proof -
    1.19 +  from 3 and 1 have P .
    1.20 +  with 1 have Q ..
    1.21 +  with 2 show R .
    1.22 +qed
    1.23 +
    1.24 +lemma allE':
    1.25 +  (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
    1.26 +proof -
    1.27 +  from 1 have "P(x)" by (rule spec)
    1.28 +  from this and 1 show Q by (rule 2)
    1.29 +qed
    1.30 +
    1.31 +lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
    1.32 +proof -
    1.33 +  from 2 and 1 have P .
    1.34 +  with 1 show R by (rule notE)
    1.35 +qed
    1.36 +
    1.37 +lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
    1.38 +  and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
    1.39 +  and [Pure.elim 2] = allE notE' impE'
    1.40 +  and [Pure.intro] = exI disjI2 disjI1
    1.41 +
    1.42 +ML_setup {*
    1.43 +  Context.>> (RuleContext.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
    1.44 +*}
    1.45 +
    1.46 +
    1.47  subsection {* Atomizing meta-level rules *}
    1.48  
    1.49  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.50 @@ -191,6 +222,6 @@
    1.51    mp
    1.52    trans
    1.53  
    1.54 -lemmas [Pure.elim] = sym
    1.55 +lemmas [Pure.elim?] = sym
    1.56  
    1.57  end