139 |
139 |
140 ML{*fun str_of_cterm ctxt t = |
140 ML{*fun str_of_cterm ctxt t = |
141 Syntax.string_of_term ctxt (term_of t)*} |
141 Syntax.string_of_term ctxt (term_of t)*} |
142 |
142 |
143 text {* |
143 text {* |
|
144 The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}. |
144 If there are more than one @{ML_type cterm}s to be printed, you can use the |
145 If there are more than one @{ML_type cterm}s to be printed, you can use the |
145 function @{ML commas} to separate them. |
146 function @{ML commas} to separate them. |
146 *} |
147 *} |
147 |
148 |
148 ML{*fun str_of_cterms ctxt ts = |
149 ML{*fun str_of_cterms ctxt ts = |
386 @{ML_response_fake [display,gray] "@{thms conj_ac}" |
387 @{ML_response_fake [display,gray] "@{thms conj_ac}" |
387 "(?P \<and> ?Q) = (?Q \<and> ?P) |
388 "(?P \<and> ?Q) = (?Q \<and> ?P) |
388 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R) |
389 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R) |
389 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} |
390 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} |
390 |
391 |
391 You can also refer to the current simpsets. To illustrate this we use the |
392 You can also refer to the current simpset. To illustrate this we use the |
392 function that extracts the theorem names stored in a simpset. |
393 function that extracts the theorem names stored in a simpset. |
393 *} |
394 *} |
394 |
395 |
395 ML{*fun get_thm_names simpset = |
396 ML{*fun get_thm_names simpset = |
396 let |
397 let |
402 text {* |
403 text {* |
403 The function @{ML rep_ss in MetaSimplifier} returns a record containing all |
404 The function @{ML rep_ss in MetaSimplifier} returns a record containing all |
404 information about the simpset. The rules of a simpset are stored in a |
405 information about the simpset. The rules of a simpset are stored in a |
405 \emph{discrimination net} (a data structure for fast indexing). From this |
406 \emph{discrimination net} (a data structure for fast indexing). From this |
406 net you can extract the entries using the function @{ML Net.entries}. |
407 net you can extract the entries using the function @{ML Net.entries}. |
407 You can now use @{ML get_thm_names} to obtain all names of theorems of |
408 You can now use @{ML get_thm_names} to obtain all names of theorems stored |
408 the current simpset using the antiquotation @{text "@{simpset}"}.\footnote |
409 in the current simpset---this simpset can be referred to using the antiquotation |
|
410 @{text "@{simpset}"}.\footnote |
409 {FIXME: you cannot cleanly match against lists with ommited parts} |
411 {FIXME: you cannot cleanly match against lists with ommited parts} |
410 |
412 |
411 @{ML_response_fake [display,gray] |
413 @{ML_response_fake [display,gray] |
412 "get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
414 "get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
413 |
415 |
569 text {* This can be equally written as: *} |
571 text {* This can be equally written as: *} |
570 |
572 |
571 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} |
573 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} |
572 |
574 |
573 text {* |
575 text {* |
|
576 A handy function for manipulating terms is @{ML map_types}: it takes a |
|
577 function and applies it to every type in the term. You can, for example, |
|
578 change every @{typ nat} in a term into an @{typ int} using the function: |
|
579 *} |
|
580 |
|
581 ML{*fun nat_to_int t = |
|
582 (case t of |
|
583 @{typ nat} => @{typ int} |
|
584 | Type (s, ts) => Type (s, map nat_to_int ts) |
|
585 | _ => t)*} |
|
586 |
|
587 text {* |
|
588 An example as follows: |
|
589 |
|
590 @{ML_response_fake [display,gray] |
|
591 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
|
592 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
|
593 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
|
594 |
574 \begin{readmore} |
595 \begin{readmore} |
575 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
596 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
576 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
597 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
577 and types easier.\end{readmore} |
598 and types easier.\end{readmore} |
578 |
599 |
592 \begin{exercise}\label{fun:makesum} |
613 \begin{exercise}\label{fun:makesum} |
593 Write a function which takes two terms representing natural numbers |
614 Write a function which takes two terms representing natural numbers |
594 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the |
615 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the |
595 number representing their sum. |
616 number representing their sum. |
596 \end{exercise} |
617 \end{exercise} |
597 |
|
598 A handy function for manipulating terms is @{ML map_types}: it takes a |
|
599 function and applies it to every type in the term. You can, for example, |
|
600 change every @{typ nat} in a term into an @{typ int} using the function: |
|
601 *} |
|
602 |
|
603 ML{*fun nat_to_int t = |
|
604 (case t of |
|
605 @{typ nat} => @{typ int} |
|
606 | Type (s, ts) => Type (s, map nat_to_int ts) |
|
607 | _ => t)*} |
|
608 |
|
609 text {* |
|
610 An example as follows: |
|
611 |
|
612 @{ML_response_fake [display,gray] |
|
613 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
|
614 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
|
615 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
|
616 |
|
617 |
618 |
618 There are a few subtle issues with constants. They usually crop up when |
619 There are a few subtle issues with constants. They usually crop up when |
619 pattern matching terms or types, or constructing them. While it is perfectly ok |
620 pattern matching terms or types, or constructing them. While it is perfectly ok |
620 to write the function @{text is_true} as follows |
621 to write the function @{text is_true} as follows |
621 *} |
622 *} |