# HG changeset patch
# User chunhan
# Date 1370240294 -28800
# Node ID c8b7c24f1db6dae3dc23fc0b2755fa9b15dc8e45
# Parent  4ca824cd0c594143b81b0caeec5ecbe97a5ae82f
done with cph2spshs simpset

diff -r 4ca824cd0c59 -r c8b7c24f1db6 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Mon Jun 03 10:34:58 2013 +0800
+++ b/Co2sobj_prop.thy	Mon Jun 03 14:18:14 2013 +0800
@@ -960,12 +960,145 @@
 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
 done
 
+lemma cph2spshs_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow>     
+   cph2spshs (DeleteShM p h # s) = (\<lambda> p'. 
+    (case (ch2sshm s h, flag_of_proc_shm s p' h) of 
+       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+                  then cph2spshs s p' else cph2spshs s p' - {(sh, flag)}
+     | _       \<Rightarrow> cph2spshs s p')   )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
 
+apply (clarsimp)
+apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits)
+apply (rule conjI, rule impI)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] 
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
+apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+)
+apply (rule_tac x = ha in exI, simp)
+apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+)
+
+apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
+
+apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
+apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
+apply (case_tac "ha = h", simp)
+apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+
+apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
+apply (case_tac "ha = h", simp)
+apply (rule_tac x = h' in exI, simp)
+apply (frule_tac flag = flag in procs_of_shm_prop4, simp+)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
+apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+
+apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
+apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
+apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
+apply (simp split:if_splits)
+apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (rule notI, simp split:if_splits)
+apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
+apply (simp split:if_splits)
+apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
+apply (case_tac "ha = h", simp add:procs_of_shm_prop4)
+apply (frule_tac h = ha in procs_of_shm_prop1, simp+)
+using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
+done
+
+lemma flag_of_proc_shm_prop1:
+  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
+apply (induct s arbitrary:p)
+apply (simp add:init_shmflag_has_proc)
+apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits)
+done
+
+lemma cph2spshs_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> 
+   cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' := 
+     {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag} )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+using ch2sshm_other[where e = "Clone p p' fds shms" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
+apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4)
+apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1)
+apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)+
+done
+
+lemma cph2spshs_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow>
+  cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+using ch2sshm_other[where e = "Execve p f fds" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
+apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
+done
+
+lemma cph2spshs_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> cph2spshs (Kill p p' # s) = (cph2spshs s) (p' := {})"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+using ch2sshm_other[where e = "Kill p p'" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
+apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
+done
+
+lemma cph2spshs_exit:
+  "valid (Exit p # s) \<Longrightarrow> cph2spshs (Exit p # s) = (cph2spshs s) (p := {})"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+using ch2sshm_other[where e = "Exit p" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
+apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
+done
+
+lemma cph2spshs_createshm:
+  "valid (CreateShM p h # s) \<Longrightarrow> cph2spshs (CreateShM p h # s) = cph2spshs s"
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:cph2spshs_def)
+using ch2sshm_createshm
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
+apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1)
+done
 
 lemma cph2spshs_other:
-  "\<lbrakk>valid (e # s); "
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cph2spshs (e # s) = cph2spshs s"
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+unfolding cph2spshs_def 
+apply (rule set_eqI, rule iffI)
+apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)+
+apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI)
+apply (case_tac e)
+using ch2sshm_other[where e = e and s = s] 
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3
+ simp:ch2sshm_createshm)
+apply (rule_tac x = h in exI, case_tac e)
+using ch2sshm_other[where e = e and s = s] 
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 
+ simp:ch2sshm_createshm)
+done
 
-lemmas cph2spshs_simps = cph2spshs_other
+lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve
+  cph2spshs_exit cph2spshs_kill cph2spshs_other
 
 (******** cp2sproc simpset *********)