removal of HOL_Lemmas
authorpaulson
Wed Dec 15 10:19:01 2004 +0100 (2004-12-15)
changeset 154111d195de59497
parent 15410 18914688a5fd
child 15412 7f373e478a5a
removal of HOL_Lemmas
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 14 14:53:02 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 15 10:19:01 2004 +0100
     1.3 @@ -7,8 +7,7 @@
     1.4  
     1.5  theory HOL
     1.6  imports CPure
     1.7 -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
     1.8 -      ("antisym_setup.ML")
     1.9 +files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("antisym_setup.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Primitive logic *}
    1.13 @@ -217,11 +216,568 @@
    1.14    abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    1.15  
    1.16  
    1.17 +subsection {*Equality*}
    1.18 +
    1.19 +lemma sym: "s=t ==> t=s"
    1.20 +apply (erule subst)
    1.21 +apply (rule refl)
    1.22 +done
    1.23 +
    1.24 +(*calling "standard" reduces maxidx to 0*)
    1.25 +lemmas ssubst = sym [THEN subst, standard]
    1.26 +
    1.27 +lemma trans: "[| r=s; s=t |] ==> r=t"
    1.28 +apply (erule subst , assumption)
    1.29 +done
    1.30 +
    1.31 +lemma def_imp_eq:  assumes meq: "A == B" shows "A = B"
    1.32 +apply (unfold meq)
    1.33 +apply (rule refl)
    1.34 +done
    1.35 +
    1.36 +(*Useful with eresolve_tac for proving equalties from known equalities.
    1.37 +        a = b
    1.38 +        |   |
    1.39 +        c = d   *)
    1.40 +lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
    1.41 +apply (rule trans)
    1.42 +apply (rule trans)
    1.43 +apply (rule sym)
    1.44 +apply assumption+
    1.45 +done
    1.46 +
    1.47 +
    1.48 +subsection {*Congruence rules for application*}
    1.49 +
    1.50 +(*similar to AP_THM in Gordon's HOL*)
    1.51 +lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
    1.52 +apply (erule subst)
    1.53 +apply (rule refl)
    1.54 +done
    1.55 +
    1.56 +(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    1.57 +lemma arg_cong: "x=y ==> f(x)=f(y)"
    1.58 +apply (erule subst)
    1.59 +apply (rule refl)
    1.60 +done
    1.61 +
    1.62 +lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    1.63 +apply (erule subst)+
    1.64 +apply (rule refl)
    1.65 +done
    1.66 +
    1.67 +
    1.68 +subsection {*Equality of booleans -- iff*}
    1.69 +
    1.70 +lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
    1.71 +apply (rules intro: iff [THEN mp, THEN mp] impI prems)
    1.72 +done
    1.73 +
    1.74 +lemma iffD2: "[| P=Q; Q |] ==> P"
    1.75 +apply (erule ssubst)
    1.76 +apply assumption
    1.77 +done
    1.78 +
    1.79 +lemma rev_iffD2: "[| Q; P=Q |] ==> P"
    1.80 +apply (erule iffD2)
    1.81 +apply assumption
    1.82 +done
    1.83 +
    1.84 +lemmas iffD1 = sym [THEN iffD2, standard]
    1.85 +lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard]
    1.86 +
    1.87 +lemma iffE:
    1.88 +  assumes major: "P=Q"
    1.89 +      and minor: "[| P --> Q; Q --> P |] ==> R"
    1.90 +  shows "R"
    1.91 +by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1])
    1.92 +
    1.93 +
    1.94 +subsection {*True*}
    1.95 +
    1.96 +lemma TrueI: "True"
    1.97 +apply (unfold True_def)
    1.98 +apply (rule refl)
    1.99 +done
   1.100 +
   1.101 +lemma eqTrueI: "P ==> P=True"
   1.102 +by (rules intro: iffI TrueI)
   1.103 +
   1.104 +lemma eqTrueE: "P=True ==> P"
   1.105 +apply (erule iffD2)
   1.106 +apply (rule TrueI)
   1.107 +done
   1.108 +
   1.109 +
   1.110 +subsection {*Universal quantifier*}
   1.111 +
   1.112 +lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
   1.113 +apply (unfold All_def)
   1.114 +apply (rules intro: ext eqTrueI p)
   1.115 +done
   1.116 +
   1.117 +lemma spec: "ALL x::'a. P(x) ==> P(x)"
   1.118 +apply (unfold All_def)
   1.119 +apply (rule eqTrueE)
   1.120 +apply (erule fun_cong)
   1.121 +done
   1.122 +
   1.123 +lemma allE:
   1.124 +  assumes major: "ALL x. P(x)"
   1.125 +      and minor: "P(x) ==> R"
   1.126 +  shows "R"
   1.127 +by (rules intro: minor major [THEN spec])
   1.128 +
   1.129 +lemma all_dupE:
   1.130 +  assumes major: "ALL x. P(x)"
   1.131 +      and minor: "[| P(x); ALL x. P(x) |] ==> R"
   1.132 +  shows "R"
   1.133 +by (rules intro: minor major major [THEN spec])
   1.134 +
   1.135 +
   1.136 +subsection {*False*}
   1.137 +(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
   1.138 +
   1.139 +lemma FalseE: "False ==> P"
   1.140 +apply (unfold False_def)
   1.141 +apply (erule spec)
   1.142 +done
   1.143 +
   1.144 +lemma False_neq_True: "False=True ==> P"
   1.145 +by (erule eqTrueE [THEN FalseE])
   1.146 +
   1.147 +
   1.148 +subsection {*Negation*}
   1.149 +
   1.150 +lemma notI:
   1.151 +  assumes p: "P ==> False"
   1.152 +  shows "~P"
   1.153 +apply (unfold not_def)
   1.154 +apply (rules intro: impI p)
   1.155 +done
   1.156 +
   1.157 +lemma False_not_True: "False ~= True"
   1.158 +apply (rule notI)
   1.159 +apply (erule False_neq_True)
   1.160 +done
   1.161 +
   1.162 +lemma True_not_False: "True ~= False"
   1.163 +apply (rule notI)
   1.164 +apply (drule sym)
   1.165 +apply (erule False_neq_True)
   1.166 +done
   1.167 +
   1.168 +lemma notE: "[| ~P;  P |] ==> R"
   1.169 +apply (unfold not_def)
   1.170 +apply (erule mp [THEN FalseE])
   1.171 +apply assumption
   1.172 +done
   1.173 +
   1.174 +(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
   1.175 +lemmas notI2 = notE [THEN notI, standard]
   1.176 +
   1.177 +
   1.178 +subsection {*Implication*}
   1.179 +
   1.180 +lemma impE:
   1.181 +  assumes "P-->Q" "P" "Q ==> R"
   1.182 +  shows "R"
   1.183 +by (rules intro: prems mp)
   1.184 +
   1.185 +(* Reduces Q to P-->Q, allowing substitution in P. *)
   1.186 +lemma rev_mp: "[| P;  P --> Q |] ==> Q"
   1.187 +by (rules intro: mp)
   1.188 +
   1.189 +lemma contrapos_nn:
   1.190 +  assumes major: "~Q"
   1.191 +      and minor: "P==>Q"
   1.192 +  shows "~P"
   1.193 +by (rules intro: notI minor major [THEN notE])
   1.194 +
   1.195 +(*not used at all, but we already have the other 3 combinations *)
   1.196 +lemma contrapos_pn:
   1.197 +  assumes major: "Q"
   1.198 +      and minor: "P ==> ~Q"
   1.199 +  shows "~P"
   1.200 +by (rules intro: notI minor major notE)
   1.201 +
   1.202 +lemma not_sym: "t ~= s ==> s ~= t"
   1.203 +apply (erule contrapos_nn)
   1.204 +apply (erule sym)
   1.205 +done
   1.206 +
   1.207 +(*still used in HOLCF*)
   1.208 +lemma rev_contrapos:
   1.209 +  assumes pq: "P ==> Q"
   1.210 +      and nq: "~Q"
   1.211 +  shows "~P"
   1.212 +apply (rule nq [THEN contrapos_nn])
   1.213 +apply (erule pq)
   1.214 +done
   1.215 +
   1.216 +subsection {*Existential quantifier*}
   1.217 +
   1.218 +lemma exI: "P x ==> EX x::'a. P x"
   1.219 +apply (unfold Ex_def)
   1.220 +apply (rules intro: allI allE impI mp)
   1.221 +done
   1.222 +
   1.223 +lemma exE:
   1.224 +  assumes major: "EX x::'a. P(x)"
   1.225 +      and minor: "!!x. P(x) ==> Q"
   1.226 +  shows "Q"
   1.227 +apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
   1.228 +apply (rules intro: impI [THEN allI] minor)
   1.229 +done
   1.230 +
   1.231 +
   1.232 +subsection {*Conjunction*}
   1.233 +
   1.234 +lemma conjI: "[| P; Q |] ==> P&Q"
   1.235 +apply (unfold and_def)
   1.236 +apply (rules intro: impI [THEN allI] mp)
   1.237 +done
   1.238 +
   1.239 +lemma conjunct1: "[| P & Q |] ==> P"
   1.240 +apply (unfold and_def)
   1.241 +apply (rules intro: impI dest: spec mp)
   1.242 +done
   1.243 +
   1.244 +lemma conjunct2: "[| P & Q |] ==> Q"
   1.245 +apply (unfold and_def)
   1.246 +apply (rules intro: impI dest: spec mp)
   1.247 +done
   1.248 +
   1.249 +lemma conjE:
   1.250 +  assumes major: "P&Q"
   1.251 +      and minor: "[| P; Q |] ==> R"
   1.252 +  shows "R"
   1.253 +apply (rule minor)
   1.254 +apply (rule major [THEN conjunct1])
   1.255 +apply (rule major [THEN conjunct2])
   1.256 +done
   1.257 +
   1.258 +lemma context_conjI:
   1.259 +  assumes prems: "P" "P ==> Q" shows "P & Q"
   1.260 +by (rules intro: conjI prems)
   1.261 +
   1.262 +
   1.263 +subsection {*Disjunction*}
   1.264 +
   1.265 +lemma disjI1: "P ==> P|Q"
   1.266 +apply (unfold or_def)
   1.267 +apply (rules intro: allI impI mp)
   1.268 +done
   1.269 +
   1.270 +lemma disjI2: "Q ==> P|Q"
   1.271 +apply (unfold or_def)
   1.272 +apply (rules intro: allI impI mp)
   1.273 +done
   1.274 +
   1.275 +lemma disjE:
   1.276 +  assumes major: "P|Q"
   1.277 +      and minorP: "P ==> R"
   1.278 +      and minorQ: "Q ==> R"
   1.279 +  shows "R"
   1.280 +by (rules intro: minorP minorQ impI
   1.281 +                 major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   1.282 +
   1.283 +
   1.284 +subsection {*Classical logic*}
   1.285 +
   1.286 +
   1.287 +lemma classical:
   1.288 +  assumes prem: "~P ==> P"
   1.289 +  shows "P"
   1.290 +apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   1.291 +apply assumption
   1.292 +apply (rule notI [THEN prem, THEN eqTrueI])
   1.293 +apply (erule subst)
   1.294 +apply assumption
   1.295 +done
   1.296 +
   1.297 +lemmas ccontr = FalseE [THEN classical, standard]
   1.298 +
   1.299 +(*notE with premises exchanged; it discharges ~R so that it can be used to
   1.300 +  make elimination rules*)
   1.301 +lemma rev_notE:
   1.302 +  assumes premp: "P"
   1.303 +      and premnot: "~R ==> ~P"
   1.304 +  shows "R"
   1.305 +apply (rule ccontr)
   1.306 +apply (erule notE [OF premnot premp])
   1.307 +done
   1.308 +
   1.309 +(*Double negation law*)
   1.310 +lemma notnotD: "~~P ==> P"
   1.311 +apply (rule classical)
   1.312 +apply (erule notE)
   1.313 +apply assumption
   1.314 +done
   1.315 +
   1.316 +lemma contrapos_pp:
   1.317 +  assumes p1: "Q"
   1.318 +      and p2: "~P ==> ~Q"
   1.319 +  shows "P"
   1.320 +by (rules intro: classical p1 p2 notE)
   1.321 +
   1.322 +
   1.323 +subsection {*Unique existence*}
   1.324 +
   1.325 +lemma ex1I:
   1.326 +  assumes prems: "P a" "!!x. P(x) ==> x=a"
   1.327 +  shows "EX! x. P(x)"
   1.328 +by (unfold Ex1_def, rules intro: prems exI conjI allI impI)
   1.329 +
   1.330 +text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
   1.331 +lemma ex_ex1I:
   1.332 +  assumes ex_prem: "EX x. P(x)"
   1.333 +      and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
   1.334 +  shows "EX! x. P(x)"
   1.335 +by (rules intro: ex_prem [THEN exE] ex1I eq)
   1.336 +
   1.337 +lemma ex1E:
   1.338 +  assumes major: "EX! x. P(x)"
   1.339 +      and minor: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
   1.340 +  shows "R"
   1.341 +apply (rule major [unfolded Ex1_def, THEN exE])
   1.342 +apply (erule conjE)
   1.343 +apply (rules intro: minor)
   1.344 +done
   1.345 +
   1.346 +lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
   1.347 +apply (erule ex1E)
   1.348 +apply (rule exI)
   1.349 +apply assumption
   1.350 +done
   1.351 +
   1.352 +
   1.353 +subsection {*THE: definite description operator*}
   1.354 +
   1.355 +lemma the_equality:
   1.356 +  assumes prema: "P a"
   1.357 +      and premx: "!!x. P x ==> x=a"
   1.358 +  shows "(THE x. P x) = a"
   1.359 +apply (rule trans [OF _ the_eq_trivial])
   1.360 +apply (rule_tac f = "The" in arg_cong)
   1.361 +apply (rule ext)
   1.362 +apply (rule iffI)
   1.363 + apply (erule premx)
   1.364 +apply (erule ssubst, rule prema)
   1.365 +done
   1.366 +
   1.367 +lemma theI:
   1.368 +  assumes "P a" and "!!x. P x ==> x=a"
   1.369 +  shows "P (THE x. P x)"
   1.370 +by (rules intro: prems the_equality [THEN ssubst])
   1.371 +
   1.372 +lemma theI': "EX! x. P x ==> P (THE x. P x)"
   1.373 +apply (erule ex1E)
   1.374 +apply (erule theI)
   1.375 +apply (erule allE)
   1.376 +apply (erule mp)
   1.377 +apply assumption
   1.378 +done
   1.379 +
   1.380 +(*Easier to apply than theI: only one occurrence of P*)
   1.381 +lemma theI2:
   1.382 +  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
   1.383 +  shows "Q (THE x. P x)"
   1.384 +by (rules intro: prems theI)
   1.385 +
   1.386 +lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
   1.387 +apply (rule the_equality)
   1.388 +apply  assumption
   1.389 +apply (erule ex1E)
   1.390 +apply (erule all_dupE)
   1.391 +apply (drule mp)
   1.392 +apply  assumption
   1.393 +apply (erule ssubst)
   1.394 +apply (erule allE)
   1.395 +apply (erule mp)
   1.396 +apply assumption
   1.397 +done
   1.398 +
   1.399 +lemma the_sym_eq_trivial: "(THE y. x=y) = x"
   1.400 +apply (rule the_equality)
   1.401 +apply (rule refl)
   1.402 +apply (erule sym)
   1.403 +done
   1.404 +
   1.405 +
   1.406 +subsection {*Classical intro rules for disjunction and existential quantifiers*}
   1.407 +
   1.408 +lemma disjCI:
   1.409 +  assumes "~Q ==> P" shows "P|Q"
   1.410 +apply (rule classical)
   1.411 +apply (rules intro: prems disjI1 disjI2 notI elim: notE)
   1.412 +done
   1.413 +
   1.414 +lemma excluded_middle: "~P | P"
   1.415 +by (rules intro: disjCI)
   1.416 +
   1.417 +text{*case distinction as a natural deduction rule. Note that @{term "~P"}
   1.418 +   is the second case, not the first.*}
   1.419 +lemma case_split_thm:
   1.420 +  assumes prem1: "P ==> Q"
   1.421 +      and prem2: "~P ==> Q"
   1.422 +  shows "Q"
   1.423 +apply (rule excluded_middle [THEN disjE])
   1.424 +apply (erule prem2)
   1.425 +apply (erule prem1)
   1.426 +done
   1.427 +
   1.428 +(*Classical implies (-->) elimination. *)
   1.429 +lemma impCE:
   1.430 +  assumes major: "P-->Q"
   1.431 +      and minor: "~P ==> R" "Q ==> R"
   1.432 +  shows "R"
   1.433 +apply (rule excluded_middle [of P, THEN disjE])
   1.434 +apply (rules intro: minor major [THEN mp])+
   1.435 +done
   1.436 +
   1.437 +(*This version of --> elimination works on Q before P.  It works best for
   1.438 +  those cases in which P holds "almost everywhere".  Can't install as
   1.439 +  default: would break old proofs.*)
   1.440 +lemma impCE':
   1.441 +  assumes major: "P-->Q"
   1.442 +      and minor: "Q ==> R" "~P ==> R"
   1.443 +  shows "R"
   1.444 +apply (rule excluded_middle [of P, THEN disjE])
   1.445 +apply (rules intro: minor major [THEN mp])+
   1.446 +done
   1.447 +
   1.448 +(*Classical <-> elimination. *)
   1.449 +lemma iffCE:
   1.450 +  assumes major: "P=Q"
   1.451 +      and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
   1.452 +  shows "R"
   1.453 +apply (rule major [THEN iffE])
   1.454 +apply (rules intro: minor elim: impCE notE)
   1.455 +done
   1.456 +
   1.457 +lemma exCI:
   1.458 +  assumes "ALL x. ~P(x) ==> P(a)"
   1.459 +  shows "EX x. P(x)"
   1.460 +apply (rule ccontr)
   1.461 +apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"])
   1.462 +done
   1.463 +
   1.464 +
   1.465 +
   1.466  subsection {* Theory and package setup *}
   1.467  
   1.468 -subsubsection {* Basic lemmas *}
   1.469 +ML
   1.470 +{*
   1.471 +val plusI = thm "plusI"
   1.472 +val minusI = thm "minusI"
   1.473 +val timesI = thm "timesI"
   1.474 +val eq_reflection = thm "eq_reflection"
   1.475 +val refl = thm "refl"
   1.476 +val subst = thm "subst"
   1.477 +val ext = thm "ext"
   1.478 +val impI = thm "impI"
   1.479 +val mp = thm "mp"
   1.480 +val True_def = thm "True_def"
   1.481 +val All_def = thm "All_def"
   1.482 +val Ex_def = thm "Ex_def"
   1.483 +val False_def = thm "False_def"
   1.484 +val not_def = thm "not_def"
   1.485 +val and_def = thm "and_def"
   1.486 +val or_def = thm "or_def"
   1.487 +val Ex1_def = thm "Ex1_def"
   1.488 +val iff = thm "iff"
   1.489 +val True_or_False = thm "True_or_False"
   1.490 +val Let_def = thm "Let_def"
   1.491 +val if_def = thm "if_def"
   1.492 +val sym = thm "sym"
   1.493 +val ssubst = thm "ssubst"
   1.494 +val trans = thm "trans"
   1.495 +val def_imp_eq = thm "def_imp_eq"
   1.496 +val box_equals = thm "box_equals"
   1.497 +val fun_cong = thm "fun_cong"
   1.498 +val arg_cong = thm "arg_cong"
   1.499 +val cong = thm "cong"
   1.500 +val iffI = thm "iffI"
   1.501 +val iffD2 = thm "iffD2"
   1.502 +val rev_iffD2 = thm "rev_iffD2"
   1.503 +val iffD1 = thm "iffD1"
   1.504 +val rev_iffD1 = thm "rev_iffD1"
   1.505 +val iffE = thm "iffE"
   1.506 +val TrueI = thm "TrueI"
   1.507 +val eqTrueI = thm "eqTrueI"
   1.508 +val eqTrueE = thm "eqTrueE"
   1.509 +val allI = thm "allI"
   1.510 +val spec = thm "spec"
   1.511 +val allE = thm "allE"
   1.512 +val all_dupE = thm "all_dupE"
   1.513 +val FalseE = thm "FalseE"
   1.514 +val False_neq_True = thm "False_neq_True"
   1.515 +val notI = thm "notI"
   1.516 +val False_not_True = thm "False_not_True"
   1.517 +val True_not_False = thm "True_not_False"
   1.518 +val notE = thm "notE"
   1.519 +val notI2 = thm "notI2"
   1.520 +val impE = thm "impE"
   1.521 +val rev_mp = thm "rev_mp"
   1.522 +val contrapos_nn = thm "contrapos_nn"
   1.523 +val contrapos_pn = thm "contrapos_pn"
   1.524 +val not_sym = thm "not_sym"
   1.525 +val rev_contrapos = thm "rev_contrapos"
   1.526 +val exI = thm "exI"
   1.527 +val exE = thm "exE"
   1.528 +val conjI = thm "conjI"
   1.529 +val conjunct1 = thm "conjunct1"
   1.530 +val conjunct2 = thm "conjunct2"
   1.531 +val conjE = thm "conjE"
   1.532 +val context_conjI = thm "context_conjI"
   1.533 +val disjI1 = thm "disjI1"
   1.534 +val disjI2 = thm "disjI2"
   1.535 +val disjE = thm "disjE"
   1.536 +val classical = thm "classical"
   1.537 +val ccontr = thm "ccontr"
   1.538 +val rev_notE = thm "rev_notE"
   1.539 +val notnotD = thm "notnotD"
   1.540 +val contrapos_pp = thm "contrapos_pp"
   1.541 +val ex1I = thm "ex1I"
   1.542 +val ex_ex1I = thm "ex_ex1I"
   1.543 +val ex1E = thm "ex1E"
   1.544 +val ex1_implies_ex = thm "ex1_implies_ex"
   1.545 +val the_equality = thm "the_equality"
   1.546 +val theI = thm "theI"
   1.547 +val theI' = thm "theI'"
   1.548 +val theI2 = thm "theI2"
   1.549 +val the1_equality = thm "the1_equality"
   1.550 +val the_sym_eq_trivial = thm "the_sym_eq_trivial"
   1.551 +val disjCI = thm "disjCI"
   1.552 +val excluded_middle = thm "excluded_middle"
   1.553 +val case_split_thm = thm "case_split_thm"
   1.554 +val impCE = thm "impCE"
   1.555 +val impCE = thm "impCE"
   1.556 +val iffCE = thm "iffCE"
   1.557 +val exCI = thm "exCI"
   1.558  
   1.559 -use "HOL_lemmas.ML"
   1.560 +(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   1.561 +local
   1.562 +  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
   1.563 +  |   wrong_prem (Bound _) = true
   1.564 +  |   wrong_prem _ = false
   1.565 +  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
   1.566 +in
   1.567 +  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp])
   1.568 +  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
   1.569 +end
   1.570 +
   1.571 +
   1.572 +fun strip_tac i = REPEAT(resolve_tac [impI,allI] i)
   1.573 +
   1.574 +(*Obsolete form of disjunctive case analysis*)
   1.575 +fun excluded_middle_tac sP =
   1.576 +    res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
   1.577 +
   1.578 +fun case_tac a = res_inst_tac [("P",a)] case_split_thm
   1.579 +*}
   1.580 +
   1.581  theorems case_split = case_split_thm [case_names True False]
   1.582  
   1.583  
   1.584 @@ -549,7 +1105,7 @@
   1.585  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
   1.586  setup Splitter.setup setup Clasimp.setup
   1.587  
   1.588 -declare disj_absorb [simp] conj_absorb [simp] 
   1.589 +declare disj_absorb [simp] conj_absorb [simp]
   1.590  
   1.591  lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
   1.592  by blast+
   1.593 @@ -632,14 +1188,14 @@
   1.594  ML {*
   1.595    structure InductMethod = InductMethodFun
   1.596    (struct
   1.597 -    val dest_concls = HOLogic.dest_concls;
   1.598 -    val cases_default = thm "case_split";
   1.599 -    val local_impI = thm "induct_impliesI";
   1.600 -    val conjI = thm "conjI";
   1.601 -    val atomize = thms "induct_atomize";
   1.602 -    val rulify1 = thms "induct_rulify1";
   1.603 -    val rulify2 = thms "induct_rulify2";
   1.604 -    val localize = [Thm.symmetric (thm "induct_implies_def")];
   1.605 +    val dest_concls = HOLogic.dest_concls
   1.606 +    val cases_default = thm "case_split"
   1.607 +    val local_impI = thm "induct_impliesI"
   1.608 +    val conjI = thm "conjI"
   1.609 +    val atomize = thms "induct_atomize"
   1.610 +    val rulify1 = thms "induct_rulify1"
   1.611 +    val rulify2 = thms "induct_rulify2"
   1.612 +    val localize = [Thm.symmetric (thm "induct_implies_def")]
   1.613    end);
   1.614  *}
   1.615  
   1.616 @@ -758,7 +1314,7 @@
   1.617    apply (erule contrapos_np, simp)
   1.618    done
   1.619  
   1.620 -lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"  
   1.621 +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
   1.622  by (blast intro: order_antisym)
   1.623  
   1.624  lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
   1.625 @@ -1030,15 +1586,15 @@
   1.626  	  case dec t of
   1.627  	    None => None
   1.628  	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   1.629 -	| dec (Const ("op =",  _) $ t1 $ t2) = 
   1.630 +	| dec (Const ("op =",  _) $ t1 $ t2) =
   1.631  	    if of_sort t1
   1.632  	    then Some (t1, "=", t2)
   1.633  	    else None
   1.634 -	| dec (Const ("op <=",  _) $ t1 $ t2) = 
   1.635 +	| dec (Const ("op <=",  _) $ t1 $ t2) =
   1.636  	    if of_sort t1
   1.637  	    then Some (t1, "<=", t2)
   1.638  	    else None
   1.639 -	| dec (Const ("op <",  _) $ t1 $ t2) = 
   1.640 +	| dec (Const ("op <",  _) $ t1 $ t2) =
   1.641  	    if of_sort t1
   1.642  	    then Some (t1, "<", t2)
   1.643  	    else None
   1.644 @@ -1100,7 +1656,7 @@
   1.645  (*
   1.646  method_setup trans_partial =
   1.647    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
   1.648 -  {* transitivity reasoner for partial orders *}	    
   1.649 +  {* transitivity reasoner for partial orders *}	
   1.650  method_setup trans_linear =
   1.651    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   1.652    {* transitivity reasoner for linear orders *}
   1.653 @@ -1168,36 +1724,36 @@
   1.654    fun mk v v' q n P =
   1.655      if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
   1.656      then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   1.657 -  fun all_tr' [Const ("_bound",_) $ Free (v,_), 
   1.658 -               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   1.659 +  fun all_tr' [Const ("_bound",_) $ Free (v,_),
   1.660 +               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.661      mk v v' "_lessAll" n P
   1.662  
   1.663 -  | all_tr' [Const ("_bound",_) $ Free (v,_), 
   1.664 -               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   1.665 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.666 +               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.667      mk v v' "_leAll" n P
   1.668  
   1.669 -  | all_tr' [Const ("_bound",_) $ Free (v,_), 
   1.670 -               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
   1.671 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.672 +               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.673      mk v v' "_gtAll" n P
   1.674  
   1.675 -  | all_tr' [Const ("_bound",_) $ Free (v,_), 
   1.676 -               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
   1.677 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.678 +               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.679      mk v v' "_geAll" n P;
   1.680  
   1.681 -  fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
   1.682 -               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   1.683 +  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.684 +               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.685      mk v v' "_lessEx" n P
   1.686  
   1.687 -  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
   1.688 -               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   1.689 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.690 +               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.691      mk v v' "_leEx" n P
   1.692  
   1.693 -  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
   1.694 -               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
   1.695 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.696 +               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.697      mk v v' "_gtEx" n P
   1.698  
   1.699 -  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
   1.700 -               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
   1.701 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.702 +               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.703      mk v v' "_geEx" n P
   1.704  in
   1.705  [("ALL ", all_tr'), ("EX ", ex_tr')]
   1.706 @@ -1205,3 +1761,4 @@
   1.707  *}
   1.708  
   1.709  end
   1.710 +
     2.1 --- a/src/HOL/HOL_lemmas.ML	Tue Dec 14 14:53:02 2004 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,475 +0,0 @@
     2.4 -(*  Title:      HOL/HOL_lemmas.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1991  University of Cambridge
     2.8 -
     2.9 -Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
    2.10 -*)
    2.11 -
    2.12 -(* legacy ML bindings *)
    2.13 -
    2.14 -val plusI = thm "plusI";
    2.15 -val minusI = thm "minusI";
    2.16 -val timesI = thm "timesI";
    2.17 -val eq_reflection = thm "eq_reflection";
    2.18 -val refl = thm "refl";
    2.19 -val subst = thm "subst";
    2.20 -val ext = thm "ext";
    2.21 -val impI = thm "impI";
    2.22 -val mp = thm "mp";
    2.23 -val True_def = thm "True_def";
    2.24 -val All_def = thm "All_def";
    2.25 -val Ex_def = thm "Ex_def";
    2.26 -val False_def = thm "False_def";
    2.27 -val not_def = thm "not_def";
    2.28 -val and_def = thm "and_def";
    2.29 -val or_def = thm "or_def";
    2.30 -val Ex1_def = thm "Ex1_def";
    2.31 -val iff = thm "iff";
    2.32 -val True_or_False = thm "True_or_False";
    2.33 -val Let_def = thm "Let_def";
    2.34 -val if_def = thm "if_def";
    2.35 -
    2.36 -
    2.37 -section "Equality";
    2.38 -
    2.39 -Goal "s=t ==> t=s";
    2.40 -by (etac subst 1);
    2.41 -by (rtac refl 1);
    2.42 -qed "sym";
    2.43 -
    2.44 -(*calling "standard" reduces maxidx to 0*)
    2.45 -bind_thm ("ssubst", sym RS subst);
    2.46 -
    2.47 -Goal "[| r=s; s=t |] ==> r=t";
    2.48 -by (etac subst 1 THEN assume_tac 1);
    2.49 -qed "trans";
    2.50 -
    2.51 -val prems = goal (the_context()) "(A == B) ==> A = B";
    2.52 -by (rewrite_goals_tac prems);
    2.53 -by (rtac refl 1);
    2.54 -qed "def_imp_eq";
    2.55 -
    2.56 -(*Useful with eresolve_tac for proving equalties from known equalities.
    2.57 -        a = b
    2.58 -        |   |
    2.59 -        c = d   *)
    2.60 -Goal "[| a=b;  a=c;  b=d |] ==> c=d";
    2.61 -by (rtac trans 1);
    2.62 -by (rtac trans 1);
    2.63 -by (rtac sym 1);
    2.64 -by (REPEAT (assume_tac 1)) ;
    2.65 -qed "box_equals";
    2.66 -
    2.67 -
    2.68 -section "Congruence rules for application";
    2.69 -
    2.70 -(*similar to AP_THM in Gordon's HOL*)
    2.71 -Goal "(f::'a=>'b) = g ==> f(x)=g(x)";
    2.72 -by (etac subst 1);
    2.73 -by (rtac refl 1);
    2.74 -qed "fun_cong";
    2.75 -
    2.76 -(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    2.77 -Goal "x=y ==> f(x)=f(y)";
    2.78 -by (etac subst 1);
    2.79 -by (rtac refl 1);
    2.80 -qed "arg_cong";
    2.81 -
    2.82 -Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)";
    2.83 -by (etac subst 1);
    2.84 -by (etac subst 1);
    2.85 -by (rtac refl 1);
    2.86 -qed "cong";
    2.87 -
    2.88 -
    2.89 -section "Equality of booleans -- iff";
    2.90 -
    2.91 -val prems = Goal "[| P ==> Q;  Q ==> P |] ==> P=Q";
    2.92 -by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
    2.93 -qed "iffI";
    2.94 -
    2.95 -Goal "[| P=Q; Q |] ==> P";
    2.96 -by (etac ssubst 1);
    2.97 -by (assume_tac 1);
    2.98 -qed "iffD2";
    2.99 -
   2.100 -Goal "[| Q; P=Q |] ==> P";
   2.101 -by (etac iffD2 1);
   2.102 -by (assume_tac 1);
   2.103 -qed "rev_iffD2";
   2.104 -
   2.105 -bind_thm ("iffD1", sym RS iffD2);
   2.106 -bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
   2.107 -
   2.108 -val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R";
   2.109 -by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1));
   2.110 -qed "iffE";
   2.111 -
   2.112 -
   2.113 -section "True";
   2.114 -
   2.115 -Goalw [True_def] "True";
   2.116 -by (rtac refl 1);
   2.117 -qed "TrueI";
   2.118 -
   2.119 -Goal "P ==> P=True";
   2.120 -by (REPEAT (ares_tac [iffI,TrueI] 1));
   2.121 -qed "eqTrueI";
   2.122 -
   2.123 -Goal "P=True ==> P";
   2.124 -by (etac iffD2 1);
   2.125 -by (rtac TrueI 1);
   2.126 -qed "eqTrueE";
   2.127 -
   2.128 -
   2.129 -section "Universal quantifier";
   2.130 -
   2.131 -val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";
   2.132 -by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
   2.133 -qed "allI";
   2.134 -
   2.135 -Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";
   2.136 -by (rtac eqTrueE 1);
   2.137 -by (etac fun_cong 1);
   2.138 -qed "spec";
   2.139 -
   2.140 -val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
   2.141 -by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
   2.142 -qed "allE";
   2.143 -
   2.144 -val prems = Goal
   2.145 -    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
   2.146 -by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
   2.147 -qed "all_dupE";
   2.148 -
   2.149 -
   2.150 -section "False";
   2.151 -(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
   2.152 -
   2.153 -Goalw [False_def] "False ==> P";
   2.154 -by (etac spec 1);
   2.155 -qed "FalseE";
   2.156 -
   2.157 -Goal "False=True ==> P";
   2.158 -by (etac (eqTrueE RS FalseE) 1);
   2.159 -qed "False_neq_True";
   2.160 -
   2.161 -
   2.162 -section "Negation";
   2.163 -
   2.164 -val prems = Goalw [not_def] "(P ==> False) ==> ~P";
   2.165 -by (rtac impI 1);
   2.166 -by (eresolve_tac prems 1);
   2.167 -qed "notI";
   2.168 -
   2.169 -Goal "False ~= True";
   2.170 -by (rtac notI 1);
   2.171 -by (etac False_neq_True 1);
   2.172 -qed "False_not_True";
   2.173 -
   2.174 -Goal "True ~= False";
   2.175 -by (rtac notI 1);
   2.176 -by (dtac sym 1);
   2.177 -by (etac False_neq_True 1);
   2.178 -qed "True_not_False";
   2.179 -
   2.180 -Goalw [not_def] "[| ~P;  P |] ==> R";
   2.181 -by (etac (mp RS FalseE) 1);
   2.182 -by (assume_tac 1);
   2.183 -qed "notE";
   2.184 -
   2.185 -(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
   2.186 -bind_thm ("notI2", notE RS notI);
   2.187 -
   2.188 -
   2.189 -section "Implication";
   2.190 -
   2.191 -val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
   2.192 -by (REPEAT (resolve_tac (prems@[mp]) 1));
   2.193 -qed "impE";
   2.194 -
   2.195 -(* Reduces Q to P-->Q, allowing substitution in P. *)
   2.196 -Goal "[| P;  P --> Q |] ==> Q";
   2.197 -by (REPEAT (ares_tac [mp] 1)) ;
   2.198 -qed "rev_mp";
   2.199 -
   2.200 -val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
   2.201 -by (rtac (major RS notE RS notI) 1);
   2.202 -by (etac minor 1) ;
   2.203 -qed "contrapos_nn";
   2.204 -
   2.205 -(*not used at all, but we already have the other 3 combinations *)
   2.206 -val [major,minor] = Goal "[| Q;  P ==> ~Q |] ==> ~P";
   2.207 -by (rtac (minor RS notE RS notI) 1);
   2.208 -by (assume_tac 1);
   2.209 -by (rtac major 1) ;
   2.210 -qed "contrapos_pn";
   2.211 -
   2.212 -Goal "t ~= s ==> s ~= t";
   2.213 -by (etac contrapos_nn 1); 
   2.214 -by (etac sym 1); 
   2.215 -qed "not_sym";
   2.216 -
   2.217 -(*still used in HOLCF*)
   2.218 -val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
   2.219 -by (rtac (minor RS contrapos_nn) 1);
   2.220 -by (etac major 1) ;
   2.221 -qed "rev_contrapos";
   2.222 -
   2.223 -section "Existential quantifier";
   2.224 -
   2.225 -Goalw [Ex_def] "P x ==> EX x::'a. P x";
   2.226 -by (rtac allI 1); 
   2.227 -by (rtac impI 1); 
   2.228 -by (etac allE 1); 
   2.229 -by (etac mp 1) ;
   2.230 -by (assume_tac 1); 
   2.231 -qed "exI";
   2.232 -
   2.233 -val [major,minor] =
   2.234 -Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
   2.235 -by (rtac (major RS spec RS mp) 1); 
   2.236 -by (rtac (impI RS allI) 1); 
   2.237 -by (etac minor 1); 
   2.238 -qed "exE";
   2.239 -
   2.240 -
   2.241 -section "Conjunction";
   2.242 -
   2.243 -Goalw [and_def] "[| P; Q |] ==> P&Q";
   2.244 -by (rtac (impI RS allI) 1);
   2.245 -by (etac (mp RS mp) 1);
   2.246 -by (REPEAT (assume_tac 1));
   2.247 -qed "conjI";
   2.248 -
   2.249 -Goalw [and_def] "[| P & Q |] ==> P";
   2.250 -by (dtac spec 1) ;
   2.251 -by (etac mp 1);
   2.252 -by (REPEAT (ares_tac [impI] 1));
   2.253 -qed "conjunct1";
   2.254 -
   2.255 -Goalw [and_def] "[| P & Q |] ==> Q";
   2.256 -by (dtac spec 1) ;
   2.257 -by (etac mp 1);
   2.258 -by (REPEAT (ares_tac [impI] 1));
   2.259 -qed "conjunct2";
   2.260 -
   2.261 -val [major,minor] =
   2.262 -Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
   2.263 -by (rtac minor 1);
   2.264 -by (rtac (major RS conjunct1) 1);
   2.265 -by (rtac (major RS conjunct2) 1);
   2.266 -qed "conjE";
   2.267 -
   2.268 -val prems =
   2.269 -Goal "[| P; P ==> Q |] ==> P & Q";
   2.270 -by (REPEAT (resolve_tac (conjI::prems) 1));
   2.271 -qed "context_conjI";
   2.272 -
   2.273 -
   2.274 -section "Disjunction";
   2.275 -
   2.276 -Goalw [or_def] "P ==> P|Q";
   2.277 -by (REPEAT (resolve_tac [allI,impI] 1));
   2.278 -by (etac mp 1 THEN assume_tac 1);
   2.279 -qed "disjI1";
   2.280 -
   2.281 -Goalw [or_def] "Q ==> P|Q";
   2.282 -by (REPEAT (resolve_tac [allI,impI] 1));
   2.283 -by (etac mp 1 THEN assume_tac 1);
   2.284 -qed "disjI2";
   2.285 -
   2.286 -val [major,minorP,minorQ] =
   2.287 -Goalw [or_def]  "[| P | Q; P ==> R; Q ==> R |] ==> R";
   2.288 -by (rtac (major RS spec RS mp RS mp) 1);
   2.289 -by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));
   2.290 -qed "disjE";
   2.291 -
   2.292 -
   2.293 -section "Classical logic";
   2.294 -(*CCONTR -- classical logic*)
   2.295 -
   2.296 -val [prem] = Goal  "(~P ==> P) ==> P";
   2.297 -by (rtac (True_or_False RS disjE RS eqTrueE) 1);
   2.298 -by (assume_tac 1);
   2.299 -by (rtac (notI RS prem RS eqTrueI) 1);
   2.300 -by (etac subst 1);
   2.301 -by (assume_tac 1);
   2.302 -qed "classical";
   2.303 -
   2.304 -bind_thm ("ccontr", FalseE RS classical);
   2.305 -
   2.306 -(*notE with premises exchanged; it discharges ~R so that it can be used to
   2.307 -  make elimination rules*)
   2.308 -val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R";
   2.309 -by (rtac ccontr 1);
   2.310 -by (etac ([premnot,premp] MRS notE) 1);
   2.311 -qed "rev_notE";
   2.312 -
   2.313 -(*Double negation law*)
   2.314 -Goal "~~P ==> P";
   2.315 -by (rtac classical 1);
   2.316 -by (etac notE 1);
   2.317 -by (assume_tac 1);
   2.318 -qed "notnotD";
   2.319 -
   2.320 -val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
   2.321 -by (rtac classical 1);
   2.322 -by (dtac p2 1);
   2.323 -by (etac notE 1);
   2.324 -by (rtac p1 1);
   2.325 -qed "contrapos_pp";
   2.326 -
   2.327 -
   2.328 -section "Unique existence";
   2.329 -
   2.330 -val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)";
   2.331 -by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
   2.332 -qed "ex1I";
   2.333 -
   2.334 -(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   2.335 -val [ex_prem,eq] = Goal
   2.336 -    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
   2.337 -by (rtac (ex_prem RS exE) 1);
   2.338 -by (REPEAT (ares_tac [ex1I,eq] 1)) ;
   2.339 -qed "ex_ex1I";
   2.340 -
   2.341 -val major::prems = Goalw [Ex1_def]
   2.342 -    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R";
   2.343 -by (rtac (major RS exE) 1);
   2.344 -by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
   2.345 -qed "ex1E";
   2.346 -
   2.347 -Goal "EX! x. P x ==> EX x. P x";
   2.348 -by (etac ex1E 1);
   2.349 -by (rtac exI 1);
   2.350 -by (assume_tac 1);
   2.351 -qed "ex1_implies_ex";
   2.352 -
   2.353 -
   2.354 -section "THE: definite description operator";
   2.355 -
   2.356 -val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
   2.357 -by (rtac trans 1); 
   2.358 - by (rtac (thm "the_eq_trivial") 2);
   2.359 -by (res_inst_tac [("f","The")] arg_cong 1); 
   2.360 -by (rtac ext 1); 
   2.361 - by (rtac iffI 1); 
   2.362 -by (etac premx 1); 
   2.363 -by (etac ssubst 1 THEN rtac prema 1);
   2.364 -qed "the_equality";
   2.365 -
   2.366 -val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> P (THE x. P x)";
   2.367 -by (rtac (the_equality RS ssubst) 1);
   2.368 -by (REPEAT (ares_tac [prema,premx] 1));
   2.369 -qed "theI";
   2.370 -
   2.371 -Goal "EX! x. P x ==> P (THE x. P x)";
   2.372 -by (etac ex1E 1);
   2.373 -by (etac theI 1);
   2.374 -by (etac allE 1);
   2.375 -by (etac mp 1);
   2.376 -by (atac 1);
   2.377 -qed "theI'";
   2.378 -
   2.379 -(*Easier to apply than theI: only one occurrence of P*)
   2.380 -val [prema,premx,premq] = Goal
   2.381 -     "[| P a;  !!x. P x ==> x=a;  !!x. P x ==> Q x |] \
   2.382 -\     ==> Q (THE x. P x)";
   2.383 -by (rtac premq 1); 
   2.384 -by (rtac theI 1); 
   2.385 -by (REPEAT (ares_tac [prema,premx] 1));
   2.386 -qed "theI2";
   2.387 -
   2.388 -Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a";
   2.389 -by (rtac the_equality 1);
   2.390 -by  (atac 1);
   2.391 -by (etac ex1E 1);
   2.392 -by (etac all_dupE 1);
   2.393 -by (dtac mp 1);
   2.394 -by  (atac 1);
   2.395 -by (etac ssubst 1);
   2.396 -by (etac allE 1);
   2.397 -by (etac mp 1);
   2.398 -by (atac 1);
   2.399 -qed "the1_equality";
   2.400 -
   2.401 -Goal "(THE y. x=y) = x";
   2.402 -by (rtac the_equality 1);
   2.403 -by (rtac refl 1);
   2.404 -by (etac sym 1);
   2.405 -qed "the_sym_eq_trivial";
   2.406 -
   2.407 -
   2.408 -section "Classical intro rules for disjunction and existential quantifiers";
   2.409 -
   2.410 -val prems = Goal "(~Q ==> P) ==> P|Q";
   2.411 -by (rtac classical 1);
   2.412 -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   2.413 -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
   2.414 -qed "disjCI";
   2.415 -
   2.416 -Goal "~P | P";
   2.417 -by (REPEAT (ares_tac [disjCI] 1)) ;
   2.418 -qed "excluded_middle";
   2.419 -
   2.420 -(*For disjunctive case analysis*)
   2.421 -fun excluded_middle_tac sP =
   2.422 -    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   2.423 -
   2.424 -(*Classical implies (-->) elimination. *)
   2.425 -val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
   2.426 -by (rtac (excluded_middle RS disjE) 1);
   2.427 -by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
   2.428 -qed "impCE";
   2.429 -
   2.430 -(*This version of --> elimination works on Q before P.  It works best for
   2.431 -  those cases in which P holds "almost everywhere".  Can't install as
   2.432 -  default: would break old proofs.*)
   2.433 -val major::prems = Goal
   2.434 -    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
   2.435 -by (resolve_tac [excluded_middle RS disjE] 1);
   2.436 -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
   2.437 -qed "impCE'";
   2.438 -
   2.439 -(*Classical <-> elimination. *)
   2.440 -val major::prems = Goal
   2.441 -    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
   2.442 -by (rtac (major RS iffE) 1);
   2.443 -by (REPEAT (DEPTH_SOLVE_1
   2.444 -            (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
   2.445 -qed "iffCE";
   2.446 -
   2.447 -val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
   2.448 -by (rtac ccontr 1);
   2.449 -by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
   2.450 -qed "exCI";
   2.451 -
   2.452 -(* case distinction *)
   2.453 -
   2.454 -val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
   2.455 -by (rtac (excluded_middle RS disjE) 1);
   2.456 -by (etac prem2 1);
   2.457 -by (etac prem1 1);
   2.458 -qed "case_split_thm";
   2.459 -
   2.460 -fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   2.461 -
   2.462 -
   2.463 -(** Standard abbreviations **)
   2.464 -
   2.465 -(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   2.466 -local
   2.467 -  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
   2.468 -  |   wrong_prem (Bound _) = true
   2.469 -  |   wrong_prem _ = false;
   2.470 -  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));
   2.471 -in
   2.472 -  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   2.473 -  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
   2.474 -end;
   2.475 -
   2.476 -
   2.477 -fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
   2.478 -
     3.1 --- a/src/HOL/IsaMakefile	Tue Dec 14 14:53:02 2004 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Wed Dec 15 10:19:01 2004 +0100
     3.3 @@ -84,7 +84,7 @@
     3.4    Datatype.thy Datatype_Universe.thy \
     3.5    Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
     3.6    Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
     3.7 -  HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
     3.8 +  HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
     3.9    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    3.10    Integ/IntArith.thy Integ/IntDef.thy \
    3.11    Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \