author  paulson 
Tue, 01 Feb 2005 18:01:57 +0100  
changeset 15481  fc075ae929e4 
parent 15423  761a4f8e6ad6 
child 15524  2ef571f80a55 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
2 
ID: $Id$ 

11750  3 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
4 
*) 

923  5 

11750  6 
header {* The basis of HigherOrder Logic *} 
923  7 

15131  8 
theory HOL 
15140  9 
imports CPure 
15411  10 
files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("antisym_setup.ML") 
15481  11 
("eqrule_HOL_data.ML") 
12 
("~~/src/Provers/eqsubst.ML") 

15131  13 
begin 
2260  14 

11750  15 
subsection {* Primitive logic *} 
16 

17 
subsubsection {* Core syntax *} 

2260  18 

14854  19 
classes type 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

20 
defaultsort type 
3947  21 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

22 
global 
923  23 

7357  24 
typedecl bool 
923  25 

26 
arities 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

27 
bool :: type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

28 
fun :: (type, type) type 
923  29 

11750  30 
judgment 
31 
Trueprop :: "bool => prop" ("(_)" 5) 

923  32 

11750  33 
consts 
7357  34 
Not :: "bool => bool" ("~ _" [40] 40) 
35 
True :: bool 

36 
False :: bool 

37 
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) 

3947  38 
arbitrary :: 'a 
923  39 

11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

40 
The :: "('a => bool) => 'a" 
7357  41 
All :: "('a => bool) => bool" (binder "ALL " 10) 
42 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

43 
Ex1 :: "('a => bool) => bool" (binder "EX! " 10) 

44 
Let :: "['a, 'a => 'b] => 'b" 

923  45 

7357  46 
"=" :: "['a, 'a] => bool" (infixl 50) 
47 
& :: "[bool, bool] => bool" (infixr 35) 

48 
"" :: "[bool, bool] => bool" (infixr 30) 

49 
> :: "[bool, bool] => bool" (infixr 25) 

923  50 

10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

51 
local 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

52 

2260  53 

11750  54 
subsubsection {* Additional concrete syntax *} 
2260  55 

4868  56 
nonterminals 
923  57 
letbinds letbind 
58 
case_syn cases_syn 

59 

60 
syntax 

12650  61 
"_not_equal" :: "['a, 'a] => bool" (infixl "~=" 50) 
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

62 
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) 
923  63 

7357  64 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 
65 
"" :: "letbind => letbinds" ("_") 

66 
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") 

67 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

923  68 

9060
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

69 
"_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) 
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

70 
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) 
7357  71 
"" :: "case_syn => cases_syn" ("_") 
9060
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

72 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  73 

74 
translations 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

75 
"x ~= y" == "~ (x = y)" 
13764  76 
"THE x. P" == "The (%x. P)" 
923  77 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  78 
"let x = a in e" == "Let a (%x. e)" 
923  79 

13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

80 
print_translation {* 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

81 
(* To avoid etacontraction of body: *) 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

82 
[("The", fn [Abs abs] => 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

83 
let val (x,t) = atomic_abs_tr' abs 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

84 
in Syntax.const "_The" $ x $ t end)] 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

85 
*} 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

86 

12633  87 
syntax (output) 
11687  88 
"=" :: "['a, 'a] => bool" (infix 50) 
12650  89 
"_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) 
2260  90 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

91 
syntax (xsymbols) 
11687  92 
Not :: "bool => bool" ("\<not> _" [40] 40) 
93 
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) 

94 
"op " :: "[bool, bool] => bool" (infixr "\<or>" 30) 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

95 
"op >" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) 
12650  96 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
11687  97 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 
98 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

99 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

100 
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 

14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14357
diff
changeset

101 
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*) 
2372  102 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

103 
syntax (xsymbols output) 
12650  104 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
3820  105 

6340  106 
syntax (HTML output) 
14565  107 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
11687  108 
Not :: "bool => bool" ("\<not> _" [40] 40) 
14565  109 
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) 
110 
"op " :: "[bool, bool] => bool" (infixr "\<or>" 30) 

111 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 

112 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 

113 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

114 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

6340  115 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

116 
syntax (HOL) 
7357  117 
"ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) 
118 
"EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) 

119 
"EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

120 

36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

121 

11750  122 
subsubsection {* Axioms and basic definitions *} 
2260  123 

7357  124 
axioms 
15380  125 
eq_reflection: "(x=y) ==> (x==y)" 
923  126 

15380  127 
refl: "t = (t::'a)" 
6289  128 

15380  129 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 
130 
 {*Extensionality is built into the metalogic, and this rule expresses 

131 
a related property. It is an etaexpanded version of the traditional 

132 
rule, and similar to the ABS rule of HOL*} 

6289  133 

11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

134 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  135 

15380  136 
impI: "(P ==> Q) ==> P>Q" 
137 
mp: "[ P>Q; P ] ==> Q" 

138 

139 

140 
text{*Thanks to Stephan Merz*} 

141 
theorem subst: 

142 
assumes eq: "s = t" and p: "P(s)" 

143 
shows "P(t::'a)" 

144 
proof  

145 
from eq have meta: "s \<equiv> t" 

146 
by (rule eq_reflection) 

147 
from p show ?thesis 

148 
by (unfold meta) 

149 
qed 

923  150 

151 
defs 

7357  152 
True_def: "True == ((%x::bool. x) = (%x. x))" 
153 
All_def: "All(P) == (P = (%x. True))" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

154 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  155 
False_def: "False == (!P. P)" 
156 
not_def: "~ P == P>False" 

157 
and_def: "P & Q == !R. (P>Q>R) > R" 

158 
or_def: "P  Q == !R. (P>R) > (Q>R) > R" 

159 
Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) > y=x)" 

923  160 

7357  161 
axioms 
162 
iff: "(P>Q) > (Q>P) > (P=Q)" 

163 
True_or_False: "(P=True)  (P=False)" 

923  164 

165 
defs 

7357  166 
Let_def: "Let s f == f(s)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

167 
if_def: "If P x y == THE z::'a. (P=True > z=x) & (P=False > z=y)" 
5069  168 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

169 
finalconsts 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

170 
"op =" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

171 
"op >" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

172 
The 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

173 
arbitrary 
3320  174 

11750  175 
subsubsection {* Generic algebraic operations *} 
4868  176 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

177 
axclass zero < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

178 
axclass one < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

179 
axclass plus < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

180 
axclass minus < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

181 
axclass times < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

182 
axclass inverse < type 
11750  183 

184 
global 

185 

186 
consts 

187 
"0" :: "'a::zero" ("0") 

188 
"1" :: "'a::one" ("1") 

189 
"+" :: "['a::plus, 'a] => 'a" (infixl 65) 

190 
 :: "['a::minus, 'a] => 'a" (infixl 65) 

191 
uminus :: "['a::minus] => 'a" (" _" [81] 80) 

192 
* :: "['a::times, 'a] => 'a" (infixl 70) 

193 

13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

194 
syntax 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

195 
"_index1" :: index ("\<^sub>1") 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

196 
translations 
14690  197 
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" 
13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

198 

11750  199 
local 
200 

201 
typed_print_translation {* 

202 
let 

203 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 

204 
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match 

205 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 

206 
in [tr' "0", tr' "1"] end; 

207 
*}  {* show types that are presumably too general *} 

208 

209 

210 
consts 

211 
abs :: "'a::minus => 'a" 

212 
inverse :: "'a::inverse => 'a" 

213 
divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) 

214 

215 
syntax (xsymbols) 

216 
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") 

217 
syntax (HTML output) 

218 
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") 

219 

220 

15411  221 
subsection {*Equality*} 
222 

223 
lemma sym: "s=t ==> t=s" 

224 
apply (erule subst) 

225 
apply (rule refl) 

226 
done 

227 

228 
(*calling "standard" reduces maxidx to 0*) 

229 
lemmas ssubst = sym [THEN subst, standard] 

230 

231 
lemma trans: "[ r=s; s=t ] ==> r=t" 

232 
apply (erule subst , assumption) 

233 
done 

234 

235 
lemma def_imp_eq: assumes meq: "A == B" shows "A = B" 

236 
apply (unfold meq) 

237 
apply (rule refl) 

238 
done 

239 

240 
(*Useful with eresolve_tac for proving equalties from known equalities. 

241 
a = b 

242 
  

243 
c = d *) 

244 
lemma box_equals: "[ a=b; a=c; b=d ] ==> c=d" 

245 
apply (rule trans) 

246 
apply (rule trans) 

247 
apply (rule sym) 

248 
apply assumption+ 

249 
done 

250 

251 

252 
subsection {*Congruence rules for application*} 

253 

254 
(*similar to AP_THM in Gordon's HOL*) 

255 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 

256 
apply (erule subst) 

257 
apply (rule refl) 

258 
done 

259 

260 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) 

261 
lemma arg_cong: "x=y ==> f(x)=f(y)" 

262 
apply (erule subst) 

263 
apply (rule refl) 

264 
done 

265 

266 
lemma cong: "[ f = g; (x::'a) = y ] ==> f(x) = g(y)" 

267 
apply (erule subst)+ 

268 
apply (rule refl) 

269 
done 

270 

271 

272 
subsection {*Equality of booleans  iff*} 

273 

274 
lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" 

275 
apply (rules intro: iff [THEN mp, THEN mp] impI prems) 

276 
done 

277 

278 
lemma iffD2: "[ P=Q; Q ] ==> P" 

279 
apply (erule ssubst) 

280 
apply assumption 

281 
done 

282 

283 
lemma rev_iffD2: "[ Q; P=Q ] ==> P" 

284 
apply (erule iffD2) 

285 
apply assumption 

286 
done 

287 

288 
lemmas iffD1 = sym [THEN iffD2, standard] 

289 
lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard] 

290 

291 
lemma iffE: 

292 
assumes major: "P=Q" 

293 
and minor: "[ P > Q; Q > P ] ==> R" 

294 
shows "R" 

295 
by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1]) 

296 

297 

298 
subsection {*True*} 

299 

300 
lemma TrueI: "True" 

301 
apply (unfold True_def) 

302 
apply (rule refl) 

303 
done 

304 

305 
lemma eqTrueI: "P ==> P=True" 

306 
by (rules intro: iffI TrueI) 

307 

308 
lemma eqTrueE: "P=True ==> P" 

309 
apply (erule iffD2) 

310 
apply (rule TrueI) 

311 
done 

312 

313 

314 
subsection {*Universal quantifier*} 

315 

316 
lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)" 

317 
apply (unfold All_def) 

318 
apply (rules intro: ext eqTrueI p) 

319 
done 

320 

321 
lemma spec: "ALL x::'a. P(x) ==> P(x)" 

322 
apply (unfold All_def) 

323 
apply (rule eqTrueE) 

324 
apply (erule fun_cong) 

325 
done 

326 

327 
lemma allE: 

328 
assumes major: "ALL x. P(x)" 

329 
and minor: "P(x) ==> R" 

330 
shows "R" 

331 
by (rules intro: minor major [THEN spec]) 

332 

333 
lemma all_dupE: 

334 
assumes major: "ALL x. P(x)" 

335 
and minor: "[ P(x); ALL x. P(x) ] ==> R" 

336 
shows "R" 

337 
by (rules intro: minor major major [THEN spec]) 

338 

339 

340 
subsection {*False*} 

341 
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*) 

342 

343 
lemma FalseE: "False ==> P" 

344 
apply (unfold False_def) 

345 
apply (erule spec) 

346 
done 

347 

348 
lemma False_neq_True: "False=True ==> P" 

349 
by (erule eqTrueE [THEN FalseE]) 

350 

351 

352 
subsection {*Negation*} 

353 

354 
lemma notI: 

355 
assumes p: "P ==> False" 

356 
shows "~P" 

357 
apply (unfold not_def) 

358 
apply (rules intro: impI p) 

359 
done 

360 

361 
lemma False_not_True: "False ~= True" 

362 
apply (rule notI) 

363 
apply (erule False_neq_True) 

364 
done 

365 

366 
lemma True_not_False: "True ~= False" 

367 
apply (rule notI) 

368 
apply (drule sym) 

369 
apply (erule False_neq_True) 

370 
done 

371 

372 
lemma notE: "[ ~P; P ] ==> R" 

373 
apply (unfold not_def) 

374 
apply (erule mp [THEN FalseE]) 

375 
apply assumption 

376 
done 

377 

378 
(* Alternative ~ introduction rule: [ P ==> ~ Pa; P ==> Pa ] ==> ~ P *) 

379 
lemmas notI2 = notE [THEN notI, standard] 

380 

381 

382 
subsection {*Implication*} 

383 

384 
lemma impE: 

385 
assumes "P>Q" "P" "Q ==> R" 

386 
shows "R" 

387 
by (rules intro: prems mp) 

388 

389 
(* Reduces Q to P>Q, allowing substitution in P. *) 

390 
lemma rev_mp: "[ P; P > Q ] ==> Q" 

391 
by (rules intro: mp) 

392 

393 
lemma contrapos_nn: 

394 
assumes major: "~Q" 

395 
and minor: "P==>Q" 

396 
shows "~P" 

397 
by (rules intro: notI minor major [THEN notE]) 

398 

399 
(*not used at all, but we already have the other 3 combinations *) 

400 
lemma contrapos_pn: 

401 
assumes major: "Q" 

402 
and minor: "P ==> ~Q" 

403 
shows "~P" 

404 
by (rules intro: notI minor major notE) 

405 

406 
lemma not_sym: "t ~= s ==> s ~= t" 

407 
apply (erule contrapos_nn) 

408 
apply (erule sym) 

409 
done 

410 

411 
(*still used in HOLCF*) 

412 
lemma rev_contrapos: 

413 
assumes pq: "P ==> Q" 

414 
and nq: "~Q" 

415 
shows "~P" 

416 
apply (rule nq [THEN contrapos_nn]) 

417 
apply (erule pq) 

418 
done 

419 

420 
subsection {*Existential quantifier*} 

421 

422 
lemma exI: "P x ==> EX x::'a. P x" 

423 
apply (unfold Ex_def) 

424 
apply (rules intro: allI allE impI mp) 

425 
done 

426 

427 
lemma exE: 

428 
assumes major: "EX x::'a. P(x)" 

429 
and minor: "!!x. P(x) ==> Q" 

430 
shows "Q" 

431 
apply (rule major [unfolded Ex_def, THEN spec, THEN mp]) 

432 
apply (rules intro: impI [THEN allI] minor) 

433 
done 

434 

435 

436 
subsection {*Conjunction*} 

437 

438 
lemma conjI: "[ P; Q ] ==> P&Q" 

439 
apply (unfold and_def) 

440 
apply (rules intro: impI [THEN allI] mp) 

441 
done 

442 

443 
lemma conjunct1: "[ P & Q ] ==> P" 

444 
apply (unfold and_def) 

445 
apply (rules intro: impI dest: spec mp) 

446 
done 

447 

448 
lemma conjunct2: "[ P & Q ] ==> Q" 

449 
apply (unfold and_def) 

450 
apply (rules intro: impI dest: spec mp) 

451 
done 

452 

453 
lemma conjE: 

454 
assumes major: "P&Q" 

455 
and minor: "[ P; Q ] ==> R" 

456 
shows "R" 

457 
apply (rule minor) 

458 
apply (rule major [THEN conjunct1]) 

459 
apply (rule major [THEN conjunct2]) 

460 
done 

461 

462 
lemma context_conjI: 

463 
assumes prems: "P" "P ==> Q" shows "P & Q" 

464 
by (rules intro: conjI prems) 

465 

466 

467 
subsection {*Disjunction*} 

468 

469 
lemma disjI1: "P ==> PQ" 

470 
apply (unfold or_def) 

471 
apply (rules intro: allI impI mp) 

472 
done 

473 

474 
lemma disjI2: "Q ==> PQ" 

475 
apply (unfold or_def) 

476 
apply (rules intro: allI impI mp) 

477 
done 

478 

479 
lemma disjE: 

480 
assumes major: "PQ" 

481 
and minorP: "P ==> R" 

482 
and minorQ: "Q ==> R" 

483 
shows "R" 

484 
by (rules intro: minorP minorQ impI 

485 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 

486 

487 

488 
subsection {*Classical logic*} 

489 

490 

491 
lemma classical: 

492 
assumes prem: "~P ==> P" 

493 
shows "P" 

494 
apply (rule True_or_False [THEN disjE, THEN eqTrueE]) 

495 
apply assumption 

496 
apply (rule notI [THEN prem, THEN eqTrueI]) 

497 
apply (erule subst) 

498 
apply assumption 

499 
done 

500 

501 
lemmas ccontr = FalseE [THEN classical, standard] 

502 

503 
(*notE with premises exchanged; it discharges ~R so that it can be used to 

504 
make elimination rules*) 

505 
lemma rev_notE: 

506 
assumes premp: "P" 

507 
and premnot: "~R ==> ~P" 

508 
shows "R" 

509 
apply (rule ccontr) 

510 
apply (erule notE [OF premnot premp]) 

511 
done 

512 

513 
(*Double negation law*) 

514 
lemma notnotD: "~~P ==> P" 

515 
apply (rule classical) 

516 
apply (erule notE) 

517 
apply assumption 

518 
done 

519 

520 
lemma contrapos_pp: 

521 
assumes p1: "Q" 

522 
and p2: "~P ==> ~Q" 

523 
shows "P" 

524 
by (rules intro: classical p1 p2 notE) 

525 

526 

527 
subsection {*Unique existence*} 

528 

529 
lemma ex1I: 

530 
assumes prems: "P a" "!!x. P(x) ==> x=a" 

531 
shows "EX! x. P(x)" 

532 
by (unfold Ex1_def, rules intro: prems exI conjI allI impI) 

533 

534 
text{*Sometimes easier to use: the premises have no shared variables. Safe!*} 

535 
lemma ex_ex1I: 

536 
assumes ex_prem: "EX x. P(x)" 

537 
and eq: "!!x y. [ P(x); P(y) ] ==> x=y" 

538 
shows "EX! x. P(x)" 

539 
by (rules intro: ex_prem [THEN exE] ex1I eq) 

540 

541 
lemma ex1E: 

542 
assumes major: "EX! x. P(x)" 

543 
and minor: "!!x. [ P(x); ALL y. P(y) > y=x ] ==> R" 

544 
shows "R" 

545 
apply (rule major [unfolded Ex1_def, THEN exE]) 

546 
apply (erule conjE) 

547 
apply (rules intro: minor) 

548 
done 

549 

550 
lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x" 

551 
apply (erule ex1E) 

552 
apply (rule exI) 

553 
apply assumption 

554 
done 

555 

556 

557 
subsection {*THE: definite description operator*} 

558 

559 
lemma the_equality: 

560 
assumes prema: "P a" 

561 
and premx: "!!x. P x ==> x=a" 

562 
shows "(THE x. P x) = a" 

563 
apply (rule trans [OF _ the_eq_trivial]) 

564 
apply (rule_tac f = "The" in arg_cong) 

565 
apply (rule ext) 

566 
apply (rule iffI) 

567 
apply (erule premx) 

568 
apply (erule ssubst, rule prema) 

569 
done 

570 

571 
lemma theI: 

572 
assumes "P a" and "!!x. P x ==> x=a" 

573 
shows "P (THE x. P x)" 

574 
by (rules intro: prems the_equality [THEN ssubst]) 

575 

576 
lemma theI': "EX! x. P x ==> P (THE x. P x)" 

577 
apply (erule ex1E) 

578 
apply (erule theI) 

579 
apply (erule allE) 

580 
apply (erule mp) 

581 
apply assumption 

582 
done 

583 

584 
(*Easier to apply than theI: only one occurrence of P*) 

585 
lemma theI2: 

586 
assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" 

587 
shows "Q (THE x. P x)" 

588 
by (rules intro: prems theI) 

589 

590 
lemma the1_equality: "[ EX!x. P x; P a ] ==> (THE x. P x) = a" 

591 
apply (rule the_equality) 

592 
apply assumption 

593 
apply (erule ex1E) 

594 
apply (erule all_dupE) 

595 
apply (drule mp) 

596 
apply assumption 

597 
apply (erule ssubst) 

598 
apply (erule allE) 

599 
apply (erule mp) 

600 
apply assumption 

601 
done 

602 

603 
lemma the_sym_eq_trivial: "(THE y. x=y) = x" 

604 
apply (rule the_equality) 

605 
apply (rule refl) 

606 
apply (erule sym) 

607 
done 

608 

609 

610 
subsection {*Classical intro rules for disjunction and existential quantifiers*} 

611 

612 
lemma disjCI: 

613 
assumes "~Q ==> P" shows "PQ" 

614 
apply (rule classical) 

615 
apply (rules intro: prems disjI1 disjI2 notI elim: notE) 

616 
done 

617 

618 
lemma excluded_middle: "~P  P" 

619 
by (rules intro: disjCI) 

620 

621 
text{*case distinction as a natural deduction rule. Note that @{term "~P"} 

622 
is the second case, not the first.*} 

623 
lemma case_split_thm: 

624 
assumes prem1: "P ==> Q" 

625 
and prem2: "~P ==> Q" 

626 
shows "Q" 

627 
apply (rule excluded_middle [THEN disjE]) 

628 
apply (erule prem2) 

629 
apply (erule prem1) 

630 
done 

631 

632 
(*Classical implies (>) elimination. *) 

633 
lemma impCE: 

634 
assumes major: "P>Q" 

635 
and minor: "~P ==> R" "Q ==> R" 

636 
shows "R" 

637 
apply (rule excluded_middle [of P, THEN disjE]) 

638 
apply (rules intro: minor major [THEN mp])+ 

639 
done 

640 

641 
(*This version of > elimination works on Q before P. It works best for 

642 
those cases in which P holds "almost everywhere". Can't install as 

643 
default: would break old proofs.*) 

644 
lemma impCE': 

645 
assumes major: "P>Q" 

646 
and minor: "Q ==> R" "~P ==> R" 

647 
shows "R" 

648 
apply (rule excluded_middle [of P, THEN disjE]) 

649 
apply (rules intro: minor major [THEN mp])+ 

650 
done 

651 

652 
(*Classical <> elimination. *) 

653 
lemma iffCE: 

654 
assumes major: "P=Q" 

655 
and minor: "[ P; Q ] ==> R" "[ ~P; ~Q ] ==> R" 

656 
shows "R" 

657 
apply (rule major [THEN iffE]) 

658 
apply (rules intro: minor elim: impCE notE) 

659 
done 

660 

661 
lemma exCI: 

662 
assumes "ALL x. ~P(x) ==> P(a)" 

663 
shows "EX x. P(x)" 

664 
apply (rule ccontr) 

665 
apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"]) 

666 
done 

667 

668 

669 

11750  670 
subsection {* Theory and package setup *} 
671 

15411  672 
ML 
673 
{* 

674 
val plusI = thm "plusI" 

675 
val minusI = thm "minusI" 

676 
val timesI = thm "timesI" 

677 
val eq_reflection = thm "eq_reflection" 

678 
val refl = thm "refl" 

679 
val subst = thm "subst" 

680 
val ext = thm "ext" 

681 
val impI = thm "impI" 

682 
val mp = thm "mp" 

683 
val True_def = thm "True_def" 

684 
val All_def = thm "All_def" 

685 
val Ex_def = thm "Ex_def" 

686 
val False_def = thm "False_def" 

687 
val not_def = thm "not_def" 

688 
val and_def = thm "and_def" 

689 
val or_def = thm "or_def" 

690 
val Ex1_def = thm "Ex1_def" 

691 
val iff = thm "iff" 

692 
val True_or_False = thm "True_or_False" 

693 
val Let_def = thm "Let_def" 

694 
val if_def = thm "if_def" 

695 
val sym = thm "sym" 

696 
val ssubst = thm "ssubst" 

697 
val trans = thm "trans" 

698 
val def_imp_eq = thm "def_imp_eq" 

699 
val box_equals = thm "box_equals" 

700 
val fun_cong = thm "fun_cong" 

701 
val arg_cong = thm "arg_cong" 

702 
val cong = thm "cong" 

703 
val iffI = thm "iffI" 

704 
val iffD2 = thm "iffD2" 

705 
val rev_iffD2 = thm "rev_iffD2" 

706 
val iffD1 = thm "iffD1" 

707 
val rev_iffD1 = thm "rev_iffD1" 

708 
val iffE = thm "iffE" 

709 
val TrueI = thm "TrueI" 

710 
val eqTrueI = thm "eqTrueI" 

711 
val eqTrueE = thm "eqTrueE" 

712 
val allI = thm "allI" 

713 
val spec = thm "spec" 

714 
val allE = thm "allE" 

715 
val all_dupE = thm "all_dupE" 

716 
val FalseE = thm "FalseE" 

717 
val False_neq_True = thm "False_neq_True" 

718 
val notI = thm "notI" 

719 
val False_not_True = thm "False_not_True" 

720 
val True_not_False = thm "True_not_False" 

721 
val notE = thm "notE" 

722 
val notI2 = thm "notI2" 

723 
val impE = thm "impE" 

724 
val rev_mp = thm "rev_mp" 

725 
val contrapos_nn = thm "contrapos_nn" 

726 
val contrapos_pn = thm "contrapos_pn" 

727 
val not_sym = thm "not_sym" 

728 
val rev_contrapos = thm "rev_contrapos" 

729 
val exI = thm "exI" 

730 
val exE = thm "exE" 

731 
val conjI = thm "conjI" 

732 
val conjunct1 = thm "conjunct1" 

733 
val conjunct2 = thm "conjunct2" 

734 
val conjE = thm "conjE" 

735 
val context_conjI = thm "context_conjI" 

736 
val disjI1 = thm "disjI1" 

737 
val disjI2 = thm "disjI2" 

738 
val disjE = thm "disjE" 

739 
val classical = thm "classical" 

740 
val ccontr = thm "ccontr" 

741 
val rev_notE = thm "rev_notE" 

742 
val notnotD = thm "notnotD" 

743 
val contrapos_pp = thm "contrapos_pp" 

744 
val ex1I = thm "ex1I" 

745 
val ex_ex1I = thm "ex_ex1I" 

746 
val ex1E = thm "ex1E" 

747 
val ex1_implies_ex = thm "ex1_implies_ex" 

748 
val the_equality = thm "the_equality" 

749 
val theI = thm "theI" 

750 
val theI' = thm "theI'" 

751 
val theI2 = thm "theI2" 

752 
val the1_equality = thm "the1_equality" 

753 
val the_sym_eq_trivial = thm "the_sym_eq_trivial" 

754 
val disjCI = thm "disjCI" 

755 
val excluded_middle = thm "excluded_middle" 

756 
val case_split_thm = thm "case_split_thm" 

757 
val impCE = thm "impCE" 

758 
val impCE = thm "impCE" 

759 
val iffCE = thm "iffCE" 

760 
val exCI = thm "exCI" 

4868  761 

15411  762 
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) 
763 
local 

764 
fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t 

765 
 wrong_prem (Bound _) = true 

766 
 wrong_prem _ = false 

767 
val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t))))) 

768 
in 

769 
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]) 

770 
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac] 

771 
end 

772 

773 

774 
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i) 

775 

776 
(*Obsolete form of disjunctive case analysis*) 

777 
fun excluded_middle_tac sP = 

778 
res_inst_tac [("Q",sP)] (excluded_middle RS disjE) 

779 

780 
fun case_tac a = res_inst_tac [("P",a)] case_split_thm 

781 
*} 

782 

11687  783 
theorems case_split = case_split_thm [case_names True False] 
9869  784 

12386  785 

786 
subsubsection {* Intuitionistic Reasoning *} 

787 

788 
lemma impE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

789 
assumes 1: "P > Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

790 
and 2: "Q ==> R" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

791 
and 3: "P > Q ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

792 
shows R 
12386  793 
proof  
794 
from 3 and 1 have P . 

795 
with 1 have Q by (rule impE) 

796 
with 2 show R . 

797 
qed 

798 

799 
lemma allE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

800 
assumes 1: "ALL x. P x" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

801 
and 2: "P x ==> ALL x. P x ==> Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

802 
shows Q 
12386  803 
proof  
804 
from 1 have "P x" by (rule spec) 

805 
from this and 1 show Q by (rule 2) 

806 
qed 

807 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

808 
lemma notE': 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

809 
assumes 1: "~ P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

810 
and 2: "~ P ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

811 
shows R 
12386  812 
proof  
813 
from 2 and 1 have P . 

814 
with 1 show R by (rule notE) 

815 
qed 

816 

817 
lemmas [CPure.elim!] = disjE iffE FalseE conjE exE 

818 
and [CPure.intro!] = iffI conjI impI TrueI notI allI refl 

819 
and [CPure.elim 2] = allE notE' impE' 

820 
and [CPure.intro] = exI disjI2 disjI1 

821 

822 
lemmas [trans] = trans 

823 
and [sym] = sym not_sym 

824 
and [CPure.elim?] = iffD1 iffD2 impE 

11750  825 

11438
3d9222b80989
declare trans [trans] (*overridden in theory Calculation*);
wenzelm
parents:
11432
diff
changeset

826 

11750  827 
subsubsection {* Atomizing metalevel connectives *} 
828 

829 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 

12003  830 
proof 
9488  831 
assume "!!x. P x" 
10383  832 
show "ALL x. P x" by (rule allI) 
9488  833 
next 
834 
assume "ALL x. P x" 

10383  835 
thus "!!x. P x" by (rule allE) 
9488  836 
qed 
837 

11750  838 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  839 
proof 
9488  840 
assume r: "A ==> B" 
10383  841 
show "A > B" by (rule impI) (rule r) 
9488  842 
next 
843 
assume "A > B" and A 

10383  844 
thus B by (rule mp) 
9488  845 
qed 
846 

14749  847 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
848 
proof 

849 
assume r: "A ==> False" 

850 
show "~A" by (rule notI) (rule r) 

851 
next 

852 
assume "~A" and A 

853 
thus False by (rule notE) 

854 
qed 

855 

11750  856 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
12003  857 
proof 
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

858 
assume "x == y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

859 
show "x = y" by (unfold prems) (rule refl) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

860 
next 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

861 
assume "x = y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

862 
thus "x == y" by (rule eq_reflection) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

863 
qed 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

864 

12023  865 
lemma atomize_conj [atomize]: 
866 
"(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 

12003  867 
proof 
11953  868 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
869 
show "A & B" by (rule conjI) 

870 
next 

871 
fix C 

872 
assume "A & B" 

873 
assume "A ==> B ==> PROP C" 

874 
thus "PROP C" 

875 
proof this 

876 
show A by (rule conjunct1) 

877 
show B by (rule conjunct2) 

878 
qed 

879 
qed 

880 

12386  881 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
882 

11750  883 

884 
subsubsection {* Classical Reasoner setup *} 

9529  885 

10383  886 
use "cladata.ML" 
887 
setup hypsubst_setup 

11977  888 

12386  889 
ML_setup {* 
890 
Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); 

891 
*} 

11977  892 

10383  893 
setup Classical.setup 
894 
setup clasetup 

895 

12386  896 
lemmas [intro?] = ext 
897 
and [elim?] = ex1_implies_ex 

11977  898 

9869  899 
use "blastdata.ML" 
900 
setup Blast.setup 

4868  901 

11750  902 

15481  903 
subsection {* Simplifier setup *} 
11750  904 

12281  905 
lemma meta_eq_to_obj_eq: "x == y ==> x = y" 
906 
proof  

907 
assume r: "x == y" 

908 
show "x = y" by (unfold r) (rule refl) 

909 
qed 

910 

911 
lemma eta_contract_eq: "(%s. f s) = f" .. 

912 

913 
lemma simp_thms: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

914 
shows not_not: "(~ ~ P) = P" 
15354  915 
and Not_eq_iff: "((~P) = (~Q)) = (P = Q)" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

916 
and 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

917 
"(P ~= Q) = (P = (~Q))" 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

918 
"(P  ~P) = True" "(~P  P) = True" 
12281  919 
"(x = x) = True" 
920 
"(~True) = False" "(~False) = True" 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

921 
"(~P) ~= P" "P ~= (~P)" 
12281  922 
"(True=P) = P" "(P=True) = P" "(False=P) = (~P)" "(P=False) = (~P)" 
923 
"(True > P) = P" "(False > P) = True" 

924 
"(P > True) = True" "(P > P) = True" 

925 
"(P > False) = (~P)" "(P > ~P) = (~P)" 

926 
"(P & True) = P" "(True & P) = P" 

927 
"(P & False) = False" "(False & P) = False" 

928 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

929 
"(P & ~P) = False" "(~P & P) = False" 

930 
"(P  True) = True" "(True  P) = True" 

931 
"(P  False) = P" "(False  P) = P" 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

932 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  933 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
934 
 {* needed for the onepointrule quantifier simplification procs *} 

935 
 {* essential for termination!! *} and 

936 
"!!P. (EX x. x=t & P(x)) = P(t)" 

937 
"!!P. (EX x. t=x & P(x)) = P(t)" 

938 
"!!P. (ALL x. x=t > P(x)) = P(t)" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

939 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

940 
by (blast, blast, blast, blast, blast, rules+) 
13421  941 

12281  942 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
12354  943 
by rules 
12281  944 

945 
lemma ex_simps: 

946 
"!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" 

947 
"!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" 

948 
"!!P Q. (EX x. P x  Q) = ((EX x. P x)  Q)" 

949 
"!!P Q. (EX x. P  Q x) = (P  (EX x. Q x))" 

950 
"!!P Q. (EX x. P x > Q) = ((ALL x. P x) > Q)" 

951 
"!!P Q. (EX x. P > Q x) = (P > (EX x. Q x))" 

952 
 {* Miniscoping: pushing in existential quantifiers. *} 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

953 
by (rules  blast)+ 
12281  954 

955 
lemma all_simps: 

956 
"!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)" 

957 
"!!P Q. (ALL x. P & Q x) = (P & (ALL x. Q x))" 

958 
"!!P Q. (ALL x. P x  Q) = ((ALL x. P x)  Q)" 

959 
"!!P Q. (ALL x. P  Q x) = (P  (ALL x. Q x))" 

960 
"!!P Q. (ALL x. P x > Q) = ((EX x. P x) > Q)" 

961 
"!!P Q. (ALL x. P > Q x) = (P > (ALL x. Q x))" 

962 
 {* Miniscoping: pushing in universal quantifiers. *} 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

963 
by (rules  blast)+ 
12281  964 

14201  965 
lemma disj_absorb: "(A  A) = A" 
966 
by blast 

967 

968 
lemma disj_left_absorb: "(A  (A  B)) = (A  B)" 

969 
by blast 

970 

971 
lemma conj_absorb: "(A & A) = A" 

972 
by blast 

973 

974 
lemma conj_left_absorb: "(A & (A & B)) = (A & B)" 

975 
by blast 

976 

12281  977 
lemma eq_ac: 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

978 
shows eq_commute: "(a=b) = (b=a)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

979 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

980 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+) 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

981 
lemma neq_commute: "(a~=b) = (b~=a)" by rules 
12281  982 

983 
lemma conj_comms: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

984 
shows conj_commute: "(P&Q) = (Q&P)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

985 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+ 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

986 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules 
12281  987 

988 
lemma disj_comms: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

989 
shows disj_commute: "(PQ) = (QP)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

990 
and disj_left_commute: "(P(QR)) = (Q(PR))" by rules+ 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

991 
lemma disj_assoc: "((PQ)R) = (P(QR))" by rules 
12281  992 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

993 
lemma conj_disj_distribL: "(P&(QR)) = (P&Q  P&R)" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

994 
lemma conj_disj_distribR: "((PQ)&R) = (P&R  Q&R)" by rules 
12281  995 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

996 
lemma disj_conj_distribL: "(P(Q&R)) = ((PQ) & (PR))" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

997 
lemma disj_conj_distribR: "((P&Q)R) = ((PR) & (QR))" by rules 
12281  998 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

999 
lemma imp_conjR: "(P > (Q&R)) = ((P>Q) & (P>R))" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1000 
lemma imp_conjL: "((P&Q) >R) = (P > (Q > R))" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1001 
lemma imp_disjL: "((PQ) > R) = ((P>R)&(Q>R))" by rules 
12281  1002 

1003 
text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *} 

1004 
lemma imp_disj_not1: "(P > Q  R) = (~Q > P > R)" by blast 

1005 
lemma imp_disj_not2: "(P > Q  R) = (~R > P > Q)" by blast 

1006 

1007 
lemma imp_disj1: "((P>Q)R) = (P> QR)" by blast 

1008 
lemma imp_disj2: "(Q(P>R)) = (P> QR)" by blast 

1009 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1010 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by rules 
12281  1011 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1012 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

1013 
lemma not_iff: "(P~=Q) = (P = (~Q))" by blast 

1014 
lemma disj_not1: "(~P  Q) = (P > Q)" by blast 

1015 
lemma disj_not2: "(P  ~Q) = (Q > P)"  {* changes orientation :( *} 

1016 
by blast 

1017 
lemma imp_conv_disj: "(P > Q) = ((~P)  Q)" by blast 

1018 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1019 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by rules 
12281  1020 

1021 

1022 
lemma cases_simp: "((P > Q) & (~P > Q)) = Q" 

1023 
 {* Avoids duplication of subgoals after @{text split_if}, when the true and false *} 

1024 
 {* cases boil down to the same thing. *} 

1025 
by blast 

1026 

1027 
lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast 

1028 
lemma imp_all: "((! x. P x) > Q) = (? x. P x > Q)" by blast 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1029 
lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1030 
lemma imp_ex: "((? x. P x) > Q) = (! x. P x > Q)" by rules 
12281  1031 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1032 
lemma ex_disj_distrib: "(? x. P(x)  Q(x)) = ((? x. P(x))  (? x. Q(x)))" by rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1033 
lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by rules 
12281  1034 

1035 
text {* 

1036 
\medskip The @{text "&"} congruence rule: not included by default! 

1037 
May slow rewrite proofs down by as much as 50\% *} 

1038 

1039 
lemma conj_cong: 

1040 
"(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))" 

12354  1041 
by rules 
12281  1042 

1043 
lemma rev_conj_cong: 

1044 
"(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))" 

12354  1045 
by rules 
12281  1046 

1047 
text {* The @{text ""} congruence rule: not included by default! *} 

1048 

1049 
lemma disj_cong: 

1050 
"(P = P') ==> (~P' ==> (Q = Q')) ==> ((P  Q) = (P'  Q'))" 

1051 
by blast 

1052 

1053 
lemma eq_sym_conv: "(x = y) = (y = x)" 

12354  1054 
by rules 
12281  1055 

1056 

1057 
text {* \medskip ifthenelse rules *} 

1058 

1059 
lemma if_True: "(if True then x else y) = x" 

1060 
by (unfold if_def) blast 

1061 

1062 
lemma if_False: "(if False then x else y) = y" 

1063 
by (unfold if_def) blast 

1064 

1065 
lemma if_P: "P ==> (if P then x else y) = x" 

1066 
by (unfold if_def) blast 

1067 

1068 
lemma if_not_P: "~P ==> (if P then x else y) = y" 

1069 
by (unfold if_def) blast 

1070 

1071 
lemma split_if: "P (if Q then x else y) = ((Q > P(x)) & (~Q > P(y)))" 

1072 
apply (rule case_split [of Q]) 

15481  1073 
apply (simplesubst if_P) 
1074 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1075 
done 
1076 

1077 
lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x)  (~Q & ~P y)))" 

15481  1078 
by (simplesubst split_if, blast) 
12281  1079 

1080 
lemmas if_splits = split_if split_if_asm 

1081 

1082 
lemma if_def2: "(if Q then x else y) = ((Q > x) & (~ Q > y))" 

1083 
by (rule split_if) 

1084 

1085 
lemma if_cancel: "(if c then x else x) = x" 

15481  1086 
by (simplesubst split_if, blast) 
12281  1087 

1088 
lemma if_eq_cancel: "(if x = y then y else x) = x" 

15481  1089 
by (simplesubst split_if, blast) 
12281  1090 

1091 
lemma if_bool_eq_conj: "(if P then Q else R) = ((P>Q) & (~P>R))" 

1092 
 {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *} 

1093 
by (rule split_if) 

1094 

1095 
lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q)  (~P&R))" 

1096 
 {* And this form is useful for expanding @{text if}s on the LEFT. *} 

15481  1097 
apply (simplesubst split_if, blast) 
12281  1098 
done 
1099 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1100 
lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1101 
lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules 
12281  1102 

15423  1103 
text {* \medskip let rules for simproc *} 
1104 

1105 
lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g" 

1106 
by (unfold Let_def) 

1107 

1108 
lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g" 

1109 
by (unfold Let_def) 

1110 

14201  1111 
subsubsection {* Actual Installation of the Simplifier *} 
1112 

9869  1113 
use "simpdata.ML" 
1114 
setup Simplifier.setup 

1115 
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup 

1116 
setup Splitter.setup setup Clasimp.setup 

1117 

15481  1118 

1119 
subsubsection {* Lucas Dixon's eqstep tactic *} 

1120 

1121 
use "~~/src/Provers/eqsubst.ML"; 

1122 
use "eqrule_HOL_data.ML"; 

1123 

1124 
setup EQSubstTac.setup 

1125 

1126 

1127 
subsection {* Other simple lemmas *} 

1128 

15411  1129 
declare disj_absorb [simp] conj_absorb [simp] 
14201  1130 

13723  1131 
lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x" 
1132 
by blast+ 

1133 

15481  1134 

13638  1135 
theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))" 
1136 
apply (rule iffI) 

1137 
apply (rule_tac a = "%x. THE y. P x y" in ex1I) 

1138 
apply (fast dest!: theI') 

1139 
apply (fast intro: ext the1_equality [symmetric]) 

1140 
apply (erule ex1E) 

1141 
apply (rule allI) 

1142 
apply (rule ex1I) 

1143 
apply (erule spec) 

1144 
apply (erule_tac x = "%z. if z = x then y else f z" in allE) 

1145 
apply (erule impE) 

1146 
apply (rule allI) 

1147 
apply (rule_tac P = "xa = x" in case_split_thm) 

14208  1148 
apply (drule_tac [3] x = x in fun_cong, simp_all) 
13638  1149 
done 
1150 

13438
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1151 
text{*Needs only HOLlemmas:*} 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1152 
lemma mk_left_commute: 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1153 
assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1154 
c: "\<And>x y. f x y = f y x" 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1155 
shows "f x (f y z) = f y (f x z)" 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1156 
by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]]) 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1157 

11750  1158 

15481  1159 
subsection {* Generic cases and induction *} 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1160 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1161 
constdefs 
11989  1162 
induct_forall :: "('a => bool) => bool" 
1163 
"induct_forall P == \<forall>x. P x" 

1164 
induct_implies :: "bool => bool => bool" 

1165 
"induct_implies A B == A > B" 

1166 
induct_equal :: "'a => 'a => bool" 

1167 
"induct_equal x y == x = y" 

1168 
induct_conj :: "bool => bool => bool" 

1169 
"induct_conj A B == A & B" 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1170 

11989  1171 
lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" 
1172 
by (simp only: atomize_all induct_forall_def) 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1173 

11989  1174 
lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" 
1175 
by (simp only: atomize_imp induct_implies_def) 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1176 

11989  1177 
lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" 
1178 
by (simp only: atomize_eq induct_equal_def) 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1179 

11989  1180 
lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = 
1181 
induct_conj (induct_forall A) (induct_forall B)" 

12354  1182 
by (unfold induct_forall_def induct_conj_def) rules 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1183 

11989  1184 
lemma induct_implies_conj: "induct_implies C (induct_conj A B) = 
1185 
induct_conj (induct_implies C A) (induct_implies C B)" 

12354  1186 
by (unfold induct_implies_def induct_conj_def) rules 
11989  1187 

13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1188 
lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1189 
proof 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1190 
assume r: "induct_conj A B ==> PROP C" and A B 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1191 
show "PROP C" by (rule r) (simp! add: induct_conj_def) 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1192 
next 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1193 
assume r: "A ==> B ==> PROP C" and "induct_conj A B" 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1194 
show "PROP C" by (rule r) (simp! add: induct_conj_def)+ 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1195 
qed 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1196 

11989  1197 
lemma induct_impliesI: "(A ==> B) ==> induct_implies A B" 
1198 
by (simp add: induct_implies_def) 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1199 

12161  1200 
lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq 
1201 
lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq 

1202 
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11989  1203 
lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1204 

11989  1205 
hide const induct_forall induct_implies induct_equal induct_conj 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1206 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1207 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1208 
text {* Method setup. *} 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1209 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1210 
ML {* 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1211 
structure InductMethod = InductMethodFun 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1212 
(struct 
15411  1213 
val dest_concls = HOLogic.dest_concls 
1214 
val cases_default = thm "case_split" 

1215 
val local_impI = thm "induct_impliesI" 

1216 
val conjI = thm "conjI" 

1217 
val atomize = thms "induct_atomize" 

1218 
val rulify1 = thms "induct_rulify1" 

1219 
val rulify2 = thms "induct_rulify2" 

1220 
val localize = [Thm.symmetric (thm "induct_implies_def")] 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1221 
end); 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1222 
*} 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1223 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1224 
setup InductMethod.setup 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1225 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1226 

11750  1227 
subsection {* Order signatures and orders *} 
1228 

1229 
axclass 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

1230 
ord < type 
11750  1231 

1232 
syntax 

1233 
"op <" :: "['a::ord, 'a] => bool" ("op <") 

1234 
"op <=" :: "['a::ord, 'a] => bool" ("op <=") 

1235 

1236 
global 

1237 

1238 
consts 

1239 
"op <" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50) 

1240 
"op <=" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50) 

1241 

1242 
local 

1243 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

1244 
syntax (xsymbols) 
11750  1245 
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>") 
1246 
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) 

1247 

14565  1248 
syntax (HTML output) 
1249 
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>") 

1250 
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) 

1251 

15354  1252 
text{* Syntactic sugar: *} 
11750  1253 

15354  1254 
consts 
1255 
"_gt" :: "'a::ord => 'a => bool" (infixl ">" 50) 

1256 
"_ge" :: "'a::ord => 'a => bool" (infixl ">=" 50) 

1257 
translations 

1258 
"x > y" => "y < x" 

1259 
"x >= y" => "y <= x" 

1260 

1261 
syntax (xsymbols) 

1262 
"_ge" :: "'a::ord => 'a => bool" (infixl "\<ge>" 50) 

1263 

1264 
syntax (HTML output) 

1265 
"_ge" :: "['a::ord, 'a] => bool" (infixl "\<ge>" 50) 

1266 

14295  1267 

11750  1268 
subsubsection {* Monotonicity *} 
1269 

13412  1270 
locale mono = 
1271 
fixes f 

1272 
assumes mono: "A <= B ==> f A <= f B" 

11750  1273 

13421  1274 
lemmas monoI [intro?] = mono.intro 
13412  1275 
and monoD [dest?] = mono.mono 
11750  1276 

1277 
constdefs 

1278 
min :: "['a::ord, 'a] => 'a" 

1279 
"min a b == (if a <= b then a else b)" 

1280 
max :: "['a::ord, 'a] => 'a" 

1281 
"max a b == (if a <= b then b else a)" 

1282 

1283 
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" 

1284 
by (simp add: min_def) 

1285 

1286 
lemma min_of_mono: 

1287 
"ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)" 

1288 
by (simp add: min_def) 

1289 

1290 
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" 

1291 
by (simp add: max_def) 

1292 

1293 
lemma max_of_mono: 

1294 
"ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)" 

1295 
by (simp add: max_def) 

1296 

1297 

1298 
subsubsection "Orders" 

1299 

1300 
axclass order < ord 

1301 
order_refl [iff]: "x <= x" 

1302 
order_trans: "x <= y ==> y <= z ==> x <= z" 

1303 
order_antisym: "x <= y ==> y <= x ==> x = y" 

1304 
order_less_le: "(x < y) = (x <= y & x ~= y)" 

1305 

1306 

1307 
text {* Reflexivity. *} 

1308 

1309 
lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" 

1310 
 {* This form is useful with the classical reasoner. *} 

1311 
apply (erule ssubst) 

1312 
apply (rule order_refl) 

1313 
done 

1314 

13553  1315 
lemma order_less_irrefl [iff]: "~ x < (x::'a::order)" 
11750  1316 
by (simp add: order_less_le) 
1317 

1318 
lemma order_le_less: "((x::'a::order) <= y) = (x < y  x = y)" 

1319 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 

14208  1320 
apply (simp add: order_less_le, blast) 
11750  1321 
done 
1322 

1323 
lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] 

1324 

1325 
lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" 

1326 
by (simp add: order_less_le) 

1327 

1328 

1329 
text {* Asymmetry. *} 

1330 

1331 
lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)" 

1332 
by (simp add: order_less_le order_antisym) 

1333 

1334 
lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" 

1335 
apply (drule order_less_not_sym) 

14208  1336 
apply (erule contrapos_np, simp) 
11750  1337 
done 
1338 

15411  1339 
lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)" 
14295  1340 
by (blast intro: order_antisym) 
1341 

15197  1342 
lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)" 
1343 
by(blast intro:order_antisym) 

11750  1344 

1345 
text {* Transitivity. *} 

1346 

1347 
lemma order_less_trans: "!!x::'a::order. [ x < y; y < z ] ==> x < z" 

1348 
apply (simp add: order_less_le) 

1349 
apply (blast intro: order_trans order_antisym) 

1350 
done 

1351 

1352 
lemma order_le_less_trans: "!!x::'a::order. [ x <= y; y < z ] ==> x < z" 

1353 
apply (simp add: order_less_le) 

1354 
apply (blast intro: order_trans order_antisym) 

1355 
done 

1356 

1357 
lemma order_less_le_trans: "!!x::'a::order. [ x < y; y <= z ] ==> x < z" 

1358 
apply (simp add: order_less_le) 

1359 
apply (blast intro: order_trans order_antisym) 

1360 
done 

1361 

1362 

1363 
text {* Useful for simplification, but too risky to include by default. *} 

1364 

1365 
lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" 

1366 
by (blast elim: order_less_asym) 

1367 

1368 
lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x > P) = True" 

1369 
by (blast elim: order_less_asym) 

1370 

1371 
lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" 

1372 
by auto 

1373 

1374 
lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" 

1375 
by auto 

1376 

1377 

1378 
text {* Other operators. *} 

1379 

1380 
lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least" 

1381 
apply (simp add: min_def) 

1382 
apply (blast intro: order_antisym) 

1383 
done 

1384 

1385 
lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x" 

1386 
apply (simp add: max_def) 

1387 
apply (blast intro: order_antisym) 

1388 
done 

1389 

1390 

1391 
subsubsection {* Least value operator *} 

1392 

1393 
constdefs 

1394 
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) 

1395 
"Least P == THE x. P x & (ALL y. P y > x <= y)" 
