48 \isamarkuptrue% |
48 \isamarkuptrue% |
49 \isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
49 \isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
50 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline |
50 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline |
51 \ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline |
51 \ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline |
52 \isamarkupfalse% |
52 \isamarkupfalse% |
53 \isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline |
|
54 \ \isamarkupfalse% |
|
55 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
|
56 \isamarkupfalse% |
53 \isamarkupfalse% |
57 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
58 \isamarkupfalse% |
54 \isamarkupfalse% |
59 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline |
|
60 \isamarkupfalse% |
55 \isamarkupfalse% |
61 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline |
|
62 \isamarkupfalse% |
56 \isamarkupfalse% |
63 \isacommand{done}\isamarkupfalse% |
57 \isamarkupfalse% |
|
58 \isamarkupfalse% |
64 % |
59 % |
65 \begin{isamarkuptext}% |
60 \begin{isamarkuptext}% |
66 \noindent |
61 \noindent |
67 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}. |
62 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}. |
68 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
63 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
79 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
74 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
80 \end{isamarkuptext}% |
75 \end{isamarkuptext}% |
81 \isamarkuptrue% |
76 \isamarkuptrue% |
82 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
77 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
83 \ \ {\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}\isamarkupfalse% |
78 \ \ {\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}\isamarkupfalse% |
84 % |
|
85 \begin{isamarkuptxt}% |
|
86 \noindent |
|
87 The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. |
|
88 If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is |
|
89 trivial. If \isa{t} is not in \isa{A} but all successors are in |
|
90 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is |
|
91 again trivial. |
|
92 |
|
93 The formal counterpart of this proof sketch is a well-founded induction |
|
94 on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking: |
|
95 \begin{isabelle}% |
|
96 \ \ \ \ \ {\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}% |
|
97 \end{isabelle} |
|
98 As we shall see presently, the absence of infinite \isa{A}-avoiding paths |
|
99 starting from \isa{s} implies well-foundedness of this relation. For the |
|
100 moment we assume this and proceed with the induction:% |
|
101 \end{isamarkuptxt}% |
|
102 \isamarkuptrue% |
79 \isamarkuptrue% |
103 \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 |
|
104 \ \isamarkupfalse% |
|
105 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
106 \ \isamarkupfalse% |
|
107 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% |
|
108 \isamarkupfalse% |
80 \isamarkupfalse% |
109 % |
81 \isamarkupfalse% |
110 \begin{isamarkuptxt}% |
82 \isamarkupfalse% |
111 \noindent |
83 \isamarkupfalse% |
112 \begin{isabelle}% |
|
113 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline |
|
114 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline |
|
115 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline |
|
116 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline |
|
117 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline |
|
118 \ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline |
|
119 \isaindent{\ {\isadigit{2}}{\isachardot}\ }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}% |
|
120 \end{isabelle} |
|
121 Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A} |
|
122 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in |
|
123 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first |
|
124 subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors |
|
125 of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. But if \isa{t} is not in \isa{A}, |
|
126 the second |
|
127 \isa{Avoid}-rule implies that all successors of \isa{t} are in |
|
128 \isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}. |
|
129 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in |
|
130 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% |
|
131 \end{isamarkuptxt}% |
|
132 \ \isamarkuptrue% |
|
133 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline |
|
134 \ \isamarkupfalse% |
|
135 \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline |
|
136 \ \isamarkupfalse% |
|
137 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse% |
|
138 % |
|
139 \begin{isamarkuptxt}% |
|
140 Having proved the main goal, we return to the proof obligation that the |
|
141 relation used above is indeed well-founded. This is proved by contradiction: if |
|
142 the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem |
|
143 \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: |
|
144 \begin{isabelle}% |
|
145 \ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}% |
|
146 \end{isabelle} |
|
147 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite |
|
148 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.% |
|
149 \end{isamarkuptxt}% |
|
150 \isamarkuptrue% |
84 \isamarkuptrue% |
151 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline |
|
152 \isamarkupfalse% |
85 \isamarkupfalse% |
153 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline |
|
154 \isamarkupfalse% |
86 \isamarkupfalse% |
155 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
156 \isamarkupfalse% |
87 \isamarkupfalse% |
157 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline |
88 \isamarkuptrue% |
158 \isamarkupfalse% |
89 \isamarkupfalse% |
159 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline |
|
160 \isamarkupfalse% |
90 \isamarkupfalse% |
161 \isacommand{done}\isamarkupfalse% |
91 \isamarkupfalse% |
|
92 \isamarkupfalse% |
|
93 \isamarkupfalse% |
|
94 \isamarkupfalse% |
162 % |
95 % |
163 \begin{isamarkuptext}% |
96 \begin{isamarkuptext}% |
164 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the |
97 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the |
165 statement of the lemma means |
98 statement of the lemma means |
166 that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p} |
99 that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p} |