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') = Local_Theory.define "" 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, the string @{ML "\"\""} is a flag |
38 definition has been made. We use @{ML_ind empty_binding in Attrib} in Line 3, |
39 attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} |
39 since the definitions for our inductive predicates are not meant to be seen |
40 and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.} |
40 by the user and therefore do not need to have any theorem attributes. |
41 These flags just classify theorems and have no |
41 |
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 |
|
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 |
|
46 do not need to have any theorem attributes. A testcase for this function is |
|
47 *} |
|
48 |
|
49 local_setup %gray {* fn lthy => |
|
50 let |
|
51 val arg = ((@{binding "My_True"}, NoSyn), @{term True}) |
|
52 val (def, lthy') = make_defn arg lthy |
|
53 in |
|
54 tracing (string_of_thm_no_vars lthy' def); lthy' |
|
55 end *} |
|
56 |
|
57 text {* |
|
58 which introduces the definition @{thm My_True_def} and then prints it out. |
|
59 Since we are testing the function inside \isacommand{local\_setup}, i.e., make |
|
60 actual changes to the ambient theory, we can query the definition with the usual |
|
61 command \isacommand{thm}: |
|
62 |
|
63 \begin{isabelle} |
|
64 \isacommand{thm}~@{thm [source] "My_True_def"}\\ |
|
65 @{text ">"}~@{thm "My_True_def"} |
|
66 \end{isabelle} |
|
67 |
|
68 The next two functions construct the right-hand sides of the definitions, |
42 The next two functions construct the right-hand sides of the definitions, |
69 which are terms whose general form is: |
43 which are terms whose general form is: |
70 |
44 |
71 @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
45 @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
72 |
46 |