10 Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ |
10 Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ |
11 24~Nov.~2009 |
11 24~Nov.~2009 |
12 \end{flushright} |
12 \end{flushright} |
13 |
13 |
14 \medskip |
14 \medskip |
15 Isabelle is build around a few central ideas. One central idea is the |
15 Isabelle is built around a few central ideas. One central idea is the |
16 LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there |
16 LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there |
17 is a small trusted core and everything else is built on top of this trusted |
17 is a small trusted core and everything else is built on top of this trusted |
18 core. The fundamental data structures involved in this core are certified |
18 core. The fundamental data structures involved in this core are certified |
19 terms and certified types, as well as theorems. |
19 terms and certified types, as well as theorems. |
20 *} |
20 *} |
45 | Abs of string * typ * term |
45 | Abs of string * typ * term |
46 | $ of term * term *} |
46 | $ of term * term *} |
47 |
47 |
48 text {* |
48 text {* |
49 This datatype implements Church-style lambda-terms, where types are |
49 This datatype implements Church-style lambda-terms, where types are |
50 explicitly recorded in variables, constants and abstractions. As can be |
50 explicitly recorded in variables, constants and abstractions. The |
51 seen in Line 5, terms use the usual de Bruijn index mechanism for |
51 important point of having terms is that you can pattern-match against them; |
52 representing bound variables. For example in |
52 this cannot be done with certified terms. As can be seen in Line 5, |
|
53 terms use the usual de Bruijn index mechanism for representing bound |
|
54 variables. For example in |
53 |
55 |
54 @{ML_response_fake [display, gray] |
56 @{ML_response_fake [display, gray] |
55 "@{term \"\<lambda>x y. x y\"}" |
57 "@{term \"\<lambda>x y. x y\"}" |
56 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} |
58 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} |
57 |
59 |
76 This is one common source for puzzlement in Isabelle, which has |
78 This is one common source for puzzlement in Isabelle, which has |
77 tacitly eta-contracted the output. You obtain a similar result |
79 tacitly eta-contracted the output. You obtain a similar result |
78 with beta-redexes |
80 with beta-redexes |
79 |
81 |
80 @{ML_response_fake [display, gray] |
82 @{ML_response_fake [display, gray] |
81 "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"} |
83 "let |
82 |> pretty_term @{context} |
84 val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} |
83 |> pwriteln" |
85 val arg1 = @{term \"1::int\"} |
|
86 val arg2 = @{term \"2::int\"} |
|
87 in |
|
88 pretty_term @{context} (redex $ arg1 $ arg2) |
|
89 |> pwriteln |
|
90 end" |
84 "1"} |
91 "1"} |
85 |
92 |
86 There is a dedicated configuration value for switching off the tacit |
93 There is a dedicated configuration value for switching off tacit |
87 eta-contraction, namely @{ML_ind eta_contract in Syntax} (see Section |
94 eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section |
88 \ref{sec:printing}), but none for beta-contractions. However you can avoid |
95 \ref{sec:printing}), but none for beta-contractions. However you can avoid |
89 the beta-contractions by switching off abbreviation using the configuration |
96 the beta-contractions by switching off abbreviations using the configuration |
90 value @{ML_ind show_abbrevs in Syntax}. For example |
97 value @{ML_ind show_abbrevs in Syntax}. For example |
91 |
98 |
92 |
99 |
93 @{ML_response_fake [display, gray] |
100 @{ML_response_fake [display, gray] |
94 "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"} |
101 "let |
95 |> pretty_term (Config.put show_abbrevs false @{context}) |
102 val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} |
96 |> pwriteln" |
103 val arg1 = @{term \"1::int\"} |
|
104 val arg2 = @{term \"2::int\"} |
|
105 val ctxt = Config.put show_abbrevs false @{context} |
|
106 in |
|
107 pretty_term ctxt (redex $ arg1 $ arg2) |
|
108 |> pwriteln |
|
109 end" |
97 "(\<lambda>x y. x) 1 2"} |
110 "(\<lambda>x y. x) 1 2"} |
98 |
111 |
99 Isabelle makes a distinction between \emph{free} variables (term-constructor |
112 Isabelle makes a distinction between \emph{free} variables (term-constructor |
100 @{ML Free} and written on the user level in blue colour) and |
113 @{ML Free} and written on the user level in blue colour) and |
101 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
114 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
193 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
206 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
194 |
207 |
195 The corresponding datatype is |
208 The corresponding datatype is |
196 *} |
209 *} |
197 |
210 |
198 ML_val{*datatype typ = |
211 ML_val %grayML{*datatype typ = |
199 Type of string * typ list |
212 Type of string * typ list |
200 | TFree of string * sort |
213 | TFree of string * sort |
201 | TVar of indexname * sort *} |
214 | TVar of indexname * sort *} |
202 |
215 |
203 text {* |
216 text {* |