diff -r 0781a2fc93f1 -r 66ed924aaa5c Test.thy --- a/Test.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/Test.thy Mon Jun 09 16:01:28 2014 +0100 @@ -74,6 +74,20 @@ [] => [] | (_ # qs) => SOME q. distinct q \ set q = set qs" +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) + +abbreviation + "next_to_run ths \ hd (SOME q::thread list. distinct q \ set q = set ths)" + + fun schs :: "state \ schedule_state" where "schs [] = (| wq_fun = \ cs. [], cprec_fun = (\_. Prc 0 0) |)" @@ -127,8 +141,6 @@ 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 exists_distinct: obtains ys where "distinct ys" "set ys = set xs" @@ -169,12 +181,63 @@ unfolding readys_def by auto +lemma wq_threads: + assumes vt: "vt s" + and h: "th \ set (wq s cs)" + shows "th \ threads s" +using assms +apply(induct) +apply(simp add: wq_def) +apply(erule step.cases) +apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) +apply(simp add: waits_def) +apply(auto simp add: waits_def split: if_splits)[1] +apply(auto split: if_splits) +apply(simp only: waits_def) +by (metis insert_iff set_simps(2)) + + + +lemma Domain_RAG_threads: + assumes vt: "vt s" + and in_dom: "(Th th) \ Domain (RAG2 s)" + shows "th \ threads s" +proof - + from in_dom obtain n where "(Th th, n) \ RAG2 s" by auto + then obtain cs where "n = Cs cs" "(Th th, Cs cs) \ RAG2 s" + unfolding RAG2_def RAG_def by auto + then have "th \ set (wq s cs)" + unfolding wq_def RAG_def RAG2_def waits_def by auto + with wq_threads [OF vt] show ?thesis . +qed + +lemma dependants_threads: + assumes vt: "vt s" + shows "dependants2 s th \ threads s" +proof + fix th1 + assume "th1 \ dependants2 s th" + then have h: "(Th th1, Th th) \ (RAG2 s)\<^sup>+" + unfolding dependants2_def dependants_def RAG2_def by simp + then have "Th th1 \ Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto + then have "Th th1 \ Domain (RAG2 s)" using trancl_domain by simp + then show "th1 \ threads s" using vt by (rule_tac Domain_RAG_threads) +qed + +lemma finite_threads: + assumes vt: "vt s" + shows "finite (threads s)" +using vt by (induct) (auto elim: step.cases) + + +section {* Distinctness of @{const wq} *} + lemma wq_distinct_step: assumes "step s e" "distinct (wq s cs)" shows "distinct (wq (e # s) cs)" using assms unfolding wq_def -apply(induct) +apply(erule_tac step.cases) apply(auto simp add: RAG2_def RAG_def Let_def)[1] apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def) apply(auto split: list.split) @@ -191,72 +254,8 @@ apply(simp add: wq_distinct_step) done -lemma RAG_set_unchanged[simp]: - shows "RAG2 (Set th prio # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) -lemma RAG_create_unchanged[simp]: - "RAG2 (Create th prio # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) - -lemma RAG_exit_unchanged[simp]: - shows "RAG2 (Exit th # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) - -lemma RAG_p1: - assumes "wq s cs = []" - 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 "(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) - -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_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 single_valued_waits2: - assumes "vt s" - shows "single_valuedP (waits2 s)" -using assms -apply(induct) -apply(simp add: waits2_def waits_def) -apply(erule step.cases) -apply(auto simp add: Let_def waits2_def) -unfolding single_valued_def waits2_def waits_def -apply(auto) -*) - +section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *} lemma waits2_unique: assumes "vt s" @@ -274,34 +273,85 @@ apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) +lemma single_valued_waits2: + assumes "vt s" + shows "single_valuedP (waits2 s)" +using assms +unfolding single_valued_def +by (metis Collect_splitD fst_eqD sndI waits2_unique) + lemma single_valued_holds2: assumes "vt s" shows "single_valuedP (\cs th. holds2 s th cs)" unfolding single_valued_def holds2_def holds_def by simp - -lemma holds2_unique: - assumes "holds2 s th1 cs" - and "holds2 s th2 cs" - shows "th1 = th2" -using assms -unfolding holds2_def holds_def by auto - -lemma single_valued_waits2: - assumes "vt s" - shows "single_valuedP (waits2 s)" -by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique) - - -(* was unique_RAG2 *) lemma single_valued_RAG2: assumes "vt s" shows "single_valued (RAG2 s)" using single_valued_waits2[OF assms] single_valued_holds2[OF assms] -unfolding RAG2_def RAG_def -unfolding single_valued_def -unfolding holds2_def waits2_def -by auto +unfolding RAG2_def RAG_def +apply(rule_tac single_valued_union) +unfolding holds2_def[symmetric] waits2_def[symmetric] +apply(rule single_valued_Collect) +apply(simp) +apply(simp add: inj_on_def) +apply(rule single_valued_Collect) +apply(simp) +apply(simp add: inj_on_def) +apply(auto) +done + + +section {* Properties of @{const RAG2} under events *} + +lemma RAG_Set [simp]: + shows "RAG2 (Set th prio # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_Create [simp]: + "RAG2 (Create th prio # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_Exit [simp]: + shows "RAG2 (Exit th # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_P1: + assumes "wq s cs = []" + 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 "(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 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_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) + + + +section {* Acyclicity of @{const RAG2} *} lemma acyclic_RAG_step: assumes vt: "vt s" @@ -321,14 +371,14 @@ with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def) qed with ac have "acyclic (RAG2 s \ {(Cs cs, Th th)})" by simp - then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty] + then have "acyclic (RAG2 (P th cs # s))" using RAG_P1[OF wq_empty] by (rule acyclic_subset) } moreover { assume wq_not_empty: "wq s cs \ []" -- "case waiting queue is not empty" from ac ds have "acyclic (RAG2 s \ {(Th th, Cs cs)})" by simp - then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty] + then have "acyclic (RAG2 (P th cs # s))" using RAG_P2[OF ds wq_not_empty] by (rule acyclic_subset) } ultimately show "acyclic (RAG2 (P th cs # s))" by metis @@ -343,7 +393,7 @@ -- "case no thread present in the waiting queue to take over" { assume "wts = []" 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) + 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) @@ -352,11 +402,13 @@ -- "at least one thread present to take over" { def nth \ "next_to_run wts" assume wq_not_empty: "wts \ []" - have waits2_cs: "waits2 s nth cs" + have "waits2 s nth cs" using eq_wq wq_not_empty wq_distinct unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto + then have cs_in_RAG: "(Th nth, Cs cs) \ RAG2 s" + unfolding RAG2_def RAG_def waits2_def by auto have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth)}" - unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto) + unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_V2) (auto) moreover have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth)})" proof - @@ -368,14 +420,9 @@ 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 - moreover - have "waits2 s nth cs'" - using b(2) unfolding RAG2_def RAG_def waits2_def by simp - ultimately have "cs = cs'" - by (rule_tac waits2_unique[OF vt waits2_cs]) - then show "False" using a b(1) by simp + then have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt] + by (simp add: single_valued_def) + then show "False" using a by simp qed ultimately show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth) })" by simp @@ -397,11 +444,11 @@ apply(auto) apply(case_tac "wq sa cs = []") apply(rule finite_subset) -apply(rule RAG_p1) +apply(rule RAG_P1) apply(simp) apply(simp) apply(rule finite_subset) -apply(rule RAG_p2) +apply(rule RAG_P2) apply(simp) apply(simp) apply(simp) @@ -409,11 +456,11 @@ apply(erule exE) apply(case_tac "wts = []") apply(rule finite_subset) -apply(rule RAG_v1) +apply(rule RAG_V1) apply(simp) apply(simp) apply(rule finite_subset) -apply(rule RAG_v2) +apply(rule RAG_V2) apply(simp) apply(simp) apply(simp) @@ -423,20 +470,39 @@ apply(auto simp add: holds2_def holds_def wq_def) done -lemma wq_threads: + + +lemma dchain_unique: assumes vt: "vt s" - and h: "th \ set (wq s cs)" - shows "th \ threads s" -using assms -apply(induct) -apply(simp add: wq_def) -apply(erule step.cases) -apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) -apply(simp add: waits_def) -apply(auto simp add: waits_def split: if_splits)[1] -apply(auto split: if_splits) -apply(simp only: waits_def) -by (metis insert_iff set_simps(2)) + and th1_d: "(n, Th th1) \ (RAG2 s)^+" + and th1_r: "th1 \ readys s" + and th2_d: "(n, Th th2) \ (RAG2 s)^+" + and th2_r: "th2 \ readys s" + shows "th1 = th2" +proof(rule ccontr) + assume neq: "th1 \ th2" + with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d + have "(Th th1, Th th2) \ (RAG2 s)\<^sup>+ \ (Th th2, Th th1) \ (RAG2 s)\<^sup>+" by auto + moreover + { assume "(Th th1, Th th2) \ (RAG2 s)\<^sup>+" + then obtain n where dd: "(Th th1, n) \ RAG2 s" by (metis converse_tranclE) + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th1 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th1_r have "False" by auto + } + moreover + { assume "(Th th2, Th th1) \ (RAG2 s)\<^sup>+" + then obtain n where dd: "(Th th2, n) \ RAG2 s" by (metis converse_tranclE) + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th2 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th2_r have "False" by auto + } + ultimately show "False" by metis +qed lemma max_cpreceds_readys_threads: assumes vt: "vt s" @@ -452,46 +518,51 @@ defer oops - +lemma readys_Exit: + shows "readys (Exit th # s) \ readys s" +by (auto simp add: readys_def waits2_def Let_def) +lemma readys_Create: + shows "readys (Create th prio # s) \ {th} \ readys s" +by (auto simp add: readys_def waits2_def Let_def) +lemma readys_Set: + shows "readys (Set th prio # s) \ readys s" +by (auto simp add: readys_def waits2_def Let_def) -lemma dchain_unique: - assumes vt: "vt s" - and th1_d: "(n, Th th1) \ (RAG2 s)^+" - and th1_r: "th1 \ readys s" - and th2_d: "(n, Th th2) \ (RAG2 s)^+" - and th2_r: "th2 \ readys s" - shows "th1 = th2" -proof(rule ccontr) - assume neq: "th1 \ th2" - hence "Th th1 \ Th th2" by simp - from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt] - have "(Th th1, Th th2) \ (RAG2 s)\<^sup>+ \ (Th th2, Th th1) \ (RAG2 s)\<^sup>+" - unfolding single_valued_def by auto - then show "False" - proof - assume "(Th th1, Th th2) \ (RAG2 s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th1, n) \ RAG2 s" by auto - then obtain cs where eq_n: "n = Cs cs" - unfolding RAG2_def RAG_def by (case_tac n) (auto) - from dd eq_n have "th1 \ readys s" - unfolding RAG2_def RAG_def waits2_def readys_def by (auto) - with th1_r show ?thesis by auto - next - assume "(Th th2, Th th1) \ (RAG2 s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th2, n) \ RAG2 s" by auto - then obtain cs where eq_n: "n = Cs cs" - unfolding RAG2_def RAG_def by (case_tac n) (auto) - from dd eq_n have "th2 \ readys s" - unfolding RAG2_def RAG_def waits2_def readys_def by (auto) - with th2_r show ?thesis by auto - qed -qed +lemma readys_P: + shows "readys (P th cs # s) \ readys s" +apply(auto simp add: readys_def waits2_def Let_def) +apply(simp add: waits_def) +apply(case_tac "csa = cs") +apply(simp) +apply(drule_tac x="cs" in spec) +apply(simp) +apply (metis hd_append2 in_set_insert insert_Nil list.sel(1)) +apply(drule_tac x="csa" in spec) +apply(simp) +done +lemma readys_V: + shows "readys (V th cs # s) \ readys s \ set (wq s cs)" +apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) +done + +lemma + assumes "vt s" + shows "card (runing s) \ 1" +proof (rule ccontr) + assume "\ card (runing s) \ 1" + then have "2 \ card (runing s)" by auto + moreover + have "finite (runing s)" sorry + ultimately obtain th1 th2 where "th1 \ th2" "th1 \ runing s" "th2 \ runing s" + by (auto simp add: numerals card_le_Suc_iff) (blast) + + show "False" +apply(simp) +oops end \ No newline at end of file