# HG changeset patch
# User chunhan
# Date 1371132765 -28800
# Node ID 4294abb1f38c9755f9cf7269dd180e3be794121f
# Parent  4d25a9919688979b8d6f97bb6b2c0e3ebf471167
update scripts with no new_* in admissable-check

diff -r 4d25a9919688 -r 4294abb1f38c all_sobj_prop.thy
--- a/all_sobj_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/all_sobj_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -248,8 +248,10 @@
         by (auto split:option.splits if_splits simp:obj2sobj.simps 
                   dest:current_proc_has_sproc)
       have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os
-        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
-        apply (rule ai_cipc) using SP sproc rc ev by auto
+        apply (auto simp:obj2sobj.simps split:option.splits)
+        apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+)      
+        using SP sproc rc ev 
+        by (auto intro:ai_cipc)
       with True show ?thesis by simp
     next
       case False 
@@ -271,7 +273,7 @@
         by (auto split:option.splits if_splits simp:obj2sobj.simps 
                   dest:current_proc_has_sproc)
       have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os 
-        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+        apply (auto simp:obj2sobj.simps split:option.splits)
         apply (rule ap_crole) using SP sproc rc ev srproc by auto
       with True show ?thesis by simp
     next
@@ -652,7 +654,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1179,7 +1181,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1305,7 +1307,7 @@
     have valid: "valid (e#\<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau exp by (simp)
+        using ev tau exp by (simp add:np_notin_curp)
       moreover have "rc_grant \<tau> e" 
         using ev tau ap'_crole(3) SPab 
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1420,7 +1422,7 @@
     have valid: "valid (e#\<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau exp ap'_chown(3) by (simp)
+        using ev tau exp ap'_chown(3) by (simp add:np_notin_curp)
       moreover have "rc_grant \<tau> e" 
         using ev tau ap'_chown(5) SPab 
         by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
@@ -1927,7 +1929,7 @@
     have valid: "valid (e # \<tau>)" 
     proof-
       have "os_grant \<tau> e"
-        using ev tau expab by (simp)
+        using ev tau expab by (simp add:ni_notin_curi)
       moreover have "rc_grant \<tau> e" 
         using ev tau ai'_cipc(3) SPab
         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
diff -r 4d25a9919688 -r 4294abb1f38c del_vs_del_s.thy
--- a/del_vs_del_s.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/del_vs_del_s.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -135,7 +135,7 @@
   from initp fstdel vs' have "source_proc s' p = Some p"
     apply (induct s', simp)
     apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
-    by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp)
+    by (case_tac a, auto dest:not_deleted_imp_exists)
   with exp initp vs' obtain r fr pt u 
     where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"
     apply (frule_tac current_proc_has_sobj, simp)
diff -r 4d25a9919688 -r 4294abb1f38c obj2sobj_prop.thy
--- a/obj2sobj_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/obj2sobj_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -601,8 +601,7 @@
   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk>
   \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"
 apply (frule valid_cons, frule valid_os, case_tac e)
-by (auto simp:ni_init_deled ni_notin_curi split:option.splits
-        dest!:current_proc_has_role')
+by (auto split:option.splits dest!:current_proc_has_role')
 
 lemma obj2sobj_ipc_remains_cons':
   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk>
diff -r 4d25a9919688 -r 4294abb1f38c os_rc.thy
--- a/os_rc.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/os_rc.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -274,6 +274,35 @@
 apply (induct s) defer apply (case_tac a)
 using init_finite by auto
 
+end
+
+context tainting_s_complete begin
+
+lemma init_notin_curf_deleted:
+  "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curi_deleted:
+  "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curp_deleted:
+  "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
+by (induct s, simp, case_tac a, auto)
+  
+lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+by (induct f, auto split:if_splits)
+
+lemma source_proc_in_init:
+  "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
+apply (induct s arbitrary:p, simp split:if_splits)
+apply (frule valid_os, frule valid_cons, case_tac a)
+by (auto split:if_splits)
+
+end
+
+context tainting_s_sound begin
+
 (*** properties of new-proc new-ipc ... ***)
 
 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
@@ -299,22 +328,6 @@
 lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"
 by (simp add:ni_notin_curi)
 
-end
-
-context tainting_s_complete begin
-
-lemma init_notin_curf_deleted:
-  "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curi_deleted:
-  "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curp_deleted:
-  "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
-by (induct s, simp, case_tac a, auto)
-  
 lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"
 using ni_notin_curi[where \<tau> = s]
 by (drule_tac init_notin_curi_deleted, simp+)
@@ -323,18 +336,6 @@
 using np_notin_curp[where \<tau> = s]
 by (drule_tac init_notin_curp_deleted, simp+)
 
-lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
-by (induct f, auto split:if_splits)
-
-lemma source_proc_in_init:
-  "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
-apply (induct s arbitrary:p, simp split:if_splits)
-apply (frule valid_os, frule valid_cons, case_tac a)
-by (auto simp:np_notin_curp split:if_splits)
-
-end
-
-context tainting_s_sound begin
 
 lemma len_fname_all: "length (fname_all_a len) = len"
 by (induct len, auto simp:fname_all_a.simps)
@@ -366,7 +367,7 @@
 lemma clone_event_no_limit: 
   "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"
 apply (rule vs_step)
-apply (auto intro:clone_no_limit split:option.splits
+apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp'
             dest:current_proc_has_role current_proc_has_type)
 done 
 
diff -r 4d25a9919688 -r 4294abb1f38c rc_theory.thy
--- a/rc_theory.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/rc_theory.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -463,21 +463,6 @@
        (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible
      | _                \<Rightarrow> False               )"
 
-
-(**** OS' job: checking resources existence & grant new resource ****)
-
-definition next_nat :: "nat set \<Rightarrow> nat"
-where
-  "next_nat ps = (Max ps) + 1"
-
-definition new_proc :: "t_state \<Rightarrow> t_process"
-where 
-  "new_proc \<tau> = next_nat (current_procs \<tau>)"
-
-definition new_ipc :: "t_state \<Rightarrow> t_ipc"
-where
-  "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
-
 (* new file pathname is user-defined, so os just check if its unexistence *) 
 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
 where
@@ -487,10 +472,10 @@
 | "os_grant \<tau> (ReadFile p f)   = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
 | "os_grant \<tau> (WriteFile p f)  = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
 | "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"
-| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)"
+| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *)
 | "os_grant \<tau> (Send p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
 | "os_grant \<tau> (Recv p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
-| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)"
+| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *)
 | "os_grant \<tau> (Kill p p')      = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" 
 | "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"
 | "os_grant \<tau> (DeleteIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
@@ -961,7 +946,19 @@
   "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p"
 | "initp_intact_but s _                   = initp_intact s"
 
-(*** how to generating new valid pathname for examples of CreateFile ***)
+(*** how to generating new valid pathname for examples of new_proc, new_ipc and new_file as CreateFile ***)
+
+definition next_nat :: "nat set \<Rightarrow> nat"
+where
+  "next_nat ps = (Max ps) + 1"
+
+definition new_proc :: "t_state \<Rightarrow> t_process"
+where 
+  "new_proc \<tau> = next_nat (current_procs \<tau>)"
+
+definition new_ipc :: "t_state \<Rightarrow> t_ipc"
+where
+  "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
 
 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
 where
diff -r 4d25a9919688 -r 4294abb1f38c sound_defs_prop.thy
--- a/sound_defs_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/sound_defs_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -137,8 +137,9 @@
 apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp)
 apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
 apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e)
-apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps dest:nodel_imp_exists[where obj = "Proc pa"]
            split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
 done
 
 lemma initp_intact_I_exec:
@@ -191,6 +192,7 @@
 apply (erule_tac x = p in allE, case_tac e)
 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
            split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
 done
 
 end
diff -r 4d25a9919688 -r 4294abb1f38c source_prop.thy
--- a/source_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/source_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -23,7 +23,7 @@
   "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p"
 apply (induct s, simp)
 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
-apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists)
+apply (case_tac a, auto dest:not_deleted_imp_exists)
 done
 
 lemma init_proc_keeps_source:
diff -r 4d25a9919688 -r 4294abb1f38c tainted_vs_tainted_s.thy
--- a/tainted_vs_tainted_s.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/tainted_vs_tainted_s.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -105,7 +105,7 @@
   with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
     by (auto simp:obj2sobj.simps cp2sproc.simps)
   show ?case using p3 sproc os rc TP 
-    by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps 
+    by (auto simp:obj2sobj.simps cp2sproc.simps dest:not_deleted_imp_exists
             split:option.splits intro!:ts_cipc)
 next
   case (t_read f s p)
@@ -211,9 +211,8 @@
   next
     case (IPC i) 
     have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC
-      by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps 
-                          split:option.splits
-                          dest!:current_proc_has_role')
+      by (case_tac e, auto simp:obj2sobj.simps dest:not_deleted_imp_exists
+                          split:option.splits  dest!:current_proc_has_role')
     with IPC t_remain(2) show ?thesis by simp
   next
     case (Proc p) 
@@ -298,7 +297,7 @@
       have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk>
         \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
         using t_remain(2,3,4) os p5 Proc
-        by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp 
+        by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps dest:not_deleted_imp_exists 
                              simp del:cp2sproc.simps  split:option.splits) 
       ultimately show ?thesis using Proc
         by (case_tac e, auto simp del:obj2sobj.simps) 
@@ -588,7 +587,7 @@
   have valid: "valid (e # s)" 
   proof-
     have "os_grant s e"
-      using ev exp by (simp)
+      using ev exp by (simp add:ni_notin_curi)
     moreover have "rc_grant s e" 
       using ev ts'_cipc(3) SP
       by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1141,7 +1140,7 @@
   have valid: "valid (e # s)" 
   proof-
     have "os_grant s e"
-      using ev exp by (simp)
+      using ev exp by (simp add:ni_notin_curi)
     moreover have "rc_grant s e" 
       using ev ts'_cipc(3) SP
       by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)