1167 

  1167 

  1168   Sometimes it is a bit inconvenient to construct a term with 

  1168   Sometimes it is a bit inconvenient to construct a term with 

  1169   complete typing annotations, especially in cases where the typing 

  1169   complete typing annotations, especially in cases where the typing 

  1170   information is redundant. A short-cut is to use the ``place-holder'' 

  1170   information is redundant. A short-cut is to use the ``place-holder'' 

  1171   type @{ML_ind dummyT in Term} and then let type-inference figure out the 

  1171   type @{ML_ind dummyT in Term} and then let type-inference figure out the 

  1173 

  1174 

  1174   @{ML_response_fake [display,gray] 

  1175   @{ML_response_fake [display,gray] 

  1175 "let

  1176 "let

  1176   val c = Const (@{const_name \"plus\"}, dummyT) 

  1177   val c = Const (@{const_name \"plus\"}, dummyT) 

  1177   val o = @{term \"1::nat\"} 

  1178   val o = @{term \"1::nat\"} 

  1323   Qt 

  1324   Qt 

  1324   |> implies_intr assm2

  1325   |> implies_intr assm2

  1325   |> implies_intr assm1

  1326   |> implies_intr assm1

  1326 end*}

  1327 end*}

  1327 

  1328 

  1329   If we print out the value of @{ML my_thm} then we see only the 

  1330   If we print out the value of @{ML my_thm} then we see only the 

  1330   final statement of the theorem.

  1331   final statement of the theorem.

  1331 

  1332 

  1332   @{ML_response_fake [display, gray]

  1333   @{ML_response_fake [display, gray]

  1333   "tracing (string_of_thm @{context} my_thm)"

  1334   "tracing (string_of_thm @{context} my_thm)"

  1422    val merge = merge Thm.eq_thm_prop)

  1423    val merge = merge Thm.eq_thm_prop)

  1423 

  1424 

  1424 fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}

  1425 fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}

  1425 

  1426 

  1426 text {*

  1427 text {*

  1429   The function @{ML update} allows us to update the theorem list, for example

  1428   The function @{ML update} allows us to update the theorem list, for example

  1430   by adding the theorem @{thm [source] TrueI}.

  1429   by adding the theorem @{thm [source] TrueI}.

  1431 *}

  1430 *}

  1432 

  1431 

  1433 setup %gray {* update @{thm TrueI} *}

  1432 setup %gray {* update @{thm TrueI} *}

  1464   \isacommand{thm}~@{text "mythmlist"}\\

  1463   \isacommand{thm}~@{text "mythmlist"}\\

  1465   @{text "> False \<Longrightarrow> ?P"}\\

  1464   @{text "> False \<Longrightarrow> ?P"}\\

  1466   @{text "> True"}

  1465   @{text "> True"}

  1467   \end{isabelle}

  1466   \end{isabelle}

  1468 

  1467 

  1473 *}

  1480 *}

  1474 

  1481 

  1475 lemma

  1482 lemma

  1476   shows thm1: "\<forall>x. P x" 

  1483   shows thm1: "\<forall>x. P x" 

  1477   and   thm2: "\<forall>y. P y" 

  1484   and   thm2: "\<forall>y. P y" 

  1478   and   thm3: "\<forall>y. Q y" sorry

  1485   and   thm3: "\<forall>y. Q y" sorry

  1479 

  1486 

  1480 text {*

  1487 text {*

  1482 

  1489 

  1483   @{ML_response [display,gray]

  1490   @{ML_response [display,gray]

  1486 "(true, false)"}

  1493 "(true, false)"}

  1487 

  1494 

  1488   Many functions destruct theorems into @{ML_type cterm}s. For example

  1495   Many functions destruct theorems into @{ML_type cterm}s. For example

  1489   the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 

  1496   the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 

  1490   the left and right-hand side, respectively, of a meta-equality.

  1497   the left and right-hand side, respectively, of a meta-equality.

  1744   in the body, which we feed into the recursive call. In Line 3 and 4, we also

  1751   in the body, which we feed into the recursive call. In Line 3 and 4, we also

  1745   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 

  1752   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 

  1746   install this function as the theorem style named @{text "my_strip_allq"}. 

  1753   install this function as the theorem style named @{text "my_strip_allq"}. 

  1747 *}

  1754 *}

  1748 

  1755 

  1750   Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) 

  1757   Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) 

  1751 *}

  1758 *}

  1752 

  1759 

  1753 text {*

  1760 text {*

  1754   We can test this theorem style with the following theorem

  1761   We can test this theorem style with the following theorem

  1769   as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 

  1776   as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 

  1770   we obtain

  1777   we obtain

  1771 

  1778 

  1772   \begin{isabelle}

  1779   \begin{isabelle}

  1773   @{text "@{thm (my_strip_allq) style_test}"}\\

  1780   @{text "@{thm (my_strip_allq) style_test}"}\\

  1775   \end{isabelle}

  1782   \end{isabelle}

  1776   

  1783   

  1777   without the leading quantifiers. We can improve this theorem style by explicitly 

  1784   without the leading quantifiers. We can improve this theorem style by explicitly 

  1778   giving a list of strings that should be used for the replacement of the

  1785   giving a list of strings that should be used for the replacement of the

  1779   variables. For this we implement the function which takes a list of strings

  1786   variables. For this we implement the function which takes a list of strings