--- a/Current_prop.thy Tue Jul 09 14:43:51 2013 +0800
+++ b/Current_prop.thy Thu Jul 11 07:52:06 2013 +0800
@@ -177,87 +177,10 @@
\<Longrightarrow> P"
by (erule Info_flow_shm.cases, auto)
-
lemma Info_flow_shm_prop1:
"\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s"
by (rule notI, drule Info_flow_shm.intros(1), simp)
-lemma Info_flow_shm_intro4:
- "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
-by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
-
-(********* simpset for inductive Info_flow_shm **********)
-
-lemma Info_flow_shm_attach1:
- "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
- ((Info_flow_shm s pa pb) \<or>
- (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
- (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
- (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
- (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"
-proof (induct rule:Info_flow_shm.induct)
- case (ifs_self proc \<tau>)
- show ?case
- proof (rule impI)
- assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
- hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
- hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
- from ifs_self pre have "proc \<in> current_procs s" by simp
- hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
- show "Info_flow_shm s proc proc \<or>
- (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and>
- (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>
- (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and>
- (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"
- using p4 p3 by auto
- qed
-next
- case (ifs_flow \<tau> pa pb h' pc)
- thus ?case
- proof (rule_tac impI)
- assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or>
- \<not> Info_flow_shm s pa pb \<and> pa = p \<and>
- pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
- \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"
- and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
- from p2 and p4 have p2': "Info_flow_shm s pa pb \<or>
- (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
- (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
- (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
- (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
- by (erule_tac impE, simp)
- from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
- from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
- from p3 p4 have p8: "if (h' = h)
- then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
- (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
- (one_flow_shm s h pb pc)
- else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach)
-
- have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp
- moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
- \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
- sorry
- moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
- \<Longrightarrow> Info_flow_shm s pa pc"
- sorry
- moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>
- \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"
- sorry
- ultimately
-
-
-
- show "Info_flow_shm s pa pc \<or>
- (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and>
- (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>
- (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and>
- (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
- apply auto
- sorry
- qed
-qed
-
lemma Info_flow_shm_intro3:
"\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>
\<Longrightarrow> Info_flow_shm s p to"
@@ -265,7 +188,13 @@
apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)
by (rule_tac x = flag in exI, simp)
-lemma Info_flow_shm_attach1:
+lemma Info_flow_shm_intro4:
+ "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
+by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
+
+(********* simpset for inductive Info_flow_shm **********)
+
+lemma Info_flow_shm_attach1_aux:
"Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
(if Info_flow_shm s pa pb then True else
(if (pa = p \<and> flag = SHM_RDWR)
@@ -352,35 +281,93 @@
qed
qed
-
+lemma Info_flow_shm_attach1:
+ "\<lbrakk>valid (Attach p h flag # s); Info_flow_shm (Attach p h flag # s) pa pb\<rbrakk>
+ \<Longrightarrow> (if Info_flow_shm s pa pb then True else
+ (if (pa = p \<and> flag = SHM_RDWR)
+ then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+ else if (pb = p)
+ then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+ else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ Info_flow_shm s p' pb) \<or>
+ (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+ ) )"
+apply (drule_tac p = p and h = h and flag = flag in Info_flow_shm_attach1_aux)
+by auto
-
+lemma Info_flow_shm_attach_aux[rule_format]:
+ "Info_flow_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb"
+apply (erule Info_flow_shm.induct)
+apply (rule impI, rule Info_flow_shm.intros(1), simp)
+apply (rule impI, simp, rule_tac h = ha in Info_flow_shm.intros(2), simp)
+apply (auto simp add:one_flow_shm_simps)
+done
-
+lemma Info_flow_shm_attach2:
+ "\<lbrakk>valid (Attach p h flag # s); if Info_flow_shm s pa pb then True else
+ (if (pa = p \<and> flag = SHM_RDWR)
+ then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+ else if (pb = p)
+ then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+ else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ Info_flow_shm s p' pb) \<or>
+ (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))\<rbrakk>
+ \<Longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def intro:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p' in Info_flow_trans)
+apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2))
+apply (rule Info_flow_shm.intros(1), simp)
+apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p' in Info_flow_trans)
+apply (rule_tac p' = p in Info_flow_trans)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2))
+apply (rule Info_flow_shm.intros(1), simp)
+apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p in Info_flow_trans)
+apply (rule_tac p' = p' in Info_flow_trans)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2))
+apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2)
+apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+apply (rule notI, simp)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p in Info_flow_trans)
+apply (rule_tac p' = p' in Info_flow_trans)
+apply (simp add:Info_flow_shm_attach_aux)
+apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2))
+apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2)
+apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+apply (rule notI, simp)
+apply (simp add:Info_flow_shm_attach_aux)
+done
lemma Info_flow_shm_attach:
"valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb.
- (Info_flow_shm s pa pb) \<or>
- (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
- (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"
+ Info_flow_shm s pa pb \<or>
+ (if (pa = p \<and> flag = SHM_RDWR)
+ then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+ else if (pb = p)
+ then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+ else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ Info_flow_shm s p' pb) \<or>
+ (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+ ) )"
apply (rule ext, rule ext, rule iffI)
-apply (case_tac "Info_flow_shm s pa pb", simp)
-apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)
+apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach1, simp)
+apply (auto split:if_splits)[1]
+apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach2)
+apply (auto split:if_splits)
+done
-apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)
-apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)
-
-
-
-apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)
-apply (simp)
-apply (simp, erule Info_flow_shm_cases', simp, simp)
-apply (rule_tac x =
-apply (auto dest:Info_flow_shm.cases)
-apply (auto simp add:one_flow_shm_simps)
lemma info_flow_shm_detach:
"valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb.