theory Prio

imports Precedence_ord Moment Lsp Happen_within

begin

type_synonym thread = nat

type_synonym priority = nat

type_synonym cs = nat

datatype event = 

  Create thread priority |

  Exit thread |

  P thread cs |

  V thread cs |

  Set thread priority

datatype node = 

   Th "thread" |

   Cs "cs"

type_synonym state = "event list"

fun threads :: "state \<Rightarrow> thread set"

where 

  "threads [] = {}" |

  "threads (Create thread prio#s) = {thread} \<union> threads s" |

  "threads (Exit thread # s) = (threads s) - {thread}" |

  "threads (e#s) = threads s"

fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> nat"

where

  "original_priority thread [] = 0" |

  "original_priority thread (Create thread' prio#s) = 

     (if thread' = thread then prio else original_priority thread s)" |

  "original_priority thread (Set thread' prio#s) = 

     (if thread' = thread then prio else original_priority thread s)" |

  "original_priority thread (e#s) = original_priority thread s"

fun birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"

where

  "birthtime thread [] = 0" |

  "birthtime thread ((Create thread' prio)#s) = (if (thread = thread') then length s 

                                                  else birthtime thread s)" |

  "birthtime thread ((Set thread' prio)#s) = (if (thread = thread') then length s 

                                                  else birthtime thread s)" |

  "birthtime thread (e#s) = birthtime thread s"

definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

  where "preced thread s = Prc (original_priority thread s) (birthtime thread s)"

consts holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"

       waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"

       depend :: "'b \<Rightarrow> (node \<times> node) set"

       dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"

defs (overloaded) cs_holding_def: "holding wq thread cs == (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"

                  cs_waiting_def: "waiting wq thread cs == (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

                  cs_depend_def: "depend (wq::cs \<Rightarrow> thread list) == {(Th t, Cs c) | t c. waiting wq t c} \<union> 

                                               {(Cs c, Th t) | c t. holding wq t c}"

                  cs_dependents_def: "dependents (wq::cs \<Rightarrow> thread list) th == {th' . (Th th', Th th) \<in> (depend wq)^+}"

record schedule_state = 

    waiting_queue :: "cs \<Rightarrow> thread list"

    cur_preced :: "thread \<Rightarrow> precedence"

definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"

where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"

fun schs :: "state \<Rightarrow> schedule_state"

where

   "schs [] = \<lparr>waiting_queue = \<lambda> cs. [], 

               cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |

   "schs (e#s) = (let ps = schs s in

                  let pwq = waiting_queue ps in

                  let pcp = cur_preced ps in

                  let nwq = case e of

                             P thread cs \<Rightarrow>  pwq(cs:=(pwq cs @ [thread])) |

                             V thread cs \<Rightarrow> let nq = case (pwq cs) of

                                                      [] \<Rightarrow> [] | 

                                                      (th#pq) \<Rightarrow> case (lsp pcp pq) of

                                                                   (l, [], r) \<Rightarrow> []

                                                                 | (l, m#ms, r) \<Rightarrow> m#(l@ms@r)

                                            in pwq(cs:=nq)                 |

                              _ \<Rightarrow> pwq

                  in let ncp = cpreced (e#s) nwq in 

                     \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>

                 )"

definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 

where "wq s == waiting_queue (schs s)"

definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

where "cp s = cur_preced (schs s)"

defs (overloaded) s_holding_def: "holding (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"

                  s_waiting_def: "waiting (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"

                  s_depend_def: "depend (s::state) == {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> 

                                               {(Cs c, Th t) | c t. holding (wq s) t c}"

                  s_dependents_def: "dependents (s::state) th == {th' . (Th th', Th th) \<in> (depend (wq s))^+}"

definition readys :: "state \<Rightarrow> thread set"

where

  "readys s = 

     {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}"

definition runing :: "state \<Rightarrow> thread set"

where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"

definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"

  where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"

inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"

where

  thread_create: "\<lbrakk>prio \<le> max_prio; thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |

  thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |

  thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (depend s)^+\<rbrakk> \<Longrightarrow> step s (P thread cs)" |

  thread_V: "\<lbrakk>thread \<in> runing s;  holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |

  thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"

inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"

 for cs

where

  vt_nil[intro]: "vt cs []" |

  vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)"

lemma runing_ready: "runing s \<subseteq> readys s"

  by (auto simp only:runing_def readys_def)

lemma wq_v_eq_nil: 

  fixes s cs thread rest

  assumes eq_wq: "wq s cs = thread # rest"

  and eq_lsp: "lsp (cp s) rest = (l, [], r)"

  shows "wq (V thread cs#s) cs = []"

proof -

  from prems show ?thesis

    by (auto simp:wq_def Let_def cp_def split:list.splits)

qed

lemma wq_v_eq: 

  fixes s cs thread rest

  assumes eq_wq: "wq s cs = thread # rest"

  and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"

  shows "wq (V thread cs#s) cs = th'#l@r"

proof -

  from prems show ?thesis

    by (auto simp:wq_def Let_def cp_def split:list.splits)

qed

lemma wq_v_neq:

   "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"

  by (auto simp:wq_def Let_def cp_def split:list.splits)

lemma wq_distinct: "vt step s \<Longrightarrow> distinct (wq s cs)"

proof(erule_tac vt.induct, simp add:wq_def)

  fix s e

  assume h1: "step s e"

  and h2: "distinct (wq s cs)"

  thus "distinct (wq (e # s) cs)"

  proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)

    fix thread s

    assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"

      and h2: "thread \<in> set (waiting_queue (schs s) cs)"

      and h3: "thread \<in> runing s"

    show "False" 

    proof -

      from h3 have "\<And> cs. thread \<in>  set (waiting_queue (schs s) cs) \<Longrightarrow> 

                             thread = hd ((waiting_queue (schs s) cs))" 

        by (simp add:runing_def readys_def s_waiting_def wq_def)

      from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .

      with h2

      have "(Cs cs, Th thread) \<in> (depend s)"

        by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)

      with h1 show False by auto

    qed

  next

    fix thread s a list

    assume h1: "thread \<in> runing s" 

      and h2: "holding s thread cs"

      and h3: "waiting_queue (schs s) cs = a # list"

      and h4: "a \<notin> set list"

      and h5: "distinct list"

    thus "distinct

           ((\<lambda>(l, a, r). case a of [] \<Rightarrow> [] | m # ms \<Rightarrow> m # l @ ms @ r)

             (lsp (cur_preced (schs s)) list))"

    apply (cases "(lsp (cur_preced (schs s)) list)", simp)

    apply (case_tac b, simp)

    by (drule_tac lsp_set_eq, simp)

  qed

qed

lemma block_pre: 

  fixes thread cs s

  assumes s_ni: "thread \<notin>  set (wq s cs)"

  and s_i: "thread \<in> set (wq (e#s) cs)"

  shows "e = P thread cs"

proof -

  have ee: "\<And> x y. \<lbrakk>x = y\<rbrakk> \<Longrightarrow> set x = set y"

    by auto

  from s_ni s_i show ?thesis

  proof (cases e, auto split:if_splits simp add:Let_def wq_def)

    fix uu uub uuc uud uue

    assume h: "(uuc, thread # uu, uub) = lsp (cur_preced (schs s)) uud"

      and h1 [symmetric]: "uue # uud = waiting_queue (schs s) cs"

      and h2: "thread \<notin> set (waiting_queue (schs s) cs)"

    from lsp_set [OF h] have "set (uuc @ (thread # uu) @ uub) = set uud" .

    hence "thread \<in> set uud" by auto

    with h1 have "thread \<in> set (waiting_queue (schs s) cs)" by auto

    with h2 show False by auto

  next

    fix uu uua uub uuc uud uue

    assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

      and h2: "uue # uud = waiting_queue (schs s) cs"

      and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

      and h4: "thread \<in> set uuc"

    from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

    with h4 have "thread \<in> set uud" by auto

    with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

      apply (drule_tac ee) by auto

    with h1 show "False" by fast

  next

    fix uu uua uub uuc uud uue

    assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

      and h2: "uue # uud = waiting_queue (schs s) cs"

      and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

      and h4: "thread \<in> set uu"

    from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

    with h4 have "thread \<in> set uud" by auto

    with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

      apply (drule_tac ee) by auto

    with h1 show "False" by fast

  next

    fix uu uua uub uuc uud uue

    assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

      and h2: "uue # uud = waiting_queue (schs s) cs"

      and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

      and h4: "thread \<in> set uub"

    from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

    with h4 have "thread \<in> set uud" by auto

    with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

      apply (drule_tac ee) by auto

    with h1 show "False" by fast

  qed

qed

lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 

  thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (depend s)^+"

apply (ind_cases "vt step ((P thread cs)#s)")

apply (ind_cases "step s (P thread cs)")

by auto

lemma abs1:

  fixes e es

  assumes ein: "e \<in> set es"

  and neq: "hd es \<noteq> hd (es @ [x])"

  shows "False"

proof -

  from ein have "es \<noteq> []" by auto

  then obtain e ess where "es = e # ess" by (cases es, auto)

  with neq show ?thesis by auto

qed

lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"

  by (cases es, auto)

inductive_cases evt_cons: "vt cs (a#s)"

lemma abs2:

  assumes vt: "vt step (e#s)"

  and inq: "thread \<in> set (wq s cs)"

  and nh: "thread = hd (wq s cs)"

  and qt: "thread \<noteq> hd (wq (e#s) cs)"

  and inq': "thread \<in> set (wq (e#s) cs)"

  shows "False"

proof -

  have ee: "\<And> uuc thread uu uub s list. (uuc, thread # uu, uub) = lsp (cur_preced (schs s)) list \<Longrightarrow> 

                 lsp (cur_preced (schs s)) list = (uuc, thread # uu, uub) 

               " by simp

  from prems show "False"

    apply (cases e)

    apply ((simp split:if_splits add:Let_def wq_def)[1])+

    apply (insert abs1, fast)[1] 

    apply ((simp split:if_splits add:Let_def)[1])+

    apply (simp split:if_splits list.splits add:Let_def wq_def) 

    apply (auto dest!:ee)

    apply (drule_tac lsp_set_eq, simp)

    apply (subgoal_tac "distinct (waiting_queue (schs s) cs)", simp, fold wq_def)

    apply (rule_tac wq_distinct, auto)

    apply (erule_tac evt_cons, auto)

    apply (drule_tac lsp_set_eq, simp)

    apply (subgoal_tac "distinct (wq s cs)", simp)

    apply (rule_tac wq_distinct, auto)

    apply (erule_tac evt_cons, auto)

    apply (drule_tac lsp_set_eq, simp)

    apply (subgoal_tac "distinct (wq s cs)", simp)

    apply (rule_tac wq_distinct, auto)

    apply (erule_tac evt_cons, auto)

    apply (auto simp:wq_def Let_def split:if_splits prod.splits)

    done

qed

lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"

proof(induct s, simp)

  fix a s t

  assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"

    and vt_a: "vt cs (a # s)"

    and le_t: "t \<le> length (a # s)"

  show "vt cs (moment t (a # s))"

  proof(cases "t = length (a#s)")

    case True

    from True have "moment t (a#s) = a#s" by simp

    with vt_a show ?thesis by simp

  next

    case False

    with le_t have le_t1: "t \<le> length s" by simp

    from vt_a have "vt cs s"

      by (erule_tac evt_cons, simp)

    from h [OF this le_t1] have "vt cs (moment t s)" .

    moreover have "moment t (a#s) = moment t s"

    proof -

      from moment_app [OF le_t1, of "[a]"] 

      show ?thesis by simp

    qed

    ultimately show ?thesis by auto

  qed

qed

(* Wrong:

    lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

*)

lemma waiting_unique_pre:

  fixes cs1 cs2 s thread

  assumes vt: "vt step s"

  and h11: "thread \<in> set (wq s cs1)"

  and h12: "thread \<noteq> hd (wq s cs1)"

  assumes h21: "thread \<in> set (wq s cs2)"

  and h22: "thread \<noteq> hd (wq s cs2)"

  and neq12: "cs1 \<noteq> cs2"

  shows "False"

proof -

  let "?Q cs s" = "thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"

  from h11 and h12 have q1: "?Q cs1 s" by simp

  from h21 and h22 have q2: "?Q cs2 s" by simp

  have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)

  have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)

  from p_split [of "?Q cs1", OF q1 nq1]

  obtain t1 where lt1: "t1 < length s"

    and np1: "\<not>(thread \<in> set (wq (moment t1 s) cs1) \<and>

        thread \<noteq> hd (wq (moment t1 s) cs1))"

    and nn1: "(\<forall>i'>t1. thread \<in> set (wq (moment i' s) cs1) \<and>

             thread \<noteq> hd (wq (moment i' s) cs1))" by auto

  from p_split [of "?Q cs2", OF q2 nq2]

  obtain t2 where lt2: "t2 < length s"

    and np2: "\<not>(thread \<in> set (wq (moment t2 s) cs2) \<and>

        thread \<noteq> hd (wq (moment t2 s) cs2))"

    and nn2: "(\<forall>i'>t2. thread \<in> set (wq (moment i' s) cs2) \<and>

             thread \<noteq> hd (wq (moment i' s) cs2))" by auto

  show ?thesis

  proof -

    { 

      assume lt12: "t1 < t2"

      let ?t3 = "Suc t2"

      from lt2 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto

      have "t2 < ?t3" by simp

      from nn2 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

        h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

      have vt_e: "vt step (e#moment t2 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt step (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

        case True

        from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

          by auto

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF False h1]

        have "e = P thread cs2" .

        with vt_e have "vt step ((P thread cs2)# moment t2 s)" by simp

        from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp

        with runing_ready have "thread \<in> readys (moment t2 s)" by auto

        with nn1 [rule_format, OF lt12]

        show ?thesis  by (simp add:readys_def s_waiting_def, auto)

      qed

    } moreover {

      assume lt12: "t2 < t1"

      let ?t3 = "Suc t1"

      from lt1 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

      have lt_t3: "t1 < ?t3" by simp

      from nn1 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

        h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

      have vt_e: "vt step (e#moment t1 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt step (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

        case True

        from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

          by auto

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF False h1]

        have "e = P thread cs1" .

        with vt_e have "vt step ((P thread cs1)# moment t1 s)" by simp

        from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp

        with runing_ready have "thread \<in> readys (moment t1 s)" by auto

        with nn2 [rule_format, OF lt12]

        show ?thesis  by (simp add:readys_def s_waiting_def, auto)

      qed

    } moreover {

      assume eqt12: "t1 = t2"

      let ?t3 = "Suc t1"

      from lt1 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

      have lt_t3: "t1 < ?t3" by simp

      from nn1 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

        h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

      have vt_e: "vt step (e#moment t1 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt step (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

        case True

        from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

          by auto

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF False h1]

        have eq_e1: "e = P thread cs1" .

        have lt_t3: "t1 < ?t3" by simp

        with eqt12 have "t2 < ?t3" by simp

        from nn2 [rule_format, OF this] and eq_m and eqt12

        have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

          h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

        show ?thesis

        proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

          case True

          from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

            by auto

          from vt_e and eqt12 have "vt step (e#moment t2 s)" by simp 

          from abs2 [OF this True eq_th h2 h1]

          show ?thesis .

        next

          case False

          from block_pre [OF False h1]

          have "e = P thread cs2" .

          with eq_e1 neq12 show ?thesis by auto

        qed

      qed

    } ultimately show ?thesis by arith

  qed

qed

lemma waiting_unique:

  assumes "vt step s"

  and "waiting s th cs1"

  and "waiting s th cs2"

  shows "cs1 = cs2"

proof -

  from waiting_unique_pre and prems

  show ?thesis

    by (auto simp add:s_waiting_def)

qed

lemma holded_unique:

  assumes "vt step s"

  and "holding s th1 cs"

  and "holding s th2 cs"

  shows "th1 = th2"

proof -

  from prems show ?thesis

    unfolding s_holding_def

    by auto

qed

lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits)

lemma birthtime_unique: 

  "\<lbrakk>birthtime th1 s = birthtime th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>

          \<Longrightarrow> th1 = th2"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits dest:birthtime_lt)

lemma preced_unique : 

  assumes pcd_eq: "preced th1 s = preced th2 s"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "th1 = th2"

proof -

  from pcd_eq have "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)

  from birthtime_unique [OF this th_in1 th_in2]

  show ?thesis .

qed

lemma preced_linorder: 

  assumes neq_12: "th1 \<noteq> th2"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"

proof -

  from preced_unique [OF _ th_in1 th_in2] and neq_12 

  have "preced th1 s \<noteq> preced th2 s" by auto

  thus ?thesis by auto

qed