1320 conversions: core of the simplifier

  1320 Conversions are meta-equalities depending on some input term. There type is

  1321 

  1321 as follows:

  1322 see: Pure/conv.ML

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

  1328 

  1329 *}

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

  1330 

  1330 

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

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

  1332 

  1332 

  1333 ML {*

  1333 Further basic conversions are, for example, @{ML "Thm.beta_conversion"} and

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

  1334  @{ML "Conv.rewr_conv"}:

  1335 *}

  1335 *}

  1336 

  1336 

  1337 ML {*

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

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

  1338 

  1339 *}

  1339 text {*

  1340 

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

  1341 text {*

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

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

  1342 

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

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

  1344 *}

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

  1345 

  1345 

  1346 text {*

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

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

  1347 conversion combinators:

  1348 *}

  1348 

  1349 

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

  1350 ML {*

  1350 

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

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

  1352 *}

  1352 

  1353 

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

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

  1354 

  1355 

  1355 \begin{readmore}

  1356 ML {*

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

  1357 fun all_true1_conv ctxt ct =

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

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

  1359 \end{readmore}

  1360 

  1361 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

  1363 will demonstrate this feature in the following example.

  1364 

  1365 For the moment, let's assumes we want to simplify according to the rewrite rule

  1366 @{thm true_conj1}. As a conversion, this may look as follows:

  1367 *}

  1368 

  1369 ML {*fun all_true1_conv ctxt ct =

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

  1371     @{term "op \<and>"} $ @{term True} $ _ => Conv.rewr_conv @{thm true_conj1} ct

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

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

  1362 *}

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

  1363 

  1375 

  1364 text {*

  1376 text {*

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

  1377 Here is the new conversion in action:

  1378 

  1379 @{ML_response_fake "all_true1_conv @{context} @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}"

  1367 *}

  1381 

  1368 

  1382 Now, let's complicate the task: Rewrite according to the rule

  1369 

  1383 @{thm true_conj1}, but only in the first arguments of @{term If}:

  1370 text {*

  1384 *}

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

  1385 

  1372 

  1386 ML {*fun if_true1_conv ctxt ct =

  1373 example:

  1374 *}

  1375 

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

  1377 

  1378 text {*

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

  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 =

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

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

  1390 *}

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

  1391 

  1392 

  1392 text {* show example *}

  1393 text {*

  1393 

  1394 Here is an application of this new conversion:

  1394 text {*

  1395 

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

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

  1396 *}

  1397 *}

  1397 

  1398 

  1398 ML {*

  1399 text {*

  1399 local open Conv 

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

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

  1402 

  1403 @{term "\<And>x. P \<Longrightarrow> Q"}: 

  1404 

  1405 The conversional

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

  1407 @{ML Conv.prems_conv} applies a conversion to all premises in @{term "P \<Longrightarrow> Q"}, and

  1408 @{ML Conv.concl_conv} applies a conversion to the conclusion @{term Q} in @{term "P \<Longrightarrow> Q"}.

  1409 

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

  1412 Here is a tactic doing exactly that:

  1413 *}

  1414 

  1415 ML {*local open Conv 

  1401 fun true1_tac ctxt =

  1417 val true1_tac = CSUBGOAL (fn (goal, i) =>

  1402   CONVERSION (

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

  1403     Conv.params_conv ~1 (fn cx =>

  1419   in

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

  1420     CONVERSION (

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

  1421       Conv.params_conv ~1 (fn cx =>

  1406 end

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

  1407 *}

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

  1408 

  1424   end)

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

  1425 end*}

  1426 

  1427 text {* FIXME: give example, show that the conditional rewriting works *}

  1428 

  1429 

  1430 text {*

  1431 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

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

  1434 conversion @{ML all_true1_conv} again:

  1435 

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

  1437 *}