tuned declarations (rules, sym, etc.);
authorwenzelm
Wed Dec 05 03:19:14 2001 +0100 (2001-12-05)
changeset 123869c38ec9eca1c
parent 12385 389d11fb62c8
child 12387 fe2353a8d1e8
tuned declarations (rules, sym, etc.);
src/HOL/HOL.thy
     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.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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.61  use "cladata.ML"
    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"