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) |
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, rule CollectI, (erule exE)+) |
712 apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) defer |
712 apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer |
713 apply (drule CollectD, rule CollectI, (erule exE)+) |
713 apply (drule CollectD, rule CollectI, (erule exE)+) |
714 apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) |
714 apply (rule_tac x = fd in exI, rule_tac x = f in exI) |
715 using cfd2sfd_nil_prop by auto |
715 using cfd2sfd_nil_prop |
|
716 by auto |
716 |
717 |
717 lemma ch2sshm_nil_prop: |
718 lemma ch2sshm_nil_prop: |
718 "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h" |
719 "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h" |
719 by (simp add:ch2sshm_def init_sectxt_prop init_ch2sshm_def) |
720 by (simp add:ch2sshm_def init_sectxt_prop init_ch2sshm_def) |
720 |
721 |