author wenzelm Wed Dec 05 03:19:14 2001 +0100 (2001-12-05) changeset 12386 9c38ec9eca1c parent 12385 389d11fb62c8 child 12387 fe2353a8d1e8
tuned declarations (rules, sym, etc.);
 src/HOL/HOL.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/HOL.thy	Wed Dec 05 03:18:03 2001 +0100
1.2 +++ b/src/HOL/HOL.thy	Wed Dec 05 03:19:14 2001 +0100
1.3 @@ -1,6 +1,7 @@
1.4  (*  Title:      HOL/HOL.thy
1.5      ID:         \$Id\$
1.6      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
1.8  *)
1.9
1.10  header {* The basis of Higher-Order Logic *}
1.11 @@ -196,8 +197,38 @@
1.12  use "HOL_lemmas.ML"
1.13  theorems case_split = case_split_thm [case_names True False]
1.14
1.15 -declare trans [trans]
1.16 -declare impE [CPure.elim]  iffD1 [CPure.elim]  iffD2 [CPure.elim]
1.17 +
1.18 +subsubsection {* Intuitionistic Reasoning *}
1.19 +
1.20 +lemma impE':
1.21 +  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
1.22 +proof -
1.23 +  from 3 and 1 have P .
1.24 +  with 1 have Q by (rule impE)
1.25 +  with 2 show R .
1.26 +qed
1.27 +
1.28 +lemma allE':
1.29 +  (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
1.30 +proof -
1.31 +  from 1 have "P x" by (rule spec)
1.32 +  from this and 1 show Q by (rule 2)
1.33 +qed
1.34 +
1.35 +lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
1.36 +proof -
1.37 +  from 2 and 1 have P .
1.38 +  with 1 show R by (rule notE)
1.39 +qed
1.40 +
1.41 +lemmas [CPure.elim!] = disjE iffE FalseE conjE exE
1.42 +  and [CPure.intro!] = iffI conjI impI TrueI notI allI refl
1.43 +  and [CPure.elim 2] = allE notE' impE'
1.44 +  and [CPure.intro] = exI disjI2 disjI1
1.45 +
1.46 +lemmas [trans] = trans
1.47 +  and [sym] = sym not_sym
1.48 +  and [CPure.elim?] = iffD1 iffD2 impE
1.49
1.50
1.51  subsubsection {* Atomizing meta-level connectives *}
1.52 @@ -245,57 +276,28 @@
1.53    qed
1.54  qed
1.55
1.56 +lemmas [symmetric, rulify] = atomize_all atomize_imp
1.57 +
1.58
1.59  subsubsection {* Classical Reasoner setup *}
1.60
1.62  setup hypsubst_setup
1.63
1.64 -declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
1.65 +ML_setup {*
1.66 +  Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
1.67 +*}
1.68
1.69  setup Classical.setup
1.70  setup clasetup
1.71
1.72 -declare ext [intro?]
1.73 -declare disjI1 [elim?]  disjI2 [elim?]  ex1_implies_ex [elim?]  sym [elim?]
1.74 +lemmas [intro?] = ext
1.75 +  and [elim?] = ex1_implies_ex
1.76
1.77  use "blastdata.ML"
1.78  setup Blast.setup
1.79
1.80
1.81 -subsubsection {* Intuitionistic Reasoning *}
1.82 -
1.83 -lemma impE':
1.84 -  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
1.85 -proof -
1.86 -  from 3 and 1 have P .
1.87 -  with 1 have Q ..
1.88 -  with 2 show R .
1.89 -qed
1.90 -
1.91 -lemma allE':
1.92 -  (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
1.93 -proof -
1.94 -  from 1 have "P x" ..
1.95 -  from this and 1 show Q by (rule 2)
1.96 -qed
1.97 -
1.98 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
1.99 -proof -
1.100 -  from 2 and 1 have P .
1.101 -  with 1 show R by (rule notE)
1.102 -qed
1.103 -
1.104 -lemmas [CPure.elim!] = disjE iffE FalseE conjE exE
1.105 -  and [CPure.intro!] = iffI conjI impI TrueI notI allI refl
1.106 -  and [CPure.elim 2] = allE notE' impE'
1.107 -  and [CPure.intro] = exI disjI2 disjI1
1.108 -
1.109 -ML_setup {*
1.110 -  Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
1.111 -*}
1.112 -
1.113 -
1.114  subsubsection {* Simplifier setup *}
1.115
1.116  lemma meta_eq_to_obj_eq: "x == y ==> x = y"
```