equal
deleted
inserted
replaced
1015 |
1015 |
1016 section {* Simplifier Tactics *} |
1016 section {* Simplifier Tactics *} |
1017 |
1017 |
1018 text {* |
1018 text {* |
1019 A lot of convenience in the reasoning with Isabelle derives from its |
1019 A lot of convenience in the reasoning with Isabelle derives from its |
1020 powerful simplifier. The power of simplifier is a strength and a weakness at |
1020 powerful simplifier. The power of the simplifier is a strength and a weakness at |
1021 the same time, because you can easily make the simplifier to run into a loop and its |
1021 the same time, because you can easily make the simplifier run into a loop and |
|
1022 in general its |
1022 behaviour can be difficult to predict. There is also a multitude |
1023 behaviour can be difficult to predict. There is also a multitude |
1023 of options that you can configure to control the behaviour of the simplifier. |
1024 of options that you can configure to control the behaviour of the simplifier. |
1024 We describe some of them in this and the next section. |
1025 We describe some of them in this and the next section. |
1025 |
1026 |
1026 There are the following five main tactics behind |
1027 There are the following five main tactics behind |
1088 equations, which are then internally transformed into meta-equations. |
1089 equations, which are then internally transformed into meta-equations. |
1089 |
1090 |
1090 |
1091 |
1091 The rewriting with rules involving preconditions requires what is in |
1092 The rewriting with rules involving preconditions requires what is in |
1092 Isabelle called a subgoaler, a solver and a looper. These can be arbitrary |
1093 Isabelle called a subgoaler, a solver and a looper. These can be arbitrary |
1093 tactics that can be installed in a simpset and which are called during |
1094 tactics that can be installed in a simpset and which are called at |
1094 various stages during simplification. However, simpsets also include |
1095 various stages during simplification. However, simpsets also include |
1095 simprocs, which can produce rewrite rules on demand (see next |
1096 simprocs, which can produce rewrite rules on demand (see next |
1096 section). Another component are split-rules, which can simplify for example |
1097 section). Another component are split-rules, which can simplify for example |
1097 the ``then'' and ``else'' branches of if-statements under the corresponding |
1098 the ``then'' and ``else'' branches of if-statements under the corresponding |
1098 preconditions. |
1099 preconditions. |
1415 THEN' simp_tac (HOL_basic_ss addsimps thms3) |
1416 THEN' simp_tac (HOL_basic_ss addsimps thms3) |
1416 end*} |
1417 end*} |
1417 |
1418 |
1418 text {* |
1419 text {* |
1419 For all three phases we have to build simpsets adding specific lemmas. As is sufficient |
1420 For all three phases we have to build simpsets adding specific lemmas. As is sufficient |
1420 for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain |
1421 for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain |
1421 the desired results. Now we can solve the following lemma |
1422 the desired results. Now we can solve the following lemma |
1422 *} |
1423 *} |
1423 |
1424 |
1424 lemma |
1425 lemma |
1425 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm" |
1426 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm" |
1481 |
1482 |
1482 simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *} |
1483 simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *} |
1483 |
1484 |
1484 text {* |
1485 text {* |
1485 where the second argument specifies the pattern and the right-hand side |
1486 where the second argument specifies the pattern and the right-hand side |
1486 contains the code of the simproc (we have to use @{ML K} since we ignoring |
1487 contains the code of the simproc (we have to use @{ML K} since we are ignoring |
1487 an argument about morphisms. |
1488 an argument about morphisms. |
1488 After this, the simplifier is aware of the simproc and you can test whether |
1489 After this, the simplifier is aware of the simproc and you can test whether |
1489 it fires on the lemma: |
1490 it fires on the lemma: |
1490 *} |
1491 *} |
1491 |
1492 |
1636 the default simpset contains a rule which just does the opposite of @{ML plus_one_sp}, |
1637 the default simpset contains a rule which just does the opposite of @{ML plus_one_sp}, |
1637 namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful |
1638 namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful |
1638 in choosing the right simpset to which you add a simproc. |
1639 in choosing the right simpset to which you add a simproc. |
1639 |
1640 |
1640 Next let us implement a simproc that replaces terms of the form @{term "Suc n"} |
1641 Next let us implement a simproc that replaces terms of the form @{term "Suc n"} |
1641 with the number @{text n} increase by one. First we implement a function that |
1642 with the number @{text n} increased by one. First we implement a function that |
1642 takes a term and produces the corresponding integer value. |
1643 takes a term and produces the corresponding integer value. |
1643 *} |
1644 *} |
1644 |
1645 |
1645 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t |
1646 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t |
1646 | dest_suc_trm t = snd (HOLogic.dest_number t)*} |
1647 | dest_suc_trm t = snd (HOLogic.dest_number t)*} |