equal
deleted
inserted
replaced
411 \end{isabelle} |
411 \end{isabelle} |
412 |
412 |
413 \noindent |
413 \noindent |
414 This allows us to define what actions a set of threads @{text ths} might |
414 This allows us to define what actions a set of threads @{text ths} might |
415 perform in a list of events @{text s}, namely |
415 perform in a list of events @{text s}, namely |
416 @{thm actions_of_def[THEN eq_reflection]}. |
416 |
417 A \emph{precedence} of a thread @{text th} in a |
417 \begin{isabelle}\ \ \ \ \ %%% |
|
418 @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}. |
|
419 \end{isabelle} |
|
420 |
|
421 where we use Isabelle's notation for list-comprehensions. This |
|
422 notation is very similar to notation used in Haskell for list |
|
423 comprehensions. A \emph{precedence} of a thread @{text th} in a |
418 state @{text s} is the pair of natural numbers defined as |
424 state @{text s} is the pair of natural numbers defined as |
419 |
425 |
420 \begin{isabelle}\ \ \ \ \ %%% |
426 \begin{isabelle}\ \ \ \ \ %%% |
421 @{thm preced_def} |
427 @{thm preced_def} |
422 \end{isabelle} |
428 \end{isabelle} |
1116 subtrees together form the set of threads. |
1122 subtrees together form the set of threads. |
1117 But the maximum of all threads is the @{term "cp"} of @{text "th"}, |
1123 But the maximum of all threads is the @{term "cp"} of @{text "th"}, |
1118 which is equal to the @{term preced} of @{text th}.\qed |
1124 which is equal to the @{term preced} of @{text th}.\qed |
1119 \end{proof} |
1125 \end{proof} |
1120 |
1126 |
1121 \endnote{ |
1127 %\endnote{ |
1122 @{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1128 %@{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1123 |
1129 % |
1124 @{text "th_kept"} shows that th is a thread in s'-s |
1130 % @{text "th_kept"} shows that th is a thread in s'-s |
1125 } |
1131 % } |
1126 |
1132 |
1127 Next we show that a running thread @{text "th'"} must either wait for or |
1133 Next we show that a running thread @{text "th'"} must either wait for or |
1128 hold a resource in state @{text s}. |
1134 hold a resource in state @{text s}. |
1129 |
1135 |
1130 \begin{lemma}\label{notdetached} |
1136 \begin{lemma}\label{notdetached} |