113 pretty_terms @{context} [v1, v2, v3] |
113 pretty_terms @{context} [v1, v2, v3] |
114 |> pwriteln |
114 |> pwriteln |
115 end" |
115 end" |
116 "?x3, ?x1.3, x"} |
116 "?x3, ?x1.3, x"} |
117 |
117 |
118 When constructing terms, you are usually concerned with free variables (as |
118 When constructing terms, you are usually concerned with free |
119 mentioned earlier, you cannot construct schematic variables using the |
119 variables (as mentioned earlier, you cannot construct schematic |
120 antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to, |
120 variables using the built in antiquotation \mbox{@{text "@{term |
121 however, observe the distinction. The reason is that only schematic |
121 \<dots>}"}}). If you deal with theorems, you have to, however, observe the |
122 variables can be instantiated with terms when a theorem is applied. A |
122 distinction. The reason is that only schematic variables can be |
123 similar distinction between free and schematic variables holds for types |
123 instantiated with terms when a theorem is applied. A similar |
|
124 distinction between free and schematic variables holds for types |
124 (see below). |
125 (see below). |
125 |
126 |
126 \begin{readmore} |
127 \begin{readmore} |
127 Terms and types are described in detail in \isccite{sec:terms}. Their |
128 Terms and types are described in detail in \isccite{sec:terms}. Their |
128 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
129 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
1553 \] |
1554 \] |
1554 |
1555 |
1555 While we obtained a theorem as result, this theorem is not |
1556 While we obtained a theorem as result, this theorem is not |
1556 yet stored in Isabelle's theorem database. Consequently, it cannot be |
1557 yet stored in Isabelle's theorem database. Consequently, it cannot be |
1557 referenced on the user level. One way to store it in the theorem database is |
1558 referenced on the user level. One way to store it in the theorem database is |
1558 by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer |
1559 by using the function @{ML_ind note in Local_Theory} from the structure |
1559 to the section about local-setup is given here.} |
1560 @{ML_struct Local_Theory} (the Isabelle command |
|
1561 \isacommand{local\_setup} will be explained in more detail in |
|
1562 Section~\ref{sec:local}). |
1560 *} |
1563 *} |
1561 |
1564 |
1562 local_setup %gray {* |
1565 local_setup %gray {* |
1563 Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
1566 Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
1564 |
1567 |
1596 |
1599 |
1597 The main point of storing the theorems @{thm [source] my_thm} and @{thm |
1600 The main point of storing the theorems @{thm [source] my_thm} and @{thm |
1598 [source] my_thm_simp} is that they can now also be referenced with the |
1601 [source] my_thm_simp} is that they can now also be referenced with the |
1599 \isacommand{thm}-command on the user-level of Isabelle |
1602 \isacommand{thm}-command on the user-level of Isabelle |
1600 |
1603 |
1601 |
1604 |
1602 \begin{isabelle} |
1605 \begin{isabelle} |
1603 \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline |
1606 \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline |
1604 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline |
1607 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline |
1605 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
1608 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
1606 \end{isabelle} |
1609 \end{isabelle} |
2007 text {* |
2010 text {* |
2008 Now printing out in a document the theorem @{thm [source] style_test} normally |
2011 Now printing out in a document the theorem @{thm [source] style_test} normally |
2009 using @{text "@{thm \<dots>}"} produces |
2012 using @{text "@{thm \<dots>}"} produces |
2010 |
2013 |
2011 \begin{isabelle} |
2014 \begin{isabelle} |
|
2015 \begin{graybox} |
2012 @{text "@{thm style_test}"}\\ |
2016 @{text "@{thm style_test}"}\\ |
2013 @{text ">"}~@{thm style_test} |
2017 @{text ">"}~@{thm style_test} |
|
2018 \end{graybox} |
2014 \end{isabelle} |
2019 \end{isabelle} |
2015 |
2020 |
2016 as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} |
2021 as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} |
2017 we obtain |
2022 we obtain |
2018 |
2023 |
2019 \begin{isabelle} |
2024 \begin{isabelle} |
|
2025 \begin{graybox} |
2020 @{text "@{thm (my_strip_allq) style_test}"}\\ |
2026 @{text "@{thm (my_strip_allq) style_test}"}\\ |
2021 @{text ">"}~@{thm (my_strip_allq) style_test} |
2027 @{text ">"}~@{thm (my_strip_allq) style_test} |
|
2028 \end{graybox} |
2022 \end{isabelle} |
2029 \end{isabelle} |
2023 |
2030 |
2024 without the leading quantifiers. We can improve this theorem style by explicitly |
2031 without the leading quantifiers. We can improve this theorem style by explicitly |
2025 giving a list of strings that should be used for the replacement of the |
2032 giving a list of strings that should be used for the replacement of the |
2026 variables. For this we implement the function which takes a list of strings |
2033 variables. For this we implement the function which takes a list of strings |
2049 The parser reads a list of names. In the function @{text action} we first |
2056 The parser reads a list of names. In the function @{text action} we first |
2050 call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} |
2057 call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} |
2051 on the resulting term. We can now suggest, for example, two variables for |
2058 on the resulting term. We can now suggest, for example, two variables for |
2052 stripping off the first two @{text \<forall>}-quantifiers. |
2059 stripping off the first two @{text \<forall>}-quantifiers. |
2053 |
2060 |
2054 |
|
2055 \begin{isabelle} |
2061 \begin{isabelle} |
|
2062 \begin{graybox} |
2056 @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ |
2063 @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ |
2057 @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} |
2064 @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} |
|
2065 \end{graybox} |
2058 \end{isabelle} |
2066 \end{isabelle} |
2059 |
2067 |
2060 Such styles allow one to print out theorems in documents formatted to |
2068 Such styles allow one to print out theorems in documents formatted to |
2061 ones heart content. The styles can also be used in the document |
2069 ones heart content. The styles can also be used in the document |
2062 antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"} |
2070 antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"} |