1 theory Tactical

     1 theory Tactical

     2 imports Base First_Steps

     2 imports Base First_Steps

     3 begin

     3 begin

    12 

     4 

    13 chapter {* Tactical Reasoning\label{chp:tactical} *}

     5 chapter {* Tactical Reasoning\label{chp:tactical} *}

    14 

     6 

    15 text {*

     7 text {*

    16    \begin{flushright}

     8    \begin{flushright}

   102   the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 

    94   the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 

   103   Consider the following sequence of tactics

    95   Consider the following sequence of tactics

   104 

    96 

   105 *}

    97 *}

   106 

    98 

   108       (etac @{thm disjE} 1

   100       (etac @{thm disjE} 1

   109        THEN rtac @{thm disjI2} 1

   101        THEN rtac @{thm disjI2} 1

   110        THEN atac 1

   102        THEN atac 1

   111        THEN rtac @{thm disjI1} 1

   103        THEN rtac @{thm disjI1} 1

   112        THEN atac 1)*}

   104        THEN atac 1)*}

   131   tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding

   123   tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding

   132   of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, 

   124   of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, 

   133   you can write

   125   you can write

   134 *}

   126 *}

   135 

   127 

   137       (etac @{thm disjE} 

   129       (etac @{thm disjE} 

   138        THEN' rtac @{thm disjI2} 

   130        THEN' rtac @{thm disjI2} 

   139        THEN' atac 

   131        THEN' atac 

   140        THEN' rtac @{thm disjI1} 

   132        THEN' rtac @{thm disjI1} 

   141        THEN' atac)*}text_raw{*\label{tac:footacprime}*}

   133        THEN' atac)*}text_raw{*\label{tac:footacprime}*}

   175   This means they failed. The reason for this error message is that tactics

   167   This means they failed. The reason for this error message is that tactics

   176   are functions mapping a goal state to a (lazy) sequence of successor

   168   are functions mapping a goal state to a (lazy) sequence of successor

   177   states. Hence the type of a tactic is:

   169   states. Hence the type of a tactic is:

   178 *}

   170 *}

   179   

   171   

   181 

   173 

   182 text {*

   174 text {*

   183   By convention, if a tactic fails, then it should return the empty sequence. 

   175   By convention, if a tactic fails, then it should return the empty sequence. 

   184   Therefore, if you write your own tactics, they  should not raise exceptions 

   176   Therefore, if you write your own tactics, they  should not raise exceptions 

   185   willy-nilly; only in very grave failure situations should a tactic raise the 

   177   willy-nilly; only in very grave failure situations should a tactic raise the 

   188   The simplest tactics are @{ML_ind no_tac in Tactical} and 

   180   The simplest tactics are @{ML_ind no_tac in Tactical} and 

   189   @{ML_ind all_tac in Tactical}. The first returns the empty sequence and 

   181   @{ML_ind all_tac in Tactical}. The first returns the empty sequence and 

   190   is defined as

   182   is defined as

   191 *}

   183 *}

   192 

   184 

   194 

   186 

   195 text {*

   187 text {*

   196   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 

   188   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 

   197   in a single member sequence; it is defined as

   189   in a single member sequence; it is defined as

   198 *}

   190 *}

   199 

   191 

   201 

   193 

   202 text {*

   194 text {*

   203   which means @{ML all_tac} always succeeds, but also does not make any progress 

   195   which means @{ML all_tac} always succeeds, but also does not make any progress 

   204   with the proof.

   196   with the proof.

   205 

   197 

   235   goal state is indeed a theorem. To shed more light on this,

   227   goal state is indeed a theorem. To shed more light on this,

   236   let us modify the code of @{ML all_tac} to obtain the following

   228   let us modify the code of @{ML all_tac} to obtain the following

   237   tactic

   229   tactic

   238 *}

   230 *}

   239 

   231 

   241 let

   233 let

   242   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))

   234   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))

   243 in 

   235 in 

   244   Seq.single thm

   236   Seq.single thm

   245 end*}

   237 end*}

   471   expects a list of theorems as argument. From this list it will apply the

   463   expects a list of theorems as argument. From this list it will apply the

   472   first applicable theorem (later theorems that are also applicable can be

   464   first applicable theorem (later theorems that are also applicable can be

   473   explored via the lazy sequences mechanism). Given the code

   465   explored via the lazy sequences mechanism). Given the code

   474 *}

   466 *}

   475 

   467 

   477 

   469 

   478 text {*

   470 text {*

   479   an example for @{ML resolve_tac} is the following proof where first an outermost 

   471   an example for @{ML resolve_tac} is the following proof where first an outermost 

   480   implication is analysed and then an outermost conjunction.

   472   implication is analysed and then an outermost conjunction.

   481 *}

   473 *}

   527 \begin{figure}[t]

   519 \begin{figure}[t]

   528 \begin{minipage}{\textwidth}

   520 \begin{minipage}{\textwidth}

   529 \begin{isabelle}

   521 \begin{isabelle}

   530 *}

   522 *}

   531 

   523 

   533 let 

   525 let 

   534   fun assgn1 f1 f2 xs =

   526   fun assgn1 f1 f2 xs =

   535     Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 

   527     Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 

   536 

   528 

   537   fun assgn2 f xs = assgn1 f f xs 

   529   fun assgn2 f xs = assgn1 f f xs 

   618   the arguments @{text "asms"} and @{text "prems"}, respectively. This 

   610   the arguments @{text "asms"} and @{text "prems"}, respectively. This 

   619   means we can apply them using the usual assumption tactics. With this you can 

   611   means we can apply them using the usual assumption tactics. With this you can 

   620   for example easily implement a tactic that behaves almost like @{ML atac}:

   612   for example easily implement a tactic that behaves almost like @{ML atac}:

   621 *}

   613 *}

   622 

   614 

   624 

   616 

   625 text {*

   617 text {*

   626   If you apply @{ML atac'} to the next lemma

   618   If you apply @{ML atac'} to the next lemma

   627 *}

   619 *}

   628 

   620 

   980   one specified subgoal, you can use the combinator @{ML_ind EVERY' in

   972   one specified subgoal, you can use the combinator @{ML_ind EVERY' in

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

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

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

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

   983 *}

   975 *}

   984 

   976 

   986                         atac, rtac @{thm disjI1}, atac]*}

   978                         atac, rtac @{thm disjI1}, atac]*}

   987 

   979 

   988 text {*

   980 text {*

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

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

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

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

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

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

   992   subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"}, 

   984   subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"}, 

   993   you can also just write

   985   you can also just write

   994 *}

   986 *}

   995 

   987 

   997                        atac, rtac @{thm disjI1}, atac]*}

   989                        atac, rtac @{thm disjI1}, atac]*}

   998 

   990 

   999 text {*

   991 text {*

  1000   and call @{ML foo_tac1}.  

   992   and call @{ML foo_tac1}.  

  1001 

   993 

  1005   then you can use the combinator @{ML_ind  ORELSE' in Tactical} for two tactics, and @{ML_ind

   997   then you can use the combinator @{ML_ind  ORELSE' in Tactical} for two tactics, and @{ML_ind

  1006    FIRST' in Tactical} (or @{ML_ind  FIRST1 in Tactical}) for a list of tactics. For example, the tactic

   998    FIRST' in Tactical} (or @{ML_ind  FIRST1 in Tactical}) for a list of tactics. For example, the tactic

  1007 

   999 

  1008 *}

  1000 *}

  1009 

  1001 

  1011 

  1003 

  1012 text {*

  1004 text {*

  1013   will first try out whether theorem @{text disjI} applies and in case of failure 

  1005   will first try out whether theorem @{text disjI} applies and in case of failure 

  1014   will try @{text conjI}. To see this consider the proof

  1006   will try @{text conjI}. To see this consider the proof

  1015 *}

  1007 *}

  1029 text {*

  1021 text {*

  1030   Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} 

  1022   Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} 

  1031   as follows:

  1023   as follows:

  1032 *}

  1024 *}

  1033 

  1025 

  1035                           rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}

  1027                           rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}

  1036 

  1028 

  1037 text {*

  1029 text {*

  1038   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 

  1030   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 

  1039   we must include @{ML all_tac} at the end of the list, otherwise the tactic will

  1031   we must include @{ML all_tac} at the end of the list, otherwise the tactic will

  1072   always  succeeds by fact of having @{ML all_tac} at the end of the tactic

  1064   always  succeeds by fact of having @{ML all_tac} at the end of the tactic

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

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

  1074   For example:

  1066   For example:

  1075 *}

  1067 *}

  1076 

  1068 

  1078                                  rtac @{thm notI}, rtac @{thm allI}]*}

  1070                                  rtac @{thm notI}, rtac @{thm allI}]*}

  1079 text_raw{*\label{tac:selectprimeprime}*}

  1071 text_raw{*\label{tac:selectprimeprime}*}

  1080 

  1072 

  1081 text {*

  1073 text {*

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

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

  1125   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 

  1117   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 

  1126   completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example 

  1118   completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example 

  1127   suppose the following tactic

  1119   suppose the following tactic

  1128 *}

  1120 *}

  1129 

  1121 

  1131 

  1123 

  1132 text {* which applied to the proof *}

  1124 text {* which applied to the proof *}

  1133 

  1125 

  1134 lemma 

  1126 lemma 

  1135   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"

  1127   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"

  1149 

  1141 

  1150   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 

  1142   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 

  1151   can implement it as

  1143   can implement it as

  1152 *}

  1144 *}

  1153 

  1145 

  1155 

  1147 

  1156 text {*

  1148 text {*

  1157   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.

  1149   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.

  1158 

  1150 

  1159   If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}

  1151   If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}

  1162   is applied repeatedly only to the first subgoal. To analyse also all

  1154   is applied repeatedly only to the first subgoal. To analyse also all

  1163   resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW in Tactical}. 

  1155   resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW in Tactical}. 

  1164   Supposing the tactic

  1156   Supposing the tactic

  1165 *}

  1157 *}

  1166 

  1158 

  1168 

  1160 

  1169 text {* 

  1161 text {* 

  1170   you can see that the following goal

  1162   you can see that the following goal

  1171 *}

  1163 *}

  1172 

  1164 

  1428 

  1420 

  1429 text_raw {*

  1421 text_raw {*

  1430 \begin{figure}[t]

  1422 \begin{figure}[t]

  1431 \begin{minipage}{\textwidth}

  1423 \begin{minipage}{\textwidth}

  1432 \begin{isabelle}*}

  1424 \begin{isabelle}*}

  1434 let

  1426 let

  1435   val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss

  1427   val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss

  1436 

  1428 

  1437   fun name_thm (nm, thm) =

  1429   fun name_thm (nm, thm) =

  1438     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]

  1430     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]

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

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

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

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

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

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

  1472 *}

  1464 *}

  1473 

  1465 

  1475 

  1467 

  1476 text {*

  1468 text {*

  1477   Printing then out the components of the simpset gives:

  1469   Printing then out the components of the simpset gives:

  1478 

  1470 

  1479   @{ML_response_fake [display,gray]

  1471   @{ML_response_fake [display,gray]

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

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

  1487 

  1479 

  1488   Adding also the congruence rule @{thm [source] UN_cong} 

  1480   Adding also the congruence rule @{thm [source] UN_cong} 

  1489 *}

  1481 *}

  1490 

  1482 

  1492 

  1484 

  1493 text {*

  1485 text {*

  1494   gives

  1486   gives

  1495 

  1487 

  1496   @{ML_response_fake [display,gray]

  1488   @{ML_response_fake [display,gray]

  1845   want this, then you have to use a slightly different method for setting 

  1837   want this, then you have to use a slightly different method for setting 

  1846   up the simproc. First the function @{ML fail_simproc} needs to be modified

  1838   up the simproc. First the function @{ML fail_simproc} needs to be modified

  1847   to

  1839   to

  1848 *}

  1840 *}

  1849 

  1841 

  1851 let

  1843 let

  1852   val ctxt = Simplifier.the_context simpset

  1844   val ctxt = Simplifier.the_context simpset

  1853   val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex])

  1845   val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex])

  1854 in

  1846 in

  1855   NONE

  1847   NONE

  1861   We can turn this function into a proper simproc using the function 

  1853   We can turn this function into a proper simproc using the function 

  1862   @{ML Simplifier.simproc_global_i}:

  1854   @{ML Simplifier.simproc_global_i}:

  1863 *}

  1855 *}

  1864 

  1856 

  1865 

  1857 

  1867 let 

  1859 let 

  1868   val thy = @{theory}

  1860   val thy = @{theory}

  1869   val pat = [@{term "Suc n"}]

  1861   val pat = [@{term "Suc n"}]

  1870 in

  1862 in

  1871   Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')

  1863   Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')

  1909   the rewriting with simprocs, let us further assume we want that the simproc

  1901   the rewriting with simprocs, let us further assume we want that the simproc

  1910   only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write 

  1902   only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write 

  1911 *}

  1903 *}

  1912 

  1904 

  1913 

  1905 

  1915   case redex of

  1907   case redex of

  1916     @{term "Suc 0"} => NONE

  1908     @{term "Suc 0"} => NONE

  1917   | _ => SOME @{thm plus_one}*}

  1909   | _ => SOME @{thm plus_one}*}

  1918 

  1910 

  1919 text {*

  1911 text {*

  1920   and set up the simproc as follows.

  1912   and set up the simproc as follows.

  1921 *}

  1913 *}

  1922 

  1914 

  1924 let

  1916 let

  1925   val thy = @{theory}

  1917   val thy = @{theory}

  1926   val pat = [@{term "Suc n"}] 

  1918   val pat = [@{term "Suc n"}] 

  1927 in

  1919 in

  1928   Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)

  1920   Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)

  1956   Next let us implement a simproc that replaces terms of the form @{term "Suc n"}

  1948   Next let us implement a simproc that replaces terms of the form @{term "Suc n"}

  1957   with the number @{text n} increased by one. First we implement a function that

  1949   with the number @{text n} increased by one. First we implement a function that

  1958   takes a term and produces the corresponding integer value.

  1950   takes a term and produces the corresponding integer value.

  1959 *}

  1951 *}

  1960 

  1952 

  1962   | dest_suc_trm t = snd (HOLogic.dest_number t)*}

  1954   | dest_suc_trm t = snd (HOLogic.dest_number t)*}

  1963 

  1955 

  1964 text {* 

  1956 text {* 

  1965   It uses the library function @{ML_ind  dest_number in HOLogic} that transforms

  1957   It uses the library function @{ML_ind  dest_number in HOLogic} that transforms

  1966   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so

  1958   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so

  1986   arith_tac in Arith_Data} is fine, but there is also an alternative employing

  1978   arith_tac in Arith_Data} is fine, but there is also an alternative employing

  1987   the simplifier with a special simpset. For the kind of lemmas we

  1979   the simplifier with a special simpset. For the kind of lemmas we

  1988   want to prove here, the simpset @{text "num_ss"} should suffice.

  1980   want to prove here, the simpset @{text "num_ss"} should suffice.

  1989 *}

  1981 *}

  1990 

  1982 

  1992 let

  1984 let

  1993   val num = HOLogic.mk_number @{typ "nat"} n

  1985   val num = HOLogic.mk_number @{typ "nat"} n

  1994   val goal = Logic.mk_equals (t, num)

  1986   val goal = Logic.mk_equals (t, num)

  1995   val num_ss = HOL_ss addsimps @{thms semiring_norm}

  1987   val num_ss = HOL_ss addsimps @{thms semiring_norm}

  1996 in

  1988 in

  2010 

  2002 

  2011   Anyway, either version can be used in the function that produces the actual 

  2003   Anyway, either version can be used in the function that produces the actual 

  2012   theorem for the simproc.

  2004   theorem for the simproc.

  2013 *}

  2005 *}

  2014 

  2006 

  2016 let 

  2008 let 

  2017   val ctxt = Simplifier.the_context ss

  2009   val ctxt = Simplifier.the_context ss

  2018 in

  2010 in

  2019   SOME (get_thm_alt ctxt (t, dest_suc_trm t))

  2011   SOME (get_thm_alt ctxt (t, dest_suc_trm t))

  2020   handle TERM _ => NONE

  2012   handle TERM _ => NONE

  2025   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no

  2017   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no

  2026   theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc 

  2018   theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc 

  2027   on an example, you can set it up as follows:

  2019   on an example, you can set it up as follows:

  2028 *}

  2020 *}

  2029 

  2021 

  2031 let

  2023 let

  2032   val thy = @{theory}

  2024   val thy = @{theory}

  2033   val pat = [@{term "Suc n"}]

  2025   val pat = [@{term "Suc n"}]

  2034 in 

  2026 in 

  2035   Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) 

  2027   Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) 

  2072   The purpose of conversions is to manipulate @{ML_type cterm}s. However,

  2064   The purpose of conversions is to manipulate @{ML_type cterm}s. However,

  2073   we will also show in this section how conversions can be applied to theorems

  2065   we will also show in this section how conversions can be applied to theorems

  2074   and to goal states. The type of conversions is

  2066   and to goal states. The type of conversions is

  2075 *}

  2067 *}

  2076 

  2068 

  2078 

  2070 

  2079 text {*

  2071 text {*

  2080   whereby the produced theorem is always a meta-equality. A simple conversion

  2072   whereby the produced theorem is always a meta-equality. A simple conversion

  2081   is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an

  2073   is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an

  2082   instance of the (meta)reflexivity theorem. For example:

  2074   instance of the (meta)reflexivity theorem. For example:

  2310   Conversions that traverse terms, like @{ML true_conj1_conv} above, can be

  2302   Conversions that traverse terms, like @{ML true_conj1_conv} above, can be

  2311   implemented more succinctly with the combinators @{ML_ind bottom_conv in

  2303   implemented more succinctly with the combinators @{ML_ind bottom_conv in

  2312   Conv} and @{ML_ind top_conv in Conv}. For example:

  2304   Conv} and @{ML_ind top_conv in Conv}. For example:

  2313 *}

  2305 *}

  2314 

  2306 

  2316 let

  2308 let

  2317   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})

  2309   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})

  2318 in

  2310 in

  2319   Conv.bottom_conv (K conv) ctxt

  2311   Conv.bottom_conv (K conv) ctxt

  2320 end*}

  2312 end*}

  2356   make the task a bit more complicated by rewriting according to the rule

  2348   make the task a bit more complicated by rewriting according to the rule

  2357   @{text true_conj1}, but only in the first arguments of @{term If}s. Then 

  2349   @{text true_conj1}, but only in the first arguments of @{term If}s. Then 

  2358   the conversion should be as follows.

  2350   the conversion should be as follows.

  2359 *}

  2351 *}

  2360 

  2352 

  2362   case Thm.term_of ctrm of

  2354   case Thm.term_of ctrm of

  2363     Const (@{const_name If}, _) $ _ =>

  2355     Const (@{const_name If}, _) $ _ =>

  2364       Conv.arg_conv (true_conj1_conv ctxt) ctrm

  2356       Conv.arg_conv (true_conj1_conv ctxt) ctrm

  2365   | _ => Conv.no_conv ctrm 

  2357   | _ => Conv.no_conv ctrm 

  2366 

  2358 

  2428   Assume we want to apply @{ML true_conj1_conv} only in the conclusion

  2420   Assume we want to apply @{ML true_conj1_conv} only in the conclusion

  2429   of the goal, and @{ML if_true1_conv} should only apply to the premises.

  2421   of the goal, and @{ML if_true1_conv} should only apply to the premises.

  2430   Here is a tactic doing exactly that:

  2422   Here is a tactic doing exactly that:

  2431 *}

  2423 *}

  2432 

  2424 

  2434   CONVERSION 

  2426   CONVERSION 

  2435     (Conv.params_conv ~1 (fn ctxt =>

  2427     (Conv.params_conv ~1 (fn ctxt =>

  2436        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv

  2428        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv

  2437           Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}

  2429           Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}

  2438 

  2430