2 theory CpsG

     5 theory CpsG

     3 imports PrioG Max

     6 imports PrioG Max

     4 begin

     7 begin

     5 

     8 

     6 lemma not_thread_holdents:

    10 lemma not_thread_holdents:

     7   fixes th s

    11   fixes th s

     8   assumes vt: "vt s"

    12   assumes vt: "vt s"

     9   and not_in: "th \<notin> threads s" 

    13   and not_in: "th \<notin> threads s" 

    10   shows "holdents s th = {}"

    14   shows "holdents s th = {}"

   124       show ?case

   128       show ?case

   125       by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)

   129       by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)

   126   qed

   130   qed

   127 qed

   131 qed

   128 

   132 

   131 lemma next_th_neq: 

   134 lemma next_th_neq: 

   132   assumes vt: "vt s"

   135   assumes vt: "vt s"

   133   and nt: "next_th s th cs th'"

   136   and nt: "next_th s th cs th'"

   134   shows "th' \<noteq> th"

   137   shows "th' \<noteq> th"

   135 proof -

   138 proof -

   153     qed

   156     qed

   154     with wq_distinct[OF vt, of cs] eq_wq show False by auto

   157     with wq_distinct[OF vt, of cs] eq_wq show False by auto

   155   qed

   158   qed

   156 qed

   159 qed

   157 

   160 

   158 lemma next_th_unique: 

   162 lemma next_th_unique: 

   159   assumes nt1: "next_th s th cs th1"

   163   assumes nt1: "next_th s th cs th1"

   160   and nt2: "next_th s th cs th2"

   164   and nt2: "next_th s th cs th2"

   161   shows "th1 = th2"

   165   shows "th1 = th2"

   162 using assms by (unfold next_th_def, auto)

   166 using assms by (unfold next_th_def, auto)

   167 proof(rule finite_acyclic_wf)

   171 proof(rule finite_acyclic_wf)

   168   from finite_RAG[OF vt] show "finite (RAG s)" .

   172   from finite_RAG[OF vt] show "finite (RAG s)" .

   169 next

   173 next

   170   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .

   174   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .

   171 qed

   175 qed

   174 

   176 

   175 definition child :: "state \<Rightarrow> (node \<times> node) set"

   177 definition child :: "state \<Rightarrow> (node \<times> node) set"

   176   where "child s \<equiv>

   178   where "child s \<equiv>

   177             {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

   179             {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

   178 

   180 

   308     moreover have "(n1, y) \<in> (RAG s)^+" by fact

   310     moreover have "(n1, y) \<in> (RAG s)^+" by fact

   309     ultimately show ?case by auto

   311     ultimately show ?case by auto

   310   qed

   312   qed

   311 qed

   313 qed

   312 

   314 

   313 lemma child_RAG_eq: 

   317 lemma child_RAG_eq: 

   314   assumes vt: "vt s"

   318   assumes vt: "vt s"

   315   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"

   319   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"

   316   by (auto intro: RAG_child[OF vt] child_RAG_p)

   320   by (auto intro: RAG_child[OF vt] child_RAG_p)

   317 

   321 

   318 lemma children_no_dep:

   324 lemma children_no_dep:

   319   fixes s th th1 th2 th3

   325   fixes s th th1 th2 th3

   320   assumes vt: "vt s"

   326   assumes vt: "vt s"

   321   and ch1: "(Th th1, Th th) \<in> child s"

   327   and ch1: "(Th th1, Th th) \<in> child s"

   322   and ch2: "(Th th2, Th th) \<in> child s"

   328   and ch2: "(Th th2, Th th) \<in> child s"

   346     qed

   352     qed

   347     ultimately show False by auto

   353     ultimately show False by auto

   348   qed

   354   qed

   349 qed

   355 qed

   350 

   356 

   351 lemma unique_RAG_p:

   359 lemma unique_RAG_p:

   352   assumes vt: "vt s"

   360   assumes vt: "vt s"

   353   and dp1: "(n, n1) \<in> (RAG s)^+"

   361   and dp1: "(n, n1) \<in> (RAG s)^+"

   354   and dp2: "(n, n2) \<in> (RAG s)^+"

   362   and dp2: "(n, n2) \<in> (RAG s)^+"

   355   and neq: "n1 \<noteq> n2"

   363   and neq: "n1 \<noteq> n2"

   357 proof(rule unique_chain [OF _ dp1 dp2 neq])

   365 proof(rule unique_chain [OF _ dp1 dp2 neq])

   358   from unique_RAG[OF vt]

   366   from unique_RAG[OF vt]

   359   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto

   367   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto

   360 qed

   368 qed

   361 

   369 

   362 lemma dependants_child_unique:

   372 lemma dependants_child_unique:

   363   fixes s th th1 th2 th3

   373   fixes s th th1 th2 th3

   364   assumes vt: "vt s"

   374   assumes vt: "vt s"

   365   and ch1: "(Th th1, Th th) \<in> child s"

   375   and ch1: "(Th th1, Th th) \<in> child s"

   366   and ch2: "(Th th2, Th th) \<in> child s"

   376   and ch2: "(Th th2, Th th) \<in> child s"

   393   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"

   403   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"

   394   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]

   404   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]

   395   apply (unfold children_def)

   405   apply (unfold children_def)

   396   by (metis assms(2) children_def RAG_children eq_RAG)

   406   by (metis assms(2) children_def RAG_children eq_RAG)

   397 

   407 

   398 lemma dependants_expand:

   410 lemma dependants_expand:

   399   assumes "vt s"

   411   assumes "vt s"

   400   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"

   412   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"

   401 apply(simp add: image_def)

   413 apply(simp add: image_def)

   402 unfolding cs_dependants_def

   414 unfolding cs_dependants_def

   433 

   445 

   434 lemma UN_exists:

   446 lemma UN_exists:

   435   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"

   447   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"

   436 by auto

   448 by auto

   437 

   449 

   438 lemma cp_rec:

   452 lemma cp_rec:

   439   fixes s th

   453   fixes s th

   440   assumes vt: "vt s"

   454   assumes vt: "vt s"

   441   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"

   455   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"

   442 proof(cases "children s th = {}")

   456 proof(cases "children s th = {}")

   898     ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp

   912     ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp

   899     with eq_wq and wq_distinct[OF vt, of cs]

   913     with eq_wq and wq_distinct[OF vt, of cs]

   900     show False by auto

   914     show False by auto

   901   qed

   915   qed

   902 qed

   916 qed

   905 

   917 

   906 

   918 

   907 locale step_v_cps =

   919 locale step_v_cps =

   908   fixes s' th cs s 

   920   fixes s' th cs s 

   909   defines s_def : "s \<equiv> (V th cs#s')"

   921   defines s_def : "s \<equiv> (V th cs#s')"