22 We also generally assume you are working with HOL. The given examples might |
22 We also generally assume you are working with HOL. The given examples might |
23 need to be adapted slightly if you work in a different logic. |
23 need to be adapted slightly if you work in a different logic. |
24 *} |
24 *} |
25 |
25 |
26 section {* Including ML-Code *} |
26 section {* Including ML-Code *} |
27 |
|
28 |
|
29 |
27 |
30 text {* |
28 text {* |
31 The easiest and quickest way to include code in a theory is |
29 The easiest and quickest way to include code in a theory is |
32 by using the \isacommand{ML}-command. For example: |
30 by using the \isacommand{ML}-command. For example: |
33 |
31 |
152 ML{*fun str_of_cterms ctxt ts = |
150 ML{*fun str_of_cterms ctxt ts = |
153 commas (map (str_of_cterm ctxt) ts)*} |
151 commas (map (str_of_cterm ctxt) ts)*} |
154 |
152 |
155 text {* |
153 text {* |
156 The easiest way to get the string of a theorem is to transform it |
154 The easiest way to get the string of a theorem is to transform it |
157 into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems |
155 into a @{ML_type cterm} using the function @{ML crep_thm}. |
158 also include schematic variables, such as @{text "?P"}, @{text "?Q"} |
156 *} |
159 and so on. In order to improve the readability of theorems we convert |
157 |
|
158 ML{*fun str_of_thm_raw ctxt thm = |
|
159 str_of_cterm ctxt (#prop (crep_thm thm))*} |
|
160 |
|
161 text {* |
|
162 Theorems also include schematic variables, such as @{text "?P"}, |
|
163 @{text "?Q"} and so on. |
|
164 |
|
165 @{ML_response_fake [display, gray] |
|
166 "warning (str_of_thm_raw @{context} @{thm conjI})" |
|
167 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
|
168 |
|
169 In order to improve the readability of theorems we convert |
160 these schematic variables into free variables using the |
170 these schematic variables into free variables using the |
161 function @{ML Variable.import_thms}. |
171 function @{ML Variable.import_thms}. |
162 *} |
172 *} |
163 |
173 |
164 ML{*fun no_vars ctxt thm = |
174 ML{*fun no_vars ctxt thm = |
170 |
180 |
171 fun str_of_thm ctxt thm = |
181 fun str_of_thm ctxt thm = |
172 str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} |
182 str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} |
173 |
183 |
174 text {* |
184 text {* |
|
185 Theorem @{thm [source] conjI} looks now as follows |
|
186 |
|
187 @{ML_response_fake [display, gray] |
|
188 "warning (str_of_thm_raw @{context} @{thm conjI})" |
|
189 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
|
190 |
175 Again the function @{ML commas} helps with printing more than one theorem. |
191 Again the function @{ML commas} helps with printing more than one theorem. |
176 *} |
192 *} |
177 |
193 |
178 ML{*fun str_of_thms ctxt thms = |
194 ML{*fun str_of_thms ctxt thms = |
179 commas (map (str_of_thm ctxt) thms)*} |
195 commas (map (str_of_thm ctxt) thms) |
|
196 |
|
197 fun str_of_thms_raw ctxt thms = |
|
198 commas (map (str_of_thm_raw ctxt) thms)*} |
180 |
199 |
181 text {* |
200 text {* |
182 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug}) |
201 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug}) |
183 *} |
202 *} |
184 |
203 |
597 "Const \<dots> $ |
616 "Const \<dots> $ |
598 Abs (\"x\", \<dots>, |
617 Abs (\"x\", \<dots>, |
599 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
618 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
600 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
619 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
601 |
620 |
602 (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}) |
621 (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}, |
|
622 @{ML subst_free}) |
603 *} |
623 *} |
604 |
624 |
605 |
625 |
606 text {* |
626 text {* |
607 \begin{readmore} |
627 \begin{readmore} |