--- 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.