theory ExtGG

begin

lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"

  apply (induct s, simp)

proof -

  fix a s

  assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"

    and eq_as: "a # s \<noteq> []"

  show "last_set th (a # s) < length (a # s)"

  proof(cases "s \<noteq> []")

    case False

    from False show ?thesis

      by (cases a, auto simp:last_set.simps)

  next

    case True

    from ih [OF True] show ?thesis

      by (cases a, auto simp:last_set.simps)

  qed

qed

lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"

  by (induct s, auto simp:threads.simps)

lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"

  apply (drule_tac th_in_ne)

  by (unfold preced_def, auto intro: birth_time_lt)

locale highest_gen =

  fixes s th prio tm

  assumes vt_s: "vt s"

  and threads_s: "th \<in> threads s"

  and highest: "preced th s = Max ((cp s)`threads s)"

  and preced_th: "preced th s = Prc prio tm"

context highest_gen

begin

lemma lt_tm: "tm < length s"

  by (insert preced_tm_lt[OF threads_s preced_th], simp)

proof -

qed

lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"

  by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp)

lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"

  by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

lemma highest': "cp s th = Max (cp s ` threads s)"

proof -

  from highest_cp_preced max_cp_eq[OF vt_s, symmetric]

  show ?thesis by simp

qed

end

locale extend_highest_gen = highest_gen + 

  fixes t 

  assumes vt_t: "vt (t@s)"

  and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"

  and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"

  and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"

lemma step_back_vt_app: 

  assumes vt_ts: "vt (t@s)" 

  shows "vt s"

proof -

  from vt_ts show ?thesis

  proof(induct t)

    case Nil

    from Nil show ?case by auto

  next

    case (Cons e t)

    assume ih: " vt (t @ s) \<Longrightarrow> vt s"

      and vt_et: "vt ((e # t) @ s)"

    show ?case

    proof(rule ih)

      show "vt (t @ s)"

      proof(rule step_back_vt)

        from vt_et show "vt (e # t @ s)" by simp

      qed

    qed

  qed

qed

  apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

  apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)

  by (unfold highest_gen_def, auto dest:step_back_vt_app)

  assumes 

    h0: "R []"

  and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 

                    extend_highest_gen s th prio tm t; 

                    extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

  shows "R t"

proof -

  from vt_t extend_highest_gen_axioms show ?thesis

  proof(induct t)

    from h0 show "R []" .

  next

    case (Cons e t')

    assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"

      and vt_e: "vt ((e # t') @ s)"

      and et: "extend_highest_gen s th prio tm (e # t')"

    from vt_e and step_back_step have stp: "step (t'@s) e" by auto

    from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto

    show ?case

    proof(rule h2 [OF vt_ts stp _ _ _ ])

      show "R t'"

      proof(rule ih)

        from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

      next

        from vt_ts show "vt (t' @ s)" .

      qed

    next

      from et show "extend_highest_gen s th prio tm (e # t')" .

    next

      from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

    qed

  qed

qed

lemma th_kept: "th \<in> threads (t @ s) \<and> 

proof -

  show ?thesis

  proof(induct rule:ind)

    case Nil

    from threads_s

      by auto

  next

    case (Cons e t)

    show ?case

    proof(cases e)

      case (Create thread prio)

      show ?thesis

      proof -

        hence "th \<noteq> thread"

        proof(cases)

          with Cons show ?thesis by auto

        qed

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

        moreover note Cons

        ultimately show ?thesis

      qed

    next

      case (Exit thread)

      have neq_th: "thread \<noteq> th" by auto

      with Cons

      show ?thesis

    next

      case (P thread cs)

      with Cons

      show ?thesis 

    next

      case (V thread cs)

      with Cons

      show ?thesis 

    next

      case (Set thread prio')

      show ?thesis

      proof -

        have "th \<noteq> thread" by auto

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

        moreover note Cons

        ultimately show ?thesis

      qed

    qed

  qed

qed

proof(induct rule:ind)

  case Nil

  from highest_preced_thread

next

  case (Cons e t)

  show ?case

  proof(cases e)

    case (Create thread prio')

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"

        show "finite (?f ` (threads (t@s)))" by simp

      proof -

        have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = 

      qed

      moreover have "?f thread < ?t"

      proof -

        have "prio' \<le> prio" by auto

        thus ?thesis

    qed

    case (Exit thread)

    proof -

      next

      qed

    qed

  next

    case (P thread cs)

    with Cons

  next

    case (V thread cs)

    with Cons

    case (Set thread prio')

    proof -

      let ?B = "threads (t@s)"

      from Cons have "extend_highest_gen s th prio tm (e # t)" by auto

      from extend_highest_gen.set_diff_low[OF this] and Set

      have neq_thread: "thread \<noteq> th" and le_p: "prio' \<le> prio" by auto

      from Set have "Max (?f ` ?A) = Max (?f ` ?B)" by simp

      also have "\<dots> = ?t"

      proof(rule Max_eqI)

        fix y

        assume y_in: "y \<in> ?f ` ?B"

        then obtain th1 where 

          th1_in: "th1 \<in> ?B" and eq_y: "y = ?f th1" by auto

        show "y \<le> ?t"

        proof(cases "th1 = thread")

          case True

          with neq_thread le_p eq_y Set

          show ?thesis

            apply (subst preced_th, insert lt_tm)

            by (auto simp:preced_def precedence_le_def)

        next

          case False

          with Set eq_y

          have "y  = preced th1 (t@s)"

            by (simp add:preced_def)

          moreover have "\<dots> \<le> ?t"

          proof -

            from Cons

            have "?t = Max ((\<lambda> th'. preced th' (t@s)) ` (threads (t@s)))"

              by auto

            moreover have "preced th1 (t@s) \<le> \<dots>"

            proof(rule Max_ge)

              from th1_in 

              show "preced th1 (t @ s) \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"

                by simp

            next

              show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"

              proof -

                from Cons have "vt (t @ s)" by auto

                from finite_threads[OF this] show ?thesis by auto

              qed

            qed

            ultimately show ?thesis by auto

          qed

          ultimately show ?thesis by auto

        qed

      next

        from Cons and finite_threads

        show "finite (?f ` ?B)" by auto

      next

        from Cons have "extend_highest_gen s th prio tm t" by auto

        from extend_highest_gen.th_kept [OF this]

        have h: "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .

        show "?t \<in> (?f ` ?B)" 

        proof -

          from neq_thread Set h

          have "?t = ?f th" by (auto simp:preced_def)

          with h show ?thesis by auto

        qed

      qed

      finally show ?thesis .

    qed

  qed

qed

lemma max_preced: "preced th (t@s) = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))"

  by (insert th_kept max_kept, auto)

lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" 

  (is "?L = ?R")

proof -

  have "?L = cpreced (wq (t@s)) (t@s) th" 

    by (unfold cp_eq_cpreced, simp)

  also have "\<dots> = ?R"

  proof(unfold cpreced_def)

    show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependants (wq (t @ s)) th)) =

          Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"

      (is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)")

    proof(cases "?A = {}")

      case False

      have "Max (?f ` ({th} \<union> ?A)) = Max (insert (?f th) (?f ` ?A))" by simp

      moreover have "\<dots> = max (?f th) (Max (?f ` ?A))"

      proof(rule Max_insert)

        show "finite (?f ` ?A)"

        proof -

          from dependants_threads[OF vt_t]

          have "?A \<subseteq> threads (t@s)" .

          moreover from finite_threads[OF vt_t] have "finite \<dots>" .

          ultimately show ?thesis 

            by (auto simp:finite_subset)

        qed

      next

        from False show "(?f ` ?A) \<noteq> {}" by simp

      qed

      moreover have "\<dots> = Max (?f ` ?B)"

      proof -

        from max_preced have "?f th = Max (?f ` ?B)" .

        moreover have "Max (?f ` ?A) \<le> \<dots>" 

        proof(rule Max_mono)

          from False show "(?f ` ?A) \<noteq> {}" by simp

        next

          show "?f ` ?A \<subseteq> ?f ` ?B" 

          proof -

            have "?A \<subseteq> ?B" by (rule dependants_threads[OF vt_t])

            thus ?thesis by auto

          qed

        next

          from finite_threads[OF vt_t] 

          show "finite (?f ` ?B)" by simp

        qed

        ultimately show ?thesis

          by (auto simp:max_def)

      qed

      ultimately show ?thesis by auto

    next

      case True

      with max_preced show ?thesis by auto

    qed

  qed

  finally show ?thesis .

qed

lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"

  by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp)

lemma th_cp_preced: "cp (t@s) th = preced th s"

  by (fold max_kept, unfold th_cp_max_preced, simp)

lemma preced_less:

  fixes th'

  assumes th'_in: "th' \<in> threads s"

  and neq_th': "th' \<noteq> th"

  shows "preced th' s < preced th s"

proof -

  have "preced th' s \<le> Max ((\<lambda>th'. preced th' s) ` threads s)"

  proof(rule Max_ge)

    from finite_threads [OF vt_s]

    show "finite ((\<lambda>th'. preced th' s) ` threads s)" by simp

  next

    from th'_in show "preced th' s \<in> (\<lambda>th'. preced th' s) ` threads s"

      by simp

  qed

  moreover have "preced th' s \<noteq> preced th s"

  proof

    assume "preced th' s = preced th s"

    from preced_unique[OF this th'_in] neq_th' threads_s

    show "False" by  (auto simp:readys_def)

  qed

  ultimately show ?thesis using highest_preced_thread

    by auto

qed

lemma pv_blocked_pre:

  fixes th'

  assumes th'_in: "th' \<in> threads (t@s)"

  and neq_th': "th' \<noteq> th"

  and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"

  shows "th' \<notin> runing (t@s)"

proof

  assume "th' \<in> runing (t@s)"

  hence "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" 

    by (auto simp:runing_def)

  with max_cp_readys_threads [OF vt_t]

  have "cp (t @ s) th' = Max (cp (t@s) ` threads (t@s))"

    by auto

  moreover from th_cp_max have "cp (t @ s) th = \<dots>" by simp

  ultimately have "cp (t @ s) th' = cp (t @ s) th" by simp

  moreover from th_cp_preced and th_kept have "\<dots> = preced th (t @ s)"