406 function that extracts the theorem names stored in a simpset. |
406 function that extracts the theorem names stored in a simpset. |
407 *} |
407 *} |
408 |
408 |
409 ML{*fun get_thm_names_from_ss simpset = |
409 ML{*fun get_thm_names_from_ss simpset = |
410 let |
410 let |
411 val ({rules,...}, _) = MetaSimplifier.rep_ss simpset |
411 val {simps,...} = MetaSimplifier.dest_ss simpset |
412 in |
412 in |
413 map #name (Net.entries rules) |
413 map #1 simps |
414 end*} |
414 end*} |
415 |
415 |
416 text {* |
416 text {* |
417 The function @{ML rep_ss in MetaSimplifier} returns a record containing all |
417 The function @{ML dest_ss in MetaSimplifier} returns a record containing all |
418 information about the simpset. The rules of a simpset are stored in a |
418 information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored |
419 \emph{discrimination net} (a data structure for fast indexing). From this |
|
420 net you can extract the entries using the function @{ML Net.entries}. |
|
421 You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored |
|
422 in the current simpset. This simpset can be referred to using the antiquotation |
419 in the current simpset. This simpset can be referred to using the antiquotation |
423 @{text "@{simpset}"}. |
420 @{text "@{simpset}"}. |
424 |
421 |
425 @{ML_response_fake [display,gray] |
422 @{ML_response_fake [display,gray] |
426 "get_thm_names_from_ss @{simpset}" |
423 "get_thm_names_from_ss @{simpset}" |
442 statically at compile-time. However, this static linkage also limits their |
439 statically at compile-time. However, this static linkage also limits their |
443 usefulness in cases where data needs to be build up dynamically. In the |
440 usefulness in cases where data needs to be build up dynamically. In the |
444 course of this chapter you will learn more about these antiquotations: |
441 course of this chapter you will learn more about these antiquotations: |
445 they can simplify Isabelle programming since one can directly access all |
442 they can simplify Isabelle programming since one can directly access all |
446 kinds of logical elements from th ML-level. |
443 kinds of logical elements from th ML-level. |
447 |
|
448 *} |
444 *} |
449 |
445 |
450 section {* Terms and Types *} |
446 section {* Terms and Types *} |
451 |
447 |
452 text {* |
448 text {* |
708 | is_nil_or_all _ = false *} |
704 | is_nil_or_all _ = false *} |
709 |
705 |
710 text {* |
706 text {* |
711 Occasional you have to calculate what the ``base'' name of a given |
707 Occasional you have to calculate what the ``base'' name of a given |
712 constant is. For this you can use the function @{ML Sign.extern_const} or |
708 constant is. For this you can use the function @{ML Sign.extern_const} or |
713 @{ML NameSpace.base_name}. For example: |
709 @{ML Long_Name.base_name}. For example: |
714 |
710 |
715 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
711 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
716 |
712 |
717 The difference between both functions is that @{ML extern_const in Sign} returns |
713 The difference between both functions is that @{ML extern_const in Sign} returns |
718 the smallest name that is still unique, whereas @{ML base_name in NameSpace} always |
714 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
719 strips off all qualifiers. |
715 strips off all qualifiers. |
720 |
716 |
721 \begin{readmore} |
717 \begin{readmore} |
722 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
718 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
723 functions about signatures in @{ML_file "Pure/sign.ML"}. |
719 functions about signatures in @{ML_file "Pure/sign.ML"}. |
1180 |
1176 |
1181 |
1177 |
1182 (* FIXME: some code below *) |
1178 (* FIXME: some code below *) |
1183 |
1179 |
1184 (*<*) |
1180 (*<*) |
|
1181 (* |
1185 setup {* |
1182 setup {* |
1186 Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] |
1183 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] |
1187 *} |
1184 *} |
1188 |
1185 *) |
1189 lemma "bar = (1::nat)" |
1186 lemma "bar = (1::nat)" |
1190 oops |
1187 oops |
1191 |
1188 |
|
1189 (* |
1192 setup {* |
1190 setup {* |
1193 Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] |
1191 Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] |
1194 #> PureThy.add_defs false [((Binding.name "foo_def", |
1192 #> PureThy.add_defs false [((Binding.name "foo_def", |
1195 Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] |
1193 Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] |
1196 #> snd |
1194 #> snd |
1197 *} |
1195 *} |
1198 |
1196 *) |
|
1197 (* |
1199 lemma "foo = (1::nat)" |
1198 lemma "foo = (1::nat)" |
1200 apply(simp add: foo_def) |
1199 apply(simp add: foo_def) |
1201 done |
1200 done |
1202 |
1201 |
1203 thm foo_def |
1202 thm foo_def |
|
1203 *) |
1204 (*>*) |
1204 (*>*) |
1205 |
1205 |
1206 section {* Pretty-Printing (TBD) *} |
1206 section {* Pretty-Printing (TBD) *} |
1207 |
1207 |
1208 text {* |
1208 text {* |
1209 @{ML Pretty.big_list} |
1209 @{ML Pretty.big_list}, |
|
1210 @{ML Pretty.brk}, |
|
1211 @{ML Pretty.block}, |
|
1212 @{ML Pretty.chunks} |
1210 *} |
1213 *} |
1211 |
1214 |
1212 section {* Misc (TBD) *} |
1215 section {* Misc (TBD) *} |
1213 |
1216 |
1214 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |
1217 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |