71 |
71 |
72 Isabelle automatically computes the type of each variable in a term. This is |
72 Isabelle automatically computes the type of each variable in a term. This is |
73 called \concept{type inference}. Despite type inference, it is sometimes |
73 called \concept{type inference}. Despite type inference, it is sometimes |
74 necessary to attach an explicit \concept{type constraint} (or \concept{type |
74 necessary to attach an explicit \concept{type constraint} (or \concept{type |
75 annotation}) to a variable or term. The syntax is @{text "t :: \<tau>"} as in |
75 annotation}) to a variable or term. The syntax is @{text "t :: \<tau>"} as in |
76 \mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be |
76 \mbox{\noquotes{@{term[source] "m + (n::nat)"}}}. Type constraints may be |
77 needed to |
77 needed to |
78 disambiguate terms involving overloaded functions such as @{text "+"}, @{text |
78 disambiguate terms involving overloaded functions such as @{text "+"}. |
79 "*"} and @{text"\<le>"}. |
|
80 |
79 |
81 Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication |
80 Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication |
82 @{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic |
81 @{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic |
83 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and |
82 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and |
84 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become |
83 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become |
98 \subsection{Theories} |
97 \subsection{Theories} |
99 \label{sec:Basic:Theories} |
98 \label{sec:Basic:Theories} |
100 |
99 |
101 Roughly speaking, a \concept{theory} is a named collection of types, |
100 Roughly speaking, a \concept{theory} is a named collection of types, |
102 functions, and theorems, much like a module in a programming language. |
101 functions, and theorems, much like a module in a programming language. |
103 All the Isabelle text that you ever type needs to go into a theory. |
102 All Isabelle text needs to go into a theory. |
104 The general format of a theory @{text T} is |
103 The general format of a theory @{text T} is |
105 \begin{quote} |
104 \begin{quote} |
106 \indexed{\isacom{theory}}{theory} @{text T}\\ |
105 \indexed{\isacom{theory}}{theory} @{text T}\\ |
107 \indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ |
106 \indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ |
108 \isacom{begin}\\ |
107 \isacom{begin}\\ |