789 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop |
789 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop |
790 intro:msgq_has_sec_imp_init split:option.splits) |
790 intro:msgq_has_sec_imp_init split:option.splits) |
791 *) |
791 *) |
792 |
792 |
793 lemma co2sobj_nil_prop: |
793 lemma co2sobj_nil_prop: |
794 "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj" |
794 "init_dalive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj" |
795 apply (case_tac obj) |
795 apply (case_tac obj) |
796 apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop |
796 apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop |
797 cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1 |
797 cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1 |
798 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *) |
798 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *) |
799 same_inode_nil_prop (*cm2smsg_nil_prop *) |
799 same_inode_nil_prop (*cm2smsg_nil_prop *) |
800 dest:init_same_inode_prop1 |
800 dest:init_same_inode_prop1 |
801 split:option.splits) |
801 split:option.splits) |
802 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
802 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
803 done |
803 done |
804 |
804 |
|
805 lemma init_dalive_prop: "init_dalive obj = dalive [] obj" |
|
806 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props |
|
807 is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil |
|
808 is_tcp_sock_nil is_udp_sock_nil) |
|
809 done |
|
810 |
805 lemma s2ss_nil_prop: |
811 lemma s2ss_nil_prop: |
806 "s2ss [] = init_static_state" |
812 "s2ss [] = init_static_state" |
807 using co2sobj_nil_prop init_alive_prop |
813 using co2sobj_nil_prop init_dalive_prop |
808 by (auto simp add:s2ss_def init_static_state_def) |
814 by (auto simp add:s2ss_def init_static_state_def) |
809 |
815 |
810 end |
816 end |
811 |
817 |
812 (*<*) |
818 (*<*) |