section {* This file contains lemmas used to guide the recalculation of current precedence after every system call (or system operation)*}theory CpsGimports PrioG Max RTreebegindefinition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}"definition "tRAG s = wRAG s O hRAG s"definition "pairself f = (\<lambda>(a, b). (f a, f b))"definition "rel_map f r = (pairself f ` r)"fun the_thread :: "node \<Rightarrow> thread" where "the_thread (Th th) = th"definition "tG s = rel_map the_thread (tRAG s)"locale pip = fixes s assumes vt: "vt s"lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv s_holding_abv cs_RAG_def, auto)lemma relpow_mult: "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"proof(induct n arbitrary:m) case (Suc k m) thus ?case (is "?L = ?R") proof - have h: "(m * k + m) = (m + m * k)" by auto show ?thesis apply (simp add:Suc relpow_add[symmetric]) by (unfold h, simp) qedqed simplemma compose_relpow_2: assumes "r1 \<subseteq> r" and "r2 \<subseteq> r" shows "r1 O r2 \<subseteq> r ^^ (2::nat)"proof - { fix a b assume "(a, b) \<in> r1 O r2" then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2" by auto with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto } thus ?thesis by (auto simp:numeral_2_eq_2)qedlemma acyclic_compose: assumes "acyclic r" and "r1 \<subseteq> r" and "r2 \<subseteq> r" shows "acyclic (r1 O r2)"proof - { fix a assume "(a, a) \<in> (r1 O r2)^+" from trancl_mono[OF this compose_relpow_2[OF assms(2, 3)]] have "(a, a) \<in> (r ^^ 2) ^+" . from trancl_power[THEN iffD1, OF this] obtain n where h: "(a, a) \<in> (r ^^ 2) ^^ n" "n > 0" by blast from this(1)[unfolded relpow_mult] have h2: "(a, a) \<in> r ^^ (2 * n)" . have "(a, a) \<in> r^+" proof(cases rule:trancl_power[THEN iffD2]) from h(2) h2 show "\<exists>n>0. (a, a) \<in> r ^^ n" by (rule_tac x = "2*n" in exI, auto) qed with assms have "False" by (auto simp:acyclic_def) } thus ?thesis by (auto simp:acyclic_def)qedlemma range_tRAG: "Range (tRAG s) \<subseteq> {Th th | th. True}"proof - have "Range (wRAG s O hRAG s) \<subseteq> {Th th |th. True}" (is "?L \<subseteq> ?R") proof - have "?L \<subseteq> Range (hRAG s)" by auto also have "... \<subseteq> ?R" by (unfold hRAG_def, auto) finally show ?thesis by auto qed thus ?thesis by (simp add:tRAG_def)qedlemma domain_tRAG: "Domain (tRAG s) \<subseteq> {Th th | th. True}"proof - have "Domain (wRAG s O hRAG s) \<subseteq> {Th th |th. True}" (is "?L \<subseteq> ?R") proof - have "?L \<subseteq> Domain (wRAG s)" by auto also have "... \<subseteq> ?R" by (unfold wRAG_def, auto) finally show ?thesis by auto qed thus ?thesis by (simp add:tRAG_def)qedlemma rel_mapE: assumes "(a, b) \<in> rel_map f r" obtains c d where "(c, d) \<in> r" "(a, b) = (f c, f d)" using assms by (unfold rel_map_def pairself_def, auto)lemma rel_mapI: assumes "(a, b) \<in> r" and "c = f a" and "d = f b" shows "(c, d) \<in> rel_map f r" using assms by (unfold rel_map_def pairself_def, auto)lemma map_appendE: assumes "map f zs = xs @ ys" obtains xs' ys' where "zs = xs' @ ys'" "xs = map f xs'" "ys = map f ys'"proof - have "\<exists> xs' ys'. zs = xs' @ ys' \<and> xs = map f xs' \<and> ys = map f ys'" using assms proof(induct xs arbitrary:zs ys) case (Nil zs ys) thus ?case by auto next case (Cons x xs zs ys) note h = this show ?case proof(cases zs) case (Cons e es) with h have eq_x: "map f es = xs @ ys" "x = f e" by auto from h(1)[OF this(1)] obtain xs' ys' where "es = xs' @ ys'" "xs = map f xs'" "ys = map f ys'" by blast with Cons eq_x have "zs = (e#xs') @ ys' \<and> x # xs = map f (e#xs') \<and> ys = map f ys'" by auto thus ?thesis by metis qed (insert h, auto) qed thus ?thesis by (auto intro!:that)qedlemma rel_map_mono: assumes "r1 \<subseteq> r2" shows "rel_map f r1 \<subseteq> rel_map f r2" using assms by (auto simp:rel_map_def pairself_def)lemma rel_map_compose [simp]: shows "rel_map f1 (rel_map f2 r) = rel_map (f1 o f2) r" by (auto simp:rel_map_def pairself_def)lemma edges_on_map: "edges_on (map f xs) = rel_map f (edges_on xs)"proof - { fix a b assume "(a, b) \<in> edges_on (map f xs)" then obtain l1 l2 where eq_map: "map f xs = l1 @ [a, b] @ l2" by (unfold edges_on_def, auto) hence "(a, b) \<in> rel_map f (edges_on xs)" by (auto elim!:map_appendE intro!:rel_mapI simp:edges_on_def) } moreover { fix a b assume "(a, b) \<in> rel_map f (edges_on xs)" then obtain c d where h: "(c, d) \<in> edges_on xs" "(a, b) = (f c, f d)" by (elim rel_mapE, auto) then obtain l1 l2 where eq_xs: "xs = l1 @ [c, d] @ l2" by (auto simp:edges_on_def) hence eq_map: "map f xs = map f l1 @ [f c, f d] @ map f l2" by auto have "(a, b) \<in> edges_on (map f xs)" proof - from h(2) have "[f c, f d] = [a, b]" by simp from eq_map[unfolded this] show ?thesis by (auto simp:edges_on_def) qed } ultimately show ?thesis by autoqedlemma plus_rpath: assumes "(a, b) \<in> r^+" obtains xs where "rpath r a xs b" "xs \<noteq> []"proof - from assms obtain m where h: "(a, m) \<in> r" "(m, b) \<in> r^*" by (auto dest!:tranclD) from star_rpath[OF this(2)] obtain xs where "rpath r m xs b" by auto from rstepI[OF h(1) this] have "rpath r a (m # xs) b" . from that[OF this] show ?thesis by autoqedlemma edges_on_unfold: "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")proof - { fix c d assume "(c, d) \<in> ?L" then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2" by (auto simp:edges_on_def) have "(c, d) \<in> ?R" proof(cases "l1") case Nil with h have "(c, d) = (a, b)" by auto thus ?thesis by auto next case (Cons e es) from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto thus ?thesis by (auto simp:edges_on_def) qed } moreover { fix c d assume "(c, d) \<in> ?R" moreover have "(a, b) \<in> ?L" proof - have "(a # b # xs) = []@[a,b]@xs" by simp hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto thus ?thesis by (unfold edges_on_def, simp) qed moreover { assume "(c, d) \<in> edges_on (b#xs)" then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto) hence "a#b#xs = (a#l1)@[c,d]@l2" by simp hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp) } ultimately have "(c, d) \<in> ?L" by auto } ultimately show ?thesis by autoqedlemma edges_on_rpathI: assumes "edges_on (a#xs@[b]) \<subseteq> r" shows "rpath r a (xs@[b]) b" using assmsproof(induct xs arbitrary: a b) case Nil moreover have "(a, b) \<in> edges_on (a # [] @ [b])" by (unfold edges_on_def, auto) ultimately have "(a, b) \<in> r" by auto thus ?case by autonext case (Cons x xs a b) from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold) from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" . moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold) ultimately show ?case by (auto intro!:rstepI)qedlemma image_id: assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x" shows "f ` A = A" using assms by (auto simp:image_def)lemma rel_map_inv_id: assumes "inj_on f ((Domain r) \<union> (Range r))" shows "(rel_map (inv_into ((Domain r) \<union> (Range r)) f \<circ> f) r) = r"proof - let ?f = "(inv_into (Domain r \<union> Range r) f \<circ> f)" { fix a b assume h0: "(a, b) \<in> r" have "pairself ?f (a, b) = (a, b)" proof - from assms h0 have "?f a = a" by (auto intro:inv_into_f_f) moreover have "?f b = b" by (insert h0, simp, intro inv_into_f_f[OF assms], auto intro!:RangeI) ultimately show ?thesis by (auto simp:pairself_def) qed } thus ?thesis by (unfold rel_map_def, intro image_id, case_tac x, auto)qed lemma rel_map_acyclic: assumes "acyclic r" and "inj_on f ((Domain r) \<union> (Range r))" shows "acyclic (rel_map f r)"proof - let ?D = "Domain r \<union> Range r" { fix a assume "(a, a) \<in> (rel_map f r)^+" from plus_rpath[OF this] obtain xs where rp: "rpath (rel_map f r) a xs a" "xs \<noteq> []" by auto from rpath_nnl_lastE[OF this] obtain xs' where eq_xs: "xs = xs'@[a]" by auto from rpath_edges_on[OF rp(1)] have h: "edges_on (a # xs) \<subseteq> rel_map f r" . from edges_on_map[of "inv_into ?D f" "a#xs"] have "edges_on (map (inv_into ?D f) (a # xs)) = rel_map (inv_into ?D f) (edges_on (a # xs))" . with rel_map_mono[OF h, of "inv_into ?D f"] have "edges_on (map (inv_into ?D f) (a # xs)) \<subseteq> rel_map ((inv_into ?D f) o f) r" by simp from this[unfolded eq_xs] have subr: "edges_on (map (inv_into ?D f) (a # xs' @ [a])) \<subseteq> rel_map (inv_into ?D f \<circ> f) r" . have "(map (inv_into ?D f) (a # xs' @ [a])) = (inv_into ?D f a) # map (inv_into ?D f) xs' @ [inv_into ?D f a]" by simp from edges_on_rpathI[OF subr[unfolded this]] have "rpath (rel_map (inv_into ?D f \<circ> f) r) (inv_into ?D f a) (map (inv_into ?D f) xs' @ [inv_into ?D f a]) (inv_into ?D f a)" . hence "(inv_into ?D f a, inv_into ?D f a) \<in> (rel_map (inv_into ?D f \<circ> f) r)^+" by (rule rpath_plus, simp) moreover have "(rel_map (inv_into ?D f \<circ> f) r) = r" by (rule rel_map_inv_id[OF assms(2)]) moreover note assms(1) ultimately have False by (unfold acyclic_def, auto) } thus ?thesis by (auto simp:acyclic_def)qedcontext pipbegininterpretation rtree_RAG: rtree "RAG s"proof show "single_valued (RAG s)" by (unfold single_valued_def, auto intro: unique_RAG[OF vt]) show "acyclic (RAG s)" by (rule acyclic_RAG[OF vt])qedlemma sgv_wRAG: shows "single_valued (wRAG s)" using waiting_unique[OF vt] by (unfold single_valued_def wRAG_def, auto)lemma sgv_hRAG: shows "single_valued (hRAG s)" using held_unique by (unfold single_valued_def hRAG_def, auto)lemma sgv_tRAG: shows "single_valued (tRAG s)" by (unfold tRAG_def, rule Relation.single_valued_relcomp, insert sgv_hRAG sgv_wRAG, auto)lemma acyclic_hRAG: shows "acyclic (hRAG s)" by (rule acyclic_subset[OF acyclic_RAG[OF vt]], insert RAG_split, auto)lemma acyclic_wRAG: shows "acyclic (wRAG s)" by (rule acyclic_subset[OF acyclic_RAG[OF vt]], insert RAG_split, auto)lemma acyclic_tRAG: shows "acyclic (tRAG s)" by (unfold tRAG_def, rule acyclic_compose[OF acyclic_RAG[OF vt]], unfold RAG_split, auto)lemma acyclic_tG: shows "acyclic (tG s)"proof(unfold tG_def, rule rel_map_acyclic[OF acyclic_tRAG]) show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))" proof(rule subset_inj_on) show " inj_on the_thread {Th th |th. True}" by (unfold inj_on_def, auto) next from domain_tRAG range_tRAG show " Domain (tRAG s) \<union> Range (tRAG s) \<subseteq> {Th th |th. True}" by auto qedqedend