diff -r 0fd478e14e87 -r f1b39d77db00 red_1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/red_1.thy	Thu Dec 03 14:34:29 2015 +0800
@@ -0,0 +1,359 @@
+section {*
+  This file contains lemmas used to guide the recalculation of current precedence 
+  after every system call (or system operation)
+*}
+theory CpsG
+imports PrioG Max RTree
+begin
+
+
+definition "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)
+  qed
+qed simp
+
+lemma 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)
+qed
+
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 auto
+qed
+
+lemma edges_on_rpathI:
+  assumes "edges_on (a#xs@[b]) \<subseteq> r"
+  shows "rpath r a (xs@[b]) b"
+  using assms
+proof(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 auto
+next
+  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)
+qed
+
+lemma 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)
+qed
+
+context pip
+begin
+
+interpretation 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])
+qed
+
+lemma 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
+  qed
+qed
+
+end