1320 conversions: core of the simplifier

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

  1321 

  1322 as follows:

  1322 see: Pure/conv.ML

  1323 *}

  1323 *}

  1324 

  1324 

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

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

  1326 

  1326 

  1327 text {*

  1327 text {*

  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 simple example:

  1329 

  1329 *}

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

  1330 

  1331 

  1331 lemma true_conj_1: "True \<and> P \<equiv> P" by simp

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

  1332 

  1333 

  1333 ML {*

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

  1334 val true1_conv = Conv.rewr_conv @{thm true_conj_1}

  1335 

  1335 *}

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

  1336 

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

  1337 ML {*

  1338 

  1338 true1_conv @{cterm "True \<and> False"}

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

  1339 *}

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

  1340 

  1341 *}

  1341 text {*

  1342 

  1342 @{ML_response_fake "true1_conv @{cterm \"True \<and> False\"}"

  1343 lemma true_conj1: "True \<and> P \<equiv> P" by simp

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

  1344 

  1344 *}

  1345 text {*

  1345 

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

  1346 text {*

  1347 

  1347 how to extend rewriting to more complex cases? e.g.:

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

  1348 *}

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

  1349 

  1350 *}

  1350 ML {*

  1351 

  1351 val complex = @{cterm "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> (x::int)"}

  1352 text {*

  1352 *}

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

  1353 

  1354 conversion combinators:

  1354 text {* conversionals: basically a count-down version of MetaSimplifier.rewrite *}

  1355 

  1355 

  1356 @{ML_response_fake

  1356 ML {*

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

  1357 fun all_true1_conv ctxt ct =

  1358   @{cterm \"(\<lambda>x. x \<and> False) True\"}"

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

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

  1370 

  1371 \begin{readmore}

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

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

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

  1375 \end{readmore}

  1376 

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

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

  1379 will demonstrate this feature in the following example.

  1380 

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

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

  1383 *}

  1384 

  1385 ML {*fun all_true1_conv ctxt ct =

  1359     @{term "op \<and>"} $ @{term True} $ _ => true1_conv ct

  1387     @{term "op \<and>"} $ @{term True} $ _ => 

  1360   | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) (all_true1_conv ctxt) ct

  1388       (Conv.arg_conv (all_true1_conv ctxt) then_conv

  1361   | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct)

  1389         Conv.rewr_conv @{thm true_conj1}) ct

  1362 *}

  1390   | _ $ _ => Conv.combination_conv (all_true1_conv ctxt)

  1363 

  1391       (all_true1_conv ctxt) ct

  1364 text {*

  1392   | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct

  1365 @{ML_response_fake "all_true1_conv @{context} complex"

  1393   | _ => Conv.all_conv ct)*}

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

  1394 

  1367 *}

  1395 text {*

  1368 

  1396 Here is this conversion in action:

  1369 

  1397 

  1370 text {*

  1398 @{ML_response_fake

  1371 transforming theorems: @{ML "Conv.fconv_rule"} (give type)

  1399 "all_true1_conv @{context}

  1372 

  1400   @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}"

  1373 example:

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

  1374 *}

  1402 

  1375 

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

  1376 lemma foo: "True \<and> (P \<or> \<not>P)" by simp

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

  1377 

  1405 *}

  1378 text {*

  1406 

  1379 @{ML_response_fake "Conv.fconv_rule (Conv.arg_conv (all_true1_conv @{context})) @{thm foo}" "P \<or> \<not>P"}

  1407 ML {*fun if_true1_conv ctxt ct =

  1380 *}

  1381 

  1382 text {* now, replace "True and P" with "P" if it occurs inside an If *}

  1383 

  1384 ML {*

  1385 fun if_true1_conv ctxt ct =

  1387     Const (@{const_name If}, _) $ _ => Conv.arg_conv (all_true1_conv ctxt) ct

  1409     Const (@{const_name If}, _) $ _ =>

  1388   | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) (if_true1_conv ctxt) ct

  1410       Conv.arg_conv (all_true1_conv ctxt) ct

  1389   | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct)

  1411   | _ $ _ => Conv.combination_conv (if_true1_conv ctxt)

  1390 *}

  1412       (if_true1_conv ctxt) ct

  1391 

  1413   | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct

  1392 text {* show example *}

  1414   | _ => Conv.all_conv ct)*}

  1393 

  1415 

  1394 text {*

  1416 text {*

  1395 conversions inside a tactic: replace "true" in conclusion, "if true" in assumptions

  1417 Here is an application of this conversion:

  1396 *}

  1418 

  1397 

  1419 @{ML_response_fake

  1398 ML {*

  1420 "if_true1_conv @{context}

  1399 local open Conv 

  1421   @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}"

  1400 in

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

  1401 fun true1_tac ctxt =

  1423 *}

  1402   CONVERSION (

  1424 

  1403     Conv.params_conv ~1 (fn cx =>

  1425 text {*

  1404       (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv

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

  1405         (Conv.concl_conv ~1 (all_true1_conv cx))) ctxt)

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

  1406 end

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

  1407 *}

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

  1408 

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

  1409 text {* give example, show that the conditional rewriting works *}

  1431 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

  1433 the conclusion @{term Q}.

  1434 

  1435 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.

  1437 Here is a tactic doing exactly that:

  1438 *}

  1439 

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

  1441   let val ctxt = ProofContext.init (Thm.theory_of_cterm goal)

  1442   in

  1443     CONVERSION (

  1444       Conv.params_conv ~1 (fn cx =>

  1445         (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv

  1446           Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i

  1447   end)*}

  1448 

  1449 text {* 

  1450 To demonstrate this tactic, consider the following example:

  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(*>*)

  1461 

  1462 text {*

  1463 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

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

  1466 conversion @{ML all_true1_conv} again:

  1467 

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

  1471 *}