author  ballarin 
Tue, 02 Aug 2005 16:50:55 +0200  
changeset 16999  307b2ec590ff 
parent 16775  c1b87ef4a1c3 
child 17197  917c6e7ca28d 
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 
16417  10 
uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML") 
15481  11 
("~~/src/Provers/eqsubst.ML") 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16633
diff
changeset

12 

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 

3947  37 
arbitrary :: 'a 
923  38 

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

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

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

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

923  44 

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

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

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

923  49 

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

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

51 

16587  52 
consts 
53 
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) 

2260  54 

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

4868  57 
nonterminals 
923  58 
letbinds letbind 
59 
case_syn cases_syn 

60 

61 
syntax 

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

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

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

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

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

923  69 

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

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

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

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

75 
translations 

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

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

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

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

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

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

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

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

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

87 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

6340  116 

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

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

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

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

121 

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

122 

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

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

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

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

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

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

6289  134 

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

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

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

139 

140 

141 
text{*Thanks to Stephan Merz*} 

142 
theorem subst: 

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

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

145 
proof  

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

147 
by (rule eq_reflection) 

148 
from p show ?thesis 

149 
by (unfold meta) 

150 
qed 

923  151 

152 
defs 

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

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

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

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

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

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

923  161 

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

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

923  165 

166 
defs 

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

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

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

170 
finalconsts 
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 
"op >" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

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

174 
arbitrary 
3320  175 

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

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

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

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

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

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

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

183 
axclass inverse < type 
11750  184 

185 
global 

186 

187 
consts 

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

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

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

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

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

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

194 

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

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

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

197 
translations 
14690  198 
(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

199 

11750  200 
local 
201 

202 
typed_print_translation {* 

203 
let 

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

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

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

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

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

209 

210 

211 
consts 

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

213 
inverse :: "'a::inverse => 'a" 

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

215 

216 
syntax (xsymbols) 

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

218 
syntax (HTML output) 

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

220 

221 

15411  222 
subsection {*Equality*} 
223 

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

225 
apply (erule subst) 

226 
apply (rule refl) 

227 
done 

228 

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

230 
lemmas ssubst = sym [THEN subst, standard] 

231 

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

233 
apply (erule subst , assumption) 

234 
done 

235 

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

237 
apply (unfold meq) 

238 
apply (rule refl) 

239 
done 

240 

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

242 
a = b 

243 
  

244 
c = d *) 

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

246 
apply (rule trans) 

247 
apply (rule trans) 

248 
apply (rule sym) 

249 
apply assumption+ 

250 
done 

251 

15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

252 
text {* For calculational reasoning: *} 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

253 

2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

254 
lemma forw_subst: "a = b ==> P b ==> P a" 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

255 
by (rule ssubst) 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

256 

2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

257 
lemma back_subst: "P a ==> a = b ==> P b" 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

258 
by (rule subst) 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

259 

15411  260 

261 
subsection {*Congruence rules for application*} 

262 

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

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

265 
apply (erule subst) 

266 
apply (rule refl) 

267 
done 

268 

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

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

271 
apply (erule subst) 

272 
apply (rule refl) 

273 
done 

274 

15655  275 
lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d" 
276 
apply (erule ssubst)+ 

277 
apply (rule refl) 

278 
done 

279 

280 

15411  281 
lemma cong: "[ f = g; (x::'a) = y ] ==> f(x) = g(y)" 
282 
apply (erule subst)+ 

283 
apply (rule refl) 

284 
done 

285 

286 

287 
subsection {*Equality of booleans  iff*} 

288 

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

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

291 
done 

292 

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

294 
apply (erule ssubst) 

295 
apply assumption 

296 
done 

297 

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

299 
apply (erule iffD2) 

300 
apply assumption 

301 
done 

302 

303 
lemmas iffD1 = sym [THEN iffD2, standard] 

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

305 

306 
lemma iffE: 

307 
assumes major: "P=Q" 

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

309 
shows "R" 

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

311 

312 

313 
subsection {*True*} 

314 

315 
lemma TrueI: "True" 

316 
apply (unfold True_def) 

317 
apply (rule refl) 

318 
done 

319 

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

321 
by (rules intro: iffI TrueI) 

322 

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

324 
apply (erule iffD2) 

325 
apply (rule TrueI) 

326 
done 

327 

328 

329 
subsection {*Universal quantifier*} 

330 

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

332 
apply (unfold All_def) 

333 
apply (rules intro: ext eqTrueI p) 

334 
done 

335 

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

337 
apply (unfold All_def) 

338 
apply (rule eqTrueE) 

339 
apply (erule fun_cong) 

340 
done 

341 

342 
lemma allE: 

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

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

345 
shows "R" 

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

347 

348 
lemma all_dupE: 

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

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

351 
shows "R" 

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

353 

354 

355 
subsection {*False*} 

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

357 

358 
lemma FalseE: "False ==> P" 

359 
apply (unfold False_def) 

360 
apply (erule spec) 

361 
done 

362 

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

364 
by (erule eqTrueE [THEN FalseE]) 

365 

366 

367 
subsection {*Negation*} 

368 

369 
lemma notI: 

370 
assumes p: "P ==> False" 

371 
shows "~P" 

372 
apply (unfold not_def) 

373 
apply (rules intro: impI p) 

374 
done 

375 

376 
lemma False_not_True: "False ~= True" 

377 
apply (rule notI) 

378 
apply (erule False_neq_True) 

379 
done 

380 

381 
lemma True_not_False: "True ~= False" 

382 
apply (rule notI) 

383 
apply (drule sym) 

384 
apply (erule False_neq_True) 

385 
done 

386 

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

388 
apply (unfold not_def) 

389 
apply (erule mp [THEN FalseE]) 

390 
apply assumption 

391 
done 

392 

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

394 
lemmas notI2 = notE [THEN notI, standard] 

395 

396 

397 
subsection {*Implication*} 

398 

399 
lemma impE: 

400 
assumes "P>Q" "P" "Q ==> R" 

401 
shows "R" 

402 
by (rules intro: prems mp) 

403 

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

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

406 
by (rules intro: mp) 

407 

408 
lemma contrapos_nn: 

409 
assumes major: "~Q" 

410 
and minor: "P==>Q" 

411 
shows "~P" 

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

413 

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

415 
lemma contrapos_pn: 

416 
assumes major: "Q" 

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

418 
shows "~P" 

419 
by (rules intro: notI minor major notE) 

420 

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

422 
apply (erule contrapos_nn) 

423 
apply (erule sym) 

424 
done 

425 

426 
(*still used in HOLCF*) 

427 
lemma rev_contrapos: 

428 
assumes pq: "P ==> Q" 

429 
and nq: "~Q" 

430 
shows "~P" 

431 
apply (rule nq [THEN contrapos_nn]) 

432 
apply (erule pq) 

433 
done 

434 

435 
subsection {*Existential quantifier*} 

436 

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

438 
apply (unfold Ex_def) 

439 
apply (rules intro: allI allE impI mp) 

440 
done 

441 

442 
lemma exE: 

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

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

445 
shows "Q" 

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

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

448 
done 

449 

450 

451 
subsection {*Conjunction*} 

452 

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

454 
apply (unfold and_def) 

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

456 
done 

457 

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

459 
apply (unfold and_def) 

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

461 
done 

462 

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

464 
apply (unfold and_def) 

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

466 
done 

467 

468 
lemma conjE: 

469 
assumes major: "P&Q" 

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

471 
shows "R" 

472 
apply (rule minor) 

473 
apply (rule major [THEN conjunct1]) 

474 
apply (rule major [THEN conjunct2]) 

475 
done 

476 

477 
lemma context_conjI: 

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

479 
by (rules intro: conjI prems) 

480 

481 

482 
subsection {*Disjunction*} 

483 

484 
lemma disjI1: "P ==> PQ" 

485 
apply (unfold or_def) 

486 
apply (rules intro: allI impI mp) 

487 
done 

488 

489 
lemma disjI2: "Q ==> PQ" 

490 
apply (unfold or_def) 

491 
apply (rules intro: allI impI mp) 

492 
done 

493 

494 
lemma disjE: 

495 
assumes major: "PQ" 

496 
and minorP: "P ==> R" 

497 
and minorQ: "Q ==> R" 

498 
shows "R" 

499 
by (rules intro: minorP minorQ impI 

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

501 

502 

503 
subsection {*Classical logic*} 

504 

505 

506 
lemma classical: 

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

508 
shows "P" 

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

510 
apply assumption 

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

512 
apply (erule subst) 

513 
apply assumption 

514 
done 

515 

516 
lemmas ccontr = FalseE [THEN classical, standard] 

517 

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

519 
make elimination rules*) 

520 
lemma rev_notE: 

521 
assumes premp: "P" 

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

523 
shows "R" 

524 
apply (rule ccontr) 

525 
apply (erule notE [OF premnot premp]) 

526 
done 

527 

528 
(*Double negation law*) 

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

530 
apply (rule classical) 

531 
apply (erule notE) 

532 
apply assumption 

533 
done 

534 

535 
lemma contrapos_pp: 

536 
assumes p1: "Q" 

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

538 
shows "P" 

539 
by (rules intro: classical p1 p2 notE) 

540 

541 

542 
subsection {*Unique existence*} 

543 

544 
lemma ex1I: 

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

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

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

548 

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

550 
lemma ex_ex1I: 

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

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

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

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

555 

556 
lemma ex1E: 

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

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

559 
shows "R" 

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

561 
apply (erule conjE) 

562 
apply (rules intro: minor) 

563 
done 

564 

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

566 
apply (erule ex1E) 

567 
apply (rule exI) 

568 
apply assumption 

569 
done 

570 

571 

572 
subsection {*THE: definite description operator*} 

573 

574 
lemma the_equality: 

575 
assumes prema: "P a" 

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

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

578 
apply (rule trans [OF _ the_eq_trivial]) 

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

580 
apply (rule ext) 

581 
apply (rule iffI) 

582 
apply (erule premx) 

583 
apply (erule ssubst, rule prema) 

584 
done 

585 

586 
lemma theI: 

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

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

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

590 

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

592 
apply (erule ex1E) 

593 
apply (erule theI) 

594 
apply (erule allE) 

595 
apply (erule mp) 

596 
apply assumption 

597 
done 

598 

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

600 
lemma theI2: 

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

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

603 
by (rules intro: prems theI) 

604 

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

606 
apply (rule the_equality) 

607 
apply assumption 

608 
apply (erule ex1E) 

609 
apply (erule all_dupE) 

610 
apply (drule mp) 

611 
apply assumption 

612 
apply (erule ssubst) 

613 
apply (erule allE) 

614 
apply (erule mp) 

615 
apply assumption 

616 
done 

617 

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

619 
apply (rule the_equality) 

620 
apply (rule refl) 

621 
apply (erule sym) 

622 
done 

623 

624 

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

626 

627 
lemma disjCI: 

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

629 
apply (rule classical) 

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

631 
done 

632 

633 
lemma excluded_middle: "~P  P" 

634 
by (rules intro: disjCI) 

635 

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

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

638 
lemma case_split_thm: 

639 
assumes prem1: "P ==> Q" 

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

641 
shows "Q" 

642 
apply (rule excluded_middle [THEN disjE]) 

643 
apply (erule prem2) 

644 
apply (erule prem1) 

645 
done 

646 

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

648 
lemma impCE: 

649 
assumes major: "P>Q" 

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

651 
shows "R" 

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

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

654 
done 

655 

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

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

658 
default: would break old proofs.*) 

659 
lemma impCE': 

660 
assumes major: "P>Q" 

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

662 
shows "R" 

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

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

665 
done 

666 

667 
(*Classical <> elimination. *) 

668 
lemma iffCE: 

669 
assumes major: "P=Q" 

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

671 
shows "R" 

672 
apply (rule major [THEN iffE]) 

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

674 
done 

675 

676 
lemma exCI: 

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

678 
shows "EX x. P(x)" 

679 
apply (rule ccontr) 

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

681 
done 

682 

683 

684 

11750  685 
subsection {* Theory and package setup *} 
686 

15411  687 
ML 
688 
{* 

689 
val plusI = thm "plusI" 

690 
val minusI = thm "minusI" 

691 
val timesI = thm "timesI" 

692 
val eq_reflection = thm "eq_reflection" 

693 
val refl = thm "refl" 

694 
val subst = thm "subst" 

695 
val ext = thm "ext" 

696 
val impI = thm "impI" 

697 
val mp = thm "mp" 

698 
val True_def = thm "True_def" 

699 
val All_def = thm "All_def" 

700 
val Ex_def = thm "Ex_def" 

701 
val False_def = thm "False_def" 

702 
val not_def = thm "not_def" 

703 
val and_def = thm "and_def" 

704 
val or_def = thm "or_def" 

705 
val Ex1_def = thm "Ex1_def" 

706 
val iff = thm "iff" 

707 
val True_or_False = thm "True_or_False" 

708 
val Let_def = thm "Let_def" 

709 
val if_def = thm "if_def" 

710 
val sym = thm "sym" 

711 
val ssubst = thm "ssubst" 

712 
val trans = thm "trans" 

713 
val def_imp_eq = thm "def_imp_eq" 

714 
val box_equals = thm "box_equals" 

715 
val fun_cong = thm "fun_cong" 

716 
val arg_cong = thm "arg_cong" 

717 
val cong = thm "cong" 

718 
val iffI = thm "iffI" 

719 
val iffD2 = thm "iffD2" 

720 
val rev_iffD2 = thm "rev_iffD2" 

721 
val iffD1 = thm "iffD1" 

722 
val rev_iffD1 = thm "rev_iffD1" 

723 
val iffE = thm "iffE" 

724 
val TrueI = thm "TrueI" 

725 
val eqTrueI = thm "eqTrueI" 

726 
val eqTrueE = thm "eqTrueE" 

727 
val allI = thm "allI" 

728 
val spec = thm "spec" 

729 
val allE = thm "allE" 

730 
val all_dupE = thm "all_dupE" 

731 
val FalseE = thm "FalseE" 

732 
val False_neq_True = thm "False_neq_True" 

733 
val notI = thm "notI" 

734 
val False_not_True = thm "False_not_True" 

735 
val True_not_False = thm "True_not_False" 

736 
val notE = thm "notE" 

737 
val notI2 = thm "notI2" 

738 
val impE = thm "impE" 

739 
val rev_mp = thm "rev_mp" 

740 
val contrapos_nn = thm "contrapos_nn" 

741 
val contrapos_pn = thm "contrapos_pn" 

742 
val not_sym = thm "not_sym" 

743 
val rev_contrapos = thm "rev_contrapos" 

744 
val exI = thm "exI" 

745 
val exE = thm "exE" 

746 
val conjI = thm "conjI" 

747 
val conjunct1 = thm "conjunct1" 

748 
val conjunct2 = thm "conjunct2" 

749 
val conjE = thm "conjE" 

750 
val context_conjI = thm "context_conjI" 

751 
val disjI1 = thm "disjI1" 

752 
val disjI2 = thm "disjI2" 

753 
val disjE = thm "disjE" 

754 
val classical = thm "classical" 

755 
val ccontr = thm "ccontr" 

756 
val rev_notE = thm "rev_notE" 

757 
val notnotD = thm "notnotD" 

758 
val contrapos_pp = thm "contrapos_pp" 

759 
val ex1I = thm "ex1I" 

760 
val ex_ex1I = thm "ex_ex1I" 

761 
val ex1E = thm "ex1E" 

762 
val ex1_implies_ex = thm "ex1_implies_ex" 

763 
val the_equality = thm "the_equality" 

764 
val theI = thm "theI" 

765 
val theI' = thm "theI'" 

766 
val theI2 = thm "theI2" 

767 
val the1_equality = thm "the1_equality" 

768 
val the_sym_eq_trivial = thm "the_sym_eq_trivial" 

769 
val disjCI = thm "disjCI" 

770 
val excluded_middle = thm "excluded_middle" 

771 
val case_split_thm = thm "case_split_thm" 

772 
val impCE = thm "impCE" 

773 
val impCE = thm "impCE" 

774 
val iffCE = thm "iffCE" 

775 
val exCI = thm "exCI" 

4868  776 

15411  777 
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) 
778 
local 

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

780 
 wrong_prem (Bound _) = true 

781 
 wrong_prem _ = false 

15570  782 
val filter_right = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t))))) 
15411  783 
in 
784 
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]) 

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

786 
end 

787 

788 

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

790 

791 
(*Obsolete form of disjunctive case analysis*) 

792 
fun excluded_middle_tac sP = 

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

794 

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

796 
*} 

797 

11687  798 
theorems case_split = case_split_thm [case_names True False] 
9869  799 

12386  800 

801 
subsubsection {* Intuitionistic Reasoning *} 

802 

803 
lemma impE': 

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

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

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

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

807 
shows R 
12386  808 
proof  
809 
from 3 and 1 have P . 

810 
with 1 have Q by (rule impE) 

811 
with 2 show R . 

812 
qed 

813 

814 
lemma allE': 

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

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

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

817 
shows Q 
12386  818 
proof  
819 
from 1 have "P x" by (rule spec) 

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

821 
qed 

822 

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

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

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

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

826 
shows R 
12386  827 
proof  
828 
from 2 and 1 have P . 

829 
with 1 show R by (rule notE) 

830 
qed 

831 

15801  832 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 
833 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

834 
and [Pure.elim 2] = allE notE' impE' 

835 
and [Pure.intro] = exI disjI2 disjI1 

12386  836 

837 
lemmas [trans] = trans 

838 
and [sym] = sym not_sym 

15801  839 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  840 

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

841 

11750  842 
subsubsection {* Atomizing metalevel connectives *} 
843 

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

12003  845 
proof 
9488  846 
assume "!!x. P x" 
10383  847 
show "ALL x. P x" by (rule allI) 
9488  848 
next 
849 
assume "ALL x. P x" 

10383  850 
thus "!!x. P x" by (rule allE) 
9488  851 
qed 
852 

11750  853 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  854 
proof 
9488  855 
assume r: "A ==> B" 
10383  856 
show "A > B" by (rule impI) (rule r) 
9488  857 
next 
858 
assume "A > B" and A 

10383  859 
thus B by (rule mp) 
9488  860 
qed 
861 

14749  862 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
863 
proof 

864 
assume r: "A ==> False" 

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

866 
next 

867 
assume "~A" and A 

868 
thus False by (rule notE) 

869 
qed 

870 

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

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

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

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

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

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

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

879 

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

12003  882 
proof 
11953  883 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
884 
show "A & B" by (rule conjI) 

885 
next 

886 
fix C 

887 
assume "A & B" 

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

889 
thus "PROP C" 

890 
proof this 

891 
show A by (rule conjunct1) 

892 
show B by (rule conjunct2) 

893 
qed 

894 
qed 

895 

12386  896 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
897 

11750  898 

899 
subsubsection {* Classical Reasoner setup *} 

9529  900 

10383  901 
use "cladata.ML" 
902 
setup hypsubst_setup 

11977  903 

16121  904 
setup {* 
905 
[ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)] 

12386  906 
*} 
11977  907 

10383  908 
setup Classical.setup 
909 
setup clasetup 

910 

12386  911 
lemmas [intro?] = ext 
912 
and [elim?] = ex1_implies_ex 

11977  913 

9869  914 
use "blastdata.ML" 
915 
setup Blast.setup 

4868  916 

11750  917 

15481  918 
subsection {* Simplifier setup *} 
11750  919 

12281  920 
lemma meta_eq_to_obj_eq: "x == y ==> x = y" 
921 
proof  

922 
assume r: "x == y" 

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

924 
qed 

925 

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

927 

928 
lemma simp_thms: 

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

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

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

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

933 
"(P  ~P) = True" "(~P  P) = True" 
12281  934 
"(x = x) = True" 
935 
"(~True) = False" "(~False) = True" 

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

936 
"(~P) ~= P" "P ~= (~P)" 
12281  937 
"(True=P) = P" "(P=True) = P" "(False=P) = (~P)" "(P=False) = (~P)" 
938 
"(True > P) = P" "(False > P) = True" 

939 
"(P > True) = True" "(P > P) = True" 

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

941 
"(P & True) = P" "(True & P) = P" 

942 
"(P & False) = False" "(False & P) = False" 

943 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

945 
"(P  True) = True" "(True  P) = True" 

946 
"(P  False) = P" "(False  P) = P" 

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

947 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  948 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
949 
 {* needed for the onepointrule quantifier simplification procs *} 

950 
 {* essential for termination!! *} and 

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

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

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

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

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

955 
by (blast, blast, blast, blast, blast, rules+) 
13421  956 

12281  957 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
12354  958 
by rules 
12281  959 

960 
lemma ex_simps: 

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

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

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

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

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

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

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

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

968 
by (rules  blast)+ 
12281  969 

970 
lemma all_simps: 

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

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

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

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

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

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

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

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

978 
by (rules  blast)+ 
12281  979 

14201  980 
lemma disj_absorb: "(A  A) = A" 
981 
by blast 

982 

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

984 
by blast 

985 

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

987 
by blast 

988 

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

990 
by blast 

991 

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

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

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

995 
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

996 
lemma neq_commute: "(a~=b) = (b~=a)" by rules 
12281  997 

998 
lemma conj_comms: 

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

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

1000 
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

1001 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules 
12281  1002 

1003 
lemma disj_comms: 

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

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

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

1006 
lemma disj_assoc: "((PQ)R) = (P(QR))" by rules 
12281  1007 

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

1008 
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

1009 
lemma conj_disj_distribR: "((PQ)&R) = (P&R  Q&R)" by rules 
12281  1010 

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

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

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

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

1014 
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

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

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

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

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

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

1021 

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

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

1024 

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

1025 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by rules 
12281  1026 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1027 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1031 
by blast 

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

1033 

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

1034 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by rules 
12281  1035 

1036 

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

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

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

1040 
by blast 

1041 

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

1043 
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

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

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

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

1047 
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

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

1050 
text {* 

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

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

1053 

1054 
lemma conj_cong: 

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

12354  1056 
by rules 
12281  1057 

1058 
lemma rev_conj_cong: 

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

12354  1060 
by rules 
12281  1061 

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

1063 

1064 
lemma disj_cong: 

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

1066 
by blast 

1067 

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

12354  1069 
by rules 
12281  1070 

1071 

1072 
text {* \medskip ifthenelse rules *} 

1073 

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

1075 
by (unfold if_def) blast 

1076 

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

1078 
by (unfold if_def) blast 

1079 

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

1081 
by (unfold if_def) blast 

1082 

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

1084 
by (unfold if_def) blast 

1085 

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

1087 
apply (rule case_split [of Q]) 

15481  1088 
apply (simplesubst if_P) 
1089 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1090 
done 
1091 

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

15481  1093 
by (simplesubst split_if, blast) 
12281  1094 

1095 
lemmas if_splits = split_if split_if_asm 

1096 

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

1098 
by (rule split_if) 

1099 

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

15481  1101 
by (simplesubst split_if, blast) 
12281  1102 

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

15481  1104 
by (simplesubst split_if, blast) 
12281  1105 

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

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

1108 
by (rule split_if) 

1109 

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

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

15481  1112 
apply (simplesubst split_if, blast) 
12281  1113 
done 
1114 

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

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

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

15423  1118 
text {* \medskip let rules for simproc *} 
1119 

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

1121 
by (unfold Let_def) 

1122 

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

1124 
by (unfold Let_def) 

1125 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1126 
text {* 
16999  1127 
The following copy of the implication operator is useful for 
1128 
finetuning congruence rules. It instructs the simplifier to simplify 

1129 
its premise. 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1130 
*} 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1131 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1132 
consts 
16999  1133 
"=simp=>" :: "[prop, prop] => prop" (infixr 1) 
1134 
(* 

1135 
"op =simp=>" :: "[prop, prop] => prop" ("(_/ =simp=> _)" [2, 1] 1) 

1136 
syntax 

1137 
"op =simp=>" :: "[prop, prop] => prop" ("op =simp=>") 

1138 
*) 

1139 
defs simp_implies_def: "op =simp=> \<equiv> op ==>" 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1140 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1141 
lemma simp_impliesI: 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1142 
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1143 
shows "PROP P =simp=> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1144 
apply (unfold simp_implies_def) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1145 
apply (rule PQ) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1146 
apply assumption 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1147 
done 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1148 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1149 
lemma simp_impliesE: 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1150 
assumes PQ:"PROP P =simp=> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1151 
and P: "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1152 
and QR: "PROP Q \<Longrightarrow> PROP R" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1153 
shows "PROP R" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1154 
apply (rule QR) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1155 
apply (rule PQ [unfolded simp_implies_def]) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1156 
apply (rule P) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1157 
done 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1158 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1159 
lemma simp_implies_cong: 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1160 
assumes PP' :"PROP P == PROP P'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1161 
and P'QQ': "PROP P' ==> (PROP Q == PROP Q')" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1162 
shows "(PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1163 
proof (unfold simp_implies_def, rule equal_intr_rule) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1164 
assume PQ: "PROP P \<Longrightarrow> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1165 
and P': "PROP P'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1166 
from PP' [symmetric] and P' have "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1167 
by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1168 
hence "PROP Q" by (rule PQ) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1169 
with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1170 
next 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1171 
assume P'Q': "PROP P' \<Longrightarrow> PROP Q'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1172 
and P: "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1173 
from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1174 
hence "PROP Q'" by (rule P'Q') 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1175 
with P'QQ' [OF P', symmetric] show "PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1176 
by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1177 
qed 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1178 

14201  1179 
subsubsection {* Actual Installation of the Simplifier *} 
1180 

9869  1181 
use "simpdata.ML" 
1182 
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup 

1183 
setup Splitter.setup setup Clasimp.setup 

1184 

15481  1185 

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

1187 

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

1189 
use "eqrule_HOL_data.ML"; 

1190 

1191 
setup EQSubstTac.setup 

1192 

1193 

1194 
subsection {* Other simple lemmas *} 

1195 

15411  1196 
declare disj_absorb [simp] conj_absorb [simp] 
14201  1197 

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

1200 

15481  1201 

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

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

1205 
apply (fast dest!: theI') 

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

1207 
apply (erule ex1E) 

1208 
apply (rule allI) 

1209 
apply (rule ex1I) 

1210 
apply (erule spec) 

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

1212 
apply (erule impE) 

1213 
apply (rule allI) 

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

14208  1215 
apply (drule_tac [3] x = x in fun_cong, simp_all) 
13638  1216 
done 
1217 

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

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

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

1220 
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

1221 
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

1222 
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

1223 
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

1224 

11750  1225 

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

1227 

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

1228 
constdefs 
11989  1229 
induct_forall :: "('a => bool) => bool" 
1230 
"induct_forall P == \<forall>x. P x" 

1231 
induct_implies :: "bool => bool => bool" 

1232 
"induct_implies A B == A > B" 

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

1234 
"induct_equal x y == x = y" 

1235 
induct_conj :: "bool => bool => bool" 

1236 
"induct_conj A B == A & B" 

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

1237 

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

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

1240 

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

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

1243 

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

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

1246 

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

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

1250 

11989  1251 
lemma induct_implies_conj: "induct_implies C (induct_conj A B) = 
1252 
induct_conj (induct_implies C A) (induct_implies C B)" 

12354  1253 
by (unfold induct_implies_def induct_conj_def) rules 
11989  1254 

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

1255 
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

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

1257 
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

1258 
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

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

1260 
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

1261 
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

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

1263 

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

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

1266 

12161  1267 
lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq 
1268 
lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq 

1269 
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11989  1270 
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

1271 

11989  1272 
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

1273 

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

1274 

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

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

1276 

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

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

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

1279 
(struct 
15411  1280 
val dest_concls = HOLogic.dest_concls 
1281 
val cases_default = thm "case_split" 

1282 
val local_impI = thm "induct_impliesI" 

1283 
val conjI = thm "conjI" 

1284 
val atomize = thms "induct_atomize" 

1285 
val rulify1 = thms "induct_rulify1" 

1286 
val rulify2 = thms "induct_rulify2" 

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

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

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

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

1290 

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

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

1292 

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

1293 

14357  1294 
end 
15411  1295 