1120   let 

  1120 let 

  1121     val thy = @{theory}

  1121   val thy = @{theory}

  1122     val pat = [@{term "Suc n"}]

  1122   val pat = [@{term "Suc n"}]

  1123   in

  1123 in

  1124     Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')

  1124   Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')

  1125   end*}

  1125 end*}

  1176   let

  1176 let

  1177     val thy = @{theory}

  1177   val thy = @{theory}

  1178     val pat = [@{term "Suc n"}] 

  1178   val pat = [@{term "Suc n"}] 

  1179   in

  1179 in

  1180     Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)

  1180   Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)

  1181   end*}

  1181 end*}

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

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

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

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

  1325   as follows:

  1325   acts on theorems. The type for conversions is

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

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

  1332   term to an instance of the reflexivity theorem, and 

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

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

  1333   the (meta)reflexivity theorem. For example:

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

  1336   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"

  1337   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}

  1338 

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

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

  1345   A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it 

  1346   produces an equation between a term and its beta-normal form. For example

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

  1349   "let

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

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

  1347 

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

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

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

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

  1353 in

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

  1355 end"

  1356   "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}

  1357 

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

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

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

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

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

  1363 

  1364   The argument @{ML true} in @{ML Thm.beta_conversion} indicates that 

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

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

  1367   For example

  1368 

  1369   @{ML_response_fake [display,gray]

  1370   "let

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

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

  1373 in

  1374   Thm.beta_conversion false (Thm.capply add two)

  1375 end"

  1376   "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"} 

  1377 

  1378   Again, we actually see as output only the fully normalised term 

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

  1380 

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

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

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

  1384 

  1354 text {*

  1389 text {* 

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

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

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

  1393 "let 

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

  1394   val ctrm =  @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}

  1360 *}

  1395 in

  1361 

  1396   Conv.rewr_conv @{thm true_conj1} ctrm

  1362 text {*

  1397 end"

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

  1398   "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}

  1364   conversion combinators:

  1399 

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

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

  1402 

  1403   This very primitive way of rewriting can be made more powerful by

  1404   combining several conversions into one. For this you can use conversion

  1405   combinators. The simplest conversion combinator is @{ML then_conv}, 

  1406   which applies one conversion after another. For example

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

  1409 "let

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

  1410   val conv1 = Thm.beta_conversion true

  1411   val conv2 = Conv.rewr_conv @{thm true_conj1}

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

  1413 in

  1414   (conv1 then_conv conv2) ctrm

  1415 end"

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

  1422 "let

  1373   @{cterm \"P \<or> (True \<and> Q)\"}"

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

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

  1424              else_conv Conv.all_conv

  1425   val ctrm1 = @{cterm \"True \<and> Q\"}

  1426   val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}

  1427 in

  1428   (conv ctrm1, conv ctrm2)

  1429 end"

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

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

  1432 

  1433   Here the conversion of @{thm [source] true_conj1} only applies

  1434   in the first case, but fails in the second. The whole conversion

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

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

  1437 

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

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

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

  1441   For example

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

  1444 "let 

  1378   @{cterm \"P \<or> (True \<and> Q)\"}"

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

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

  1446   val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}

  1380 

  1447 in

  1381   \begin{readmore}

  1448   Conv.arg_conv conv ctrm

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

  1449 end"

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

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

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

  1451 

  1385   \end{readmore}

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

  1386 

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

  1387   We will demonstrate this feature in the following example.

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

  1388 

  1455 

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

  1456 *}

  1457 

  1458 

  1459 text {*

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

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

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