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

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

  1324   A difference is that conversions simplify @{ML_type cterm}s, while teh simplifier

  1326   One difference between conversions and the simplifier is that the former

  1325   acts on theorems. The type for conversions is

  1327   act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. 

  1328   However, we will also show in this section how conversions can be applied

  1329   to theorems via tactics. The type for conversions is

  1331   whereby the theorem is always a meta-equality. A simple conversion is 

  1335   whereby the produced theorem is always a meta-equality. A simple conversion

  1332   the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an instance of 

  1336   is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an

  1333   the (meta)reflexivity theorem. For example:

  1337   instance of the (meta)reflexivity theorem. For example:

  1339   Another simple conversion is @{ML Conv.no_conv} which always raises the exception @{ML CTERM}

  1343   Another simple conversion is @{ML Conv.no_conv} which always raises the 

  1344   exception @{ML CTERM}.

  1358   Note that the actual response in the example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 

  1363   Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 

  1359   since the pretty-printer of @{ML_type cterm}s already beta-normalises terms.

  1364   since the pretty printer for @{ML_type cterm}s already beta-normalises terms.

  1360   However, we can by how we constructed the term (using the function 

  1365   But by the way how we constructed the term (using the function 

  1361   @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm})

  1366   @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s),

  1362   that the left-hand side must contain beta-redexes.

  1367   we can be sure the left-hand side must contain beta-redexes. Indeed

  1368   if we obtain the ``raw'' representation of the produced theorem, we

  1369   can see the difference:

  1370 

  1371   @{ML_response [display,gray]

  1372 "let

  1373   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  1374   val two = @{cterm \"2::nat\"}

  1375   val ten = @{cterm \"10::nat\"}

  1376 in

  1377   #prop (rep_thm 

  1378           (Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)))

  1379 end"

  1380 "Const (\"==\",\<dots>) $ 

  1381   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 

  1382     (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 

  1365   the right-hand side should be fully beta-normalised. If @{ML false} is

  1385   the right-hand side will be fully beta-normalised. If instead 

  1366   given, then only a beta-reduction is performed on the outer-most level.

  1386   @{ML false} is given, then only a single beta-reduction is performed 

  1367   For example

  1387   on the outer-most level. For example

  1379   @{term "\<lambda>y. 2 + y"}.

  1399   @{text "\<lambda>y. 2 + y"}.

  1380 

  1400 

  1381   The main point of conversions is that they can be used for rewriting terms.

  1401   The main point of conversions is that they can be used for rewriting

  1382   For this you can use the function @{ML "Conv.rewr_conv"}. Suppose we want 

  1402   @{ML_type cterm}s. To do this you can use the function @{ML

  1383   to rewrite a term according to the (meta)equation:

  1403   "Conv.rewr_conv"} which expects a meta-equation as an argument. Suppose we

  1384 

  1404   want to rewrite a @{ML_type cterm} according to the (meta)equation:

  1390   then we can use it in order to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}:

  1410   You can see how this function works with the example 

  1411   @{term "True \<and> (Foo \<longrightarrow> Bar)"}:

  1400   The function @{ML Conv.rewr_conv} only does rewriting on the outer-most

  1421   Note, however, that the function @{ML Conv.rewr_conv} only rewrites the 

  1401   level, otherwise it raises the exception @{ML CTERM}.

  1422   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match the 

  1423   left-hand side of the theorem, then  @{ML Conv.rewr_conv} raises 

  1424   the exception @{ML CTERM}.

  1410   val conv1 = Thm.beta_conversion true

  1433   val conv1 = Thm.beta_conversion false

  1412   val ctrm = Thm.capply (@{cterm \"\<lambda>x. x \<and> False\"}) (@{cterm \"True\"})

  1435   val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}

  1423   val conv = Conv.rewr_conv @{thm true_conj1} 

  1449   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv

  1424              else_conv Conv.all_conv

  1430 "(True \<and> Q \<equiv> Q, 

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

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

  1435   does not fail because the combinator @{ML else_conv} will then 

  1459   does not fail, however, because the combinator @{ML else_conv} will then 

  1436   try out @{ML Conv.all_conv}, which allways succeeds.

  1460   try out @{ML Conv.all_conv}, which always succeeds.

  1437 

  1461 

  1438   The combinator @{ML Conv.arg_conv} will apply the conversion on

  1462   Apart from the function @{ML beta_conversion in Thm}, which able to fully

  1439   the first argument, taht is the term must be of the form 

  1463   beta-normalise a term, the restriction of conversions so far is that they

  1440   @{ML "t1 $ t2" for t1 t2} and the conversion is applied to @{text t2}.

  1464   only apply to the outer-most level of a @{ML_type cterm}. In what follows we

  1441   For example

  1465   will lift this restriction. The combinator @{ML Conv.arg_conv} will apply

  1466   the conversion on the first argument of an application, that is the term

  1467   must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied

  1468   to @{text t2}.  For example

  1452   The reason for this behaviour is that @{text "(op \<or>)"} expects two arguments

  1479   The reason for this behaviour is that @{text "(op \<or>)"} expects two

  1453   and so is of the form @{text "Const \<dots> $ t1 $ t2"}. The conversion is then 

  1480   arguments.  So the term must be of the form @{text "Const \<dots> $ t1 $ t2"}. The

  1454   applied to @{text "t2"} which stands for @{term "True \<and> Q"}.

  1481   conversion is then applied to @{text "t2"} which in the example above

  1455 

  1482   stands for @{term "True \<and> Q"}.

  1456 *}

  1483 

  1457 

  1484   The function @{ML Conv.abs_conv} applies a conversion under an abstractions.

  1458 

  1485   For example:

  1459 text {*

  1486 

  1460   To begin with, let us assumes we want to simplify with the rewrite rule

  1487   @{ML_response_fake [display,gray]

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

  1488 "let 

  1462 *}

  1489   val conv = K (Conv.rewr_conv @{thm true_conj1}) 

  1463 

  1490   val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}

  1464 

  1491 in

  1465 ML{*fun all_true1_conv ctxt ct =

  1492   Conv.abs_conv conv @{context} ctrm

  1466   (case Thm.term_of ct of

  1493 end"

  1494   "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}

  1495   

  1496   The conversion that goes under an application is

  1497   @{ML Conv.combination_conv}. It expects two conversions, which each of them

  1498   is applied to the corresponding ``branch'' of the application. 

  1499 

  1500   We can now apply all these functions in a

  1501   conversion that recursively descends a term and applies a conversion in all

  1502   possible positions.

  1503 *}

  1504 

  1505 ML %linenosgray{*fun all_true1_conv ctxt ctrm =

  1506   case (Thm.term_of ctrm) of

  1469         Conv.rewr_conv @{thm true_conj1}) ct

  1509          Conv.rewr_conv @{thm true_conj1}) ctrm

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

  1510   | _ $ _ => Conv.combination_conv 

  1471       (all_true1_conv ctxt) ct

  1511                  (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm

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

  1512   | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm

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

  1513   | _ => Conv.all_conv ctrm*}

  1474 

  1514 

  1475 text {*

  1515 text {*

  1476   Here is this conversion in action:

  1516   This functions descends under applications (Line 6 and 7) and abstractions 

  1517   (Line 8); and ``fires'' if the outer-most constant is an @{text "True \<and> \<dots>"}

  1518   (Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this 

  1519   conversion in action, consider the following example.

  1520 

  1521 @{ML_response_fake [display,gray]

  1522 "let

  1523   val ctxt = @{context}

  1524   val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}

  1525 in

  1526   all_true1_conv ctxt ctrm

  1527 end"

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

  1529 

  1530   To see how much control you have about rewriting via conversions, let us 

  1531   make the task a bit more complicated by rewriting according to the rule

  1532   @{text true_conj1}, but only in the first arguments of @{term If}s. The 

  1533   the conversion should be as follows.

  1534 *}

  1535 

  1536 ML{*fun if_true1_conv ctxt ctrm =

  1537   case Thm.term_of ctrm of

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

  1539       Conv.arg_conv (all_true1_conv ctxt) ctrm

  1540   | _ $ _ => Conv.combination_conv 

  1541                         (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm

  1542   | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm

  1543   | _ => Conv.all_conv ctrm *}

  1544 

  1545 text {*

  1546   Here is an application of this conversion:

  1479   "all_true1_conv @{context}

  1549 "let

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

  1550   val ctxt = @{context}

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

  1551   val ctrm = 

  1482 

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

  1483   Now, let us make the task a bit more complicated by rewriting according to the rule

  1553 in

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

  1554   if_true1_conv ctxt ctrm

  1485 *}

  1555 end"

  1486 

  1556 "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 

  1487 ML{*fun if_true1_conv ctxt ct =

  1557 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}

  1488   (case Thm.term_of ct of

  1558 *}

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

  1559 

  1490       Conv.arg_conv (all_true1_conv ctxt) ct

  1560 text {*

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

  1561   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 

  1492       (if_true1_conv ctxt) ct

  1562   also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, 

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

  1563   consider @{ML all_true1_conv} and the lemma:

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

  1564 *}

  1495 

  1565 

  1496 text {*

  1566 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp

  1497   Here is an application of this conversion:

  1567 

  1568 text {*

  1569   Using the conversion you can transform this theorem into a new theorem

  1570   as follows

  1500   "if_true1_conv @{context}

  1573   "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}" 

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

  1574   "?P \<or> \<not> ?P"}

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

  1575 

  1503 *}

  1576   Finally, conversions can also be turned into tactics and then applied to

  1504 

  1577   goal states. This can be done with the help of the function @{ML CONVERSION},

  1505 text {*

  1578   and also some predefined conversion combinator which traverse a goal

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

  1579   state. The combinators for the goal state are: @{ML Conv.params_conv} for

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

  1580   going under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>

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

  1581   Q"}); the function @{ML Conv.prems_conv} for applying the conversion to all

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

  1582   premises of a goal, and @{ML Conv.concl_conv} for applying the conversion to

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

  1583   the conclusion of a goal.

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

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

  1513   the conclusion @{term Q}.

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

  1591   let 

  1592     val ctxt = ProofContext.init (Thm.theory_of_cterm goal)

  1523     CONVERSION (

  1594     CONVERSION 

  1524       Conv.params_conv ~1 (fn cx =>

  1595       (Conv.params_conv ~1 (fn ctxt =>

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

  1596         (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv

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

  1597           Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i

  1530   To demonstrate this tactic, consider the following example:

  1601   We call the conversions with the argument @{ML "~1"} in order to 

  1602   analyse all parameters, premises and conclusions. If we call it with 

  1603   a non-negative number, say @{text n}, then these conversions will 

  1604   only be called on @{text n} premises (similar for parameters and

  1605   conclusions). To test the tactic, consider the proof

  1537 txt {* \begin{minipage}{\textwidth}

  1612 txt {* where the tactic yields the goal state

  1613 

  1614        \begin{minipage}{\textwidth}

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

  1620   To sum up this section, conversions are not as powerful as the simplifier

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

  1621   and simprocs; the advantage of conversions, however, is that you never have

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

  1622   to worry about non-termination.

  1546   conversion @{ML all_true1_conv} again:

  1547 

  1548   @{ML_response_fake [display,gray]

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

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