1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{CTLind}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsubsection{CTL Revisited% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:CTL-revisited} |
|
24 \index{CTL|(}% |
|
25 The purpose of this section is twofold: to demonstrate |
|
26 some of the induction principles and heuristics discussed above and to |
|
27 show how inductive definitions can simplify proofs. |
|
28 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a |
|
29 model checker for CTL\@. In particular the proof of the |
|
30 \isa{infinity{\isaliteral{5F}{\isacharunderscore}}lemma} on the way to \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} is not as |
|
31 simple as one might expect, due to the \isa{SOME} operator |
|
32 involved. Below we give a simpler proof of \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} |
|
33 based on an auxiliary inductive definition. |
|
34 |
|
35 Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does |
|
36 not touch any node in the set \isa{A}. Then \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} says |
|
37 that if no infinite path from some state \isa{s} is \isa{A}-avoiding, |
|
38 then \isa{s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. We prove this by inductively defining the set |
|
39 \isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path: |
|
40 % Second proof of opposite direction, directly by well-founded induction |
|
41 % on the initial segment of M that avoids A.% |
|
42 \end{isamarkuptext}% |
|
43 \isamarkuptrue% |
|
44 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
|
45 \isanewline |
|
46 \ \ Avoid\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
47 \ \ \isakeyword{for}\ s\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ state\ \isakeyword{and}\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
48 \isakeyword{where}\isanewline |
|
49 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
50 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}u{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ u\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{22}{\isachardoublequoteclose}}% |
|
51 \begin{isamarkuptext}% |
|
52 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} |
|
53 with \isa{f\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path |
|
54 starting with \isa{s} because (by definition of \isa{Avoid}) there is a |
|
55 finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}. |
|
56 The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A}. However, |
|
57 this requires the following |
|
58 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; |
|
59 the \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} directive undoes the reformulation after the proof.% |
|
60 \end{isamarkuptext}% |
|
61 \isamarkuptrue% |
|
62 \isacommand{lemma}\isamarkupfalse% |
|
63 \ ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
64 \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
|
65 \ \ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}f{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ f\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
66 % |
|
67 \isadelimproof |
|
68 % |
|
69 \endisadelimproof |
|
70 % |
|
71 \isatagproof |
|
72 \isacommand{apply}\isamarkupfalse% |
|
73 {\isaliteral{28}{\isacharparenleft}}erule\ Avoid{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
|
74 \ \isacommand{apply}\isamarkupfalse% |
|
75 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
|
76 \isacommand{apply}\isamarkupfalse% |
|
77 {\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline |
|
78 \isacommand{apply}\isamarkupfalse% |
|
79 {\isaliteral{28}{\isacharparenleft}}drule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ case\ i\ of\ {\isadigit{0}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ t\ {\isaliteral{7C}{\isacharbar}}\ Suc\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ bspec{\isaliteral{29}{\isacharparenright}}\isanewline |
|
80 \isacommand{apply}\isamarkupfalse% |
|
81 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ Paths{\isaliteral{5F}{\isacharunderscore}}def\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}\isanewline |
|
82 \isacommand{done}\isamarkupfalse% |
|
83 % |
|
84 \endisatagproof |
|
85 {\isafoldproof}% |
|
86 % |
|
87 \isadelimproof |
|
88 % |
|
89 \endisadelimproof |
|
90 % |
|
91 \begin{isamarkuptext}% |
|
92 \noindent |
|
93 The base case (\isa{t\ {\isaliteral{3D}{\isacharequal}}\ s}) is trivial and proved by \isa{blast}. |
|
94 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
|
95 starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate |
|
96 the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}f{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ t} in the induction hypothesis by the path starting with |
|
97 \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term |
|
98 expresses. Simplification shows that this is a path starting with \isa{t} |
|
99 and that the instantiated induction hypothesis implies the conclusion. |
|
100 |
|
101 Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding |
|
102 path starts from \isa{s}, we want to show \isa{s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. For the |
|
103 inductive proof this must be generalized to the statement that every point \isa{t} |
|
104 ``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A}, |
|
105 is contained in \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}:% |
|
106 \end{isamarkuptext}% |
|
107 \isamarkuptrue% |
|
108 \isacommand{lemma}\isamarkupfalse% |
|
109 \ Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
110 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
111 \isadelimproof |
|
112 % |
|
113 \endisadelimproof |
|
114 % |
|
115 \isatagproof |
|
116 % |
|
117 \begin{isamarkuptxt}% |
|
118 \noindent |
|
119 The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. |
|
120 If \isa{t} is already in \isa{A}, then \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} is |
|
121 trivial. If \isa{t} is not in \isa{A} but all successors are in |
|
122 \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} (induction hypothesis), then \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} is |
|
123 again trivial. |
|
124 |
|
125 The formal counterpart of this proof sketch is a well-founded induction |
|
126 on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isaliteral{2D}{\isacharminus}}\ A}, roughly speaking: |
|
127 \begin{isabelle}% |
|
128 \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}% |
|
129 \end{isabelle} |
|
130 As we shall see presently, the absence of infinite \isa{A}-avoiding paths |
|
131 starting from \isa{s} implies well-foundedness of this relation. For the |
|
132 moment we assume this and proceed with the induction:% |
|
133 \end{isamarkuptxt}% |
|
134 \isamarkuptrue% |
|
135 \isacommand{apply}\isamarkupfalse% |
|
136 {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}wf{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
137 \ \isacommand{apply}\isamarkupfalse% |
|
138 {\isaliteral{28}{\isacharparenleft}}erule{\isaliteral{5F}{\isacharunderscore}}tac\ a\ {\isaliteral{3D}{\isacharequal}}\ t\ \isakeyword{in}\ wf{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
|
139 \ \isacommand{apply}\isamarkupfalse% |
|
140 {\isaliteral{28}{\isacharparenleft}}clarsimp{\isaliteral{29}{\isacharparenright}}% |
|
141 \begin{isamarkuptxt}% |
|
142 \noindent |
|
143 \begin{isabelle}% |
|
144 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
145 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ }{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
146 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ }y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
147 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
148 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\isanewline |
|
149 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
|
150 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ }wf\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}% |
|
151 \end{isabelle} |
|
152 Now the induction hypothesis states that if \isa{t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A} |
|
153 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in |
|
154 \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. Unfolding \isa{lfp} in the conclusion of the first |
|
155 subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors |
|
156 of \isa{t} are in \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. But if \isa{t} is not in \isa{A}, |
|
157 the second |
|
158 \isa{Avoid}-rule implies that all successors of \isa{t} are in |
|
159 \isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A}. |
|
160 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in |
|
161 \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. Mechanically:% |
|
162 \end{isamarkuptxt}% |
|
163 \isamarkuptrue% |
|
164 \ \isacommand{apply}\isamarkupfalse% |
|
165 {\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}af{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
166 \ \isacommand{apply}\isamarkupfalse% |
|
167 {\isaliteral{28}{\isacharparenleft}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}\ add{\isaliteral{3A}{\isacharcolon}}\ af{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
|
168 \ \isacommand{apply}\isamarkupfalse% |
|
169 {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}% |
|
170 \begin{isamarkuptxt}% |
|
171 Having proved the main goal, we return to the proof obligation that the |
|
172 relation used above is indeed well-founded. This is proved by contradiction: if |
|
173 the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem |
|
174 \isa{wf{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}down{\isaliteral{5F}{\isacharunderscore}}chain}: |
|
175 \begin{isabelle}% |
|
176 \ \ \ \ \ wf\ r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}f{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ f\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
|
177 \end{isabelle} |
|
178 From lemma \isa{ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path} the existence of an infinite |
|
179 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.% |
|
180 \end{isamarkuptxt}% |
|
181 \isamarkuptrue% |
|
182 \isacommand{apply}\isamarkupfalse% |
|
183 {\isaliteral{28}{\isacharparenleft}}erule\ contrapos{\isaliteral{5F}{\isacharunderscore}}pp{\isaliteral{29}{\isacharparenright}}\isanewline |
|
184 \isacommand{apply}\isamarkupfalse% |
|
185 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ wf{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}down{\isaliteral{5F}{\isacharunderscore}}chain{\isaliteral{29}{\isacharparenright}}\isanewline |
|
186 \isacommand{apply}\isamarkupfalse% |
|
187 {\isaliteral{28}{\isacharparenleft}}erule\ exE{\isaliteral{29}{\isacharparenright}}\isanewline |
|
188 \isacommand{apply}\isamarkupfalse% |
|
189 {\isaliteral{28}{\isacharparenleft}}rule\ ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path{\isaliteral{29}{\isacharparenright}}\isanewline |
|
190 \isacommand{apply}\isamarkupfalse% |
|
191 {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ Paths{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
|
192 \isacommand{done}\isamarkupfalse% |
|
193 % |
|
194 \endisatagproof |
|
195 {\isafoldproof}% |
|
196 % |
|
197 \isadelimproof |
|
198 % |
|
199 \endisadelimproof |
|
200 % |
|
201 \begin{isamarkuptext}% |
|
202 The \isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}} modifier of the \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} directive in the |
|
203 statement of the lemma means |
|
204 that the assumption is left unchanged; otherwise the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p} |
|
205 would be turned |
|
206 into a \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}p}, which would complicate matters below. As it is, |
|
207 \isa{Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp} is now |
|
208 \begin{isabelle}% |
|
209 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}% |
|
210 \end{isabelle} |
|
211 The main theorem is simply the corollary where \isa{t\ {\isaliteral{3D}{\isacharequal}}\ s}, |
|
212 when the assumption \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A} is trivially true |
|
213 by the first \isa{Avoid}-rule. Isabelle confirms this:% |
|
214 \index{CTL|)}% |
|
215 \end{isamarkuptext}% |
|
216 \isamarkuptrue% |
|
217 \isacommand{theorem}\isamarkupfalse% |
|
218 \ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
219 % |
|
220 \isadelimproof |
|
221 % |
|
222 \endisadelimproof |
|
223 % |
|
224 \isatagproof |
|
225 \isacommand{by}\isamarkupfalse% |
|
226 {\isaliteral{28}{\isacharparenleft}}auto\ elim{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp\ intro{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}\isanewline |
|
227 \isanewline |
|
228 % |
|
229 \endisatagproof |
|
230 {\isafoldproof}% |
|
231 % |
|
232 \isadelimproof |
|
233 % |
|
234 \endisadelimproof |
|
235 % |
|
236 \isadelimtheory |
|
237 % |
|
238 \endisadelimtheory |
|
239 % |
|
240 \isatagtheory |
|
241 % |
|
242 \endisatagtheory |
|
243 {\isafoldtheory}% |
|
244 % |
|
245 \isadelimtheory |
|
246 % |
|
247 \endisadelimtheory |
|
248 \end{isabellebody}% |
|
249 %%% Local Variables: |
|
250 %%% mode: latex |
|
251 %%% TeX-master: "root" |
|
252 %%% End: |
|