author wenzelm Wed Dec 05 03:00:39 2001 +0100 (2001-12-05) changeset 12368 2af9ad81ea56 parent 12367 1cee8a0db392 child 12369 ab207f9c1e1e
sym declarations;
tuned declarations;
 src/FOL/IFOL.thy file | annotate | diff | revisions
```     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
```