16 which stands for "always in the future": |
16 which stands for "always in the future": |
17 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy |
17 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy |
18 in HOL: it is simply a function from \isa{nat} to \isa{state}.% |
18 in HOL: it is simply a function from \isa{nat} to \isa{state}.% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline |
20 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline |
21 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}% |
21 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}% |
22 \begin{isamarkuptext}% |
22 \begin{isamarkuptext}% |
23 \noindent |
23 \noindent |
24 This definition allows a very succinct statement of the semantics of \isa{AF}: |
24 This definition allows a very succinct statement of the semantics of \isa{AF}: |
25 \footnote{Do not be mislead: neither datatypes nor recursive functions can be |
25 \footnote{Do not be mislead: neither datatypes nor recursive functions can be |
26 extended by new constructors or equations. This is just a trick of the |
26 extended by new constructors or equations. This is just a trick of the |
52 \begin{isamarkuptext}% |
52 \begin{isamarkuptext}% |
53 All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}} |
53 All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}} |
54 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting |
54 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting |
55 with the easy one:% |
55 with the easy one:% |
56 \end{isamarkuptext}% |
56 \end{isamarkuptext}% |
57 \isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{1}{\isacharcolon}\isanewline |
57 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline |
58 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
58 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
59 \begin{isamarkuptxt}% |
59 \begin{isamarkuptxt}% |
60 \noindent |
60 \noindent |
61 The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed |
61 The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed |
62 by simplification and clarification% |
62 by simplification and clarification% |
74 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
74 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
76 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline |
76 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline |
77 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
77 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
78 \end{isabelle} |
78 \end{isabelle} |
79 Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:% |
79 Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:% |
80 \end{isamarkuptxt}% |
80 \end{isamarkuptxt}% |
81 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline |
81 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline |
82 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}% |
82 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}% |
83 \begin{isamarkuptxt}% |
83 \begin{isamarkuptxt}% |
84 \noindent |
84 \noindent |
85 In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:% |
85 In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:% |
86 \end{isamarkuptxt}% |
86 \end{isamarkuptxt}% |
87 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline |
87 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline |
88 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% |
88 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% |
89 \begin{isamarkuptxt}% |
89 \begin{isamarkuptxt}% |
90 \begin{isabelle} |
90 \begin{isabelle} |
91 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline |
91 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline |
92 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
92 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
93 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline |
93 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline |
94 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
94 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
95 \end{isabelle} |
95 \end{isabelle} |
96 It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ \isadigit{1}{\isacharparenright}}, i.e.\ \isa{p} without its |
96 It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its |
97 first element. The rest is practically automatic:% |
97 first element. The rest is practically automatic:% |
98 \end{isamarkuptxt}% |
98 \end{isamarkuptxt}% |
99 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline |
99 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline |
100 \isacommand{apply}\ simp\isanewline |
100 \isacommand{apply}\ simp\isanewline |
101 \isacommand{apply}\ blast\isanewline |
101 \isacommand{apply}\ blast\isanewline |
102 \isacommand{done}% |
102 \isacommand{done}% |
103 \begin{isamarkuptext}% |
103 \begin{isamarkuptext}% |
104 The opposite containment is proved by contradiction: if some state |
104 The opposite containment is proved by contradiction: if some state |
127 Now we iterate this process. The following construction of the desired |
127 Now we iterate this process. The following construction of the desired |
128 path is parameterized by a predicate \isa{P} that should hold along the path:% |
128 path is parameterized by a predicate \isa{P} that should hold along the path:% |
129 \end{isamarkuptext}% |
129 \end{isamarkuptext}% |
130 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline |
130 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline |
131 \isacommand{primrec}\isanewline |
131 \isacommand{primrec}\isanewline |
132 {\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline |
132 {\isachardoublequote}path\ s\ P\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline |
133 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}% |
133 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}% |
134 \begin{isamarkuptext}% |
134 \begin{isamarkuptext}% |
135 \noindent |
135 \noindent |
136 Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor |
136 Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor |
137 \isa{t} of element \isa{n} such that \isa{P\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t} |
137 \isa{t} of element \isa{n} such that \isa{P\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t} |
138 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of |
138 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of |
139 course, such a \isa{t} may in general not exist, but that is of no |
139 course, such a \isa{t} may in general not exist, but that is of no |
140 concern to us since we will only use \isa{path} in such cases where a |
140 concern to us since we will only use \isa{path} in such cases where a |
141 suitable \isa{t} does exist. |
141 suitable \isa{t} does exist. |
182 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline |
182 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline |
183 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M |
183 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M |
184 \end{isabelle} |
184 \end{isabelle} |
185 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} |
185 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} |
186 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning |
186 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning |
187 is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}: |
187 is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: |
188 \begin{isabelle}% |
188 \begin{isabelle}% |
189 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}% |
189 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}% |
190 \end{isabelle} |
190 \end{isabelle} |
191 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes |
191 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes |
192 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove |
192 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove |
193 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and |
193 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and |
194 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that |
194 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that |
195 \isa{fast} can prove the base case quickly:% |
195 \isa{fast} can prove the base case quickly:% |
196 \end{isamarkuptxt}% |
196 \end{isamarkuptxt}% |
197 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}% |
197 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}% |
198 \begin{isamarkuptxt}% |
198 \begin{isamarkuptxt}% |
199 \noindent |
199 \noindent |
200 What is worth noting here is that we have used \isa{fast} rather than \isa{blast}. |
200 What is worth noting here is that we have used \isa{fast} rather than \isa{blast}. |
201 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}: |
201 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: |
202 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic |
202 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic |
203 variables. For efficiency reasons \isa{blast} does not even attempt such unifications. |
203 variables. For efficiency reasons \isa{blast} does not even attempt such unifications. |
204 Although \isa{fast} can in principle cope with complicated unification problems, in practice |
204 Although \isa{fast} can in principle cope with complicated unification problems, in practice |
205 the number of unifiers arising is often prohibitive and the offending rule may need to be applied |
205 the number of unifiers arising is often prohibitive and the offending rule may need to be applied |
206 explicitly rather than automatically. |
206 explicitly rather than automatically. |
207 |
207 |
208 The induction step is similar, but more involved, because now we face nested occurrences of |
208 The induction step is similar, but more involved, because now we face nested occurrences of |
209 \isa{SOME}. We merely show the proof commands but do not describe th details:% |
209 \isa{SOME}. We merely show the proof commands but do not describe th details:% |
210 \end{isamarkuptxt}% |
210 \end{isamarkuptxt}% |
211 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
211 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
212 \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline |
212 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline |
213 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
213 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
214 \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline |
214 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline |
215 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
215 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
216 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
216 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
217 \isacommand{done}% |
217 \isacommand{done}% |
218 \begin{isamarkuptext}% |
218 \begin{isamarkuptext}% |
219 Function \isa{path} has fulfilled its purpose now and can be forgotten |
219 Function \isa{path} has fulfilled its purpose now and can be forgotten |
228 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining |
228 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining |
229 equations we omit.% |
229 equations we omit.% |
230 \end{isamarkuptext}% |
230 \end{isamarkuptext}% |
231 % |
231 % |
232 \begin{isamarkuptext}% |
232 \begin{isamarkuptext}% |
233 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:% |
233 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:% |
234 \end{isamarkuptext}% |
234 \end{isamarkuptext}% |
235 \isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline |
235 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline |
236 {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% |
236 {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% |
237 \begin{isamarkuptxt}% |
237 \begin{isamarkuptxt}% |
238 \noindent |
238 \noindent |
239 The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule |
239 The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule |
240 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):% |
240 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):% |
241 \end{isamarkuptxt}% |
241 \end{isamarkuptxt}% |
242 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
242 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
243 \isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline |
243 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline |
244 \isacommand{apply}\ simp% |
244 \isacommand{apply}\ simp% |
245 \begin{isamarkuptxt}% |
245 \begin{isamarkuptxt}% |
246 \begin{isabelle} |
246 \begin{isabelle} |
247 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A |
247 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A |
248 \end{isabelle} |
248 \end{isabelle} |
260 \end{isamarkuptxt}% |
260 \end{isamarkuptxt}% |
261 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline |
261 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline |
262 \isacommand{done}% |
262 \isacommand{done}% |
263 \begin{isamarkuptext}% |
263 \begin{isamarkuptext}% |
264 The main theorem is proved as for PDL, except that we also derive the necessary equality |
264 The main theorem is proved as for PDL, except that we also derive the necessary equality |
265 \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma\isadigit{1}} and \isa{AF{\isacharunderscore}lemma\isadigit{2}} |
265 \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} |
266 on the spot:% |
266 on the spot:% |
267 \end{isamarkuptext}% |
267 \end{isamarkuptext}% |
268 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline |
268 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline |
269 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline |
269 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline |
270 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline |
270 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline |
271 \isacommand{done}% |
271 \isacommand{done}% |
272 \begin{isamarkuptext}% |
272 \begin{isamarkuptext}% |
273 The above language is not quite CTL. The latter also includes an |
273 The above language is not quite CTL. The latter also includes an |
274 until-operator, which is the subject of the following exercise. |
274 until-operator, which is the subject of the following exercise. |
275 It is not definable in terms of the other operators! |
275 It is not definable in terms of the other operators! |