704 apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop) |
704 apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop) |
705 by (auto split:option.splits) |
705 by (auto split:option.splits) |
706 |
706 |
707 lemma cpfd2sfds_nil_prop: |
707 lemma cpfd2sfds_nil_prop: |
708 "cpfd2sfds [] p = init_cfds2sfds p" |
708 "cpfd2sfds [] p = init_cfds2sfds p" |
709 apply (simp only:cpfd2sfds_def init_cfds2sfds_def) |
709 apply (simp only:cpfd2sfds_def init_cfds2sfds_def proc_file_fds_def init_proc_file_fds_def) |
710 apply (rule set_eqI, rule iffI) |
710 apply (rule set_eqI, rule iffI) |
711 apply (drule CollectD, rule CollectI, (erule exE)+) |
711 apply (drule CollectD, erule bexE, drule CollectD, erule exE) |
712 apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer |
712 apply (rule CollectI, rule_tac x = fd in bexI) defer |
713 apply (drule CollectD, rule CollectI, (erule exE)+) |
713 apply (rule CollectI, rule_tac x = f in exI, simp) |
714 apply (rule_tac x = fd in exI, rule_tac x = f in exI) |
714 apply (drule CollectD, erule bexE, drule CollectD, erule exE) |
|
715 apply (rule CollectI, rule_tac x = fd in bexI) defer |
|
716 apply (rule CollectI, rule_tac x = f in exI) |
715 using cfd2sfd_nil_prop |
717 using cfd2sfd_nil_prop |
716 by auto |
718 by auto |
717 |
719 |
718 lemma ch2sshm_nil_prop: |
720 lemma ch2sshm_nil_prop: |
719 "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h" |
721 "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h" |