960 \<close>

   960 \<close>

   961 

   961 

   962 lemma 

   962 lemma 

   963   shows "A \<Longrightarrow> True \<and> A"

   963   shows "A \<Longrightarrow> True \<and> A"

   964 apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}] 

   964 apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}] 

   966 txt \<open>\begin{minipage}{\textwidth}

   967 txt \<open>\begin{minipage}{\textwidth}

   967        @{subgoals [display]} 

   968        @{subgoals [display]} 

   968        \end{minipage}\<close>

   969        \end{minipage}\<close>

   969 (*<*)oops(*>*)

   970 (*<*)oops(*>*)

   970 

   971 

   974   Tactical}. For example the function @{ML foo_tac'} from

   975   Tactical}. For example the function @{ML foo_tac'} from

   975   page~\pageref{tac:footacprime} can also be written as:

   976   page~\pageref{tac:footacprime} can also be written as:

   976 \<close>

   977 \<close>

   977 

   978 

   978 ML %grayML\<open>fun foo_tac'' ctxt = 

   979 ML %grayML\<open>fun foo_tac'' ctxt = 

   981 

   985 

   982 text \<open>

   986 text \<open>

   983   There is even another way of implementing this tactic: in automatic proof

   987   There is even another way of implementing this tactic: in automatic proof

   984   procedures (in contrast to tactics that might be called by the user) there

   988   procedures (in contrast to tactics that might be called by the user) there

   985   are often long lists of tactics that are applied to the first

   989   are often long lists of tactics that are applied to the first

   986   subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>}, 

   990   subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>}, 

   987   you can also just write

   991   you can also just write

   988 \<close>

   992 \<close>

   989 

   993 

   990 ML %grayML\<open>fun foo_tac1 ctxt = 

   994 ML %grayML\<open>fun foo_tac1 ctxt = 

   993 

  1000 

   994 text \<open>

  1001 text \<open>

   995   and call @{ML foo_tac1}.  

  1002   and call @{ML foo_tac1}.  

   996 

  1003 

   997   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1 in Tactical} it must be

  1004   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1 in Tactical} it must be

  1071   list. The same can be achieved with the tactic combinator @{ML_ind  TRY in Tactical}.

  1078   list. The same can be achieved with the tactic combinator @{ML_ind  TRY in Tactical}.

  1072   For example:

  1079   For example:

  1073 \<close>

  1080 \<close>

  1074 

  1081 

  1075 ML %grayML\<open>fun select_tac'' ctxt = 

  1082 ML %grayML\<open>fun select_tac'' ctxt = 

  1078 text_raw\<open>\label{tac:selectprimeprime}\<close>

  1087 text_raw\<open>\label{tac:selectprimeprime}\<close>

  1079 

  1088 

  1080 text \<open>

  1089 text \<open>

  1081   This tactic behaves in the same way as @{ML select_tac'}: it tries out

  1090   This tactic behaves in the same way as @{ML select_tac'}: it tries out

  1082   one of the given tactics and if none applies leaves the goal state 

  1091   one of the given tactics and if none applies leaves the goal state 

  1470   you can see it contains nothing. This simpset is usually not useful, except as a 

  1479   you can see it contains nothing. This simpset is usually not useful, except as a 

  1471   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 

  1480   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 

  1472   the simplification rule @{thm [source] Diff_Int} as follows:

  1481   the simplification rule @{thm [source] Diff_Int} as follows:

  1473 \<close>

  1482 \<close>

  1474 

  1483 

  1476 

  1486 

  1477 thm "INF_cong"

  1487 thm "INF_cong"

  1478 text \<open>

  1488 text \<open>

  1479   Printing then out the components of the simpset gives:

  1489   Printing then out the components of the simpset gives:

  1480 

  1490 

  1488   \footnote{\bf FIXME: Why does it print out ??.unknown}

  1498   \footnote{\bf FIXME: Why does it print out ??.unknown}

  1489 

  1499 

  1490   Adding also the congruence rule @{thm [source] INF_cong} 

  1500   Adding also the congruence rule @{thm [source] INF_cong} 

  1491 \<close>

  1501 \<close>

  1492 

  1502 

  1494 

  1505 

  1495 text \<open>

  1506 text \<open>

  1496   gives

  1507   gives

  1497 

  1508 

  1498   @{ML_response [display,gray]

  1509   @{ML_response [display,gray]

  1499   \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>

  1510   \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>

  1500 \<open>Simplification rules:

  1511 \<open>Simplification rules:

  1501   ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)

  1512   ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)

  1502 Congruences rules:

  1513 Congruences rules:

  1503   Complete_Lattices.Inf_class.Inf: 

  1514   Complete_Lattices.Inf_class.Inf: 

  1505 Simproc patterns:\<close>}

  1517 Simproc patterns:\<close>}

  1506 

  1518 

  1507   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 

  1519   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 

  1508   expects this form of the simplification and congruence rules. This is

  1520   expects this form of the simplification and congruence rules. This is

  1509   different, if we use for example the simpset @{ML HOL_basic_ss} (see below), 

  1521   different, if we use for example the simpset @{ML HOL_basic_ss} (see below),