1127 text {* |
1127 text {* |
1128 One great feature of Isabelle is its document preparation system, where |
1128 One great feature of Isabelle is its document preparation system, where |
1129 proved theorems can be quoted in documents referencing directly their |
1129 proved theorems can be quoted in documents referencing directly their |
1130 formalisation. This helps tremendously to minimise cut-and-paste errors. However, |
1130 formalisation. This helps tremendously to minimise cut-and-paste errors. However, |
1131 sometimes the verbatim quoting is not what is wanted or what can be shown to |
1131 sometimes the verbatim quoting is not what is wanted or what can be shown to |
1132 readers. For such situations Isabelle allows the installation of \emph{theorem |
1132 readers. For such situations Isabelle allows the installation of \emph{\index*{theorem |
1133 styles}. These are, roughly speaking, functions from terms to terms. The input |
1133 styles}}. These are, roughly speaking, functions from terms to terms. The input |
1134 term stands for the theorem to be presented; the output can be constructed to |
1134 term stands for the theorem to be presented; the output can be constructed to |
1135 ones wishes. Let us, for example, assume we want to quote theorems without |
1135 ones wishes. Let us, for example, assume we want to quote theorems without |
1136 leading @{text \<forall>}-quantifiers. For this we can implement the following function |
1136 leading @{text \<forall>}-quantifiers. For this we can implement the following function |
1137 that strips off meta-quantifiers. |
1137 that strips off meta-quantifiers. |
1138 *} |
1138 *} |
1139 |
1139 |
1140 ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) = |
1140 ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = |
1141 Term.dest_abs body |> snd |> strip_all_qnt |
1141 Term.dest_abs body |> snd |> strip_allq |
1142 | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) = |
1142 | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = |
1143 strip_all_qnt t |
1143 strip_allq t |
1144 | strip_all_qnt t = t*} |
1144 | strip_allq t = t*} |
1145 |
1145 |
1146 text {* |
1146 text {* |
1147 We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions, |
1147 We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions, |
1148 since this function deals correctly with potential name clashes. This function produces |
1148 since this function deals correctly with potential name clashes. This function produces |
1149 a pair consisting of the variable and the body of the abstraction. We are only interested |
1149 a pair consisting of the variable and the body of the abstraction. We are only interested |
1150 in the body, which we feed into the recursive call. In Line 3 and 4, we also |
1150 in the body, which we feed into the recursive call. In Line 3 and 4, we also |
1151 have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can |
1151 have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can |
1152 install this function as the theorem style named @{text "my_strip_all_qnt"}. |
1152 install this function as the theorem style named @{text "my_strip_allq"}. |
1153 *} |
1153 *} |
1154 |
1154 |
1155 setup %gray {* |
1155 setup %gray {* |
1156 Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt)) |
1156 Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) |
1157 *} |
1157 *} |
1158 |
1158 |
1159 text {* |
1159 text {* |
1160 We can test this theorem style with the following theorem |
1160 We can test this theorem style with the following theorem |
1161 *} |
1161 *} |
1170 \begin{isabelle} |
1170 \begin{isabelle} |
1171 @{text "@{thm style_test}"}\\ |
1171 @{text "@{thm style_test}"}\\ |
1172 @{text ">"}~@{thm style_test} |
1172 @{text ">"}~@{thm style_test} |
1173 \end{isabelle} |
1173 \end{isabelle} |
1174 |
1174 |
1175 as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \<dots>}"} |
1175 as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} |
1176 we obtain |
1176 we obtain |
1177 |
1177 |
1178 \begin{isabelle} |
1178 \begin{isabelle} |
1179 @{text "@{thm (my_strip_all_qnt) style_test}"}\\ |
1179 @{text "@{thm (my_strip_allq) style_test}"}\\ |
1180 @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\ |
1180 @{text ">"}~@{thm (my_strip_allq) style_test}\\ |
1181 \end{isabelle} |
1181 \end{isabelle} |
1182 |
1182 |
1183 without the leading quantifiers. We can improve this theorem style by explicitly |
1183 without the leading quantifiers. We can improve this theorem style by explicitly |
1184 giving a list of strings that should be used for the replacement of the |
1184 giving a list of strings that should be used for the replacement of the |
1185 variables. For this we implement the function which takes a list of strings |
1185 variables. For this we implement the function which takes a list of strings |
1186 and uses them as name in the outermost abstractions. |
1186 and uses them as name in the outermost abstractions. |
1187 *} |
1187 *} |
1188 |
1188 |
1189 ML {*fun rename_all [] t = t |
1189 ML {*fun rename_allq [] t = t |
1190 | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = |
1190 | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = |
1191 Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t) |
1191 Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t) |
1192 | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) = |
1192 | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) = |
1193 rename_all xs t |
1193 rename_allq xs t |
1194 | rename_all _ t = t*} |
1194 | rename_allq _ t = t*} |
1195 |
1195 |
1196 text {* |
1196 text {* |
1197 We can now install a the modified theorem style as follows |
1197 We can now install a the modified theorem style as follows |
1198 *} |
1198 *} |
1199 |
1199 |
1200 setup %gray {* |
1200 setup %gray {* |
1201 let |
1201 let |
1202 val parser = Scan.repeat Args.name |
1202 val parser = Scan.repeat Args.name |
1203 fun action xs = K (rename_all xs #> strip_all_qnt) |
1203 fun action xs = K (rename_allq xs #> strip_allq) |
1204 in |
1204 in |
1205 Term_Style.setup "my_strip_all_qnt2" (parser >> action) |
1205 Term_Style.setup "my_strip_allq2" (parser >> action) |
1206 end *} |
1206 end *} |
1207 |
1207 |
1208 text {* |
1208 text {* |
1209 We can now suggest, for example, two variables for stripping |
1209 The parser reads a list of names. In the function @{ML_text action} we first |
1210 off the @{text \<forall>}-quantifiers, namely: |
1210 call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} |
|
1211 on the resulting term. We can now suggest, for example, two variables for |
|
1212 stripping off the first two @{text \<forall>}-quantifiers. |
|
1213 |
1211 |
1214 |
1212 \begin{isabelle} |
1215 \begin{isabelle} |
1213 @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\ |
1216 @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ |
1214 @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test} |
1217 @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} |
1215 \end{isabelle} |
1218 \end{isabelle} |
1216 |
1219 |
1217 Such theorem styles allow one to print out theorems in documents formatted to |
1220 Such theorem styles allow one to print out theorems in documents formatted to |
1218 ones heart content. Next we explain theorem attributes, which is another |
1221 ones heart content. Next we explain theorem attributes, which is another |
1219 mechanism for dealing with theorems. |
1222 mechanism for dealing with theorems. |