Think Stitch
PRINCIPIA  最近の更新


Isabelle によるグラフ循環検出プログラムの部分正当性証明

Theorem Prover Advent Calendar 2014の参加エントリです.

先日 Coq を使って研究をしている人と話をしていて,「不変条件を見つけるのは難しいけど面白い」ということで盛り上がりました.そんな例をご紹介します.

問題は有向グラフの中に循環があるかどうかを判定するプログラムの正当性証明です.プログラムは命令型(いわゆる WHILE プログラム)です.

昨年の Theorem Prover Advent Calendar で 「Isabelle によるグラフの循環検出アルゴリズムの部分正当性証明」という記事を書きました.その時は抽象化した設定で同じ問題を解いたのですが,今回は実際に動かすことのできるレベルでプログラムを書いて,正当性を証明したいと思います.

グラフが初期ノード s0 と接続関係 R で与えられているとすると,初期ノードから到達可能な循環が存在する条件は次のようになります:

\[ \exists p. (s_0, p) \in R^* \land (p, p) \in R^+ \]

これが成り立つかどうかを判定するプログラムを書きます.プログラムでは関係 R の代わりに関数 next が与えられると考えます.関数 next は与えられたノードから接続しているノードのリストを返す関数です.

Program

プログラムに特別なところはありません.よくある深さ優先探索プログラムです.

変数 f はいわゆる探索のフロントです.fs は保留中のフロントのリスト,s は探索が終わったノードの集合,tr は初期ノードから現在調べているノードまでのトレースです.

  VARS s f fs tr xs
  {True}
  s := {};
  f := [s0];
  tr := [];
  fs := [];
  WHILE ~((f = [] & fs = []) | (f ~= [] & (hd f) : set tr))
  INV {inv}
  DO
    IF f = [] THEN
      f := hd fs;
      fs := tl fs;
      s := s Un {hd tr};
      tr := tl tr
    ELSE
      IF hd f : s THEN
        f := tl f
      ELSE
        xs := next (hd f);
        IF xs = [] THEN
          s := s Un {hd f};
          f := tl f
        ELSE
          tr := (hd f) # tr;
          fs := (tl f) # fs;
          f := xs
        FI
      FI
    FI
  OD
  {(f ~= []) = (EX q. (s0, q) : r^* & (q, q) : r^+)}"

Loop Invariants

ループ不変条件は8つの積項からなります.簡単に見えるプログラムでも,いざ論証しようと思うと結構たいへんですね.

1. s Un (set tr) Un r^* `` ((set f) Un Union (set (map set fs))) = r^* `` {s0} &
2. r `` s <= s &
3. (tr ~= [] --> set (next (hd tr)) <= s Un (set f)) &
4. (tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : r)) &
5. (ALL i. i < length tr - 1 --> (tr ! (i + 1), tr ! i) : r) &
6. (ALL i. i < length tr - 1 -->
      set (next (tr ! (i + 1))) <= s Un {tr ! i} Un set (fs ! i)) &
7. (ALL i. i < length tr - 1 -->
      (ALL q. q : set (fs ! i) --> (tr ! (i + 1), q) : r)) &
8. (ALL p. p : s --> (ALL q. (p, q) : r^* --> (q, q) ~: r^+)) &

Proof

証明は1287行あります.よいお年を.

theory Divergence imports "~~/src/HOL/Hoare/Hoare_Logic" begin

(* cycle:  EX p. (s, p) : r^* & (p, p) : r^+ *)

(*
  1.    s Un (set tr) Un r^* `` ((set f) Un Union (set (map set fs))) = r^* `` {s0} &
  2.    r `` s <= s &
  3.    (tr ~= [] --> set (next (hd tr)) <= s Un (set f)) &
  4.    (tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : r)) &
  5.    (ALL i. i < length tr - 1 --> (tr ! (i + 1), tr ! i) : r) &
  6.    (ALL i. i < length tr - 1 -->
           set (next (tr ! (i + 1))) <= s Un {tr ! i} Un set (fs ! i)) &
  7.    (ALL i. i < length tr - 1 -->
           (ALL q. q : set (fs ! i) --> (tr ! (i + 1), q) : r)) &
  8.    (ALL p. p : s --> (ALL q. (p, q) : r^* --> (q, q) ~: r^+)) &
*)

definition nrel :: "('s => 's list) => ('s * 's) set" where
  "nrel next == {(x, y). y : set (next x)}"

lemma r1: "(p, q) : nrel next ==> q : set (next p)"
apply(unfold nrel_def)
apply(auto)
done

lemma r2: "q : set (next p) ==> (p, q) : nrel next"
apply(unfold nrel_def)
apply(auto)
done

lemma r3: "[| (xa, x) : r^*; r `` s <= s |] ==> xa : s --> x : s"
apply(erule rtrancl_induct)
apply(auto)
done

lemma r4: "r `` s <= s ==> r^* `` s <= s"
apply(auto)
apply(erule r3[rule_format])
apply(auto)
done

lemma r_1_1:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> insert (hd tr)
            (s Un set (tl tr) Un
             (nrel next)^* `` (set (hd fs) Un (UN x:set (tl fs). set x))) =
           (nrel next)^* `` {s0}"

apply(case_tac fs)
apply(clarsimp)
apply(case_tac tr)
apply(clarsimp)
apply(clarsimp)
done

lemma r_1_2:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> nrel next `` insert (hd tr) s <= insert (hd tr) s"

apply(auto)
apply(drule r1)
apply(blast)
done

lemma r_1_3:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (tl tr ~= [] -->
            set (next (hd (tl tr))) <= insert (hd tr) (s Un set (hd fs)))"

apply(auto)
apply(rotate_tac 3)
apply(drule_tac x="0" in spec)
apply(case_tac tr)
apply(clarsimp)
apply(clarsimp)
apply(case_tac list)
apply(clarsimp)
apply(case_tac fs)
apply(auto)
done

lemma r_1_4:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (tl tr ~= [] --> (ALL q. q : set (hd fs) --> (hd (tl tr), q) : nrel next))"

apply(auto)
apply(rotate_tac 4)
apply(drule_tac x="0" in spec)
apply(case_tac tr)
apply(auto)
apply(rename_tac p tr)
apply(case_tac fs)
apply(auto)
apply(rename_tac f fs)
apply(case_tac tr)
apply(auto)
done

lemma r_1_5:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (ALL i set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (ALL i set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (ALL i (tl tr ! Suc i, q) : nrel next)"

apply(rule allI)
apply(case_tac fs)
apply(auto)
apply(rename_tac f fs q)
apply(case_tac tr)
apply(auto)
done

lemma r_1_8:
  "[| s Un set tr Un (nrel next)^* `` (UN x:set fs. set x) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s;
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; fs ~= [] |]
       ==> (ALL q. (hd tr, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+)"

(* Since set (next (hd tr)) <= s, no cycle from hd tr *)
apply(case_tac fs)
apply(auto)
apply(rename_tac f fs q)
apply(case_tac tr)
apply(auto)
apply(rename_tac p tr)
apply(rotate_tac -3)
apply(erule converse_rtranclE)
(* (hd tr, hd tr) ~: r *)
apply(clarsimp)
apply(frule tranclD)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule r1)
apply(subgoal_tac "z : s")
apply(rotate_tac -4)
apply(drule_tac x="z" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(clarsimp)
apply(rotate_tac -1)
apply(drule_tac x="q" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(blast)
(* (hd tr, q) : r^+ *)
apply(rotate_tac -2)
apply(drule r1)
apply(subgoal_tac "y : s")
apply(rotate_tac -4)
apply(drule_tac x="y" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(clarsimp)
apply(rotate_tac -1)
apply(drule_tac x="q" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(blast)
done

lemma r_2_1_1:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f : s |]
       ==> s Un set tr Un (nrel next)^* `` (set (tl f) Un (UN x:set fs. set x)) <=
           (nrel next)^* `` {s0}"
apply(rule subsetI)
apply(drule equalityD1)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rule disjI2)
apply(rule disjI2)
apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(erule disjE)
apply(rule UnI1)
apply(case_tac f)
apply(clarsimp)
apply(clarsimp)
apply(erule bexE)
apply(rule UnI2)
apply(simp)
apply(rule_tac x=xb in bexI)
apply(simp)
apply(simp)
apply(simp)
done

lemma r_2_1_2:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f : s |]
       ==>
           (nrel next)^* `` {s0}  <=
            s Un set tr Un (nrel next)^* `` (set (tl f) Un (UN x:set fs. set x))"
apply(rule subsetI)
apply(drule equalityD2)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(simp)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(case_tac f)
apply(simp)
apply(simp)
apply(rotate_tac -2)
apply(erule disjE)
apply(simp)
apply(drule r4)
apply(subgoal_tac "x : s")
apply(simp)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(rule_tac a=a in ImageI)
apply(simp)
apply(simp)
apply(simp)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(simp)
apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(rule UnI2)
apply(simp)
apply(rule_tac x=xb in bexI)
apply(simp)
apply(simp)
done

lemma r_2_3:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f : s |]
       ==> (tr ~= [] --> set (next (hd tr)) <= s Un set (tl f))"
apply(rule impI)
apply(drule mp)
apply(simp)
apply(rule subsetI)
apply(subgoal_tac "x : s Un set f")
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(clarsimp)
apply(case_tac f)
apply(clarsimp)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule_tac c=x in subsetD)
apply(clarsimp)
apply(clarsimp)
done

lemma r_2_4:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f : s |]
       ==> (tr ~= [] --> (ALL q. q : set (tl f) --> (hd tr, q) : nrel next))"
apply(clarsimp)
apply(case_tac f)
apply(auto)
done

lemma r_3_1_1:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==> insert (hd f)
            (s Un set tr Un (nrel next)^* `` (set (tl f) Un (UN x:set fs. set x))) <=
           (nrel next)^* `` {s0}"
apply(rule subsetI)
apply(drule equalityD1)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(subgoal_tac "x : (set f Un UNION (set fs) set)")
apply(blast)
apply(rule UnI1)
apply(case_tac f)
apply(simp)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(rule UnI1)
apply(case_tac f)
apply(simp)
apply(simp)
apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(rule UnI2)
apply(simp)
apply(rule_tac x=xb in bexI)
apply(simp)
apply(simp)
apply(simp)
done

lemma r9 [rule_format]: "x : set xs --> (EX i. i < length xs & x = xs ! i)"
apply(induct_tac xs)
apply(auto)
done

lemma r_3_1_2:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==> (nrel next)^* `` {s0} <=
           insert (hd f)
            (s Un set tr Un (nrel next)^* `` (set (tl f) Un (UN x:set fs. set x)))"

apply(rule subsetI)
apply(drule equalityD2)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(simp)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)

apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
defer
apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(rule UnI2)
apply(simp)
apply(rule_tac x=xb in bexI)
apply(simp)
apply(simp)

(* next(hd f) = [] *)
apply(rotate_tac -2)
apply(erule rtrancl_induct)
apply(case_tac f)
apply(simp)
apply(simp)
apply(erule disjE)
apply(simp)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(subgoal_tac "xa : (set list Un (UN x:set fs. set x))")
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(simp)
apply(simp)

apply(rotate_tac -1)
apply(erule disjE)
(* contradict: EX z. z = r ``(hd f) *)
apply(rotate_tac -2)
apply(drule r1)
apply(clarsimp)
apply(rotate_tac -1)
apply(erule disjE)
(* y : s --> z : s *)
apply(blast)
apply(rotate_tac -1)
apply(erule disjE)
(* image of hd tr = s Un set f, tl tr = tr or fs *)
apply(case_tac tr)
apply(clarsimp)
apply(simp)
apply(rotate_tac -2)
apply(erule disjE)
apply(simp)
apply(rotate_tac -2)
apply(drule r1)
apply(subgoal_tac "z : s Un set f")
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(simp)
apply(case_tac f)
apply(simp)
apply(simp)
apply(rotate_tac -2)
apply(erule disjE)
apply(simp)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(subgoal_tac "z : (set lista Un (UN x:set fs. set x))")
apply(blast)
apply(simp)
apply(blast)
apply(rotate_tac -1)
apply(frule r9)
apply(erule exE)
apply(rotate_tac 7)
apply(drule_tac x=i in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(simp)
apply(rotate_tac -1)
apply(drule_tac c=z in subsetD)
apply(rule r1)
apply(simp)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(case_tac i)
apply(clarsimp)
apply(clarsimp)

apply(rotate_tac -1)
apply(erule disjE)
apply(simp)

apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(subgoal_tac "z : (set (tl f) Un (UN x:set fs. set x))")
apply(blast)
apply(rule UnI2)
apply(simp)
apply(rule_tac x="fs ! i" in bexI)
apply(simp)
apply(simp)

apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xb in ImageI)
apply(erule transitive_closure_trans)
apply(blast)
apply(clarsimp)

apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xb in ImageI)
apply(erule transitive_closure_trans)
apply(blast)
apply(clarsimp)
done

lemma r_3_2:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==>
           nrel next `` insert (hd f) s <= insert (hd f) s"
apply(rule subsetI)
apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(drule_tac c=x in subsetD)
apply(rotate_tac -1)
apply(erule disjE)
apply(drule r1)
apply(clarsimp)
apply(erule ImageI)
apply(simp)
apply(simp)
done

lemma r_3_3:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==>
           (tr ~= [] --> set (next (hd tr)) <= insert (hd f) (s Un set (tl f)))"
apply(rule impI)
apply(drule mp)
apply(simp)
apply(case_tac f)
apply(auto)
done

lemma r_3_4:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==>
           (tr ~= [] --> (ALL q. q : set (tl f) --> (hd tr, q) : nrel next))"
apply(case_tac f)
apply(auto)
done

lemma r_3_6:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==>
           (ALL i set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) = [] |]
       ==>
           (ALL q. (hd f, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+)"
apply(rule allI)
apply(rule impI)
apply(rotate_tac -1)
apply(erule rtrancl_induct)
apply(erule contrapos_nn)
apply(rotate_tac -1)
apply(drule tranclD)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule r1)
apply(clarsimp)

apply(rotate_tac -3)
apply(erule converse_rtranclE)
apply(clarsimp)
apply(drule r1)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule r1)
apply(clarsimp)
done

lemma r_4_1_1:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==> insert (hd f)
            (s Un set tr Un
             (nrel next)^* ``
             (set (next (hd f)) Un (set (tl f) Un (UN x:set fs. set x)))) <=
           (nrel next)^* `` {s0}"

apply(rule subsetI)
apply(drule equalityD1)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
defer
apply(simp)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(subgoal_tac "x : (set f Un UNION (set fs) set)")
apply(blast)
apply(case_tac f)
apply(simp)
apply(clarsimp)
apply(rotate_tac -1)
apply(erule disjE)
apply(clarsimp)
apply(rotate_tac -1)
apply(erule disjE)
apply(clarsimp)
apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)
apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a="hd f" in ImageI)
apply(rule_tac b=xa in converse_rtrancl_into_rtrancl)
apply(subst nrel_def)
apply(clarsimp)
apply(simp)
apply(clarsimp)

apply(rotate_tac -1)
apply(erule disjE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a="xa" in ImageI)
apply(simp)
apply(case_tac f)
apply(clarsimp)
apply(clarsimp)

apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a="xa" in ImageI)
apply(auto)
done

lemma r_4_1_2:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==>
           (nrel next)^* `` {s0} <=
           insert (hd f)
            (s Un set tr Un
             (nrel next)^* ``
             (set (next (hd f)) Un (set (tl f) Un (UN x:set fs. set x))))"

apply(rule subsetI)
apply(drule equalityD2)
apply(rotate_tac -1)
apply(drule_tac c=x in subsetD)
apply(simp)
apply(simp)

apply(rotate_tac -1)
apply(erule disjE)
apply(clarsimp)

apply(rotate_tac -1)
apply(erule disjE)
apply(clarsimp)

apply(rotate_tac -1)
apply(erule ImageE)
apply(simp)

apply(rotate_tac -1)
apply(erule disjE)
defer
apply(erule bexE)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(simp)
apply(rule UnI2)
apply(rule UnI2)
apply(simp)
apply(rule_tac x=xb in bexI)
apply(simp)
apply(simp)

apply(case_tac f)
apply(simp)
apply(simp)
apply(rotate_tac -2)
apply(erule disjE)
apply(simp)
apply(rotate_tac -2)
apply(erule converse_rtranclE)
apply(clarsimp)
apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=y in ImageI)
apply(clarsimp)
apply(drule r1)
apply(clarsimp)

apply(rule disjI2)
apply(rule disjI2)
apply(rule disjI2)
apply(rule_tac a=xa in ImageI)
apply(clarsimp)
apply(clarsimp)
done

lemma r_4_4:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==>
           (ALL q. q : set (next (hd f)) --> (hd f, q) : nrel next)"
apply(unfold nrel_def)
apply(auto)
done

lemma r_4_5:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==>
           (ALL i set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==>
           (ALL i 0 *)
apply(rotate_tac 5)
apply(drule_tac x="nat" in spec)
apply(auto)
done

lemma r_4_7:
  "[| s Un set tr Un (nrel next)^* `` (set f Un (UN x:set fs. set x)) =
          (nrel next)^* `` {s0};
          nrel next `` s <= s; tr ~= [] --> set (next (hd tr)) <= s Un set f;
          tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : nrel next);
          ALL i (tr ! Suc i, q) : nrel next;
          ALL p. p : s -->
                 (ALL q. (p, q) : (nrel next)^* --> (q, q) ~: (nrel next)^+);
          length fs = length tr; f ~= []; hd f ~: set tr; hd f ~: s;
          next (hd f) ~= [] |]
       ==>
           (ALL i (tr ! i, q) : nrel next)"
apply(rule allI)
apply(rule impI)
apply(rule allI)
apply(rule impI)
apply(case_tac i)
(* i=0 *)
apply(simp)
apply(case_tac tr)
apply(simp)
apply(simp)
apply(drule_tac x="q" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(case_tac f)
apply(simp)
apply(simp)
apply(simp)
(* i > 0 *)
apply(rotate_tac 6)
apply(drule_tac x="nat" in spec)
apply(auto)
done


lemma r10:
  "(ALL i. i < length tr - 1 --> (tr ! Suc i, tr ! i) : r)
  --> (ALL i j. i < j & j < length tr --> (tr ! j, tr ! i) : r^+)"
apply(induct_tac tr)
apply(auto)
apply(drule_tac x="Suc ia" in spec)
apply(clarsimp)
apply(case_tac j)
apply(auto)
apply(case_tac "i=nat")
apply(clarsimp)
apply(drule_tac x="nat" in spec)
apply(clarsimp)
apply(simp)
apply(drule_tac x="i" in spec)
apply(drule_tac x="i" in spec)
apply(drule_tac x="nat" in spec)
apply(auto)
done

lemma r11:
  "[| ALL i. i < length tr - 1 --> (tr ! Suc i, tr ! i) : r;
      i < j; j < length tr |] ==>
  (tr ! j, tr ! i) : r^+"
apply(drule r10[THEN mp])
apply(auto)
done

lemma r12:
  "[| (ALL i. i < length tr - 1 --> (tr ! Suc i, tr ! i) : r);
      k < length tr;
      (hd tr, tr ! k) : r |] ==>
  (tr ! k, tr ! k) : r^+"
apply(case_tac k)
apply(case_tac tr)
apply(clarsimp)
apply(simp)
apply(clarsimp)
apply(rename_tac k)
apply(subgoal_tac "(tr ! Suc k, tr ! 0) : r^+")
apply(case_tac tr)
apply(simp)
apply(simp)
apply(rule r11)
apply(auto)
done

lemma cycle:
  "r = nrel next ==>
  VARS s f fs tr xs
  {True}
  s := {};
  f := [s0];
  tr := [];
  fs := [];
  WHILE ~((f = [] & fs = []) | (f ~= [] & (hd f) : set tr))
  INV {
    s Un (set tr) Un r^* `` ((set f) Un Union (set (map set fs))) = r^* `` {s0} &
    r `` s <= s &
    (tr ~= [] --> set (next (hd tr)) <= s Un (set f)) &
    (tr ~= [] --> (ALL q. q : set f --> (hd tr, q) : r)) &
    (ALL i. i < length tr - 1 --> (tr ! (i + 1), tr ! i) : r) &
    (ALL i. i < length tr - 1 -->
       set (next (tr ! (i + 1))) <= s Un {tr ! i} Un set (fs ! i)) &
    (ALL i. i < length tr - 1 -->
       (ALL q. q : set (fs ! i) --> (tr ! (i + 1), q) : r)) &
    (ALL p. p : s --> (ALL q. (p, q) : r^* --> (q, q) ~: r^+)) &
    length fs = length tr
  }
  DO
    IF f = [] THEN
      f := hd fs;
      fs := tl fs;
      s := s Un {hd tr};
      tr := tl tr
    ELSE
      IF hd f : s THEN
        f := tl f
      ELSE
        xs := next (hd f);
        IF xs = [] THEN
          s := s Un {hd f};
          f := tl f
        ELSE
          tr := (hd f) # tr;
          fs := (tl f) # fs;
          f := xs
        FI
      FI
    FI
  OD
  {(f ~= []) = (EX q. (s0, q) : r^* & (q, q) : r^+)}"

apply(vcg)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp)
(* 1/4 *)
apply(rule conjI)
apply(rule r_1_1)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_2)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_3)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_4)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_5)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_6)
apply(assumption+)
apply(rule conjI)
apply(rule r_1_7)
apply(assumption+)
apply(rule r_1_8)
apply(assumption+)
(* 2/4 *)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp)
apply(rule conjI)
apply(rule subset_antisym)
apply(rule r_2_1_1)
apply(assumption+)
apply(rule r_2_1_2)
apply(assumption+)
apply(rule conjI)
apply(rule r_2_3)
apply(assumption+)
apply(rule r_2_4)
apply(assumption+)
(* 3/4 *)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp)
apply(rule conjI)
apply(rule subset_antisym)
apply(rule r_3_1_1)
apply(assumption+)
apply(rule r_3_1_2)
apply(assumption+)
apply(rule conjI)
apply(rule r_3_2)
apply(assumption+)
apply(rule conjI)
apply(rule r_3_3)
apply(assumption+)
apply(rule conjI)
apply(rule r_3_4)
apply(assumption+)
apply(rule conjI)
apply(rule r_3_6)
apply(assumption+)
apply(rule r_3_8)
apply(assumption+)
(* 4/4 *)
apply(clarsimp)
apply(rule conjI)
apply(rule subset_antisym)
apply(rule r_4_1_1)
apply(assumption+)
apply(rule r_4_1_2)
apply(assumption+)
apply(rule conjI)
apply(rule r_4_4)
apply(assumption+)
apply(rule conjI)
apply(rule r_4_5)
apply(assumption+)
apply(rule conjI)
apply(rule r_4_6)
apply(assumption+)
apply(rule r_4_7)
apply(assumption+)
(* conclusion *)
apply(rule iffI)
defer
apply(clarsimp)
apply(clarsimp)
apply(rule_tac x="hd f" in exI)
apply(auto)
(* ALL q. q : set f --> (hd tr, q) : r follows (hd tr, hd f) : r *)
apply(rotate_tac -1)
apply(drule_tac x="hd f" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(simp)
(* hd f : set tr implys EX i. hd f = tr ! i *)
apply(rotate_tac -3)
apply(drule r9)
apply(clarsimp)
apply(rule r12)
apply(simp)
apply(simp)
apply(simp)
done
2014/12/16
© 2013,2014,2015 PRINCIPIA Limited