# HG changeset patch # User Christian Urban # Date 1400931552 -3600 # Node ID c820ac0f3088dca68bbe8c892b99a6d7deda3f77 # Parent af38526275f8daf81911b7a94aa3273ad09df5bb simplified RAG_acyclic proof diff -r af38526275f8 -r c820ac0f3088 Test.thy --- a/Test.thy Fri May 23 15:19:32 2014 +0100 +++ b/Test.thy Sat May 24 12:39:12 2014 +0100 @@ -72,7 +72,7 @@ abbreviation "release qs \ case qs of [] => [] - | (_#qs) => (SOME q. distinct q \ set q = set qs)" + | (_ # qs) => SOME q. distinct q \ set q = set qs" fun schs :: "state \ schedule_state" where @@ -122,6 +122,9 @@ definition holding :: "state \ thread \ cs set" where "holding s th \ {cs . holds2 s th cs}" +abbreviation + "next_to_run ths \ hd (SOME q::thread list. distinct q \ set q = set ths)" + lemma holding_RAG: "holding s th = {cs . (Cs cs, Th th) \ RAG2 s}" unfolding holding_def @@ -191,41 +194,41 @@ lemma RAG_p1: assumes "wq s cs = []" - shows "RAG2 (P th cs # s) = RAG2 s \ {(Cs cs, Th th)}" - using assms - apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def) - apply (metis in_set_insert insert_Nil list.distinct(1)) - done + shows "RAG2 (P th cs # s) \ RAG2 s \ {(Cs cs, Th th)}" +using assms +unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def +by (auto simp add: Let_def) + lemma RAG_p2: - assumes "vt (P th cs#s)" "wq s cs \ []" - shows "RAG2 (P th cs # s) = RAG2 s \ {(Th th, Cs cs)}" - using assms - apply(simp add: RAG2_def Let_def) - apply(erule_tac vt.cases) - apply(simp) - apply(clarify) - apply(simp) - apply(erule_tac step.cases) - apply(simp_all) - apply(simp add: wq_def RAG_def RAG2_def) - apply(simp add: waits_def holds_def) - apply(auto) - done + assumes "(Cs cs, Th th) \ (RAG2 s)\<^sup>+" "wq s cs \ []" + shows "RAG2 (P th cs # s) \ RAG2 s \ {(Th th, Cs cs)}" +using assms +unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def +by (auto simp add: Let_def) + +lemma [simp]: "(SOME q. distinct q \ q = []) = []" +by auto + +lemma [simp]: "(x \ set (SOME q. distinct q \ set q = set p)) = (x \ set p)" +apply auto +apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) +by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) -definition next_th:: "state \ thread \ cs \ thread \ bool" - where "next_th s th cs t = - (\ rest. wq s cs = th#rest \ rest \ [] \ t = hd (SOME q. distinct q \ set q = set rest))" +lemma RAG_v1: +assumes vt: "wq s cs = [th]" +shows "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" +using assms +unfolding RAG2_def RAG_def waits_def holds_def wq_def +by (auto simp add: Let_def) -lemma RAG_v: -assumes vt:"vt (V th cs#s)" -shows " - RAG2 (V th cs # s) = - RAG2 s - {(Cs cs, Th th)} - - {(Th th', Cs cs) |th'. next_th s th cs th'} \ - {(Cs cs, Th th') |th'. next_th s th cs th'}" - apply (insert vt, unfold RAG2_def RAG_def) - sorry +lemma RAG_v2: +assumes vt:"vt s" "wq s cs = th # wts \ wts \ []" +shows "RAG2 (V th cs # s) \ + RAG2 s - {(Cs cs, Th th)} - {(Th (next_to_run wts), Cs cs)} \ {(Cs cs, Th (next_to_run wts))}" +unfolding RAG2_def RAG_def waits_def holds_def +using assms wq_distinct[OF vt(1), of"cs"] +by (auto simp add: Let_def wq_def) lemma waiting_unique: assumes "vt s" @@ -234,11 +237,6 @@ shows "cs1 = cs2" sorry -lemma singleton_Un: - shows "A \ {x} = insert x A" -by simp - - lemma acyclic_RAG_step: assumes vt: "vt s" and stp: "step s e" @@ -247,11 +245,8 @@ using stp vt ac proof (induct) case (step_P th s cs) - have vt: "vt s" by fact have ac: "acyclic (RAG2 s)" by fact - have rn: "th \ runing s" by fact have ds: "(Cs cs, Th th) \ (RAG2 s)\<^sup>+" by fact - have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons) { assume a: "wq s cs = []" -- "case waiting queue is empty" have "(Th th, Cs cs) \ (RAG2 s)\<^sup>*" proof @@ -262,14 +257,16 @@ qed with acyclic_insert ac have "acyclic (RAG2 s \ {(Cs cs, Th th)})" by simp - then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp + then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] + by (rule acyclic_subset) } moreover { assume a: "wq s cs \ []" -- "case waiting queue is not empty" from ds have "(Cs cs, Th th) \ (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD) with acyclic_insert ac have "acyclic (RAG2 s \ {(Th th, Cs cs)})" by auto - then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp + then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a] + by (rule acyclic_subset) } ultimately show "acyclic (RAG2 (P th cs # s))" by metis next @@ -278,89 +275,53 @@ have ac: "acyclic (RAG2 s)" by fact have rn: "th \ runing s" by fact have hd: "holds2 s th cs" by fact - from hd - have th_in: "th \ set (wq s cs)" and - eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto - then obtain rest where - eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto) - show ?case - apply(subst RAG_v) - apply(rule vt_cons) - apply(rule vt) - apply(rule step.step_V) - apply(rule rn) - apply(rule hd) - using eq_wq - apply(cases "rest = []") - apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}") - apply(simp) - apply(rule acyclic_subset) - apply(rule ac) - apply(auto)[1] - apply(auto simp add: next_th_def)[1] - -- "case wq more than a singleton" - apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \ set q = set rest)))} = - {(Cs cs, Th th') |th'. next_th s th cs th'}") - apply(rotate_tac 2) - apply(drule sym) - apply(simp only: singleton_Un) - apply(simp only: acyclic_insert) - apply(rule conjI) - apply(rule acyclic_subset) - apply(rule ac) - apply(auto)[1] - apply(rotate_tac 2) - apply(thin_tac "?X") - defer - apply(simp add: next_th_def) - apply(clarify) - apply(simp add: rtrancl_eq_or_trancl) - apply(drule tranclD) - apply(erule exE) - apply(drule conjunct1) - apply(subgoal_tac "(Th (hd (SOME q. distinct q \ set q = set rest)), z) \ RAG2 s") - prefer 2 - apply(simp) - apply(case_tac z) - apply(simp add: RAG2_def RAG_def) - apply(clarify) - apply(simp) - apply(simp add: next_th_def) - apply(rule waiting_unique) - apply(rule vt) - apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def) - apply(rotate_tac 2) - apply(thin_tac "?X") - apply(subgoal_tac "distinct (wq s cs)") - prefer 2 - apply(rule wq_distinct) - apply(rule vt) - apply (unfold waits2_def waits_def wq_def, auto) - apply(subgoal_tac "(SOME q. distinct q \ set q = set rest) \ []") - prefer 2 - apply (metis (mono_tags) set_empty tfl_some) - apply(subgoal_tac "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)") - prefer 2 - apply(auto)[1] - apply(subgoal_tac "set (SOME q. distinct q \ set q = set rest) = set rest") - prefer 2 - apply(rule someI2) - apply(auto)[2] - apply(auto)[1] - apply(subgoal_tac "(SOME q. distinct q \ set q = set rest) \ []") - prefer 2 - apply (metis (mono_tags) set_empty tfl_some) - apply(subgoal_tac "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)") - prefer 2 - apply(auto)[1] - apply(subgoal_tac "set (SOME q. distinct q \ set q = set rest) = set rest") - prefer 2 - apply(rule someI2) - apply(auto)[2] - apply(auto)[1] - done + from hd have th_in: "th \ set (wq s cs)" and + eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto + then obtain wts where + eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto) + { assume "wts = []" -- "case no thread present to take over" + with eq_wq have "wq s cs = [th]" by simp + then have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1) + moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset) + ultimately + have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) + } + moreover + { def nth \ "next_to_run wts" + assume aa: "wts \ []" -- "at least one thread present to take over" + with vt eq_wq + have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \ {(Cs cs, Th nth)}" + unfolding nth_def by (rule_tac RAG_v2) (auto) + moreover + have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" + proof - + have "acyclic (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset) + moreover + have "(Th nth, Cs cs) \ (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+" + proof + assume "(Th nth, Cs cs) \ (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+" + then obtain z where a: "(Th nth, z) \ (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" + by (metis converse_tranclE) + then have "(Th nth, z) \ RAG2 s" by simp + then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \ RAG2 s" + unfolding RAG2_def RAG_def by auto + then have "cs = cs'" + apply(rule_tac waiting_unique[OF vt]) + using eq_wq aa + apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def) + apply (metis (mono_tags, lifting) `\thesis. (\wts. wq s cs = th # wts \ thesis) \ thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct) + by (metis (mono_tags, lifting) `\thesis. (\wts. wq s cs = th # wts \ thesis) \ thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct) + then show "False" using a b by simp + qed + then have "(Th nth, Cs cs) \ (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*" + by (metis node.distinct(1) rtranclD) + ultimately + show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" + by (simp add: acyclic_insert) + qed + ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) + } + ultimately show "acyclic (RAG2 (V th cs # s))" by metis qed (simp_all)