1021   @{ML rewrite_goals_tac}

  1021   A lot of convenience in the reasoning with Isabelle derives from its

  1022   powerful simplifier. There are the following five main tactics behind 

  1023   the simplifier (in parentheses is their userlevel counterpart)

  1024 

  1025   \begin{isabelle}

  1026   \begin{tabular}{l@ {\hspace{2cm}}l}

  1027    @{ML simp_tac}            & @{text "(simp (no_asm))"} \\

  1028    @{ML asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\

  1029    @{ML full_simp_tac}       & @{text "(simp (no_asm_use))"} \\

  1030    @{ML asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\

  1031    @{ML asm_full_simp_tac}   & @{text "(simp)"}

  1032   \end{tabular}

  1033   \end{isabelle}

  1034 

  1035   All of them take a simpset and an interger as argument (the latter to specify the goal 

  1036   to be analysed). So the proof

  1037 *}

  1038 

  1039 lemma "Suc (1 + 2) < 3 + 2"

  1040 apply(simp)

  1041 done

  1042 

  1043 text {*

  1044   corrsponds on the ML-level to the tactic

  1045 *}

  1046 

  1047 lemma "Suc (1 + 2) < 3 + 2"

  1048 apply(tactic {* asm_full_simp_tac @{simpset} 1 *})

  1049 done

  1050 

  1051 thm imp_cong simp_implies_cong

  1052 

  1053 text {*

  1054   The crucial information the developer has to control is the simpset

  1055   to be used by the simplifier. If not handled with care, then the 

  1056   simplifier can easily run forever. 

  1057 

  1058   It might be surprising that a simpset is quite more complex than just

  1059   a simple list of theorems. One reason for the complexity is that the

  1060   simplifier must be able to rewrite inside terms and should also be

  1061   able to rewrite according to rules that have precoditions. The rewriting

  1062   inside terms requires congruence rules which are meta-equalities 

  1063   typical of the form

  1064 

  1065   \begin{isabelle}

  1066   \mbox{\inferrule{@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}}

  1067   \end{isabelle}

  1068 

  1069   with @{text "constr"} being a term-constructor. However there are also more complicated 

  1070   congruence rules. The user can declare lemmas to be congruence rules using the 

  1071   attribute @{text "[cong]"} (theses lemmas are usually equations that are internally 

  1072   transformed into meta-equations (FIXME: check that).

  1023   @{ML ObjectLogic.full_atomize_tac}

  1074   The rewriting with rules involving preconditions requires solvers. However

  1024   

  1075   there are also simprocs, which can produce rewrite rules on demand (see 

  1025   @{ML ObjectLogic.rulify_tac}

  1076   next section). Another component are split rules, which can simplify for example

  1077   the then and else branches of if-statements under the corresponding 

  1078   precoditions. (FIXME: loopers and subgoalers?)

  1079 

  1080   The most common combinators to modify simpsets are

  1081 

  1082   \begin{isabelle}

  1083   \begin{tabular}{ll}

  1084   @{ML addsimps} & @{ML delsimps}\\

  1085   @{ML addcongs} & @{ML delcongs}\\

  1086   \end{tabular}

  1087   \end{isabelle}

  1088 

  1089   The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}.

  1090 *}

  1091 

  1092 text {*

  1093   (FIXME: what do the simplifier tactics do when nothing can be rewritten)

  1094 

  1095 

  1096   (FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac}, 

  1097   @{ML ObjectLogic.rulify_tac})

  1098 

  1099 

  1100   \begin{readmore}

  1101   For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}

  1102   and @{ML_file "Pure/simplifier.ML"}.

  1103   \end{readmore}

  1635   Write a tactic that is based on conversions which does the same as the simproc in

  1713   Write a tactic that does the same as the simproc in exercise

  1636   exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} 

  1714   \ref{ex:addsimproc}, but is based in conversions. That means replace terms

  1637   by their result. You can make the same assumptions as in \ref{ex:addsimproc}.

  1715   of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make

  1716   the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution

  1717   requires some additional functions.

  1718   \end{exercise}

  1719 

  1720   \begin{exercise}

  1721   Compare which way of rewriting such terms is more efficient. For this

  1722   you might have to construct quite large terms.

  1651 section {* Structured Proofs *}

  1736 section {* Structured Proofs (TBD) *}