19 |
19 |
20 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
20 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
21 |
21 |
22 and then ``register'' the definition inside a local theory. |
22 and then ``register'' the definition inside a local theory. |
23 To do the latter, we use the following wrapper for the function |
23 To do the latter, we use the following wrapper for the function |
24 @{ML_ind define in LocalTheory}. The wrapper takes a predicate name, a syntax |
24 @{ML_ind define in Local_Theory}. The wrapper takes a predicate name, a syntax |
25 annotation and a term representing the right-hand side of the definition. |
25 annotation and a term representing the right-hand side of the definition. |
26 *} |
26 *} |
27 |
27 |
28 ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy = |
28 ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy = |
29 let |
29 let |
30 val arg = ((predname, mx), (Attrib.empty_binding, trm)) |
30 val arg = ((predname, mx), (Attrib.empty_binding, trm)) |
31 val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy |
31 val ((_, (_ , thm)), lthy') = Local_Theory.define "" arg lthy |
32 in |
32 in |
33 (thm, lthy') |
33 (thm, lthy') |
34 end*} |
34 end*} |
35 |
35 |
36 text {* |
36 text {* |
37 It returns the definition (as a theorem) and the local theory in which the |
37 It returns the definition (as a theorem) and the local theory in which the |
38 definition has been made. In Line 4, @{ML_ind internalK in Thm} is a flag |
38 definition has been made. In Line 4, the string @{ML "\"\""} is a flag |
39 attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} |
39 attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} |
40 and @{ML_ind axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.} |
40 and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.} |
41 These flags just classify theorems and have no |
41 These flags just classify theorems and have no |
42 significant meaning, except for tools that, for example, find theorems in |
42 significant meaning, except for tools that, for example, find theorems in |
43 the theorem database.\footnote{FIXME: put in the section about theorems.} We |
43 the theorem database.\footnote{FIXME: put in the section about theorems.} We |
44 also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for |
44 also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for |
45 our inductive predicates are not meant to be seen by the user and therefore |
45 our inductive predicates are not meant to be seen by the user and therefore |
46 do not need to have any theorem attributes. A testcase for this function is |
46 do not need to have any theorem attributes. A testcase for this function is |
47 *} |
47 *} |
48 |
48 |
49 local_setup %gray {* fn lthy => |
49 local_setup %gray {* fn lthy => |
959 |
959 |
960 text {* |
960 text {* |
961 We have produced various theorems (definitions, induction principles and |
961 We have produced various theorems (definitions, induction principles and |
962 introduction rules), but apart from the definitions, we have not yet |
962 introduction rules), but apart from the definitions, we have not yet |
963 registered them with the theorem database. This is what the functions |
963 registered them with the theorem database. This is what the functions |
964 @{ML_ind note in LocalTheory} does. |
964 @{ML_ind note in Local_Theory} does. |
965 |
965 |
966 |
966 |
967 For convenience, we use the following |
967 For convenience, we use the following |
968 three wrappers this function: |
968 three wrappers this function: |
969 *} |
969 *} |
970 |
970 |
971 ML{*fun note_many qname ((name, attrs), thms) = |
971 ML{*fun note_many qname ((name, attrs), thms) = |
972 LocalTheory.note Thm.theoremK |
972 Local_Theory.note ((Binding.qualify false qname name, attrs), thms) |
973 ((Binding.qualify false qname name, attrs), thms) |
|
974 |
973 |
975 fun note_single1 qname ((name, attrs), thm) = |
974 fun note_single1 qname ((name, attrs), thm) = |
976 note_many qname ((name, attrs), [thm]) |
975 note_many qname ((name, attrs), [thm]) |
977 |
976 |
978 fun note_single2 name attrs (qname, thm) = |
977 fun note_single2 name attrs (qname, thm) = |