1013 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1013 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1014 \end{readmore} |
1014 \end{readmore} |
1015 |
1015 |
1016 *} |
1016 *} |
1017 |
1017 |
1018 section {* Simplifier Tactics *} |
1018 section {* Simplifier Tactics (TBD) *} |
1019 |
1019 |
1020 text {* |
1020 text {* |
1021 A lot of convenience in the reasoning with Isabelle derives from its |
1021 A lot of convenience in the reasoning with Isabelle derives from its |
1022 powerful simplifier. There are the following five main tactics behind |
1022 powerful simplifier. There are the following five main tactics behind |
1023 the simplifier (in parentheses is their userlevel counterpart) |
1023 the simplifier (in parentheses is their userlevel counterpart) |
1061 able to rewrite according to rules that have precoditions. The rewriting |
1061 able to rewrite according to rules that have precoditions. The rewriting |
1062 inside terms requires congruence rules which are meta-equalities |
1062 inside terms requires congruence rules which are meta-equalities |
1063 typical of the form |
1063 typical of the form |
1064 |
1064 |
1065 \begin{isabelle} |
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"}}} |
1066 \mbox{\inferrule{@{text "t\<^isub>i \<equiv> s\<^isub>i"}} |
|
1067 {@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}} |
1067 \end{isabelle} |
1068 \end{isabelle} |
1068 |
1069 |
1069 with @{text "constr"} being a term-constructor. However there are also more complicated |
1070 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 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 attribute @{text "[cong]"} (theses lemmas are usually equations that are internally |
1087 \end{isabelle} |
1088 \end{isabelle} |
1088 |
1089 |
1089 The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}. |
1090 The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}. |
1090 *} |
1091 *} |
1091 |
1092 |
|
1093 ML {* warning (Pretty.string_of (MetaSimplifier.pretty_ss HOL_ss)) *} |
|
1094 |
|
1095 ML {* |
|
1096 fun get_parts ss = |
|
1097 let |
|
1098 val ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = MetaSimplifier.rep_ss ss |
|
1099 in |
|
1100 (rules, congs, procs, loop_tacs, solvers) |
|
1101 end |
|
1102 *} |
|
1103 |
|
1104 ML {* |
|
1105 Pretty.big_list |
|
1106 *} |
|
1107 |
|
1108 |
|
1109 ML {* |
|
1110 fun print_ss ss = |
|
1111 let |
|
1112 val pretty_thms = map (enclose " " "\n" o Display.string_of_thm) |
|
1113 |
|
1114 fun pretty_cong (name, {thm, lhs}) = |
|
1115 name ^ ":" ^ (Display.string_of_thm thm); |
|
1116 |
|
1117 val (rules, congs, procs, loop_tacs, solvers) = get_parts ss; |
|
1118 val smps = map #thm (Net.entries rules); |
|
1119 |
|
1120 in |
|
1121 "simplification rules:\n" ^ |
|
1122 (implode (pretty_thms smps)) ^ |
|
1123 "congruences:" ^ (commas (map pretty_cong (fst congs))) ^ "\n" ^ |
|
1124 "loopers:" ^ (commas (map (quote o fst) loop_tacs)) |
|
1125 end; |
|
1126 *} |
|
1127 |
|
1128 thm FalseE |
|
1129 |
|
1130 thm simp_impliesI |
|
1131 lemma "P (Suc 0) \<Longrightarrow> P ?x" |
|
1132 apply(tactic {* CHANGED (simp_tac HOL_basic_ss 1) *}) |
|
1133 oops |
|
1134 |
|
1135 ML {* warning (print_ss HOL_ss) *} |
|
1136 |
|
1137 text {* |
|
1138 @{ML HOL_basic_ss} can deal essentially only with goals of the form: |
|
1139 @{thm TrueI}, @{thm refl[no_vars]} @{term "x \<equiv> x"} and @{thm FalseE}, |
|
1140 and resolve with assumptions. |
|
1141 *} |
|
1142 |
|
1143 ML {* setsubgoaler *} |
|
1144 |
1092 text {* |
1145 text {* |
1093 (FIXME: what do the simplifier tactics do when nothing can be rewritten) |
1146 (FIXME: what do the simplifier tactics do when nothing can be rewritten) |
1094 |
1147 |
1095 |
1148 |
1096 (FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac}, |
1149 (FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac}, |