equal
deleted
inserted
replaced
21 |
21 |
22 lemma source_proc_of_init_remains: |
22 lemma source_proc_of_init_remains: |
23 "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p" |
23 "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p" |
24 apply (induct s, simp) |
24 apply (induct s, simp) |
25 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp) |
25 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp) |
26 apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists) |
26 apply (case_tac a, auto dest:not_deleted_imp_exists) |
27 done |
27 done |
28 |
28 |
29 lemma init_proc_keeps_source: |
29 lemma init_proc_keeps_source: |
30 "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> |
30 "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> |
31 \<Longrightarrow> source_of_sobj (obj2sobj s (Proc p)) = Some (Proc p)" |
31 \<Longrightarrow> source_of_sobj (obj2sobj s (Proc p)) = Some (Proc p)" |