57 \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term |
57 \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term |
58 expresses. Simplification shows that this is a path starting with \isa{t} |
58 expresses. Simplification shows that this is a path starting with \isa{t} |
59 and that the instantiated induction hypothesis implies the conclusion. |
59 and that the instantiated induction hypothesis implies the conclusion. |
60 |
60 |
61 Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding |
61 Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding |
62 path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. This |
62 path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the |
63 can be generalized by proving that every point \isa{t} ``between'' |
63 inductive proof this must be generalized to the statement that every point \isa{t} |
64 \isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A}, |
64 ``between'' \isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A}, |
65 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
65 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
66 \end{isamarkuptext}% |
66 \end{isamarkuptext}% |
67 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
67 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
68 \ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% |
68 \ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% |
69 \begin{isamarkuptxt}% |
69 \begin{isamarkuptxt}% |
77 The formal counterpart of this proof sketch is a well-founded induction |
77 The formal counterpart of this proof sketch is a well-founded induction |
78 w.r.t.\ \isa{M} restricted to (roughly speaking) \isa{Avoid\ s\ A\ {\isacharminus}\ A}: |
78 w.r.t.\ \isa{M} restricted to (roughly speaking) \isa{Avoid\ s\ A\ {\isacharminus}\ A}: |
79 \begin{isabelle}% |
79 \begin{isabelle}% |
80 \ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% |
80 \ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% |
81 \end{isabelle} |
81 \end{isabelle} |
82 As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths |
82 As we shall see presently, the absence of infinite \isa{A}-avoiding paths |
83 starting from \isa{s} implies well-foundedness of this relation. For the |
83 starting from \isa{s} implies well-foundedness of this relation. For the |
84 moment we assume this and proceed with the induction:% |
84 moment we assume this and proceed with the induction:% |
85 \end{isamarkuptxt}% |
85 \end{isamarkuptxt}% |
86 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline |
86 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline |
87 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
87 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |