1319 text {*

  1320 conversions: core of the simplifier

  1321 

  1322 see: Pure/conv.ML

  1323 *}

  1324 

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

  1326 

  1327 text {*

  1328 simple example:

  1329 *}

  1330 

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

  1332 

  1333 ML {*

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

  1335 *}

  1336 

  1337 ML {*

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

  1339 *}

  1340 

  1341 text {*

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

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

  1344 *}

  1345 

  1346 text {*

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

  1348 *}

  1349 

  1350 ML {*

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

  1352 *}

  1353 

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

  1355 

  1356 ML {*

  1357 fun all_true1_conv ctxt ct =

  1358   (case Thm.term_of ct of

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

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

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

  1362 *}

  1363 

  1364 text {*

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

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

  1367 *}

  1368 

  1369 

  1370 text {*

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

  1372 

  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 =

  1386   (case Thm.term_of ct of

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

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

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

  1390 *}

  1391 

  1392 text {* show example *}

  1393 

  1394 text {*

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

  1396 *}

  1397 

  1398 ML {*

  1399 local open Conv 

  1400 in

  1401 fun true1_tac ctxt =

  1402   CONVERSION (

  1403     Conv.params_conv ~1 (fn cx =>

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

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

  1406 end

  1407 *}

  1408 

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

  1410 

  1411 

  1412 

  1413