24 then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set |
26 then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set |
25 \isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path: |
27 \isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path: |
26 % Second proof of opposite direction, directly by well-founded induction |
28 % Second proof of opposite direction, directly by well-founded induction |
27 % on the initial segment of M that avoids A.% |
29 % on the initial segment of M that avoids A.% |
28 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
|
31 \isamarkuptrue% |
29 \isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline |
32 \isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline |
|
33 \isamarkupfalse% |
30 \isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline |
34 \isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline |
31 \isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline |
35 \isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline |
32 \ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}% |
36 \ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isamarkupfalse% |
|
37 % |
33 \begin{isamarkuptext}% |
38 \begin{isamarkuptext}% |
34 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} |
39 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} |
35 with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path |
40 with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path |
36 starting with \isa{s} because (by definition of \isa{Avoid}) there is a |
41 starting with \isa{s} because (by definition of \isa{Avoid}) there is a |
37 finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}. |
42 finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}. |
38 The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However, |
43 The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However, |
39 this requires the following |
44 this requires the following |
40 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; |
45 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; |
41 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.% |
46 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.% |
42 \end{isamarkuptext}% |
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
43 \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 |
44 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline |
50 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline |
45 \ \ \ {\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% |
46 \isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline |
53 \isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline |
47 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
54 \ \isamarkupfalse% |
|
55 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
|
56 \isamarkupfalse% |
48 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
57 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
58 \isamarkupfalse% |
49 \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 |
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% |
50 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline |
61 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline |
51 \isacommand{done}% |
62 \isamarkupfalse% |
|
63 \isacommand{done}\isamarkupfalse% |
|
64 % |
52 \begin{isamarkuptext}% |
65 \begin{isamarkuptext}% |
53 \noindent |
66 \noindent |
54 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}. |
67 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}. |
55 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
68 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
56 starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate |
69 starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate |
63 path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the |
76 path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the |
64 inductive proof this must be generalized to the statement that every point \isa{t} |
77 inductive proof this must be generalized to the statement that every point \isa{t} |
65 ``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A}, |
78 ``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A}, |
66 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
79 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:% |
67 \end{isamarkuptext}% |
80 \end{isamarkuptext}% |
|
81 \isamarkuptrue% |
68 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
82 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
69 \ \ {\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}% |
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% |
|
84 % |
70 \begin{isamarkuptxt}% |
85 \begin{isamarkuptxt}% |
71 \noindent |
86 \noindent |
72 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}}. |
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}}. |
73 If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is |
88 If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is |
74 trivial. If \isa{t} is not in \isa{A} but all successors are in |
89 trivial. If \isa{t} is not in \isa{A} but all successors are in |
82 \end{isabelle} |
97 \end{isabelle} |
83 As we shall see presently, the absence of infinite \isa{A}-avoiding paths |
98 As we shall see presently, the absence of infinite \isa{A}-avoiding paths |
84 starting from \isa{s} implies well-foundedness of this relation. For the |
99 starting from \isa{s} implies well-foundedness of this relation. For the |
85 moment we assume this and proceed with the induction:% |
100 moment we assume this and proceed with the induction:% |
86 \end{isamarkuptxt}% |
101 \end{isamarkuptxt}% |
|
102 \isamarkuptrue% |
87 \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 |
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 |
88 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
104 \ \isamarkupfalse% |
89 \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% |
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% |
|
109 % |
90 \begin{isamarkuptxt}% |
110 \begin{isamarkuptxt}% |
91 \noindent |
111 \noindent |
92 \begin{isabelle}% |
112 \begin{isabelle}% |
93 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline |
113 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline |
94 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\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 |
106 \isa{Avoid}-rule implies that all successors of \isa{t} are in |
126 \isa{Avoid}-rule implies that all successors of \isa{t} are in |
107 \isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}. |
127 \isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}. |
108 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in |
128 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in |
109 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% |
129 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% |
110 \end{isamarkuptxt}% |
130 \end{isamarkuptxt}% |
111 \ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline |
131 \ \isamarkuptrue% |
112 \ \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline |
132 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline |
113 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}% |
133 \ \isamarkupfalse% |
|
134 \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline |
|
135 \ \isamarkupfalse% |
|
136 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse% |
|
137 % |
114 \begin{isamarkuptxt}% |
138 \begin{isamarkuptxt}% |
115 Having proved the main goal, we return to the proof obligation that the |
139 Having proved the main goal, we return to the proof obligation that the |
116 relation used above is indeed well-founded. This is proved by contradiction: if |
140 relation used above is indeed well-founded. This is proved by contradiction: if |
117 the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem |
141 the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem |
118 \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: |
142 \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: |
120 \ \ \ \ \ 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}% |
144 \ \ \ \ \ 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}% |
121 \end{isabelle} |
145 \end{isabelle} |
122 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite |
146 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite |
123 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.% |
147 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.% |
124 \end{isamarkuptxt}% |
148 \end{isamarkuptxt}% |
|
149 \isamarkuptrue% |
125 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline |
150 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline |
|
151 \isamarkupfalse% |
126 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline |
152 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline |
|
153 \isamarkupfalse% |
127 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
154 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
155 \isamarkupfalse% |
128 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline |
156 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline |
|
157 \isamarkupfalse% |
129 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline |
158 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline |
130 \isacommand{done}% |
159 \isamarkupfalse% |
|
160 \isacommand{done}\isamarkupfalse% |
|
161 % |
131 \begin{isamarkuptext}% |
162 \begin{isamarkuptext}% |
132 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the |
163 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the |
133 statement of the lemma means |
164 statement of the lemma means |
134 that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p} |
165 that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p} |
135 would be turned |
166 would be turned |
141 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, |
172 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, |
142 when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true |
173 when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true |
143 by the first \isa{Avoid}-rule. Isabelle confirms this:% |
174 by the first \isa{Avoid}-rule. Isabelle confirms this:% |
144 \index{CTL|)}% |
175 \index{CTL|)}% |
145 \end{isamarkuptext}% |
176 \end{isamarkuptext}% |
|
177 \isamarkuptrue% |
146 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\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}\isanewline |
178 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\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}\isanewline |
|
179 \isamarkupfalse% |
147 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline |
180 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline |
148 \isanewline |
181 \isanewline |
|
182 \isamarkupfalse% |
|
183 \isamarkupfalse% |
149 \end{isabellebody}% |
184 \end{isabellebody}% |
150 %%% Local Variables: |
185 %%% Local Variables: |
151 %%% mode: latex |
186 %%% mode: latex |
152 %%% TeX-master: "root" |
187 %%% TeX-master: "root" |
153 %%% End: |
188 %%% End: |