45 done

    45 done

    46 

    46 

    47 text \<open>

    47 text \<open>

    48   This proof translates to the following ML-code.

    48   This proof translates to the following ML-code.

    49   

    49   

    51 "let

    51 "let

    52   val ctxt = @{context}

    52   val ctxt = @{context}

    53   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

    53   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

    54 in

    54 in

    55   Goal.prove ctxt [\"P\", \"Q\"] [] goal 

    55   Goal.prove ctxt [\"P\", \"Q\"] [] goal 

   394 \<close>

   394 \<close>

   395 (*<*)oops(*>*)

   395 (*<*)oops(*>*)

   396 

   396 

   397 text \<open>

   397 text \<open>

   398   A simple tactic for easy discharge of any proof obligations, even difficult ones, is 

   398   A simple tactic for easy discharge of any proof obligations, even difficult ones, is 

   400   This tactic corresponds to the Isabelle command \isacommand{sorry} and is 

   400   This tactic corresponds to the Isabelle command \isacommand{sorry} and is 

   401   sometimes useful during the development of tactics.

   401   sometimes useful during the development of tactics.

   402 \<close>

   402 \<close>

   403 

   403 

   404 lemma 

   404 lemma 

   761   should be, then this situation can be avoided by introducing a more

   761   should be, then this situation can be avoided by introducing a more

   762   constrained version of the \<open>bspec\<close>-theorem. One way to give such 

   762   constrained version of the \<open>bspec\<close>-theorem. One way to give such 

   763   constraints is by pre-instantiating theorems with other theorems. 

   763   constraints is by pre-instantiating theorems with other theorems. 

   764   The function @{ML_ind RS in Drule}, for example, does this.

   764   The function @{ML_ind RS in Drule}, for example, does this.

   765   

   765   

   767   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}

   767   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}

   768 

   768 

   769   In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 

   769   In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 

   770   with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 

   770   with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 

   771   case of

   771   case of

   772 

   772 

   774   "@{thm conjI} RS @{thm mp}" 

   774   "@{thm conjI} RS @{thm mp}" 

   775 "*** Exception- THM (\"RSN: no unifiers\", 1, 

   775 "*** Exception- THM (\"RSN: no unifiers\", 1, 

   776 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}

   776 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}

   777 

   777 

   778   then the function raises an exception. The function @{ML_ind  RSN in Drule} 

   778   then the function raises an exception. The function @{ML_ind  RSN in Drule} 

   780   number makes explicit which premise should be instantiated. 

   780   number makes explicit which premise should be instantiated. 

   781 

   781 

   782   If you want to instantiate more than one premise of a theorem, you can use 

   782   If you want to instantiate more than one premise of a theorem, you can use 

   783   the function @{ML_ind MRS in Drule}:

   783   the function @{ML_ind MRS in Drule}:

   784 

   784 

   786   "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" 

   786   "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" 

   787   "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}

   787   "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}

   788 

   788 

   789   If you need to instantiate lists of theorems, you can use the

   789   If you need to instantiate lists of theorems, you can use the

   790   functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 

   790   functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 

   791   example in the code below, every theorem in the second list is 

   791   example in the code below, every theorem in the second list is 

   792   instantiated with every theorem in the first.

   792   instantiated with every theorem in the first.

   793 

   793 

   795 "let

   795 "let

   796   val list1 = [@{thm impI}, @{thm disjI2}]

   796   val list1 = [@{thm impI}, @{thm disjI2}]

   797   val list2 = [@{thm conjI}, @{thm disjI1}]

   797   val list2 = [@{thm conjI}, @{thm disjI1}]

   798 in

   798 in

   799   list1 RL list2

   799   list1 RL list2

  1291   introduction rule, the left rules as elimination rules. You have to to

  1291   introduction rule, the left rules as elimination rules. You have to to

  1292   prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The

  1292   prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The

  1293   tactic should explore all possibilites of applying these rules to a

  1293   tactic should explore all possibilites of applying these rules to a

  1294   propositional formula until a goal state is reached in which all subgoals

  1294   propositional formula until a goal state is reached in which all subgoals

  1295   are discharged. For this you can use the tactic combinator @{ML_ind

  1295   are discharged. For this you can use the tactic combinator @{ML_ind

  1297   \end{exercise}

  1297   \end{exercise}

  1298 

  1298 

  1299   \begin{exercise}

  1299   \begin{exercise}

  1300   Add to the sequent calculus from the previous exercise also rules for 

  1300   Add to the sequent calculus from the previous exercise also rules for 

  1301   equality and run your tactic on  the de Bruijn formulae discussed 

  1301   equality and run your tactic on  the de Bruijn formulae discussed 

  1357 

  1357 

  1358   There is one restriction you have to keep in mind when using the simplifier:

  1358   There is one restriction you have to keep in mind when using the simplifier:

  1359   it can only deal with rewriting rules whose left-hand sides are higher order 

  1359   it can only deal with rewriting rules whose left-hand sides are higher order 

  1360   pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern

  1360   pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern

  1361   or not can be tested with the function @{ML_ind pattern in Pattern} from

  1361   or not can be tested with the function @{ML_ind pattern in Pattern} from

  1363   to use it for rewriting, then you have to use simprocs or conversions, both 

  1363   to use it for rewriting, then you have to use simprocs or conversions, both 

  1364   of which we shall describe in the next section.

  1364   of which we shall describe in the next section.

  1365 

  1365 

  1366   When using the simplifier, the crucial information you have to provide is

  1366   When using the simplifier, the crucial information you have to provide is

  1367   the simpset. If this information is not handled with care, then, as

  1367   the simpset. If this information is not handled with care, then, as

  1456 text \<open>

  1456 text \<open>

  1457   To see how they work, consider the function in Figure~\ref{fig:printss}, which

  1457   To see how they work, consider the function in Figure~\ref{fig:printss}, which

  1458   prints out some parts of a simpset. If you use it to print out the components of the

  1458   prints out some parts of a simpset. If you use it to print out the components of the

  1459   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}

  1459   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}

  1460   

  1460   

  1462   "print_ss @{context} empty_ss"

  1462   "print_ss @{context} empty_ss"

  1463 "Simplification rules:

  1463 "Simplification rules:

  1464 Congruences rules:

  1464 Congruences rules:

  1465 Simproc patterns:"}

  1465 Simproc patterns:"}

  1466 

  1466 

  1472 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>

  1472 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>

  1473 

  1473 

  1474 text \<open>

  1474 text \<open>

  1475   Printing then out the components of the simpset gives:

  1475   Printing then out the components of the simpset gives:

  1476 

  1476 

  1478   "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"

  1478   "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"

  1479 "Simplification rules:

  1479 "Simplification rules:

  1480   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)

  1480   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)

  1481 Congruences rules:

  1481 Congruences rules:

  1482 Simproc patterns:"}

  1482 Simproc patterns:"}

  1489 ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close>

  1489 ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close>

  1490 

  1490 

  1491 text \<open>

  1491 text \<open>

  1492   gives

  1492   gives

  1493 

  1493 

  1495   "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"

  1495   "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"

  1496 "Simplification rules:

  1496 "Simplification rules:

  1497   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)

  1497   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)

  1498 Congruences rules:

  1498 Congruences rules:

  1499   Complete_Lattices.Inf_class.INFIMUM: 

  1499   Complete_Lattices.Inf_class.INFIMUM: 

  1506   where rules are usually added as equation. However, even 

  1506   where rules are usually added as equation. However, even 

  1507   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.

  1507   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.

  1508   In the context of HOL, the first really useful simpset is @{ML_ind

  1508   In the context of HOL, the first really useful simpset is @{ML_ind

  1509   HOL_basic_ss in Simpdata}. While printing out the components of this simpset

  1509   HOL_basic_ss in Simpdata}. While printing out the components of this simpset

  1510 

  1510 

  1512   "print_ss @{context} HOL_basic_ss"

  1512   "print_ss @{context} HOL_basic_ss"

  1513 "Simplification rules:

  1513 "Simplification rules:

  1514 Congruences rules:

  1514 Congruences rules:

  1515 Simproc patterns:"}

  1515 Simproc patterns:"}

  1516 

  1516 

  1540 

  1540 

  1541   The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing 

  1541   The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing 

  1542   already many useful simplification and congruence rules for the logical 

  1542   already many useful simplification and congruence rules for the logical 

  1543   connectives in HOL. 

  1543   connectives in HOL. 

  1544 

  1544 

  1546   "print_ss @{context} HOL_ss"

  1546   "print_ss @{context} HOL_ss"

  1547 "Simplification rules:

  1547 "Simplification rules:

  1548   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V

  1548   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V

  1549   HOL.the_eq_trivial: THE x. x = y \<equiv> y

  1549   HOL.the_eq_trivial: THE x. x = y \<equiv> y

  1550   HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y

  1550   HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y

  2062 text \<open>

  2062 text \<open>

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

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

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

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

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

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

  2066 

  2066 

  2068   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"

  2068   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"

  2069   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}

  2069   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}

  2070 

  2070 

  2071   Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 

  2071   Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 

  2072   exception @{ML CTERM}.

  2072   exception @{ML CTERM}.

  2073 

  2073 

  2075   "Conv.no_conv @{cterm True}" 

  2075   "Conv.no_conv @{cterm True}" 

  2076   "*** Exception- CTERM (\"no conversion\", []) raised"}

  2076   "*** Exception- CTERM (\"no conversion\", []) raised"}

  2077 

  2077 

  2078   A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 

  2078   A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 

  2079   produces a meta-equation between a term and its beta-normal form. For example

  2079   produces a meta-equation between a term and its beta-normal form. For example

  2080 

  2080 

  2082   "let

  2082   "let

  2083   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2083   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2084   val two = @{cterm \"2::nat\"}

  2084   val two = @{cterm \"2::nat\"}

  2085   val ten = @{cterm \"10::nat\"}

  2085   val ten = @{cterm \"10::nat\"}

  2086   val ctrm = Thm.apply (Thm.apply add two) ten

  2086   val ctrm = Thm.apply (Thm.apply add two) ten

  2094   "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for

  2094   "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for

  2095   @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.

  2095   @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.

  2096   If we get hold of the ``raw'' representation of the produced theorem, 

  2096   If we get hold of the ``raw'' representation of the produced theorem, 

  2097   we obtain the expected result.

  2097   we obtain the expected result.

  2098 

  2098 

  2100 "let

  2100 "let

  2101   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2101   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2102   val two = @{cterm \"2::nat\"}

  2102   val two = @{cterm \"2::nat\"}

  2103   val ten = @{cterm \"10::nat\"}

  2103   val ten = @{cterm \"10::nat\"}

  2104   val ctrm = Thm.apply (Thm.apply add two) ten

  2104   val ctrm = Thm.apply (Thm.apply add two) ten

  2109   (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 

  2109   (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 

  2110     (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 

  2110     (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 

  2111 

  2111 

  2112 or in the pretty-printed form

  2112 or in the pretty-printed form

  2113 

  2113 

  2115 "let

  2115 "let

  2116    val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2116    val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}

  2117    val two = @{cterm \"2::nat\"}

  2117    val two = @{cterm \"2::nat\"}

  2118    val ten = @{cterm \"10::nat\"}

  2118    val ten = @{cterm \"10::nat\"}

  2119    val ctrm = Thm.apply (Thm.apply add two) ten

  2119    val ctrm = Thm.apply (Thm.apply add two) ten

  2144 

  2144 

  2145 text \<open>

  2145 text \<open>

  2146   It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"} 

  2146   It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"} 

  2147   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.

  2147   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.

  2148 

  2148 

  2150 "let 

  2150 "let 

  2151   val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}

  2151   val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}

  2152 in

  2152 in

  2153   Conv.rewr_conv @{thm true_conj1} ctrm

  2153   Conv.rewr_conv @{thm true_conj1} ctrm

  2154 end"

  2154 end"

  2163   This very primitive way of rewriting can be made more powerful by

  2163   This very primitive way of rewriting can be made more powerful by

  2164   combining several conversions into one. For this you can use conversion

  2164   combining several conversions into one. For this you can use conversion

  2165   combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv}, 

  2165   combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv}, 

  2166   which applies one conversion after another. For example

  2166   which applies one conversion after another. For example

  2167 

  2167 

  2169 "let

  2169 "let

  2170   val conv1 = Thm.beta_conversion false

  2170   val conv1 = Thm.beta_conversion false

  2171   val conv2 = Conv.rewr_conv @{thm true_conj1}

  2171   val conv2 = Conv.rewr_conv @{thm true_conj1}

  2172   val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}

  2172   val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}

  2173 in

  2173 in

  2180   problem with the pretty-printer normalising all terms.)

  2180   problem with the pretty-printer normalising all terms.)

  2181 

  2181 

  2182   The conversion combinator @{ML_ind else_conv in Conv} tries out the 

  2182   The conversion combinator @{ML_ind else_conv in Conv} tries out the 

  2183   first one, and if it does not apply, tries the second. For example 

  2183   first one, and if it does not apply, tries the second. For example 

  2184 

  2184 

  2186 "let

  2186 "let

  2187   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv

  2187   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv

  2188   val ctrm1 = @{cterm \"True \<and> Q\"}

  2188   val ctrm1 = @{cterm \"True \<and> Q\"}

  2189   val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}

  2189   val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}

  2190 in

  2190 in

  2197   does not fail, however, because the combinator @{ML else_conv in Conv} will then 

  2197   does not fail, however, because the combinator @{ML else_conv in Conv} will then 

  2198   try out @{ML all_conv in Conv}, which always succeeds. The same

  2198   try out @{ML all_conv in Conv}, which always succeeds. The same

  2199   behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.

  2199   behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.

  2200   For example

  2200   For example

  2201   

  2201   

  2203 "let

  2203 "let

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

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

  2205   val ctrm = @{cterm \"True \<or> P\"}

  2205   val ctrm = @{cterm \"True \<or> P\"}

  2206 in

  2206 in

  2207   conv ctrm

  2207   conv ctrm

  2208 end"

  2208 end"

  2209   "True \<or> P \<equiv> True \<or> P"}

  2209   "True \<or> P \<equiv> True \<or> P"}

  2210 

  2210 

  2211   Rewriting with more than one theorem can be done using the function 

  2211   Rewriting with more than one theorem can be done using the function 

  2213   

  2213   

  2214 

  2214 

  2215   Apart from the function @{ML beta_conversion in Thm}, which is able to fully

  2215   Apart from the function @{ML beta_conversion in Thm}, which is able to fully

  2216   beta-normalise a term, the conversions so far are restricted in that they

  2216   beta-normalise a term, the conversions so far are restricted in that they

  2217   only apply to the outer-most level of a @{ML_type cterm}. In what follows we

  2217   only apply to the outer-most level of a @{ML_type cterm}. In what follows we

  2218   will lift this restriction. The combinators @{ML_ind fun_conv in Conv} 

  2218   will lift this restriction. The combinators @{ML_ind fun_conv in Conv} 

  2219   and @{ML_ind arg_conv in Conv} will apply

  2219   and @{ML_ind arg_conv in Conv} will apply

  2220   a conversion to the first, respectively second, argument of an application.  

  2220   a conversion to the first, respectively second, argument of an application.  

  2221   For example

  2221   For example

  2222 

  2222 

  2224 "let 

  2224 "let 

  2225   val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})

  2225   val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})

  2226   val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}

  2226   val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}

  2227 in

  2227 in

  2228   conv ctrm

  2228   conv ctrm

  2236   the conversion to the term \<open>(Const \<dots> $ t1)\<close>.

  2236   the conversion to the term \<open>(Const \<dots> $ t1)\<close>.

  2237 

  2237 

  2238   The function @{ML_ind  abs_conv in Conv} applies a conversion under an 

  2238   The function @{ML_ind  abs_conv in Conv} applies a conversion under an 

  2239   abstraction. For example:

  2239   abstraction. For example:

  2240 

  2240 

  2242 "let 

  2242 "let 

  2243   val conv = Conv.rewr_conv @{thm true_conj1} 

  2243   val conv = Conv.rewr_conv @{thm true_conj1} 

  2244   val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}

  2244   val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}

  2245 in

  2245 in

  2246   Conv.abs_conv (K conv) @{context} ctrm

  2246   Conv.abs_conv (K conv) @{context} ctrm

  2277   (Line 7); otherwise it leaves the term unchanged (Line 8). In Line 2

  2277   (Line 7); otherwise it leaves the term unchanged (Line 8). In Line 2

  2278   we need to transform the @{ML_type cterm} into a @{ML_type term} in order

  2278   we need to transform the @{ML_type cterm} into a @{ML_type term} in order

  2279   to be able to pattern-match the term. To see this 

  2279   to be able to pattern-match the term. To see this 

  2280   conversion in action, consider the following example:

  2280   conversion in action, consider the following example:

  2281 

  2281 

  2283 "let

  2283 "let

  2284   val conv = true_conj1_conv @{context}

  2284   val conv = true_conj1_conv @{context}

  2285   val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}

  2285   val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}

  2286 in

  2286 in

  2287   conv ctrm

  2287   conv ctrm

  2320   and the @{ML_type cterm} \<open>(a \<and> (b \<and> c)) \<and> d\<close>. Here you should

  2320   and the @{ML_type cterm} \<open>(a \<and> (b \<and> c)) \<and> d\<close>. Here you should

  2321   pause for a moment to be convinced that rewriting top-down and bottom-up 

  2321   pause for a moment to be convinced that rewriting top-down and bottom-up 

  2322   according to the two meta-equations produces two results. Below these

  2322   according to the two meta-equations produces two results. Below these

  2323   two results are calculated. 

  2323   two results are calculated. 

  2324 

  2324 

  2326   "let

  2326   "let

  2327   val ctxt = @{context}

  2327   val ctxt = @{context}

  2328   val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})

  2328   val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})

  2329   val conv_top = Conv.top_conv (K conv) ctxt

  2329   val conv_top = Conv.top_conv (K conv) ctxt

  2330   val conv_bot = Conv.bottom_conv (K conv) ctxt

  2330   val conv_bot = Conv.bottom_conv (K conv) ctxt

  2356   top_sweep_conv in Conv}, which traverses the term starting from the

  2356   top_sweep_conv in Conv}, which traverses the term starting from the

  2357   root and applies it to all the redexes on the way, but stops in each branch as

  2357   root and applies it to all the redexes on the way, but stops in each branch as

  2358   soon as it found one redex. Here is an example for this conversion:

  2358   soon as it found one redex. Here is an example for this conversion:

  2359 

  2359 

  2360 

  2360 

  2362 "let

  2362 "let

  2363   val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat)) 

  2363   val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat)) 

  2364                         then True \<and> True else True \<and> False\"}

  2364                         then True \<and> True else True \<and> False\"}

  2365 in

  2365 in

  2366   if_true1_conv @{context} ctrm

  2366   if_true1_conv @{context} ctrm

  2380 

  2380 

  2381 text \<open>

  2381 text \<open>

  2382   Using the conversion you can transform this theorem into a 

  2382   Using the conversion you can transform this theorem into a 

  2383   new theorem as follows

  2383   new theorem as follows

  2384 

  2384 

  2386 "let

  2386 "let

  2387   val conv = Conv.fconv_rule (true_conj1_conv @{context}) 

  2387   val conv = Conv.fconv_rule (true_conj1_conv @{context}) 

  2388   val thm = @{thm foo_test}

  2388   val thm = @{thm foo_test}

  2389 in

  2389 in

  2390   conv thm

  2390   conv thm

  2458 

  2458 

  2459 text \<open>

  2459 text \<open>

  2460   Although both definitions define the same function, the theorems @{thm

  2460   Although both definitions define the same function, the theorems @{thm

  2461   [source] id1_def} and @{thm [source] id2_def} are different meta-equations. However it is

  2461   [source] id1_def} and @{thm [source] id2_def} are different meta-equations. However it is

  2462   easy to transform one into the other. The function @{ML_ind abs_def

  2462   easy to transform one into the other. The function @{ML_ind abs_def

  2464   theorem @{thm [source] id1_def}

  2464   theorem @{thm [source] id1_def}

  2465   into @{thm [source] id2_def} by abstracting all variables on the 

  2465   into @{thm [source] id2_def} by abstracting all variables on the 

  2466   left-hand side in the right-hand side.

  2466   left-hand side in the right-hand side.

  2467 

  2467 

  2469   "Drule.abs_def @{thm id1_def}"

  2469   "Drule.abs_def @{thm id1_def}"

  2470   "id1 \<equiv> \<lambda>x. x"}

  2470   "id1 \<equiv> \<lambda>x. x"}

  2471 

  2471 

  2472   Unfortunately, Isabelle has no built-in function that transforms the

  2472   Unfortunately, Isabelle has no built-in function that transforms the

  2473   theorems in the other direction. We can implement one using

  2473   theorems in the other direction. We can implement one using

  2511   apply the new left-hand side to the generated conversion and obtain the the

  2511   apply the new left-hand side to the generated conversion and obtain the the

  2512   theorem we want to construct. As mentioned above, in Line 15 we only have to

  2512   theorem we want to construct. As mentioned above, in Line 15 we only have to

  2513   export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 

  2513   export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 

  2514   produce meta-variables for the theorem.  An example is as follows.

  2514   produce meta-variables for the theorem.  An example is as follows.

  2515 

  2515 

  2517   "unabs_def @{context} @{thm id2_def}"

  2517   "unabs_def @{context} @{thm id2_def}"

  2518   "id2 ?x1 \<equiv> ?x1"}

  2518   "id2 ?x1 \<equiv> ?x1"}

  2519 \<close>

  2519 \<close>

  2520 

  2520 

  2521 text \<open>

  2521 text \<open>