Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PrioG.thy
changeset 36 af38526275f8
parent 35 92f61f6a0fe7
child 38 c89013dca1aa
equal deleted inserted replaced
35:92f61f6a0fe7 36:af38526275f8 
   798   apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
 
   798   apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
 
   799   apply(case_tac "csa = cs", auto)
 
   799   apply(case_tac "csa = cs", auto)
 
   800   apply(fold wq_def)
 
   800   apply(fold wq_def)
 
   801   apply(drule_tac step_back_step)
 
   801   apply(drule_tac step_back_step)
 
   802   apply(ind_cases " step s (P (hd (wq s cs)) cs)")
 
   802   apply(ind_cases " step s (P (hd (wq s cs)) cs)")
 
   803   apply(auto simp:s_RAG_def wq_def cs_holding_def)
 
   803   apply(simp add:s_RAG_def wq_def cs_holding_def)
 
       
   804   apply(auto)
 
   804   done
 
   805   done
 
   805 
   806 
       
   807 (* FIXME: Unused
 
   806 lemma simple_A:
 
   808 lemma simple_A:
 
   807   fixes A
 
   809   fixes A
 
   808   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
 
   810   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
 
   809   shows "A = {} \<or> (\<exists> a. A = {a})"
 
   811   shows "A = {} \<or> (\<exists> a. A = {a})"
 
   810 proof(cases "A = {}")
 
   812 proof(cases "A = {}")
 
   812 next
 
   814 next
 
   813   case False then obtain a where "a \<in> A" by auto
 
   815   case False then obtain a where "a \<in> A" by auto
 
   814   with h have "A = {a}" by auto
 
   816   with h have "A = {a}" by auto
 
   815   thus ?thesis by simp
 
   817   thus ?thesis by simp
 
   816 qed
 
   818 qed
 
       
   819 *)
 
   817 
   820 
   818 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 
   821 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 
   819   by (unfold s_RAG_def, auto)
 
   822   by (unfold s_RAG_def, auto)
 
   820 
   823 
   821 lemma acyclic_RAG: 
   824 lemma acyclic_RAG: 
   822   fixes s
 
   825   fixes s
 
   823   assumes vt: "vt s"
 
   826   assumes vt: "vt s"
 
   824   shows "acyclic (RAG s)"
 
   827   shows "acyclic (RAG s)"
 
   825 proof -
 
   828 using assms
 
   826   from vt show ?thesis
 
   829 proof(induct)
 
   827   proof(induct)
 
   830   case (vt_cons s e)
 
   828     case (vt_cons s e)
 
   831   assume ih: "acyclic (RAG s)"
 
   829     assume ih: "acyclic (RAG s)"
 
   832     and stp: "step s e"
 
   830       and stp: "step s e"
 
   833     and vt: "vt s"
 
   831       and vt: "vt s"
 
   834   show ?case
 
   832     show ?case
 
   835   proof(cases e)
 
   833     proof(cases e)
 
   836     case (Create th prio)
 
   834       case (Create th prio)
 
   837     with ih
 
   835       with ih
 
   838     show ?thesis by (simp add:RAG_create_unchanged)
 
   836       show ?thesis by (simp add:RAG_create_unchanged)
 
   839   next
 
   837     next
 
   840     case (Exit th)
 
   838       case (Exit th)
 
   841     with ih show ?thesis by (simp add:RAG_exit_unchanged)
 
   839       with ih show ?thesis by (simp add:RAG_exit_unchanged)
 
   842   next
 
   840     next
 
   843     case (V th cs)
 
   841       case (V th cs)
 
   844     from V vt stp have vtt: "vt (V th cs#s)" by auto
 
   842       from V vt stp have vtt: "vt (V th cs#s)" by auto
 
   845     from step_RAG_v [OF this]
 
   843       from step_RAG_v [OF this]
 
   846     have eq_de: 
   844       have eq_de: 
   847       "RAG (e # s) = 
   845         "RAG (e # s) = 
   848       RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
 
   846             RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
 
   849       {(Cs cs, Th th') |th'. next_th s th cs th'}"
 
   847             {(Cs cs, Th th') |th'. next_th s th cs th'}"
 
   850       (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
 
   848         (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
 
   851     from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
 
   849       from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
 
   852     from step_back_step [OF vtt]
 
   850       from step_back_step [OF vtt]
 
   853     have "step s (V th cs)" .
 
   851       have "step s (V th cs)" .
 
   854     thus ?thesis
 
   852       thus ?thesis
 
   855     proof(cases)
 
   853       proof(cases)
 
   856       assume "holding s th cs"
 
   854         assume "holding s th cs"
 
   857       hence th_in: "th \<in> set (wq s cs)" and
 
   855         hence th_in: "th \<in> set (wq s cs)" and
 
   858         eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
 
   856           eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
 
   859       then obtain rest where
 
   857         then obtain rest where
 
   860         eq_wq: "wq s cs = th#rest"
 
   858           eq_wq: "wq s cs = th#rest"
 
   861         by (cases "wq s cs", auto)
 
   859           by (cases "wq s cs", auto)
 
   862       show ?thesis
 
   860         show ?thesis
 
   863       proof(cases "rest = []")
 
   861         proof(cases "rest = []")
 
   864         case False
 
   862           case False
 
   865         let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
 
   863           let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
 
   866         from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"
 
   864           from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"
 
   867           by (unfold next_th_def, auto)
 
   865             by (unfold next_th_def, auto)
 
   868         let ?E = "(?A - ?B - ?C)"
 
   866           let ?E = "(?A - ?B - ?C)"
 
   869         have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"
 
   867           have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"
 
   870         proof
 
   868           proof
 
   871           assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"
 
   869             assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"
 
   872           hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
 
   870             hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
 
   873           from tranclD [OF this]
 
   871             from tranclD [OF this]
 
   874           obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast
 
   872             obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast
 
   875           hence th_d: "(Th ?th', x) \<in> ?A" by simp
 
   873             hence th_d: "(Th ?th', x) \<in> ?A" by simp
 
   876           from RAG_target_th [OF this]
 
   874             from RAG_target_th [OF this]
 
   877           obtain cs' where eq_x: "x = Cs cs'" by auto
 
   875             obtain cs' where eq_x: "x = Cs cs'" by auto
 
   878           with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
 
   876             with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
 
   879           hence wt_th': "waiting s ?th' cs'"
 
   877             hence wt_th': "waiting s ?th' cs'"
 
   880             unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
 
   878               unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
 
   881           hence "cs' = cs"
 
   879             hence "cs' = cs"
 
   882           proof(rule waiting_unique [OF vt])
 
   880             proof(rule waiting_unique [OF vt])
 
   883             from eq_wq wq_distinct[OF vt, of cs]
 
   881               from eq_wq wq_distinct[OF vt, of cs]
 
   884             show "waiting s ?th' cs" 
   882               show "waiting s ?th' cs" 
   885               apply (unfold s_waiting_def wq_def, auto)
 
   883                 apply (unfold s_waiting_def wq_def, auto)
 
   886             proof -
 
   884               proof -
 
   887               assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
   885                 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
       
   886                 and eq_wq: "wq_fun (schs s) cs = th # rest"
 
   888                 and eq_wq: "wq_fun (schs s) cs = th # rest"
 
   887                 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
   889               have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
   888                 proof(rule someI2)
 
   890               proof(rule someI2)
 
   889                   from wq_distinct[OF vt, of cs] and eq_wq
 
   891                 from wq_distinct[OF vt, of cs] and eq_wq
 
   890                   show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 
   892                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 
   891                 next
 
       
   892                   fix x assume "distinct x \<and> set x = set rest"
 
       
   893                   with False show "x \<noteq> []" by auto
 
       
   894                 qed
 
       
   895                 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
       
   896                                   set (SOME q. distinct q \<and> set q = set rest)" by auto
 
       
   897                 moreover have "\<dots> = set rest" 
       
   898                 proof(rule someI2)
 
       
   899                   from wq_distinct[OF vt, of cs] and eq_wq
 
       
   900                   show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 
       
   901                 next
 
       
   902                   show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   903                 qed
 
       
   904                 moreover note hd_in
 
       
   905                 ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
 
       
   906               next
 
   893               next
 
   907                 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
   894                 fix x assume "distinct x \<and> set x = set rest"
 
       
   895                 with False show "x \<noteq> []" by auto
 
       
   896               qed
 
       
   897               hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
       
   898                 set (SOME q. distinct q \<and> set q = set rest)" by auto
 
       
   899               moreover have "\<dots> = set rest" 
       
   900               proof(rule someI2)
 
       
   901                 from wq_distinct[OF vt, of cs] and eq_wq
 
       
   902                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 
       
   903               next
 
       
   904                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   905               qed
 
       
   906               moreover note hd_in
 
       
   907               ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
 
       
   908             next
 
       
   909               assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
   908                 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
 
   910                 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
 
   909                 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
   911               have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
   910                 proof(rule someI2)
 
   912               proof(rule someI2)
 
   911                   from wq_distinct[OF vt, of cs] and eq_wq
 
   913                 from wq_distinct[OF vt, of cs] and eq_wq
 
   912                   show "distinct rest \<and> set rest = set rest" by auto
 
   914                 show "distinct rest \<and> set rest = set rest" by auto
 
   913                 next
 
   915               next
 
   914                   fix x assume "distinct x \<and> set x = set rest"
 
   916                 fix x assume "distinct x \<and> set x = set rest"
 
   915                   with False show "x \<noteq> []" by auto
 
   917                 with False show "x \<noteq> []" by auto
 
   916                 qed
 
       
   917                 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
       
   918                                   set (SOME q. distinct q \<and> set q = set rest)" by auto
 
       
   919                 moreover have "\<dots> = set rest" 
       
   920                 proof(rule someI2)
 
       
   921                   from wq_distinct[OF vt, of cs] and eq_wq
 
       
   922                   show "distinct rest \<and> set rest = set rest" by auto
 
       
   923                 next
 
       
   924                   show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   925                 qed
 
       
   926                 moreover note hd_in
 
       
   927                 ultimately show False by auto
 
       
   928               qed
 
   918               qed
 
       
   919               hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
       
   920                 set (SOME q. distinct q \<and> set q = set rest)" by auto
 
       
   921               moreover have "\<dots> = set rest" 
       
   922               proof(rule someI2)
 
       
   923                 from wq_distinct[OF vt, of cs] and eq_wq
 
       
   924                 show "distinct rest \<and> set rest = set rest" by auto
 
       
   925               next
 
       
   926                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   927               qed
 
       
   928               moreover note hd_in
 
       
   929               ultimately show False by auto
 
   929             qed
 
   930             qed
 
   930             with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp
 
       
   931             with False
 
       
   932             show "False" by (auto simp: next_th_def eq_wq)
 
       
   933           qed
 
   931           qed
 
   934           with acyclic_insert[symmetric] and ac
 
   932           with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp
 
   935             and eq_de eq_D show ?thesis by auto
 
   933           with False
 
   936         next
 
   934           show "False" by (auto simp: next_th_def eq_wq)
 
   937           case True
 
   935         qed
 
   938           with eq_wq
 
   936         with acyclic_insert[symmetric] and ac
 
   939           have eq_D: "?D = {}"
 
   937           and eq_de eq_D show ?thesis by auto
 
   940             by (unfold next_th_def, auto)
 
   938       next
 
   941           with eq_de ac
 
   939         case True
 
   942           show ?thesis by auto
 
   940         with eq_wq
 
   943         qed 
   941         have eq_D: "?D = {}"
 
   944       qed
 
   942           by (unfold next_th_def, auto)
 
       
   943         with eq_de ac
 
       
   944         show ?thesis by auto
 
       
   945       qed 
       
   946     qed
 
   945   next
 
   947   next
 
   946     case (P th cs)
 
   948     case (P th cs)
 
   947     from P vt stp have vtt: "vt (P th cs#s)" by auto
 
   949     from P vt stp have vtt: "vt (P th cs#s)" by auto
 
   948     from step_RAG_p [OF this] P
 
   950     from step_RAG_p [OF this] P
 
   949     have "RAG (e # s) = 
   951     have "RAG (e # s) = 
   968       hence eq_r: "?R =  RAG s \<union> {(Th th, Cs cs)}" by simp
 
   970       hence eq_r: "?R =  RAG s \<union> {(Th th, Cs cs)}" by simp
 
   969       have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*"
 
   971       have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*"
 
   970       proof
 
   972       proof
 
   971         assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*"
 
   973         assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*"
 
   972         hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
 
   974         hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
 
   973           moreover from step_back_step [OF vtt] have "step s (P th cs)" .
 
   975         moreover from step_back_step [OF vtt] have "step s (P th cs)" .
 
   974           ultimately show False
 
   976         ultimately show False
 
   975           proof -
 
   977         proof -
 
   976             show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"
 
   978           show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"
 
   977               by (ind_cases "step s (P th cs)", simp)
 
   979             by (ind_cases "step s (P th cs)", simp)
 
   978           qed
 
       
   979         qed
 
   980         qed
 
   980         with acyclic_insert ih eq_r show ?thesis by auto
 
   981       qed
 
       
   982       with acyclic_insert ih eq_r show ?thesis by auto
 
   981       qed
 
   983       qed
 
   982       ultimately show ?thesis by simp
 
   984       ultimately show ?thesis by simp
 
   983     next
 
   985     next
 
   984       case (Set thread prio)
 
   986       case (Set thread prio)
 
   985       with ih
 
   987       with ih
 
   988     qed
 
   990     qed
 
   989   next
 
   991   next
 
   990     case vt_nil
 
   992     case vt_nil
 
   991     show "acyclic (RAG ([]::state))"
 
   993     show "acyclic (RAG ([]::state))"
 
   992       by (auto simp: s_RAG_def cs_waiting_def 
   994       by (auto simp: s_RAG_def cs_waiting_def 
   993                       cs_holding_def wq_def acyclic_def)
 
   995         cs_holding_def wq_def acyclic_def)
 
   994   qed
 
   996 qed
 
   995 qed
 
   997 qed
 
   996 
   998 
   997 lemma finite_RAG: 
   999 lemma finite_RAG: 
   998   fixes s
 
  1000   fixes s
 
   999   assumes vt: "vt s"
 
  1001   assumes vt: "vt s"
pip