41 In the most basic form, interpretation just replaces the locale |
41 In the most basic form, interpretation just replaces the locale |
42 parameters by terms. The following command interprets the locale |
42 parameters by terms. The following command interprets the locale |
43 @{text partial_order} in the global context of the theory. The |
43 @{text partial_order} in the global context of the theory. The |
44 parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *} |
44 parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *} |
45 |
45 |
46 interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
46 interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
47 txt {* The locale name is succeeded by a \emph{parameter |
47 txt {* The locale name is succeeded by a \emph{parameter |
48 instantiation}. In general, this is a list of terms, which refer to |
48 instantiation}. This is a list of terms, which refer to |
49 the parameters in the order of declaration in the locale. The |
49 the parameters in the order of declaration in the locale. The |
50 locale name is preceded by an optional \emph{interpretation prefix}, |
50 locale name is preceded by an optional \emph{interpretation |
51 which is used to qualify names from the locale in the global |
51 qualifier}. |
52 context. |
|
53 |
52 |
54 The command creates the goal% |
53 The command creates the goal% |
55 \footnote{Note that @{text op} binds tighter than functions |
54 \footnote{Note that @{text op} binds tighter than functions |
56 application: parentheses around @{text "op \<le>"} are not necessary.} |
55 application: parentheses around @{text "op \<le>"} are not necessary.} |
57 @{subgoals [display]} which can be shown easily: |
56 @{subgoals [display]} which can be shown easily: |
60 |
59 |
61 text {* Now theorems from the locale are available in the theory, |
60 text {* Now theorems from the locale are available in the theory, |
62 interpreted for natural numbers, for example @{thm [source] |
61 interpreted for natural numbers, for example @{thm [source] |
63 nat.trans}: @{thm [display, indent=2] nat.trans} |
62 nat.trans}: @{thm [display, indent=2] nat.trans} |
64 |
63 |
65 Interpretation accepts a qualifier, @{text nat} in the example, |
64 The interpretation qualifier, @{text nat} in the example, is applied |
66 which is applied to all names processed by the interpretation. If |
65 to all names processed by the interpretation. If a qualifer is |
67 followed by an exclamation point the qualifier is mandatory --- that |
66 given in the \isakeyword{interpretation} command, its use is |
68 is, the above theorem cannot be referred to simply by @{text trans}. |
67 mandatory when referencing the name. For example, the above theorem |
69 A qualifier succeeded by an exclamation point is called |
68 cannot be referred to simply by @{text trans}. This prevents |
70 \emph{strict}. It prevents unwanted hiding of theorems. It is |
69 unwanted hiding of theorems. *} |
71 advisable to use strict qualifiers for all interpretations in |
|
72 theories. *} |
|
73 |
70 |
74 |
71 |
75 subsection {* Second Version: Replacement of Definitions *} |
72 subsection {* Second Version: Replacement of Definitions *} |
76 |
73 |
77 text {* The above interpretation also creates the theorem |
74 text {* The above interpretation also creates the theorem |