theory PrioG

imports PrioGDef 

begin

lemma runing_ready: 

  shows "runing s \<subseteq> readys s"

  unfolding runing_def readys_def

  by auto 

lemma readys_threads:

  shows "readys s \<subseteq> threads s"

  unfolding readys_def

  by auto

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 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 (wq_fun (schs s) cs)"

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

    show "False" 

    proof -

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

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

        by (simp add:runing_def readys_def s_waiting_def wq_def)

      from this [OF h2] have "thread = hd (wq_fun (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 dst: "distinct list"

    show "distinct (SOME q. distinct q \<and> set q = set list)"

    proof(rule someI2)

      from dst show  "distinct list \<and> set list = set list" by auto

    next

      fix q assume "distinct q \<and> set q = set list"

      thus "distinct q" by auto

    qed

  qed

qed

lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"

  by(ind_cases "vt (e#s)", simp)

lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"

  by(ind_cases "vt (e#s)", simp)

lemma block_pre: 

  fixes thread cs s

  assumes vt_e: "vt (e#s)"

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

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

  shows "e = P thread cs"

proof -

  show ?thesis

  proof(cases e)

    case (P th cs)

    with assms

    show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Create th prio)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Exit th)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Set th prio)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (V th cs)

    with assms show ?thesis

      apply (auto simp:wq_def Let_def split:if_splits)

    proof -

      fix q qs

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

        and h2: "q # qs = wq_fun (schs s) cs"

        and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"

        and vt: "vt (V th cs # s)"

      from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp

      moreover have "thread \<in> set qs"

      proof -

        have "set (SOME q. distinct q \<and> set q = set qs) = set qs"

        proof(rule someI2)

          from wq_distinct [OF step_back_vt[OF vt], of cs]

          and h2[symmetric, folded wq_def]

          show "distinct qs \<and> set qs = set qs" by auto

        next

          fix x assume "distinct x \<and> set x = set qs"

          thus "set x = set qs" by auto

        qed

        with h3 show ?thesis by simp

      qed

      ultimately show "False" by auto

      qed

  qed

qed

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

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

apply (ind_cases "vt ((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 (a#s)"

lemma abs2:

  assumes vt: "vt (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 -

  from assms show "False"

    apply (cases e)

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

    apply (insert abs1, fast)[1]

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

  proof -

    fix th qs

    assume vt: "vt (V th cs # s)"

      and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"

      and eq_wq: "wq_fun (schs s) cs = thread # qs"

    show "False"

    proof -

      from wq_distinct[OF step_back_vt[OF vt], of cs]

        and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp

      moreover have "thread \<in> set qs"

      proof -

        have "set (SOME q. distinct q \<and> set q = set qs) = set qs"

        proof(rule someI2)

          from wq_distinct [OF step_back_vt[OF vt], of cs]

          and eq_wq [folded wq_def]

          show "distinct qs \<and> set qs = set qs" by auto

        next

          fix x assume "distinct x \<and> set x = set qs"

          thus "set x = set qs" by auto

        qed

        with th_in show ?thesis by auto

      qed

      ultimately show ?thesis by auto

    qed

  qed

qed

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

proof(induct s, simp)

  fix a s t

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

    and vt_a: "vt (a # s)"

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

  show "vt (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 s"

      by (erule_tac evt_cons, simp)

    from h [OF this le_t1] have "vt (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 (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

*)

lemma waiting_unique_pre:

  fixes cs1 cs2 s thread

  assumes vt: "vt 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 (e#moment t2 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt (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 vt_e False h1]

        have "e = P thread cs2" .

        with vt_e have "vt ((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 wq_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  (e#moment t1 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt (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 vt_e False h1]

        have "e = P thread cs1" .

        with vt_e have "vt ((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 wq_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 (e#moment t1 s)"

      proof -

        from vt_moment [OF vt le_t3]

        have "vt (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 vt_e 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 (e#moment t2 s)" by simp 

          from abs2 [OF this True eq_th h2 h1]

          show ?thesis .

        next

          case False

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

          proof -

            from vt_moment [OF vt le_t3] eqt12

            have "vt (moment (Suc t2) s)" by auto

            with eq_m eqt12 show ?thesis by simp

          qed

          from block_pre [OF vt_e 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:

  fixes s cs1 cs2

  assumes "vt s"

  and "waiting s th cs1"

  and "waiting s th cs2"

  shows "cs1 = cs2"

using waiting_unique_pre assms

unfolding wq_def s_waiting_def

by auto

(* not used *)

lemma held_unique:

  fixes s::"state"

  assumes "holding s th1 cs"

  and "holding s th2 cs"

  shows "th1 = th2"

using assms

unfolding s_holding_def

by auto

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

lemma unique_minus:

  fixes x y z r

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r"

  and xz: "(x, z) \<in> r^+"

  and neq: "y \<noteq> z"

  shows "(y, z) \<in> r^+"

by (metis neq rtranclD tranclD unique xy xz)

lemma unique_base:

  fixes r x y z

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r"

  and xz: "(x, z) \<in> r^+"

  and neq_yz: "y \<noteq> z"

  shows "(y, z) \<in> r^+"

by (metis neq_yz unique unique_minus xy xz)

lemma unique_chain:

  fixes r x y z

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r^+"

  and xz: "(x, z) \<in> r^+"

  and neq_yz: "y \<noteq> z"

  shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"

proof -

  from xy xz neq_yz show ?thesis

  proof(induct)

    case (base y)

    have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto

    from unique_base [OF _ h1 h2 h3] and unique show ?case by auto

  next

    case (step y za)

    show ?case

    proof(cases "y = z")

      case True

      from True step show ?thesis by auto

    next

      case False

      from False step have "(y, z) \<in> r\<^sup>+ \<or> (z, y) \<in> r\<^sup>+" by auto

      thus ?thesis

      proof

        assume "(z, y) \<in> r\<^sup>+"

        with step have "(z, za) \<in> r\<^sup>+" by auto

        thus ?thesis by auto

      next

        assume h: "(y, z) \<in> r\<^sup>+"

        from step have yza: "(y, za) \<in> r" by simp

        from step have "za \<noteq> z" by simp

        from unique_minus [OF _ yza h this] and unique

        have "(za, z) \<in> r\<^sup>+" by auto

        thus ?thesis by auto

      qed

    qed

  qed

qed

lemma depend_set_unchanged: "(depend (Set th prio # s)) = depend s"

apply (unfold s_depend_def s_waiting_def wq_def)

by (simp add:Let_def)

lemma depend_create_unchanged: "(depend (Create th prio # s)) = depend s"

apply (unfold s_depend_def s_waiting_def wq_def)

by (simp add:Let_def)

lemma depend_exit_unchanged: "(depend (Exit th # s)) = depend s"

apply (unfold s_depend_def s_waiting_def wq_def)

by (simp add:Let_def)

lemma step_v_hold_inv[elim_format]:

  "\<And>c t. \<lbrakk>vt (V th cs # s); 

  \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"

proof -

  fix c t

  assume vt: "vt (V th cs # s)"

    and nhd: "\<not> holding (wq s) t c"

    and hd: "holding (wq (V th cs # s)) t c"

  show "next_th s th cs t \<and> c = cs"

  proof(cases "c = cs")

    case False

    with nhd hd show ?thesis

      by (unfold cs_holding_def wq_def, auto simp:Let_def)

  next

    case True

    with step_back_step [OF vt] 

    have "step s (V th c)" by simp

    hence "next_th s th cs t"

    proof(cases)

      assume "holding s th c"

      with nhd hd show ?thesis

        apply (unfold s_holding_def cs_holding_def wq_def next_th_def,

               auto simp:Let_def split:list.splits if_splits)

        proof -

          assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"

          moreover have "\<dots> = set []"

          proof(rule someI2)

            show "distinct [] \<and> [] = []" by auto

          next

            fix x assume "distinct x \<and> x = []"

            thus "set x = set []" by auto

          qed

          ultimately show False by auto

        next

          assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"