477 |
476 |
478 then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but |
477 then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but |
479 takes an additional number as argument that makes explicit which premise |
478 takes an additional number as argument that makes explicit which premise |
480 should be instantiated. |
479 should be instantiated. |
481 |
480 |
482 To improve readability of the theorems we produce below, we shall use |
481 To improve readability of the theorems we produce below, we shall use the |
483 the following function |
482 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms |
484 *} |
483 schematic variables into free ones. Using this function for the first @{ML |
485 |
484 RS}-expression above produces the more readable result: |
486 ML{*fun no_vars ctxt thm = |
|
487 let |
|
488 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt |
|
489 in |
|
490 thm' |
|
491 end*} |
|
492 |
|
493 text {* |
|
494 that transform the schematic variables of a theorem into free variables. |
|
495 Using this function for the first @{ML RS}-expression above would produce |
|
496 the more readable result: |
|
497 |
485 |
498 @{ML_response_fake [display,gray] |
486 @{ML_response_fake [display,gray] |
499 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"} |
487 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"} |
500 |
488 |
501 If you want to instantiate more than one premise of a theorem, you can use |
489 If you want to instantiate more than one premise of a theorem, you can use |
1016 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1004 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1017 \end{readmore} |
1005 \end{readmore} |
1018 |
1006 |
1019 *} |
1007 *} |
1020 |
1008 |
1021 section {* Simplifier Tactics (TBD) *} |
1009 section {* Simplifier Tactics *} |
1022 |
1010 |
1023 text {* |
1011 text {* |
1024 A lot of convenience in the reasoning with Isabelle derives from its |
1012 A lot of convenience in the reasoning with Isabelle derives from its |
1025 powerful simplifier. The power of simplifier is at the same time a |
1013 powerful simplifier. The power of simplifier is at the same time a |
1026 strength and a weakness, because you can easily make the simplifier to |
1014 strength and a weakness, because you can easily make the simplifier to |
1186 Printing out the components of this simpset gives: |
1174 Printing out the components of this simpset gives: |
1187 |
1175 |
1188 @{ML_response_fake [display,gray] |
1176 @{ML_response_fake [display,gray] |
1189 "print_parts @{context} ss1" |
1177 "print_parts @{context} ss1" |
1190 "Simplification rules: |
1178 "Simplification rules: |
1191 ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1) |
1179 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C) |
1192 Congruences rules:"} |
1180 Congruences rules:"} |
|
1181 |
|
1182 (FIXME: Why does it print out ??.unknown) |
1193 |
1183 |
1194 Adding the congruence rule @{thm [source] UN_cong} |
1184 Adding the congruence rule @{thm [source] UN_cong} |
1195 *} |
1185 *} |
1196 |
1186 |
1197 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *} |
1187 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *} |
1200 gives |
1190 gives |
1201 |
1191 |
1202 @{ML_response_fake [display,gray] |
1192 @{ML_response_fake [display,gray] |
1203 "print_parts @{context} ss2" |
1193 "print_parts @{context} ss2" |
1204 "Simplification rules: |
1194 "Simplification rules: |
1205 ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1) |
1195 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C) |
1206 Congruences rules: |
1196 Congruences rules: |
1207 UNION: \<lbrakk>?A1 = ?B1; \<And>x. x \<in> ?B1 \<Longrightarrow> ?C1 x = ?D1 x\<rbrakk> \<Longrightarrow> |
1197 UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"} |
1208 \<Union>x\<in>?A1. ?C1 x \<equiv> \<Union>x\<in>?B1. ?D1 x"} |
|
1209 |
1198 |
1210 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1199 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1211 expects this form of the simplification and congruence rules. However, even |
1200 expects this form of the simplification and congruence rules. However, even |
1212 adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. |
1201 adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. |
1213 |
1202 |
1238 already many useful simplification rules for the logical connectives in HOL. |
1227 already many useful simplification rules for the logical connectives in HOL. |
1239 |
1228 |
1240 @{ML_response_fake [display,gray] |
1229 @{ML_response_fake [display,gray] |
1241 "print_parts @{context} HOL_ss" |
1230 "print_parts @{context} HOL_ss" |
1242 "Simplification rules: |
1231 "Simplification rules: |
1243 Pure.triv_forall_equality: (\<And>x. PROP ?V) \<equiv> PROP ?V |
1232 Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V |
1244 HOL.the_eq_trivial: THE x. x = ?y \<equiv> ?y |
1233 HOL.the_eq_trivial: THE x. x = y \<equiv> y |
1245 HOL.the_sym_eq_trivial: THE y. ?y = y \<equiv> ?y |
1234 HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y |
1246 \<dots> |
1235 \<dots> |
1247 Congruences rules: |
1236 Congruences rules: |
1248 HOL.simp_implies: \<dots> |
1237 HOL.simp_implies: \<dots> |
1249 \<Longrightarrow> (PROP ?P =simp=> PROP ?Q) \<equiv> (PROP ?P' =simp=> PROP ?Q') |
1238 \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q') |
1250 op -->: \<lbrakk>?P \<equiv> ?P'; ?P' \<Longrightarrow> ?Q \<equiv> ?Q'\<rbrakk> \<Longrightarrow> ?P \<longrightarrow> ?Q \<equiv> ?P' \<longrightarrow> ?Q'"} |
1239 op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"} |
1251 |
1240 |
1252 |
1241 |
1253 The main point of these simpsets is that they are small enough to |
1242 The main point of these simpsets is that they are small enough to |
1254 not cause any loops with most of the simplification rules that |
1243 not cause any loops with most of the simplification rules that |
1255 you might like to add. |
1244 you might like to add. |