1315 *} |
1316 *} |
1316 |
1317 |
1317 section {* Conversions\label{sec:conversion} *} |
1318 section {* Conversions\label{sec:conversion} *} |
1318 |
1319 |
1319 text {* |
1320 text {* |
1320 Conversions are meta-equalities depending on some input term. There type is |
1321 Conversions are meta-equalities depending on some input term. Their type is |
1321 as follows: |
1322 as follows: |
1322 *} |
1323 *} |
1323 |
1324 |
1324 ML {*type conv = Thm.cterm -> Thm.thm*} |
1325 ML {*type conv = Thm.cterm -> Thm.thm*} |
1325 |
1326 |
1326 text {* |
1327 text {* |
1327 The simplest two conversions are @{ML "Conv.all_conv"} and @{ML "Conv.no_conv"}: |
1328 The simplest two conversions are @{ML "Conv.all_conv"}, which maps a term to an instance of the reflexivity theorem, and @{ML "Conv.no_conv"}, which always fails: |
1328 |
1329 |
1329 @{ML_response_fake "Conv.all_conv @{cterm True}" "True \<equiv> True"} |
1330 @{ML_response_fake "Conv.all_conv @{cterm True}" "True \<equiv> True"} |
1330 |
1331 |
1331 @{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"} |
1332 @{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"} |
1332 |
1333 |
1333 Further basic conversions are, for example, @{ML "Thm.beta_conversion"} and |
1334 A further basic conversion is, for example, @{ML "Thm.beta_conversion"}: |
1334 @{ML "Conv.rewr_conv"}: |
1335 |
1335 *} |
|
1336 |
|
1337 lemma true_conj1: "True \<and> P \<equiv> P" by simp |
|
1338 |
|
1339 text {* |
|
1340 @{ML_response_fake "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}" |
1336 @{ML_response_fake "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}" |
1341 "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"} |
1337 "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"} |
1342 |
1338 |
|
1339 User-defined rewrite rules can be applied by the conversion |
|
1340 @{ML "Conv.rewr_conv"}. Consider, for example, the following rule: |
|
1341 *} |
|
1342 |
|
1343 lemma true_conj1: "True \<and> P \<equiv> P" by simp |
|
1344 |
|
1345 text {* |
|
1346 Here is how this rule can be used for rewriting: |
|
1347 |
1343 @{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}" |
1348 @{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}" |
1344 "True \<and> False \<equiv> False"} |
1349 "True \<and> False \<equiv> False"} |
1345 |
1350 *} |
|
1351 |
|
1352 text {* |
1346 Basic conversions can be combined with a number of conversionals, i.e. |
1353 Basic conversions can be combined with a number of conversionals, i.e. |
1347 conversion combinators: |
1354 conversion combinators: |
1348 |
1355 |
1349 @{ML_response_fake "Conv.then_conv (Thm.beta_conversion true, Conv.rewr_conv @{thm true_conj1}) @{cterm \"(\<lambda>x. x \<and> False) True\"}" "(\<lambda>x. x \<and> False) True \<equiv> False"} |
1356 @{ML_response_fake |
1350 |
1357 "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1}) |
1351 @{ML_response_fake "Conv.else_conv (Conv.rewr_conv @{thm true_conj1}, Conv.all_conv) @{cterm \"P \<or> (True \<and> Q)\"}" "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"} |
1358 @{cterm \"(\<lambda>x. x \<and> False) True\"}" |
1352 |
1359 "(\<lambda>x. x \<and> False) True \<equiv> False"} |
1353 @{ML_response_fake "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"P \<or> (True \<and> Q)\"}" "P \<or> (True \<and> Q) \<equiv> P \<or> Q"} |
1360 |
|
1361 @{ML_response_fake |
|
1362 "(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv) |
|
1363 @{cterm \"P \<or> (True \<and> Q)\"}" |
|
1364 "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"} |
|
1365 |
|
1366 @{ML_response_fake |
|
1367 "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) |
|
1368 @{cterm \"P \<or> (True \<and> Q)\"}" |
|
1369 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"} |
1354 |
1370 |
1355 \begin{readmore} |
1371 \begin{readmore} |
1356 See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions |
1372 See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions |
1357 can be found in, for example, @{ML_file "Pure/thm.ML"}, |
1373 can be found in, for example, @{ML_file "Pure/thm.ML"}, |
1358 @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}. |
1374 @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}. |
1360 |
1376 |
1361 Conversions are a thin layer on top of Isabelle's inference kernel, and may |
1377 Conversions are a thin layer on top of Isabelle's inference kernel, and may |
1362 be seen as a controllable, bare-bone version of Isabelle's simplifier. We |
1378 be seen as a controllable, bare-bone version of Isabelle's simplifier. We |
1363 will demonstrate this feature in the following example. |
1379 will demonstrate this feature in the following example. |
1364 |
1380 |
1365 For the moment, let's assumes we want to simplify according to the rewrite rule |
1381 To begin with, let's assumes we want to simplify with the rewrite rule |
1366 @{thm true_conj1}. As a conversion, this may look as follows: |
1382 @{text true_conj1}. As a conversion, this may look as follows: |
1367 *} |
1383 *} |
1368 |
1384 |
1369 ML {*fun all_true1_conv ctxt ct = |
1385 ML {*fun all_true1_conv ctxt ct = |
1370 (case Thm.term_of ct of |
1386 (case Thm.term_of ct of |
1371 @{term "op \<and>"} $ @{term True} $ _ => Conv.rewr_conv @{thm true_conj1} ct |
1387 @{term "op \<and>"} $ @{term True} $ _ => |
1372 | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) (all_true1_conv ctxt) ct |
1388 (Conv.arg_conv (all_true1_conv ctxt) then_conv |
|
1389 Conv.rewr_conv @{thm true_conj1}) ct |
|
1390 | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) |
|
1391 (all_true1_conv ctxt) ct |
1373 | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct |
1392 | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct |
1374 | _ => Conv.all_conv ct)*} |
1393 | _ => Conv.all_conv ct)*} |
1375 |
1394 |
1376 text {* |
1395 text {* |
1377 Here is the new conversion in action: |
1396 Here is this conversion in action: |
1378 |
1397 |
1379 @{ML_response_fake "all_true1_conv @{context} @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}" |
1398 @{ML_response_fake |
1380 "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"} |
1399 "all_true1_conv @{context} |
1381 |
1400 @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}" |
1382 Now, let's complicate the task: Rewrite according to the rule |
1401 "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"} |
1383 @{thm true_conj1}, but only in the first arguments of @{term If}: |
1402 |
|
1403 Now, let's complicate the task a bit: Rewrite according to the rule |
|
1404 @{text true_conj1}, but only in the first arguments of @{term If}: |
1384 *} |
1405 *} |
1385 |
1406 |
1386 ML {*fun if_true1_conv ctxt ct = |
1407 ML {*fun if_true1_conv ctxt ct = |
1387 (case Thm.term_of ct of |
1408 (case Thm.term_of ct of |
1388 Const (@{const_name If}, _) $ _ => Conv.arg_conv (all_true1_conv ctxt) ct |
1409 Const (@{const_name If}, _) $ _ => |
1389 | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) (if_true1_conv ctxt) ct |
1410 Conv.arg_conv (all_true1_conv ctxt) ct |
|
1411 | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) |
|
1412 (if_true1_conv ctxt) ct |
1390 | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct |
1413 | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct |
1391 | _ => Conv.all_conv ct)*} |
1414 | _ => Conv.all_conv ct)*} |
1392 |
1415 |
1393 text {* |
1416 text {* |
1394 Here is an application of this new conversion: |
1417 Here is an application of this conversion: |
1395 |
1418 |
1396 @{ML_response_fake "if_true1_conv @{context} @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}" "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"} |
1419 @{ML_response_fake |
|
1420 "if_true1_conv @{context} |
|
1421 @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}" |
|
1422 "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"} |
1397 *} |
1423 *} |
1398 |
1424 |
1399 text {* |
1425 text {* |
1400 Conversions can also be turned into a tactic with the @{ML CONVERSION} |
1426 Conversions can also be turned into a tactic with the @{ML CONVERSION} |
1401 tactical, and there are predefined conversionals to traverse a goal state |
1427 tactical, and there are predefined conversionals to traverse a goal state. |
1402 |
1428 Given a state @{term "\<And>x. P \<Longrightarrow> Q"}, the conversional |
1403 @{term "\<And>x. P \<Longrightarrow> Q"}: |
1429 @{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"}; |
1404 |
1430 given a state @{term "\<lbrakk> P1; P2 \<rbrakk> \<Longrightarrow> Q"}, |
1405 The conversional |
1431 the conversional @{ML Conv.prems_conv} applies a conversion to the premises |
1406 @{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"}, |
1432 @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to |
1407 @{ML Conv.prems_conv} applies a conversion to all premises in @{term "P \<Longrightarrow> Q"}, and |
1433 the conclusion @{term Q}. |
1408 @{ML Conv.concl_conv} applies a conversion to the conclusion @{term Q} in @{term "P \<Longrightarrow> Q"}. |
|
1409 |
1434 |
1410 Assume we want to apply @{ML all_true1_conv} only in the conclusion |
1435 Assume we want to apply @{ML all_true1_conv} only in the conclusion |
1411 of the goal, and @{ML if_true1_conv} should only be applied in the premises. |
1436 of the goal, and @{ML if_true1_conv} should only be applied in the premises. |
1412 Here is a tactic doing exactly that: |
1437 Here is a tactic doing exactly that: |
1413 *} |
1438 *} |
1414 |
1439 |
1415 ML {*local open Conv |
1440 ML {*val true1_tac = CSUBGOAL (fn (goal, i) => |
1416 in |
|
1417 val true1_tac = CSUBGOAL (fn (goal, i) => |
|
1418 let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) |
1441 let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) |
1419 in |
1442 in |
1420 CONVERSION ( |
1443 CONVERSION ( |
1421 Conv.params_conv ~1 (fn cx => |
1444 Conv.params_conv ~1 (fn cx => |
1422 (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv |
1445 (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv |
1423 (Conv.concl_conv ~1 (all_true1_conv cx))) ctxt) i |
1446 Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i |
1424 end) |
1447 end)*} |
1425 end*} |
1448 |
1426 |
1449 text {* |
1427 text {* FIXME: give example, show that the conditional rewriting works *} |
1450 To demonstrate this tactic, consider the following example: |
1428 |
1451 *} |
|
1452 |
|
1453 lemma |
|
1454 "if True \<and> P then P else True \<and> False \<Longrightarrow> |
|
1455 (if True \<and> Q then Q else P) \<longrightarrow> True \<and> (True \<and> Q)" |
|
1456 apply(tactic {* true1_tac 1 *}) |
|
1457 txt {* \begin{minipage}{\textwidth} |
|
1458 @{subgoals [display]} |
|
1459 \end{minipage} *} |
|
1460 (*<*)oops(*>*) |
1429 |
1461 |
1430 text {* |
1462 text {* |
1431 Conversions are not restricted to work on certified terms only, they can also |
1463 Conversions are not restricted to work on certified terms only, they can also |
1432 be lifted to theorem transformers, i.e. functions mapping a theorem to a |
1464 be lifted to theorem transformers, i.e. functions mapping a theorem to a |
1433 theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the |
1465 theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the |
1434 conversion @{ML all_true1_conv} again: |
1466 conversion @{ML all_true1_conv} again: |
1435 |
1467 |
1436 @{ML_response_fake "Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"} |
1468 @{ML_response_fake |
|
1469 "Conv.fconv_rule (all_true1_conv @{context}) |
|
1470 @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"} |
1437 *} |
1471 *} |
1438 |
1472 |
1439 |
1473 |
1440 |
1474 |
1441 |
1475 |