doc-src/TutorialI/CTL/document/CTL.tex
author nipkow
Wed Oct 04 17:35:45 2000 +0200 (2000-10-04)
changeset 10149 7cfdf6a330a0
parent 10133 e187dacd248f
child 10159 a72ddfdbfca0
permissions -rw-r--r--
*** empty log message ***
nipkow@10123
     1
%
nipkow@10123
     2
\begin{isabellebody}%
nipkow@10123
     3
\def\isabellecontext{CTL}%
nipkow@10133
     4
%
nipkow@10133
     5
\isamarkupsubsection{Computation tree logic---CTL}
nipkow@10149
     6
%
nipkow@10149
     7
\begin{isamarkuptext}%
nipkow@10149
     8
The semantics of PDL only needs transitive reflexive closure.
nipkow@10149
     9
Let us now be a bit more adventurous and introduce a new temporal operator
nipkow@10149
    10
that goes beyond transitive reflexive closure. We extend the datatype
nipkow@10149
    11
\isa{formula} by a new constructor%
nipkow@10149
    12
\end{isamarkuptext}%
nipkow@10149
    13
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
nipkow@10149
    14
\begin{isamarkuptext}%
nipkow@10149
    15
\noindent
nipkow@10149
    16
which stands for "always in the future":
nipkow@10149
    17
on all paths, at some point the formula holds. 
nipkow@10149
    18
Introducing the notion of paths (in \isa{M})%
nipkow@10149
    19
\end{isamarkuptext}%
nipkow@10123
    20
\isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
nipkow@10149
    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}%
nipkow@10149
    22
\begin{isamarkuptext}%
nipkow@10149
    23
\noindent
nipkow@10149
    24
allows a very succinct definition of the semantics of \isa{AF}:
nipkow@10149
    25
\footnote{Do not be mislead: neither datatypes nor recursive functions can be
nipkow@10149
    26
extended by new constructors or equations. This is just a trick of the
nipkow@10149
    27
presentation. In reality one has to define a new datatype and a new function.}%
nipkow@10149
    28
\end{isamarkuptext}%
nipkow@10149
    29
{\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
nipkow@10149
    30
\begin{isamarkuptext}%
nipkow@10149
    31
\noindent
nipkow@10149
    32
Model checking \isa{AF} involves a function which
nipkow@10149
    33
is just large enough to warrant a separate definition:%
nipkow@10149
    34
\end{isamarkuptext}%
nipkow@10123
    35
\isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
nipkow@10149
    36
\ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
nipkow@10149
    37
\begin{isamarkuptext}%
nipkow@10149
    38
\noindent
nipkow@10149
    39
This function is monotone in its second argument (and also its first, but
nipkow@10149
    40
that is irrelevant), and hence \isa{af\ A} has a least fixpoint.%
nipkow@10149
    41
\end{isamarkuptext}%
nipkow@10123
    42
\isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10149
    43
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10149
    44
\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
nipkow@10149
    45
\begin{isamarkuptext}%
nipkow@10149
    46
\noindent
nipkow@10149
    47
Now we can define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
nipkow@10149
    48
\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
nipkow@10149
    49
\end{isamarkuptext}%
nipkow@10123
    50
{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
    51
\isacommand{theorem}\ lfp{\isacharunderscore}subset{\isacharunderscore}AF{\isacharcolon}\isanewline
nipkow@10123
    52
{\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}\isanewline
nipkow@10123
    53
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
nipkow@10123
    54
\isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10123
    55
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10123
    56
\isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
nipkow@10123
    57
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
    58
\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
nipkow@10123
    59
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
nipkow@10123
    60
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
nipkow@10123
    61
\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
nipkow@10123
    62
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10123
    63
\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
nipkow@10123
    64
\begin{isamarkuptext}%
nipkow@10123
    65
The opposite direction is proved by contradiction: if some state
nipkow@10123
    66
{term s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
nipkow@10123
    67
infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
nipkow@10123
    68
that by unfolding \isa{lfp} we find that if \isa{s} is not in
nipkow@10123
    69
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
nipkow@10123
    70
direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
nipkow@10123
    71
\isa{A}-avoiding path. Let us formalize this sketch.
nipkow@10123
    72
nipkow@10123
    73
The one-step argument in the above sketch%
nipkow@10123
    74
\end{isamarkuptext}%
nipkow@10123
    75
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
nipkow@10123
    76
\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
    77
\isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
nipkow@10123
    78
\isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10123
    79
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}%
nipkow@10123
    80
\begin{isamarkuptext}%
nipkow@10123
    81
\noindent
nipkow@10123
    82
is proved by a variant of contraposition (\isa{swap}:
nipkow@10123
    83
\isa{{\isasymlbrakk}{\isasymnot}\ Pa{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Pa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
nipkow@10123
    84
and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
nipkow@10123
    85
simplifying with the definition of \isa{af} finishes the proof.
nipkow@10123
    86
nipkow@10123
    87
Now we iterate this process. The following construction of the desired
nipkow@10123
    88
path is parameterized by a predicate \isa{P} that should hold along the path:%
nipkow@10123
    89
\end{isamarkuptext}%
nipkow@10123
    90
\isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
    91
\isacommand{primrec}\isanewline
nipkow@10123
    92
{\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
nipkow@10123
    93
{\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}%
nipkow@10123
    94
\begin{isamarkuptext}%
nipkow@10123
    95
\noindent
nipkow@10123
    96
Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
nipkow@10123
    97
\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Of
nipkow@10123
    98
course, such a \isa{t} may in general not exist, but that is of no
nipkow@10123
    99
concern to us since we will only use \isa{path} in such cases where a
nipkow@10123
   100
suitable \isa{t} does exist.
nipkow@10123
   101
nipkow@10123
   102
Now we prove that if each state \isa{s} that satisfies \isa{P}
nipkow@10123
   103
has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path.%
nipkow@10123
   104
\end{isamarkuptext}%
nipkow@10123
   105
\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
nipkow@10123
   106
{\isachardoublequote}{\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}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
nipkow@10123
   107
\begin{isamarkuptxt}%
nipkow@10123
   108
\noindent
nipkow@10123
   109
First we rephrase the conclusion slightly because we need to prove both the path property
nipkow@10123
   110
and the fact that \isa{P} holds simultaneously:%
nipkow@10123
   111
\end{isamarkuptxt}%
nipkow@10123
   112
\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}\ 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\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
nipkow@10123
   113
\begin{isamarkuptxt}%
nipkow@10123
   114
\noindent
nipkow@10123
   115
From this proposition the original goal follows easily%
nipkow@10123
   116
\end{isamarkuptxt}%
nipkow@10123
   117
\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isanewline
nipkow@10123
   118
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
nipkow@10123
   119
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10123
   120
\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
nipkow@10123
   121
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
nipkow@10123
   122
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10133
   123
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   124
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10133
   125
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   126
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10133
   127
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   128
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   129
\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   130
\isanewline
nipkow@10123
   131
\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
nipkow@10123
   132
{\isachardoublequote}{\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}\ {\isasymLongrightarrow}\isanewline
nipkow@10123
   133
\ {\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}\ i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
   134
\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
nipkow@10123
   135
\ {\isachardoublequote}{\isasymexists}\ p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isasymin}M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
nipkow@10123
   136
\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10123
   137
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   138
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ u{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
nipkow@10123
   139
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10123
   140
\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
nipkow@10123
   141
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
nipkow@10123
   142
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10133
   143
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   144
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10133
   145
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   146
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10133
   147
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   148
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   149
\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   150
\isanewline
nipkow@10123
   151
\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
nipkow@10123
   152
{\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
nipkow@10123
   153
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
nipkow@10123
   154
\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
nipkow@10123
   155
\isacommand{apply}\ simp\isanewline
nipkow@10123
   156
\isacommand{apply}{\isacharparenleft}drule\ seq{\isacharunderscore}lemma{\isacharparenright}\isanewline
nipkow@10123
   157
\isacommand{by}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
nipkow@10123
   158
\isanewline
nipkow@10123
   159
\isanewline
nipkow@10123
   160
\isanewline
nipkow@10123
   161
\isanewline
nipkow@10123
   162
\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
nipkow@10123
   163
\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
nipkow@10123
   164
\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
nipkow@10123
   165
\ \ \ \ \ \ \ {\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}\isanewline
nipkow@10123
   166
\isanewline
nipkow@10123
   167
\isanewline
nipkow@10123
   168
\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
nipkow@10123
   169
{\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
nipkow@10123
   170
\ {\isasymforall}f{\isachardot}\ t\ {\isacharequal}\ f\ \isadigit{0}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ i{\isacharcomma}\ f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ f\ i\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\isanewline
nipkow@10123
   171
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
   172
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10123
   173
\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10123
   174
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10123
   175
\isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
nipkow@10123
   176
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ \isadigit{0}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
nipkow@10123
   177
\isacommand{by}{\isacharparenleft}force\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
nipkow@10123
   178
\isanewline
nipkow@10123
   179
\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
nipkow@10123
   180
{\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}\isanewline
nipkow@10123
   181
\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}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
nipkow@10123
   182
\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
nipkow@10123
   183
\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
nipkow@10123
   184
\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10123
   185
\ \isacommand{apply}{\isacharparenleft}unfold\ af{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10123
   186
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
nipkow@10123
   187
\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
nipkow@10123
   188
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
nipkow@10123
   189
\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
nipkow@10123
   190
\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
nipkow@10123
   191
\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
nipkow@10123
   192
\isanewline
nipkow@10123
   193
\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
nipkow@10123
   194
{\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
nipkow@10123
   195
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
nipkow@10123
   196
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10123
   197
\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharparenright}\isanewline
nipkow@10123
   198
\isacommand{by}{\isacharparenleft}rule\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
nipkow@10123
   199
\isanewline
nipkow@10123
   200
\isanewline
nipkow@10123
   201
\isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
nipkow@10123
   202
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
nipkow@10149
   203
\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ lfp{\isacharunderscore}subset{\isacharunderscore}AF\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10123
   204
\end{isabellebody}%
nipkow@10123
   205
%%% Local Variables:
nipkow@10123
   206
%%% mode: latex
nipkow@10123
   207
%%% TeX-master: "root"
nipkow@10123
   208
%%% End: