235 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
235 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
236 |
236 |
237 |
237 |
238 subsection {*Equality*} |
238 subsection {*Equality*} |
239 |
239 |
240 lemma sym: "s=t ==> t=s" |
240 lemma sym: "s = t ==> t = s" |
241 apply (erule subst) |
241 by (erule subst) (rule refl) |
242 apply (rule refl) |
242 |
243 done |
243 lemma ssubst: "t = s ==> P s ==> P t" |
244 |
244 by (drule sym) (erule subst) |
245 (*calling "standard" reduces maxidx to 0*) |
|
246 lemmas ssubst = sym [THEN subst, standard] |
|
247 |
245 |
248 lemma trans: "[| r=s; s=t |] ==> r=t" |
246 lemma trans: "[| r=s; s=t |] ==> r=t" |
249 apply (erule subst , assumption) |
247 by (erule subst) |
250 done |
248 |
251 |
249 lemma def_imp_eq: assumes meq: "A == B" shows "A = B" |
252 lemma def_imp_eq: assumes meq: "A == B" shows "A = B" |
250 by (unfold meq) (rule refl) |
253 apply (unfold meq) |
251 |
254 apply (rule refl) |
|
255 done |
|
256 |
252 |
257 (*Useful with eresolve_tac for proving equalties from known equalities. |
253 (*Useful with eresolve_tac for proving equalties from known equalities. |
258 a = b |
254 a = b |
259 | | |
255 | | |
260 c = d *) |
256 c = d *) |
301 |
297 |
302 |
298 |
303 subsection {*Equality of booleans -- iff*} |
299 subsection {*Equality of booleans -- iff*} |
304 |
300 |
305 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" |
301 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" |
306 apply (iprover intro: iff [THEN mp, THEN mp] impI prems) |
302 by (iprover intro: iff [THEN mp, THEN mp] impI prems) |
307 done |
|
308 |
303 |
309 lemma iffD2: "[| P=Q; Q |] ==> P" |
304 lemma iffD2: "[| P=Q; Q |] ==> P" |
310 apply (erule ssubst) |
305 by (erule ssubst) |
311 apply assumption |
|
312 done |
|
313 |
306 |
314 lemma rev_iffD2: "[| Q; P=Q |] ==> P" |
307 lemma rev_iffD2: "[| Q; P=Q |] ==> P" |
315 apply (erule iffD2) |
308 by (erule iffD2) |
316 apply assumption |
|
317 done |
|
318 |
309 |
319 lemmas iffD1 = sym [THEN iffD2, standard] |
310 lemmas iffD1 = sym [THEN iffD2, standard] |
320 lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard] |
311 lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard] |
321 |
312 |
322 lemma iffE: |
313 lemma iffE: |
323 assumes major: "P=Q" |
314 assumes major: "P=Q" |
324 and minor: "[| P --> Q; Q --> P |] ==> R" |
315 and minor: "[| P --> Q; Q --> P |] ==> R" |
325 shows "R" |
316 shows R |
326 by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) |
317 by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) |
327 |
318 |
328 |
319 |
329 subsection {*True*} |
320 subsection {*True*} |
330 |
321 |
331 lemma TrueI: "True" |
322 lemma TrueI: "True" |
332 apply (unfold True_def) |
323 by (unfold True_def) (rule refl) |
333 apply (rule refl) |
|
334 done |
|
335 |
324 |
336 lemma eqTrueI: "P ==> P=True" |
325 lemma eqTrueI: "P ==> P=True" |
337 by (iprover intro: iffI TrueI) |
326 by (iprover intro: iffI TrueI) |
338 |
327 |
339 lemma eqTrueE: "P=True ==> P" |
328 lemma eqTrueE: "P=True ==> P" |
340 apply (erule iffD2) |
329 apply (erule iffD2) |
341 apply (rule TrueI) |
330 apply (rule TrueI) |
342 done |
331 done |
1144 |
1142 |
1145 constdefs |
1143 constdefs |
1146 simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) |
1144 simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) |
1147 "simp_implies \<equiv> op ==>" |
1145 "simp_implies \<equiv> op ==>" |
1148 |
1146 |
1149 lemma simp_impliesI: |
1147 lemma simp_impliesI: |
1150 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" |
1148 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" |
1151 shows "PROP P =simp=> PROP Q" |
1149 shows "PROP P =simp=> PROP Q" |
1152 apply (unfold simp_implies_def) |
1150 apply (unfold simp_implies_def) |
1153 apply (rule PQ) |
1151 apply (rule PQ) |
1154 apply assumption |
1152 apply assumption |
1280 |
1278 |
1281 |
1279 |
1282 subsection {* Generic cases and induction *} |
1280 subsection {* Generic cases and induction *} |
1283 |
1281 |
1284 constdefs |
1282 constdefs |
1285 induct_forall :: "('a => bool) => bool" |
1283 induct_forall where "induct_forall P == \<forall>x. P x" |
1286 "induct_forall P == \<forall>x. P x" |
1284 induct_implies where "induct_implies A B == A \<longrightarrow> B" |
1287 induct_implies :: "bool => bool => bool" |
1285 induct_equal where "induct_equal x y == x = y" |
1288 "induct_implies A B == A --> B" |
1286 induct_conj where "induct_conj A B == A \<and> B" |
1289 induct_equal :: "'a => 'a => bool" |
|
1290 "induct_equal x y == x = y" |
|
1291 induct_conj :: "bool => bool => bool" |
|
1292 "induct_conj A B == A & B" |
|
1293 |
1287 |
1294 lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" |
1288 lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" |
1295 by (simp only: atomize_all induct_forall_def) |
1289 by (unfold atomize_all induct_forall_def) |
1296 |
1290 |
1297 lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" |
1291 lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" |
1298 by (simp only: atomize_imp induct_implies_def) |
1292 by (unfold atomize_imp induct_implies_def) |
1299 |
1293 |
1300 lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" |
1294 lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" |
1301 by (simp only: atomize_eq induct_equal_def) |
1295 by (unfold atomize_eq induct_equal_def) |
|
1296 |
|
1297 lemma induct_conj_eq: |
|
1298 includes meta_conjunction_syntax |
|
1299 shows "(A && B) == Trueprop (induct_conj A B)" |
|
1300 by (unfold atomize_conj induct_conj_def) |
|
1301 |
|
1302 lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj |
|
1303 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
|
1304 lemmas induct_rulify [symmetric, standard] = induct_atomize |
|
1305 lemmas induct_rulify_fallback = |
|
1306 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
1307 |
1302 |
1308 |
1303 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = |
1309 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = |
1304 induct_conj (induct_forall A) (induct_forall B)" |
1310 induct_conj (induct_forall A) (induct_forall B)" |
1305 by (unfold induct_forall_def induct_conj_def) iprover |
1311 by (unfold induct_forall_def induct_conj_def) iprover |
1306 |
1312 |
1309 by (unfold induct_implies_def induct_conj_def) iprover |
1315 by (unfold induct_implies_def induct_conj_def) iprover |
1310 |
1316 |
1311 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" |
1317 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" |
1312 proof |
1318 proof |
1313 assume r: "induct_conj A B ==> PROP C" and A B |
1319 assume r: "induct_conj A B ==> PROP C" and A B |
1314 show "PROP C" by (rule r) (simp! add: induct_conj_def) |
1320 show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`) |
1315 next |
1321 next |
1316 assume r: "A ==> B ==> PROP C" and "induct_conj A B" |
1322 assume r: "A ==> B ==> PROP C" and "induct_conj A B" |
1317 show "PROP C" by (rule r) (simp! add: induct_conj_def)+ |
1323 show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def]) |
1318 qed |
1324 qed |
1319 |
1325 |
1320 lemma induct_impliesI: "(A ==> B) ==> induct_implies A B" |
|
1321 by (simp add: induct_implies_def) |
|
1322 |
|
1323 lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq |
|
1324 lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq |
|
1325 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
1326 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry |
1326 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry |
1327 |
1327 |
1328 hide const induct_forall induct_implies induct_equal induct_conj |
1328 hide const induct_forall induct_implies induct_equal induct_conj |
1329 |
1329 |
1330 |
1330 |
1331 text {* Method setup. *} |
1331 text {* Method setup. *} |
1332 |
1332 |
1333 ML {* |
1333 ML {* |
1334 structure InductMethod = InductMethodFun |
1334 structure InductMethod = InductMethodFun |
1335 (struct |
1335 (struct |
1336 val dest_concls = HOLogic.dest_concls |
|
1337 val cases_default = thm "case_split" |
1336 val cases_default = thm "case_split" |
1338 val local_impI = thm "induct_impliesI" |
1337 val atomize_old = thms "induct_atomize_old" |
1339 val conjI = thm "conjI" |
|
1340 val atomize = thms "induct_atomize" |
1338 val atomize = thms "induct_atomize" |
1341 val rulify1 = thms "induct_rulify1" |
1339 val rulify = thms "induct_rulify" |
1342 val rulify2 = thms "induct_rulify2" |
1340 val rulify_fallback = thms "induct_rulify_fallback" |
1343 val localize = [Thm.symmetric (thm "induct_implies_def")] |
|
1344 end); |
1341 end); |
1345 *} |
1342 *} |
1346 |
1343 |
1347 setup InductMethod.setup |
1344 setup InductMethod.setup |
1348 |
1345 |
1349 subsubsection{*Tags, for the ATP Linkup*} |
1346 |
|
1347 subsubsection {*Tags, for the ATP Linkup *} |
1350 |
1348 |
1351 constdefs |
1349 constdefs |
1352 tag :: "bool => bool" |
1350 tag :: "bool => bool" |
1353 "tag P == P" |
1351 "tag P == P" |
1354 |
1352 |
1355 text{*These label the distinguished literals of introduction and elimination |
1353 text{*These label the distinguished literals of introduction and elimination |
1356 rules.*} |
1354 rules.*} |
1357 |
1355 |
1358 lemma tagI: "P ==> tag P" |
1356 lemma tagI: "P ==> tag P" |