1321 Conversions are meta-equalities depending on some input term. Their type is

  1321 

  1322 as follows:

  1322   Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and 

  1323 *}

  1323   may be seen as a controllable, bare-bone version of Isabelle's simplifier.

  1324 

  1324   They are meta-equalities depending on some input term. Their type is

  1325 ML {*type conv = Thm.cterm -> Thm.thm*}

  1325   as follows:

  1326 

  1326 *}

  1327 text {*

  1327 

  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 ML{*type conv = Thm.cterm -> Thm.thm*}

  1329 

  1329 

  1330 @{ML_response_fake "Conv.all_conv @{cterm True}" "True \<equiv> True"}

  1330 text {*

  1331 

  1331   The simplest two conversions are @{ML "Conv.all_conv"}, which maps a 

  1332 @{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"}

  1332   term to an instance of the reflexivity theorem, and 

  1333 

  1333   @{ML "Conv.no_conv"}, which always fails:

  1334 A further basic conversion is, for example, @{ML "Thm.beta_conversion"}:

  1334 

  1335 

  1335   @{ML_response_fake [display,gray]

  1336 @{ML_response_fake "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"

  1336   "Conv.all_conv @{cterm True}" "True \<equiv> True"}

  1337 "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}

  1337 

  1338 

  1338   @{ML_response_fake [display,gray]

  1339 User-defined rewrite rules can be applied by the conversion

  1339   "Conv.no_conv @{cterm True}" 

  1340 @{ML "Conv.rewr_conv"}. Consider, for example, the following rule:

  1340   "*** Exception- CTERM (\"no conversion\", []) raised"}

  1341 

  1342   A further basic conversion is, for example, @{ML "Thm.beta_conversion"}:

  1343 

  1344   @{ML_response_fake [display,gray]

  1345   "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"

  1346   "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}

  1347 

  1348   User-defined rewrite rules can be applied by the conversion

  1349   @{ML "Conv.rewr_conv"}. Consider, for example, the following rule:

  1346 Here is how this rule can be used for rewriting:

  1355   Here is how this rule can be used for rewriting:

  1347 

  1356 

  1348 @{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"

  1357   @{ML_response_fake [display,gray]

  1349  "True \<and> False \<equiv> False"}

  1358   "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"

  1350 *}

  1359   "True \<and> False \<equiv> False"}

  1351 

  1360 *}

  1352 text {*

  1361 

  1353 Basic conversions can be combined with a number of conversionals, i.e.

  1362 text {*

  1354 conversion combinators:

  1363   Basic conversions can be combined with a number of conversionals, i.e.

  1355 

  1364   conversion combinators:

  1356 @{ML_response_fake

  1365 

  1357 "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1})

  1366   @{ML_response_fake [display,gray]

  1367   "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1})

  1359 "(\<lambda>x. x \<and> False) True \<equiv> False"}

  1369   "(\<lambda>x. x \<and> False) True \<equiv> False"}

  1360 

  1370 

  1361 @{ML_response_fake

  1371   @{ML_response_fake [display,gray]

  1362 "(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv)

  1372   "(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv)

  1364 "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"}

  1374   "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"}

  1365 

  1375 

  1366 @{ML_response_fake

  1376   @{ML_response_fake [display,gray]

  1367 "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})

  1377   "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})

  1369 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}

  1379   "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}

  1370 

  1380 

  1371 \begin{readmore}

  1381   \begin{readmore}

  1372 See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions

  1382   See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions

  1373 can be found in, for example, @{ML_file "Pure/thm.ML"},

  1383   can be found in, for example, @{ML_file "Pure/thm.ML"},

  1374 @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}.

  1384   @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}.

  1375 \end{readmore}

  1385   \end{readmore}

  1376 

  1386 

  1377 Conversions are a thin layer on top of Isabelle's inference kernel, and may

  1387   We will demonstrate this feature in the following example.

  1378 be seen as a controllable, bare-bone version of Isabelle's simplifier. We

  1388 

  1379 will demonstrate this feature in the following example.

  1389   To begin with, let's assumes we want to simplify with the rewrite rule

  1380 

  1390   @{text true_conj1}. As a conversion, this may look as follows:

  1381 To begin with, let's assumes we want to simplify with the rewrite rule

  1391 *}

  1382 @{text true_conj1}. As a conversion, this may look as follows:

  1392 

  1383 *}

  1393 ML{*fun all_true1_conv ctxt ct =

  1384 

  1385 ML {*fun all_true1_conv ctxt ct =

  1396 Here is this conversion in action:

  1404   Here is this conversion in action:

  1397 

  1405 

  1398 @{ML_response_fake

  1406   @{ML_response_fake [display,gray]

  1399 "all_true1_conv @{context}

  1407   "all_true1_conv @{context}

  1401 "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}

  1409   "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}

  1402 

  1410 

  1403 Now, let's complicate the task a bit: Rewrite according to the rule

  1411   Now, let make the task a bit more  complicated by rewrite according to the rule

  1404 @{text true_conj1}, but only in the first arguments of @{term If}:

  1412   @{text true_conj1}, but only in the first arguments of @{term If}:

  1405 *}

  1413 *}

  1406 

  1414 

  1407 ML {*fun if_true1_conv ctxt ct =

  1415 ML{*fun if_true1_conv ctxt ct =

  1417 Here is an application of this conversion:

  1425   Here is an application of this conversion:

  1418 

  1426 

  1419 @{ML_response_fake

  1427   @{ML_response_fake [display,gray]

  1420 "if_true1_conv @{context}

  1428   "if_true1_conv @{context}

  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"}

  1430   "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"}

  1423 *}

  1431 *}

  1424 

  1432 

  1425 text {*

  1433 text {*

  1426 Conversions can also be turned into a tactic with the @{ML CONVERSION}

  1434   Conversions can also be turned into a tactic with the @{ML CONVERSION}

  1427 tactical, and there are predefined conversionals to traverse a goal state.

  1435   tactical, and there are predefined conversionals to traverse a goal state.

  1428 Given a state @{term "\<And>x. P \<Longrightarrow> Q"},  the conversional

  1436   Given a state @{term "\<And>x. P \<Longrightarrow> Q"},  the conversional

  1429 @{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"};

  1437   @{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"};

  1430 given a state @{term "\<lbrakk> P1; P2 \<rbrakk> \<Longrightarrow> Q"},

  1438   given a state @{term "\<lbrakk> P1; P2 \<rbrakk> \<Longrightarrow> Q"},

  1431 the conversional @{ML Conv.prems_conv} applies a conversion to the premises

  1439   the conversional @{ML Conv.prems_conv} applies a conversion to the premises

  1432 @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to

  1440   @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to

  1433 the conclusion @{term Q}.

  1441   the conclusion @{term Q}.

  1434 

  1442 

  1435 Assume we want to apply @{ML all_true1_conv} only in the conclusion

  1443   Assume we want to apply @{ML all_true1_conv} only in the conclusion

  1436 of the goal, and @{ML if_true1_conv} should only be applied in the premises.

  1444   of the goal, and @{ML if_true1_conv} should only be applied in the premises.

  1437 Here is a tactic doing exactly that:

  1445   Here is a tactic doing exactly that:

  1438 *}

  1446 *}

  1439 

  1447 

  1440 ML {*val true1_tac = CSUBGOAL (fn (goal, i) =>

  1448 ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>

  1450 To demonstrate this tactic, consider the following example:

  1458   To demonstrate this tactic, consider the following example:

  1463 Conversions are not restricted to work on certified terms only, they can also

  1471   Conversions are not restricted to work on certified terms only, they can also

  1464 be lifted to theorem transformers, i.e. functions mapping a theorem to a

  1472   be lifted to theorem transformers, i.e. functions mapping a theorem to a

  1465 theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the

  1473   theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the

  1466 conversion @{ML all_true1_conv} again:

  1474   conversion @{ML all_true1_conv} again:

  1467 

  1475 

  1468 @{ML_response_fake

  1476   @{ML_response_fake [display,gray]

  1469 "Conv.fconv_rule (all_true1_conv @{context})

  1477   "Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" 

  1470   @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"}

  1478   "P \<or> \<not>P"}

  1471 *}

  1479 *}

  1472 

  1473