3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 chapter {* First Steps *} |
6 chapter {* First Steps *} |
7 |
7 |
8 text {* |
8 text {* |
|
9 |
9 Isabelle programming is done in Standard ML. |
10 Isabelle programming is done in Standard ML. |
10 Just like lemmas and proofs, code in Isabelle is part of a |
11 Just like lemmas and proofs, code in Isabelle is part of a |
11 theory. If you want to follow the code written in this chapter, we |
12 theory. If you want to follow the code written in this chapter, we |
12 assume you are working inside the theory defined by |
13 assume you are working inside the theory defined by |
13 |
14 |
25 |
26 |
26 text {* |
27 text {* |
27 The easiest and quickest way to include code in a theory is |
28 The easiest and quickest way to include code in a theory is |
28 by using the \isacommand{ML} command. For example\smallskip |
29 by using the \isacommand{ML} command. For example\smallskip |
29 |
30 |
30 \isacommand{ML} |
31 \isa{\isacommand{ML} |
31 @{ML_text "{"}@{ML_text "*"}\isanewline |
32 \isacharverbatimopen\isanewline |
32 \hspace{5mm}@{ML "3 + 4"}\isanewline |
33 \hspace{5mm}@{ML "3 + 4"}\isanewline |
33 @{ML_text "*"}@{ML_text "}"}\isanewline |
34 \isacharverbatimclose\isanewline |
34 @{ML_text "> 7"}\smallskip |
35 @{ML_text "> 7"}\smallskip} |
35 |
36 |
36 Expressions inside \isacommand{ML} commands are immediately evaluated, |
37 Expressions inside \isacommand{ML} commands are immediately evaluated, |
37 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
38 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
38 your Isabelle environment. The code inside the \isacommand{ML} command |
39 your Isabelle environment. The code inside the \isacommand{ML} command |
39 can also contain value and function bindings. However on such \isacommand{ML} |
40 can also contain value and function bindings. However on such \isacommand{ML} |
40 commands the undo operation behaves slightly counter-intuitive, because |
41 commands the undo operation behaves slightly counter-intuitive, because |
41 if you define\smallskip |
42 if you define\smallskip |
42 |
43 |
43 \isacommand{ML} |
44 \isa{\isacommand{ML} |
44 @{ML_text "{"}@{ML_text "*"}\isanewline |
45 \isacharverbatimopen\isanewline |
45 @{ML_text "val foo = true"}\isanewline |
46 \hspace{5mm}@{ML_text "val foo = true"}\isanewline |
46 @{ML_text "*"}@{ML_text "}"}\isanewline |
47 \isacharverbatimclose\isanewline |
47 @{ML_text "> true"}\smallskip |
48 @{ML_text "> true"}\smallskip} |
48 |
49 |
49 then Isabelle's undo operation has no effect on the definition of |
50 then Isabelle's undo operation has no effect on the definition of |
50 @{ML_text "foo"}. Note that from now on we will drop the |
51 @{ML_text "foo"}. Note that from now on we will drop the |
51 \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever |
52 \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever |
52 we show code and its response. |
53 we show code and its response. |
53 |
54 |
54 Once a portion of code is relatively stable, one usually wants to |
55 Once a portion of code is relatively stable, one usually wants to |
55 export it to a separate ML-file. Such files can then be included in a |
56 export it to a separate ML-file. Such files can then be included in a |
56 theory by using \isacommand{uses} in the header of the theory, like |
57 theory by using \isacommand{uses} in the header of the theory, like |
98 @{ML [display] "tracing \"foo\""} |
100 @{ML [display] "tracing \"foo\""} |
99 |
101 |
100 It is also possible to redirect the channel where the @{ML_text "foo"} is |
102 It is also possible to redirect the channel where the @{ML_text "foo"} is |
101 printed to a separate file, e.g. to prevent Proof General from choking on massive |
103 printed to a separate file, e.g. to prevent Proof General from choking on massive |
102 amounts of trace output. This rediretion can be achieved using the code |
104 amounts of trace output. This rediretion can be achieved using the code |
103 *} |
105 |
104 |
106 @{ML_decl [display] |
105 ML {* |
107 "val strip_specials = |
106 val strip_specials = |
108 let |
107 let |
109 fun strip (\"\\^A\" :: _ :: cs) = strip cs |
108 fun strip ("\^A" :: _ :: cs) = strip cs |
110 | strip (c :: cs) = c :: strip cs |
109 | strip (c :: cs) = c :: strip cs |
111 | strip [] = []; |
110 | strip [] = []; |
112 in implode o strip o explode end; |
111 in implode o strip o explode end; |
113 |
112 |
114 fun redirect_tracing stream = |
113 fun redirect_tracing stream = |
115 Output.tracing_fn := (fn s => |
114 Output.tracing_fn := (fn s => |
|
115 (TextIO.output (stream, (strip_specials s)); |
116 (TextIO.output (stream, (strip_specials s)); |
116 TextIO.output (stream, "\n"); |
117 TextIO.output (stream, \"\\n\"); |
117 TextIO.flushOut stream)); |
118 TextIO.flushOut stream));"} |
118 *} |
119 |
119 |
120 Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
120 text {* |
|
121 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
|
122 will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. |
121 will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. |
123 |
122 |
124 *} |
123 *} |
125 |
124 |
126 |
125 |
141 @{ML "Context.theory_name"}. |
140 @{ML "Context.theory_name"}. |
142 |
141 |
143 Note, however, that antiquotations are statically scoped, that is the value is |
142 Note, however, that antiquotations are statically scoped, that is the value is |
144 determined at ``compile-time'', not ``run-time''. For example the function |
143 determined at ``compile-time'', not ``run-time''. For example the function |
145 |
144 |
146 *} |
145 @{ML_decl [display] |
147 |
146 "fun not_current_thyname () = Context.theory_name @{theory}"} |
148 ML {* |
147 |
149 fun not_current_thyname () = Context.theory_name @{theory} |
|
150 *} |
|
151 |
|
152 text {* |
|
153 does \emph{not} return the name of the current theory, if it is run in a |
148 does \emph{not} return the name of the current theory, if it is run in a |
154 different theory. Instead, the code above defines the constant function |
149 different theory. Instead, the code above defines the constant function |
155 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
150 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
156 function is called. Operationally speaking, @{text "@{theory}"} is |
151 function is called. Operationally speaking, @{text "@{theory}"} is |
157 \emph{not} replaced with code that will look up the current theory in |
152 \emph{not} replaced with code that will look up the current theory in |
158 some data structure and return it. Instead, it is literally |
153 some data structure and return it. Instead, it is literally |
159 replaced with the value representing the theory name. |
154 replaced with the value representing the theory name. |
160 |
155 |
161 In a similar way you can use antiquotations to refer to theorems or simpsets: |
156 In a similar way you can use antiquotations to refer to theorems or simpsets: |
162 |
157 |
163 |
|
164 @{ML [display] "@{thm allI}"} |
158 @{ML [display] "@{thm allI}"} |
165 @{ML [display] "@{simpset}"} |
159 @{ML [display] "@{simpset}"} |
166 |
160 |
167 In the course of this introduction, we will learn more about |
161 In the course of this introduction, we will learn more about |
168 these antiquotations: they greatly simplify Isabelle programming since one |
162 these antiquotations: they greatly simplify Isabelle programming since one |
261 While antiquotations are very convenient for constructing terms and types, |
255 While antiquotations are very convenient for constructing terms and types, |
262 they can only construct fixed terms. Unfortunately, one often needs to construct them |
256 they can only construct fixed terms. Unfortunately, one often needs to construct them |
263 dynamically. For example, a function that returns the implication |
257 dynamically. For example, a function that returns the implication |
264 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"} |
258 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"} |
265 as arguments can only be written as |
259 as arguments can only be written as |
266 *} |
260 |
267 |
261 @{ML_decl [display] |
268 |
262 "fun make_imp P Q tau = |
269 ML {* |
|
270 fun make_imp P Q tau = |
|
271 let |
263 let |
272 val x = Free ("x",tau) |
264 val x = Free (\"x\",tau) |
273 in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), |
265 in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), |
274 HOLogic.mk_Trueprop (Q $ x))) |
266 HOLogic.mk_Trueprop (Q $ x))) |
275 end |
267 end"} |
276 *} |
|
277 |
|
278 text {* |
|
279 |
268 |
280 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
269 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
281 @{term "tau"} into an antiquotation. For example the following does not work. |
270 @{term "tau"} into an antiquotation. For example the following does not work. |
282 *} |
271 |
283 |
272 @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\<And>x. P x \<Longrightarrow> Q x\"}"} |
284 ML {* |
|
285 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
|
286 *} |
|
287 |
|
288 text {* |
|
289 |
273 |
290 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
274 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
291 to both functions. |
275 to both functions. |
292 |
276 |
293 One tricky point in constructing terms by hand is to obtain the |
277 One tricky point in constructing terms by hand is to obtain the |
395 text {* |
379 text {* |
396 on the ML level:\footnote{Note that @{text "|>"} is reverse |
380 on the ML level:\footnote{Note that @{text "|>"} is reverse |
397 application. This combinator, and several variants are defined in |
381 application. This combinator, and several variants are defined in |
398 @{ML_file "Pure/General/basics.ML"}.} |
382 @{ML_file "Pure/General/basics.ML"}.} |
399 |
383 |
400 *} |
384 @{ML_response_fake [display] |
401 |
385 "let |
402 ML {* |
|
403 let |
|
404 val thy = @{theory} |
386 val thy = @{theory} |
405 |
387 |
406 val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} |
388 val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"} |
407 val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"} |
389 val assm2 = cterm_of thy @{prop \"((P::nat\<Rightarrow>bool) t)\"} |
408 |
390 |
409 val Pt_implies_Qt = |
391 val Pt_implies_Qt = |
410 assume assm1 |
392 assume assm1 |
411 |> forall_elim (cterm_of thy @{term "t::nat"}); |
393 |> forall_elim (cterm_of thy @{term \"t::nat\"}); |
412 |
394 |
413 val Qt = implies_elim Pt_implies_Qt (assume assm2); |
395 val Qt = implies_elim Pt_implies_Qt (assume assm2); |
414 in |
396 in |
415 |
397 |
416 Qt |
398 Qt |
417 |> implies_intr assm2 |
399 |> implies_intr assm2 |
418 |> implies_intr assm1 |
400 |> implies_intr assm1 |
419 end |
401 end" "(FIXME)"} |
420 *} |
|
421 |
|
422 text {* |
|
423 |
402 |
424 This code-snippet constructs the following proof: |
403 This code-snippet constructs the following proof: |
425 |
404 |
426 \[ |
405 \[ |
427 \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}} |
406 \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}} |
505 up a goal state for proving the goal @{text C} under the assumptions @{text As} |
484 up a goal state for proving the goal @{text C} under the assumptions @{text As} |
506 (empty in the proof at hand) |
485 (empty in the proof at hand) |
507 with the variables @{text xs} that will be generalised once the |
486 with the variables @{text xs} that will be generalised once the |
508 goal is proved. The @{text "tac"} is the tactic which proves the goal and which |
487 goal is proved. The @{text "tac"} is the tactic which proves the goal and which |
509 can make use of the local assumptions. |
488 can make use of the local assumptions. |
510 *} |
489 |
511 |
490 @{ML_response_fake [display] |
512 |
491 "let |
513 |
|
514 ML {* |
|
515 let |
|
516 val ctxt = @{context} |
492 val ctxt = @{context} |
517 val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} |
493 val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"} |
518 in |
494 in |
519 Goal.prove ctxt ["P", "Q"] [] goal (fn _ => |
495 Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => |
520 eresolve_tac [disjE] 1 |
496 eresolve_tac [disjE] 1 |
521 THEN resolve_tac [disjI2] 1 |
497 THEN resolve_tac [disjI2] 1 |
522 THEN assume_tac 1 |
498 THEN assume_tac 1 |
523 THEN resolve_tac [disjI1] 1 |
499 THEN resolve_tac [disjI1] 1 |
524 THEN assume_tac 1) |
500 THEN assume_tac 1) |
525 end |
501 end" "(FIXME)"} |
526 *} |
|
527 |
|
528 text {* |
|
529 |
502 |
530 \begin{readmore} |
503 \begin{readmore} |
531 To learn more about the function @{ML Goal.prove} see \isccite{sec:results}. |
504 To learn more about the function @{ML Goal.prove} see \isccite{sec:results}. |
532 \end{readmore} |
505 \end{readmore} |
533 |
506 |
534 *} |
507 |
535 |
508 An alternative way to transcribe this proof is as follows |
536 |
509 |
537 text {* An alternative way to transcribe this proof is as follows *} |
510 @{ML_response_fake [display] |
538 |
511 "let |
539 ML {* |
|
540 let |
|
541 val ctxt = @{context} |
512 val ctxt = @{context} |
542 val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} |
513 val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"} |
543 in |
514 in |
544 Goal.prove ctxt ["P", "Q"] [] goal (fn _ => |
515 Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => |
545 (eresolve_tac [disjE] |
516 (eresolve_tac [disjE] |
546 THEN' resolve_tac [disjI2] |
517 THEN' resolve_tac [disjI2] |
547 THEN' assume_tac |
518 THEN' assume_tac |
548 THEN' resolve_tac [disjI1] |
519 THEN' resolve_tac [disjI1] |
549 THEN' assume_tac) 1) |
520 THEN' assume_tac) 1) |
|
521 end" "(FIXME)"} |
|
522 |
|
523 (FIXME: are there any advantages/disadvantages about this way?) |
|
524 *} |
|
525 |
|
526 section {* Storing Theorems *} |
|
527 |
|
528 section {* Theorem Attributes *} |
|
529 |
|
530 |
|
531 |
|
532 |
550 end |
533 end |
551 *} |
|
552 |
|
553 text {* (FIXME: are there any advantages/disadvantages about this way?) *} |
|
554 |
|
555 section {* Storing Theorems *} |
|
556 |
|
557 section {* Theorem Attributes *} |
|
558 |
|
559 |
|
560 |
|
561 |
|
562 end |
|