1 (* $Id$ *) |
|
2 |
|
3 theory Proof |
1 theory Proof |
4 imports Main |
2 imports Main |
5 begin |
3 begin |
6 |
4 |
7 chapter {* Proofs *} |
5 chapter {* Proofs \label{ch:proofs} *} |
8 |
6 |
9 text {* |
7 text {* |
10 Proof commands perform transitions of Isar/VM machine |
8 Proof commands perform transitions of Isar/VM machine |
11 configurations, which are block-structured, consisting of a stack of |
9 configurations, which are block-structured, consisting of a stack of |
12 nodes with three main components: logical proof context, current |
10 nodes with three main components: logical proof context, current |
13 facts, and open goals. Isar/VM transitions are \emph{typed} |
11 facts, and open goals. Isar/VM transitions are typed according to |
14 according to the following three different modes of operation: |
12 the following three different modes of operation: |
15 |
13 |
16 \begin{description} |
14 \begin{description} |
17 |
15 |
18 \item @{text "proof(prove)"} means that a new goal has just been |
16 \item @{text "proof(prove)"} means that a new goal has just been |
19 stated that is now to be \emph{proven}; the next command may refine |
17 stated that is now to be \emph{proven}; the next command may refine |
30 just picked up in order to be used when refining the goal claimed |
28 just picked up in order to be used when refining the goal claimed |
31 next. |
29 next. |
32 |
30 |
33 \end{description} |
31 \end{description} |
34 |
32 |
35 The proof mode indicator may be read as a verb telling the writer |
33 The proof mode indicator may be understood as an instruction to the |
36 what kind of operation may be performed next. The corresponding |
34 writer, telling what kind of operation may be performed next. The |
37 typings of proof commands restricts the shape of well-formed proof |
35 corresponding typings of proof commands restricts the shape of |
38 texts to particular command sequences. So dynamic arrangements of |
36 well-formed proof texts to particular command sequences. So dynamic |
39 commands eventually turn out as static texts of a certain structure. |
37 arrangements of commands eventually turn out as static texts of a |
40 \Appref{ap:refcard} gives a simplified grammar of the overall |
38 certain structure. |
41 (extensible) language emerging that way. |
39 |
|
40 \Appref{ap:refcard} gives a simplified grammar of the (extensible) |
|
41 language emerging that way from the different types of proof |
|
42 commands. The main ideas of the overall Isar framework are |
|
43 explained in \chref{ch:isar-framework}. |
42 *} |
44 *} |
43 |
45 |
44 |
46 |
45 section {* Proof structure *} |
47 section {* Proof structure *} |
46 |
48 |
961 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional) |
963 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional) |
962 facts indicated for forward chaining). |
964 facts indicated for forward chaining). |
963 \begin{matharray}{l} |
965 \begin{matharray}{l} |
964 @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex] |
966 @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex] |
965 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
967 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
966 \quad @{command "proof"}~@{text succeed} \\ |
968 \quad @{command "proof"}~@{method succeed} \\ |
967 \qquad @{command "fix"}~@{text thesis} \\ |
969 \qquad @{command "fix"}~@{text thesis} \\ |
968 \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\ |
970 \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\ |
969 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\ |
971 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\ |
970 \quad\qquad @{command "apply"}~@{text -} \\ |
972 \quad\qquad @{command "apply"}~@{text -} \\ |
971 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\ |
973 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\ |