101 lemma not_all_procs_prop3: |
101 lemma not_all_procs_prop3: |
102 "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> current_procs s" |
102 "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> current_procs s" |
103 apply (induct s, simp) |
103 apply (induct s, simp) |
104 by (case_tac a, auto) |
104 by (case_tac a, auto) |
105 |
105 |
|
106 lemma not_all_msgqs_cons: |
|
107 "p \<notin> all_msgqs (e # s) \<Longrightarrow> p \<notin> all_msgqs s" |
|
108 by (case_tac e, auto) |
|
109 |
|
110 lemma not_all_msgqs_prop: |
|
111 "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p" |
|
112 apply (induct s, rule notI, simp) |
|
113 apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI) |
|
114 apply (case_tac a, auto) |
|
115 done |
|
116 |
|
117 lemma not_all_msgqs_prop2: |
|
118 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs" |
|
119 apply (induct s, simp) |
|
120 by (case_tac a, auto) |
|
121 |
|
122 lemma not_all_msgqs_prop3: |
|
123 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s" |
|
124 apply (induct s, simp) |
|
125 by (case_tac a, auto) |
|
126 |
106 fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
127 fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
107 where |
128 where |
108 "enrich_not_alive s obj (E_file f) = (f \<notin> current_files s \<and> E_file f \<noteq> obj)" |
129 "enrich_not_alive s obj (E_file f) = (f \<notin> current_files s \<and> obj \<noteq> E_file f)" |
109 | "enrich_not_alive s obj (E_proc p) = (p \<notin> current_procs s \<and> E_proc p \<noteq> obj)" |
130 | "enrich_not_alive s obj (E_proc p) = (p \<notin> current_procs s \<and> obj \<noteq> E_proc p)" |
110 | "enrich_not_alive s obj (E_fd p fd) = ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> E_fd p fd \<noteq> obj)" |
131 | "enrich_not_alive s obj (E_fd p fd) = |
111 | "enrich_not_alive s obj (E_msgq q) = (q \<notin> current_msgqs s \<and> E_msgq q \<noteq> obj)" |
132 ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> obj \<noteq> E_fd p fd \<and> obj \<noteq> E_proc p)" |
112 | "enrich_not_alive s obj (E_inum i) = (i \<notin> current_inode_nums s \<and> E_inum i \<noteq> obj)" |
133 | "enrich_not_alive s obj (E_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q)" |
113 | "enrich_not_alive s obj (E_msg q m) = ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> E_msg q m \<noteq> obj)" |
134 | "enrich_not_alive s obj (E_inum i) = (i \<notin> current_inode_nums s \<and> obj \<noteq> E_inum i)" |
|
135 | "enrich_not_alive s obj (E_msg q m) = |
|
136 ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msg q m \<and> obj \<noteq> E_msgq q)" |
114 |
137 |
115 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf" |
138 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf" |
116 apply (case_tac f) |
139 apply (case_tac f) |
117 apply (simp, drule root_is_dir', simp+) |
140 apply (simp, drule root_is_dir', simp+) |
118 apply (simp add:parentf_is_dir_prop2) |
141 apply (simp add:parentf_is_dir_prop2) |
536 by (auto simp:Open None) |
559 by (auto simp:Open None) |
537 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
560 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
538 using os alive' p_in notin_all Open None |
561 using os alive' p_in notin_all Open None |
539 apply (erule_tac x = "E_fd p fd" in allE) |
562 apply (erule_tac x = "E_fd p fd" in allE) |
540 apply (case_tac obj') |
563 apply (case_tac obj') |
541 by auto |
564 apply (auto dest:not_all_procs_prop3) |
|
565 done |
542 have "os_grant s' e" using p_in f_in fd_not_in os |
566 have "os_grant s' e" using p_in f_in fd_not_in os |
543 by (simp add:Open None) |
567 by (simp add:Open None) |
544 moreover have "grant s' e" |
568 moreover have "grant s' e" |
545 proof- |
569 proof- |
546 from grant obtain up rp tp uf rf tf |
570 from grant obtain up rp tp uf rf tf |
587 apply (case_tac obj') |
611 apply (case_tac obj') |
588 by auto |
612 by auto |
589 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
613 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
590 using os alive' p_in Open Some notin_all |
614 using os alive' p_in Open Some notin_all |
591 apply (erule_tac x = "E_fd p fd" in allE) |
615 apply (erule_tac x = "E_fd p fd" in allE) |
592 apply (case_tac obj', auto) |
616 apply (case_tac obj', auto dest:not_all_procs_prop3) |
593 done |
617 done |
594 have inum_not_in: "inum \<notin> current_inode_nums s'" |
618 have inum_not_in: "inum \<notin> current_inode_nums s'" |
595 using os alive' Open Some notin_all |
619 using os alive' Open Some notin_all |
596 apply (erule_tac x = "E_inum inum" in allE) |
620 apply (erule_tac x = "E_inum inum" in allE) |
597 by (case_tac obj', auto) |
621 by (case_tac obj', auto) |
1114 have q_in: "q \<in> current_msgqs s'" using os alive |
1138 have q_in: "q \<in> current_msgqs s'" using os alive |
1115 apply (erule_tac x = "O_msgq q" in allE) |
1139 apply (erule_tac x = "O_msgq q" in allE) |
1116 by (simp add:SendMsg) |
1140 by (simp add:SendMsg) |
1117 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in |
1141 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in |
1118 apply (erule_tac x = "E_msg q m" in allE) |
1142 apply (erule_tac x = "E_msg q m" in allE) |
1119 apply (case_tac obj') |
1143 apply (case_tac obj', auto dest:not_all_msgqs_prop3) |
1120 by auto |
1144 done |
1121 have "os_grant s' e" using p_in q_in m_not_in |
1145 have "os_grant s' e" using p_in q_in m_not_in |
1122 by (simp add:SendMsg) |
1146 by (simp add:SendMsg) |
1123 moreover have "grant s' e" |
1147 moreover have "grant s' e" |
1124 proof- |
1148 proof- |
1125 from grant obtain up rp tp uq rq tq |
1149 from grant obtain up rp tp uq rq tq |