1027 as follows: |
1027 as follows: |
1028 \<close> |
1028 \<close> |
1029 |
1029 |
1030 ML %grayML\<open>fun select_tac' ctxt = |
1030 ML %grayML\<open>fun select_tac' ctxt = |
1031 FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], |
1031 FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], |
1032 resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close> |
1032 resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], |
|
1033 K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close> |
1033 |
1034 |
1034 text \<open> |
1035 text \<open> |
1035 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
1036 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
1036 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
1037 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
1037 fail if no theorem applies (we also have to wrap @{ML all_tac} using the |
1038 fail if no theorem applies (we also have to wrap @{ML all_tac} using the |
1471 the simplification rule @{thm [source] Diff_Int} as follows: |
1472 the simplification rule @{thm [source] Diff_Int} as follows: |
1472 \<close> |
1473 \<close> |
1473 |
1474 |
1474 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close> |
1475 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close> |
1475 |
1476 |
|
1477 thm "INF_cong" |
1476 text \<open> |
1478 text \<open> |
1477 Printing then out the components of the simpset gives: |
1479 Printing then out the components of the simpset gives: |
1478 |
1480 |
1479 @{ML_response [display,gray] |
1481 @{ML_response [display,gray] |
1480 \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close> |
1482 \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close> |
1483 Congruences rules: |
1485 Congruences rules: |
1484 Simproc patterns:\<close>} |
1486 Simproc patterns:\<close>} |
1485 |
1487 |
1486 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1488 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1487 |
1489 |
1488 Adding also the congruence rule @{thm [source] strong_INF_cong} |
1490 Adding also the congruence rule @{thm [source] INF_cong} |
1489 \<close> |
1491 \<close> |
1490 |
1492 |
1491 ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close> |
1493 ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close> |
1492 |
1494 |
1493 text \<open> |
1495 text \<open> |
1494 gives |
1496 gives |
1495 |
1497 |
1496 @{ML_response [display,gray] |
1498 @{ML_response [display,gray] |
1497 \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close> |
1499 \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close> |
1498 \<open>Simplification rules: |
1500 \<open>Simplification rules: |
1499 ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1) |
1501 ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1) |
1500 Congruences rules: |
1502 Congruences rules: |
1501 Complete_Lattices.Inf_class.Inf: |
1503 Complete_Lattices.Inf_class.Inf: |
1502 \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1 |
1504 \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1) |
1503 Simproc patterns:\<close>} |
1505 Simproc patterns:\<close>} |
1504 |
1506 |
1505 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1507 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1506 expects this form of the simplification and congruence rules. This is |
1508 expects this form of the simplification and congruence rules. This is |
1507 different, if we use for example the simpset @{ML HOL_basic_ss} (see below), |
1509 different, if we use for example the simpset @{ML HOL_basic_ss} (see below), |