sym declarations;
authorwenzelm
Wed Dec 05 03:00:39 2001 +0100 (2001-12-05)
changeset 123682af9ad81ea56
parent 12367 1cee8a0db392
child 12369 ab207f9c1e1e
sym declarations;
tuned declarations;
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Wed Dec 05 02:59:49 2001 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Wed Dec 05 03:00:39 2001 +0100
     1.3 @@ -117,19 +117,19 @@
     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 -
     1.9  use "fologic.ML"
    1.10  use "hypsubstdata.ML"
    1.11  setup hypsubst_setup
    1.12  use "intprover.ML"
    1.13  
    1.14  
    1.15 +subsubsection {* Intuitionistic Reasoning *}
    1.16 +
    1.17  lemma impE':
    1.18    (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
    1.19  proof -
    1.20    from 3 and 1 have P .
    1.21 -  with 1 have Q ..
    1.22 +  with 1 have Q by (rule impE)
    1.23    with 2 show R .
    1.24  qed
    1.25  
    1.26 @@ -156,21 +156,28 @@
    1.27  *}
    1.28  
    1.29  
    1.30 +lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
    1.31 +  by rules
    1.32 +
    1.33 +lemmas [sym] = sym iff_sym not_sym iff_not_sym
    1.34 +  and [Pure.elim?] = iffD1 iffD2 impE
    1.35 +
    1.36 +
    1.37  subsection {* Atomizing meta-level rules *}
    1.38  
    1.39  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.40  proof
    1.41    assume "!!x. P(x)"
    1.42 -  show "ALL x. P(x)" by (rule allI)
    1.43 +  show "ALL x. P(x)" ..
    1.44  next
    1.45    assume "ALL x. P(x)"
    1.46 -  thus "!!x. P(x)" by (rule allE)
    1.47 +  thus "!!x. P(x)" ..
    1.48  qed
    1.49  
    1.50  lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
    1.51  proof
    1.52 -  assume r: "A ==> B"
    1.53 -  show "A --> B" by (rule impI) (rule r)
    1.54 +  assume "A ==> B"
    1.55 +  thus "A --> B" ..
    1.56  next
    1.57    assume "A --> B" and A
    1.58    thus B by (rule mp)
    1.59 @@ -200,7 +207,7 @@
    1.60    qed
    1.61  qed
    1.62  
    1.63 -declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
    1.64 +lemmas [symmetric, rulify] = atomize_all atomize_imp
    1.65  
    1.66  
    1.67  subsection {* Calculational rules *}
    1.68 @@ -222,6 +229,4 @@
    1.69    mp
    1.70    trans
    1.71  
    1.72 -lemmas [Pure.elim?] = sym
    1.73 -
    1.74  end