Think Stitch
PRINCIPIA  最近の更新


アルファベット指定による並行合成の failures

あけましておめでとうございます。本年もよろしくお願いいたします。

2014年最初のお題として,アルファベット指定による並行合成の failures を求めてみることにします。でもそれはちょっとおかしな話です。failures は表示的意味論の一部として定義されるべきものだからです。実際,CSP の教科書を見ると,アルファベット指定による並行合成の failures は次のように定義されています。

\[ \begin{split} &\textit{failures}(P\ {}_A{||}{}_B\ Q) = \\ &\quad \{\,(u, X)\ |\\ &\quad \qquad \exists\, Y, Z.\ X \cap (A \cup B)^\checkmark = (Y \cap A^\checkmark) \cup (Z \cap B^\checkmark) \land {} \\ &\quad \qquad \qquad u \in {(A \cup B)^*}^\checkmark \land \\ &\quad \qquad \qquad (u \upharpoonright A^\checkmark, Y) \in \textit{failures}(P) \land {} \\ &\quad \qquad \qquad (u \upharpoonright B^\checkmark, Z) \in \textit{failures}(Q) \ \} \end{split} \]

では,ここでは何をするかというと,まずアルファベット指定による並行合成 apar の直観的な意味から,apar を par で表してみます。アルファベットに含まれていないイベントが制限されることと,指定されたアルファベットに共通するイベントは同期することから,次の式が思いつくでしょう。

\[ P\ {}_A{||}{}_B\ Q = (P\ \underset{\Sigma - A}{||}\ \textrm{SKIP})\ \underset{A \cap B}{||}\ (Q \underset{\Sigma - B}{||}\ \textrm{SKIP}) \]

実際,操作的意味論で考えると,まずアルファベット A に属していないイベントをプロセス P が発生させようとしても制限されます。なぜなら,終了イベント以外のいかなるイベントも発生させないプロセス SKIP と Σ - A で同期しているからです。プロセス Q についても同じです。そして,それらは2のアルファベットに共通するイベント,つまり A ∩ B に属するイベントについては同期しなければなりません。このようにアルファベット指定による並行合成と同じ遷移を持っていることが分かります。

この式を認めるとすると,インターフェイス指定による並行合成 par の failures 定義と終了プロセス SKIP の failures の定義とから,アルファベット指定による並行合成 apar の failures が計算できることになります。ここでは,この計算を実際に行って,上の定義と一致することを確かめてみることにします。考え方を説明しながら手で計算をした後で,Isabelle で計算の正しさを証明します。

終了が含まれているといろいろと細かい面倒なことが起こるので,ここでは終了を無視した簡単な問題だけ考えることにします。

式の整理

スタートの時点で持っている式を整理しておきます。まずアルファベット指定による並行合成 apar の failures の式です。終了イベントを無視した版です。これがゴールになります。

\[ \begin{split} &\textit{failures}(P\ {}_A{||}{}_B\ Q) = \\ &\quad \{\,(u, X)\ |\\ &\quad \qquad \exists\, Y, Z.\ X \cap (A \cup B) = (Y \cap A) \cup (Z \cap B) \land {} \\ &\quad \qquad \qquad u \in {(A \cup B)^*} \land \\ &\quad \qquad \qquad (u \upharpoonright A, Y) \in \textit{failures}(P) \land {} \\ &\quad \qquad \qquad (u \upharpoonright B, Z) \in \textit{failures}(Q) \ \} \end{split} \]

アルファベット指定による並行合成 apar を停止プロセス STOP とインターフェイス指定による並行合成 par で表した式です。終了イベントを無視するので,SKIP を STOP に変えてあります。

\[ P\ {}_A{||}{}_B\ Q = (P\ \underset{\Sigma - A}{||}\ \textrm{STOP})\ \underset{A \cap B}{||}\ (Q \underset{\Sigma - B}{||}\ \textrm{STOP}) \]

インターフェイス指定による並行合成 par の failures です。

\[ \begin{split} \textit{failures}(P\ \underset{X}{||}\ Q) = \\ \{ (u, Y \cup Z) \ |\ & Y - X = Z - X \land \\ & (\exists s, t. (s, Y) \in \textit{failures}(P) \land \\ & \qquad (t, Z) \in \textit{failures}(Q) \land \\ & \qquad u \in s\ \underset{X}{||}\ t) \} \end{split} \]

最後は停止プロセス STOP の failures です。

\[ \textit{failures}(\textrm{STOP}) = \{ (\langle \rangle, X) \ |\ X \subseteq \Sigma \} \]

停止プロセスとの並行合成

まず次の項,STOP との並行合成部分の failures を求めます。failures は構成的に定義されているので,式の構造に従って順番に計算していくことができます。(ただし,再帰がない場合だけです。)

\[ P\ \underset{\Sigma - A}{||}\ \textrm{STOP} \]

そのまま定義に代入します。

\[ \begin{split} \textit{failures}(P\ \underset{\Sigma - A}{||}\ \textrm{STOP}) = \\ \{ (u, Y \cup Z) \ |\ & Y - (\Sigma - A) = Z - (\Sigma - A) \land \\ & (\exists s, t. (s, Y) \in \textit{failures}(P) \land \\ & \qquad (t, Z) \in \textit{failures}(\textrm{STOP}) \land \\ & \qquad u \in s\ \underset{\Sigma - A}{||}\ t) \} \end{split} \]

まずすぐに分かるのは, \[ Y - (\Sigma - A) = Y \cap A \] です。

それから failures(STOP) の定義から, \[ (t, Z) \in \textit{failures}(\textrm{STOP}) \] となるのは t=<> かつ Z ⊆ Σのときだけです。

すると \[ u \in s\ \underset{\Sigma - A}{||}\ \langle\rangle \] となりますが,これを満たす u が存在するのは,s の要素がすべて A に含まれている場合だけで,かつそのときには u = s となります。集合 A の要素だけからなるすべての列の集合を, \[ A^* \] と書くことにします。そうすると \[ s \in A^* \] となります。u = s ですから s の存在限量も消えて,結局次のようになります。

\[ \begin{split} \textit{failures}(P\ \underset{\Sigma - A}{||}\ \textrm{STOP}) = \\ \{ (s, Y \cup Z) \ |\ & Y \cap A = Z \cap A \land \\ & (s, Y) \in \textit{failures}(P) \land \\ & s \in A^* \land Z \subseteq \Sigma \} \end{split} \]

次に \[ Y \cap A = Z \cap A \] という条件をなんとかしましょう。 恒等式 \[ A = (A \cap B) \cup (A - B) \] を使うと \[ \begin{split} Y = (Y \cap A) \cup (Y - A) \\ Z = (Z \cap A) \cup (Z - A) \end{split} \] と表すことができます。このうち,前の項は条件により一致します。 いま, \[ W = Z - A \] とおくと, \[ Y \cup Z = Y \cup W \] で,さらに \[ Z = (Y \cap A) \cup W \] です。そして, \[ \begin{split} W &= Z - A \\ &= Z \cap (\Sigma - A) \\ &= ((Y \cap A) \cup W) \cap (\Sigma - A) \\ &= W \cap (\Sigma - A) \end{split} \] したがって \[ W \subseteq \Sigma - A \] がわかります。

以上の関係を使って Z を消去し,代わりに W を導入すると,failures は次のようになります。

\[ \begin{split} \textit{failures}(P\ \underset{\Sigma - A}{||}\ \textrm{STOP}) = \\ \{ (s, Y \cup W) \ |\ & (s, Y) \in \textit{failures}(P) \land \\ & s \in A^* \land W \subseteq \Sigma - A \} \end{split} \]

この式は直観的にも理解しやすいでしょう。トレース s は A の範囲に制限されていて,かつ A に含まれていないイベントは任意に拒否に加えることができるということです。さらに次のように書き換えることができます。

\[ \textit{failures}(P\ \underset{\Sigma - A}{||}\ \textrm{STOP}) = \{ (s, X) \ |\ (s, X \cap A) \in \textit{failures}(P) \land s \in A^* \} \]

同期項の failures 計算

次に A ∩ B で同期する部分を計算します。

\[ \begin{split} \textit{failures}&((P\ \underset{\Sigma - A}{||}\ \textrm{STOP})\ \underset{A \cap B}{||}\ (Q \underset{\Sigma - B}{||}\ \textrm{STOP})) \\ &= \{(u, Y \cup Z)\ |\ Y - (A \cap B) = Z - (A \cap B) \land \\ & \qquad \exists s\ t.\ (s, Y) \in \textit{failures}(P\ \underset{\Sigma - A}{||}\ \textrm{STOP}) \land \\ & \qquad \qquad (t, Z) \in \textit{failures}(Q\ \underset{\Sigma - B}{||}\ \textrm{STOP}) \land \\ & \qquad \qquad u \in s\,\underset{A \cap B}{||}\,t \} \\ &= \{(u, Y \cup Z)\ |\ Y - (A \cap B) = Z - (A \cap B) \land \\ & \qquad \exists s\ t.\ (s, Y \cap A) \in \textit{failures}(P) \land s \in A^* \land \\ & \qquad \qquad (t, Z \cap B) \in \textit{failures}(Q) \land t \in B^* \land \\ & \qquad \qquad u \in s\,\underset{A \cap B}{||}\,t \} \\ &= \{(u, Y \cup Z)\ |\ Y - (A \cap B) = Z - (A \cap B) \land \\ & \qquad (u \upharpoonright A, Y \cap A) \in \textit{failures}(P) \land \\ & \qquad (u \upharpoonright B, Z \cap B) \in \textit{failures}(Q) \land \\ & \qquad u \in (A \cup B)^* \} \\ \end{split} \]

2番目の変形では先ほど計算した式を使いました。3番目の変形では,トレースの並行合成に関する次の性質を使いました。 \[ \begin{split} & s \in A^* \land t \in B^* \land u \in s\,\underset{A \cap B}{||}\,t \\ = &\\ & s = u \upharpoonright A \land t = u \upharpoonright B \land u \in (A \cup B)^* \end{split} \]

次に \[ Y - (A \cap B) = Z - (A \cap B) \] という条件をなんとかしましょう。これは Y と Z が A ∩ B の外側では一致していることを意味しますから,次のものと同値です。 \[ Y \cup (A \cap B) = Z \cup (A \cap B) \] この両辺と A - B との共通部分を求めると, \[ Y \cap (A - B) = Z \cap (A - B) \] となります。そこで,拒否を X = Y ∪ Z とすると, \[ \begin{split} & Y \cap A \\ =& (Y \cap (A \cap B)) \cup (Y \cap (A - B)) \\ =& (Y \cap (A \cap B)) \cup ((Y \cup Z) \cap (A - B)) \\ =& (Y \cap (A \cap B)) \cup (X \cap (A - B)) \end{split} \] 同様に, \[ Z \cap B = (Z \cap (A \cap B)) \cup (X \cap (B - A)) \] です。両者の和を求めると, \[ \begin{split} & (Y \cap A) \cup (Z \cap B) \\ =& ((Y \cup Z) \cap (A \cap B)) \cup (X \cap (A - B)) \cup (X \cap (B - A)) \\ =& (X \cap (A \cap B)) \cup (X \cap (A - B)) \cup (X \cap (B - A)) \\ =& X \cap (A \cup B) \end{split} \]

よって \[ \begin{split} \textit{failures}&((P\ \underset{\Sigma - A}{||}\ \textrm{STOP})\ \underset{A \cap B}{||}\ (Q \underset{\Sigma - B}{||}\ \textrm{STOP})) \\ &= \{(u, X)\ |\ \exists Y, Z.\ X \cap (A \cup B) = (Y \cap A) \cup (Z \cap B) \land \\ & \qquad (u \upharpoonright A, Y \cap A) \in \textit{failures}(P) \land \\ & \qquad (u \upharpoonright B, Z \cap B) \in \textit{failures}(Q) \land \\ & \qquad u \in (A \cup B)^* \} \\ \end{split} \]

さらに,拒否の部分集合は拒否であることを使うと(拒否の健全性条件),次のように書き直すことができます。 \[ \begin{split} \textit{failures}&((P\ \underset{\Sigma - A}{||}\ \textrm{STOP})\ \underset{A \cap B}{||}\ (Q \underset{\Sigma - B}{||}\ \textrm{STOP})) \\ &= \{(u, X)\ |\ \exists Y, Z.\ X \cap (A \cup B) = (Y \cap A) \cup (Z \cap B) \land \\ & \qquad (u \upharpoonright A, Y) \in \textit{failures}(P) \land \\ & \qquad (u \upharpoonright B, Z) \in \textit{failures}(Q) \land \\ & \qquad u \in (A \cup B)^* \} \\ \end{split} \]

というわけで,ゴールにたどり着くことができました。

Isabelle による証明

以上の変形が正しいことを Isabelle で証明してみました。ポイントだけ簡単に解説します。

停止プロセス STOP の failures

停止プロセス STOP の failures を定義します。

definition
  STOP :: "('e list * 'e set) set"
where
  "STOP = {(s, X). s = []}"

トレースの射影 restrict

トレースの射影 \[ tr \upharpoonright A \] を表す関数 restrict を定義します。

fun
  restrict :: "'e list => 'e set => 'e list"
where
  "restrict [] X = []" |
  "restrict (a#as) X =
     (if a : X then a#(restrict as X)
               else restrict as X)"

トレースの並行合成

トレースの並行合成 \[ s\ \underset{X}{||}\ t \] を表す関数 par_tr を定義します。

fun
  par_tr :: "'e set
          => 'e list
          => 'e list
          => 'e list set"
where
  "par_tr X [] [] = {[]}" |
  "par_tr X [] (b#bs) = 
          (if b : X then {} else {b # tr |tr. tr : (par_tr X [] bs)})" |
  "par_tr X (a#as) [] =
          (if a : X then {} else {a # tr |tr. tr : (par_tr X as [])})" |
  "par_tr X (a#as) (b#bs) =
          (if a : X then
            (if b : X then
              (if a = b then
                {a # tr |tr. tr : (par_tr X as bs)}
               else {})
             else {b # tr |tr. tr : (par_tr X (a#as) bs)})
           else
            (if b : X then {a # tr |tr. tr : (par_tr X as (b#bs))}
        else
  {a # tr |tr. tr : (par_tr X as (b#bs))} Un {b # tr |tr. tr : (par_tr X (a#as) bs)}))"

インターフェイス指定による並行合成 par の failures

インターフェイス指定による並行合成 par の failures \[ \textit{failures}(P\ \underset{X}{||}\ Q) \] を表す関数 failures_par を定義します。

definition
failures_par :: "'e set =>
  ('e list * 'e set) set =>
  ('e list * 'e set) set => 
  ('e list * 'e set) set"
where
  "failures_par X P Q = 
     {(u, W). EX s t Y Z. W = Y Un Z &
                 Y - X = Z - X &
                 (s, Y) : P & (t, Z) : Q &
                 u : par_tr X s t}"

アルファベット指定による並行合成 apar の failures

インターフェイス指定による並行合成 apar の failures \[ \textit{failures}(P\ {}_A{||}{}_B\ Q) \] を表す関数 failures_apar を定義します。

definition
  failures_apar :: "'e set =>
  ('e list * 'e set) set =>
  'e set =>  
  ('e list * 'e set) set =>
  ('e list * 'e set) set"
where
  "failures_apar A P B Q =
    {(s, X). EX Y Z.
           X Int (A Un B) = (Y Int A) Un (Z Int B) &
           (restrict s A, Y) : P &
           (restrict s B, Z) : Q &
           set s <= A Un B}"

補題

lemma x0: "[| A = B; x : A |] ==> x : B"
apply(auto)
done

lemma x1 [rule_format]:
  "ALL u. u : par_tr (UNIV - A) s [] --> u = s & set s <= A"
apply(induct_tac s)
apply(auto)
done

lemma x2: "Y - (UNIV - A) = Y Int A"
apply(auto)
done

lemma x3 [rule_format]: "set s <= A --> par_tr (UNIV - A) s [] = {s}"
apply(induct_tac s)
apply(auto)
done

STOP との並行合成項

停止プロセス STOP との並行合成を簡単にした式が正しいことを示します。

lemma apar_stop:
  "failures_par (UNIV - A) P STOP =
  {(s, Y Un W)| s Y W. (s, Y) : P & set s <= A & W Int A = {}}"
apply(unfold STOP_def failures_par_def x2)
apply(rule subset_antisym)
apply(clarsimp)
apply(rule_tac x="Y" in exI)
apply(rule_tac x="Z - A" in exI)
apply(drule x1)
apply(auto)
apply(rule_tac x="s" in exI)
apply(rule_tac x="Y" in exI)
apply(rule_tac x="W Un (Y Int A)" in exI)
apply(drule x3)
apply(auto)
done

lemma apar_stop2:
  "ALL s X X1. (s, X) : P & X1 <= X --> (s, X1) : P
  ==>
  failures_par (UNIV - A) P STOP =
  {(s, X). (s, X Int A) : P & set s <= A}"
apply(subst apar_stop)
apply(auto)
apply(subgoal_tac "(Y Un W) Int A = Y Int A")
apply(clarsimp)
apply(blast)
apply(blast)
apply(rename_tac s X)
apply(rule_tac x="X Int A" in exI)
apply(rule_tac x="X - A" in exI)
apply(auto)
done

さらに補題

lemma x4 [rule_format]: "ALL t. [] : par_tr X s t --> s = []"
apply(induct_tac s)
apply(auto)
apply(case_tac t)
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
apply(case_tac "a=aa")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
apply(case_tac t)
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
apply(case_tac "a=aa")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
done

lemma x5 [rule_format]: "ALL s. [] : par_tr X s t --> t = []"
apply(induct_tac t)
apply(auto)
apply(case_tac s)
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "a=aa")
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac s)
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "aa : X")
apply(auto)
apply(case_tac "a : X")
apply(auto)
apply(case_tac "a=aa")
apply(auto)
apply(case_tac "a : X")
apply(auto)
done

lemma x6 [rule_format]: "ALL u. set t <= B & u : par_tr (A Int B) [] t
  --> [] = restrict u A & t = restrict u B"
apply(induct_tac t)
apply(auto)
done

lemma x7 [rule_format]: "ALL u. set s <= A & u : par_tr (A Int B) s []
  --> s = restrict u A & [] = restrict u B"
apply(induct_tac s)
apply(auto)
done

lemma x7s: "[| set s <= A; u : par_tr (A Int B) s [] |]
  ==> s = restrict u A"
apply(rule x7[THEN conjunct1])
apply(auto)
done

lemma x7t: "[| set s <= A; u : par_tr (A Int B) s [] |]
  ==> [] = restrict u B"
apply(rule_tac A1="A" in x7[THEN conjunct2])
apply(auto)
done

lemma x8 [rule_format]:
"ALL u. (ALL t u. set t <= B & u : par_tr (A Int B) list t -->
             list = restrict u A & t = restrict u B) &
          a : A & set list <= A & set t <= B &
          u : par_tr (A Int B) (a # list) t 
       --> a # list = restrict u A & t = restrict u B"
apply(induct_tac t)
apply(clarsimp)
apply(rule_tac B="B" in x7s)
apply(clarsimp)
apply(clarsimp)
apply(rule allI)
apply(rule impI)
apply(clarsimp)
apply(case_tac "a:B")
apply(clarsimp)
apply(case_tac "aa:A")
apply(clarsimp)
apply(case_tac "a=aa")
apply(clarsimp)
apply(blast)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(case_tac "aa:A")
apply(clarsimp)
apply(rotate_tac 1)
apply(drule_tac x="aa#lista" in spec)
apply(rotate_tac -1)
apply(drule_tac x="tr" in spec)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(erule disjE)
apply(clarsimp)
apply(rotate_tac 1)
apply(drule_tac x="aa#lista" in spec)
apply(rotate_tac -1)
apply(drule_tac x="tr" in spec)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
done

lemma x9 [rule_format]:
  "ALL t u. u : par_tr (A Int B) s t --> set s <= A --> set t <= B
  --> s = restrict u A & t = restrict u B"
apply(induct_tac s)
apply(clarsimp)
apply(rule x6)
apply(clarsimp)
apply(clarsimp)
apply(rule x8)
apply(clarsimp)
done

lemma xa [rule_format]: "ALL s. s = restrict u A --> set s <= A"
apply(induct_tac u)
apply(auto)
done

lemma p0 [rule_format]:
  "tr : par_tr X [] bs &  e ~: X
         --> e # tr : par_tr X [e] bs"
apply(induct_tac bs)
apply(auto)
done

lemma p1 [rule_format]:
  "(ALL tr. tr : par_tr X list bs --> e # tr : par_tr X (e # list) bs) -->
  tr : par_tr X (a # list) bs --> e ~: X
  --> e # tr : par_tr X (e # a # list) bs"
apply(induct_tac bs)
apply(auto)
done

lemma p2 [rule_format]:
  "ALL e bs tr. tr : par_tr X as bs --> e ~: X --> e#tr : par_tr X (e#as) bs"
apply(induct_tac as)
apply(auto)
apply(rule p0)
apply(auto)
apply(rule p1)
apply(auto)
done

lemma p3 [rule_format]:
  "tr : par_tr X as [] &  e ~: X
         --> e # tr : par_tr X as [e]"
apply(induct_tac as)
apply(auto)
done

lemma p4 [rule_format]:
  "(ALL tr. tr : par_tr X as list --> e # tr : par_tr X as (e # list)) -->
  tr : par_tr X as (a # list) --> e ~: X
  --> e # tr : par_tr X as (e # a # list)"
apply(induct_tac as)
apply(auto)
done

lemma p5 [rule_format]:
  "ALL e as tr. tr : par_tr X as bs --> e ~: X --> e#tr : par_tr X as (e#bs)"
apply(induct_tac bs)
apply(auto)
apply(rule p3)
apply(auto)
apply(rule p4)
apply(auto)
done

lemma xb:
  "set u <= A Un B --> u : par_tr (A Int B) (restrict u A) (restrict u B)"
apply(induct_tac u)
apply(clarsimp)
apply(auto)
apply(rule p2)
apply(clarsimp)
apply(clarsimp)
apply(rule p5)
apply(auto)
done

lemma q1 [rule_format]:
  "ALL u.
       u : par_tr (A Int B) [] t -->
       set t <= B -->
  set u <= A Un B"
apply(induct_tac t)
apply(auto)
apply(blast)
done

lemma q2 [rule_format]:
  "ALL u.
       u : par_tr (A Int B) s [] -->
       set s <= A -->
  set u <= A Un B"
apply(induct_tac s)
apply(auto)
apply(blast)
done

lemma q3 [rule_format]:
  "ALL u.
  u : par_tr (A Int B) (a # list) t -->
  a : A -->
  set list <= A -->
  (ALL u t.
      set t <= B -->
      u : par_tr (A Int B) list t -->
      set u <= A Un B) -->
  set t <= B -->
  x : set u -->  x ~: B -->
  x : A"
apply(induct_tac t)
apply(clarsimp)
apply(drule_tac x="tr" in spec)
apply(drule_tac x="[]" in spec)
apply(clarsimp)
apply(blast)
apply(auto)
apply(blast)
apply(rotate_tac 1)
apply(drule_tac x="tr" in spec)
apply(rotate_tac -1)
apply(drule_tac x="aa#lista" in spec)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(blast)

apply(rotate_tac 1)
apply(drule_tac x="tr" in spec)
apply(rotate_tac -1)
apply(drule_tac x="aa#lista" in spec)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(blast)
done

lemma q0 [rule_format]:
  "ALL u t. set s <= A --> set t <= B --> u : par_tr (A Int B) s t
  --> set u <= A Un B"
apply(induct_tac  s)
apply(auto)
apply(drule q1)
apply(clarsimp)
apply(blast)
apply(erule q3)
apply(auto)
done

メイン

計算結果が定義と一致することを証明します。 前提に拒否の健全性条件を入れてあります。

theorem apar1: "[| 
  ALL s X X1. (s, X) : P & X1 <= X --> (s, X1) : P;
  ALL s X X1. (s, X) : Q & X1 <= X --> (s, X1) : Q
  |] ==>
  failures_apar A P B Q =
  failures_par (A Int B)
  {(s, X). (s, X Int A) : P & set s <= A}
  {(s, X). (s, X Int B) : Q & set s <= B}"
apply(unfold STOP_def failures_par_def failures_apar_def)
apply(clarsimp)
apply(rule subset_antisym)
apply(clarsimp)
apply(rename_tac u X Y Z)
apply(rule_tac x="restrict u A" in exI)
apply(rule_tac x="restrict u B" in exI)
apply(rule_tac x="(X - (A Un B)) Un (Y Int A) Un (Z Int (B - A))" in exI)
apply(rule_tac x="(X - (A Un B)) Un (Z Int B) Un (Y Int (A - B))" in exI)
apply(rule conjI)
apply(blast)
apply(rule conjI)
apply(blast)
apply(rule conjI)
apply(subgoal_tac "(X - (A Un B) Un Y Int A Un Z Int (B - A)) Int A <= Y")
apply(blast)
apply(blast)
apply(rule conjI)
apply(rule_tac u="u" in xa)
apply(clarsimp)
apply(rule conjI)
apply(subgoal_tac "(X - (A Un B) Un Z Int B Un Y Int (A - B)) Int B <= Z")
apply(blast)
apply(blast)
apply(rule conjI)
apply(rule_tac u="u" in xa)
apply(clarsimp)
apply(rule xb[rule_format])
apply(clarsimp)

apply(clarsimp)
apply(rule_tac x="Y Int A" in exI)
apply(rule_tac x="Z Int B" in exI)
apply(rule conjI)
apply(blast)
apply(frule x9)
apply(clarsimp)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp)
apply(rule_tac s="s" and t="t" in q0)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)

done

というわけで確認することができました。

2014/01/05
© 2013,2014,2015 PRINCIPIA Limited