(*<*)
theory Co2sobj_prop
imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
begin
(*<*)
context tainting_s begin
(****************** cf2sfile path simpset ***************)
thm cpfd2sfds_def
lemma sroot_only:
"cf2sfile s [] = Some sroot"
by (simp add:cf2sfile_def)
lemma not_file_is_dir:
"\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"
by (auto simp:is_file_def current_files_def is_dir_def
dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
lemma not_dir_is_file:
"\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"
by (auto simp:is_file_def current_files_def is_dir_def
dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
lemma is_file_or_dir:
"\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"
by (auto dest:not_dir_is_file)
lemma current_file_has_sfile:
"\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
apply (induct f)
apply (rule_tac x = "sroot" in exI, simp add:sroot_only)
apply (frule parentf_in_current', simp, clarsimp)
apply (frule parentf_is_dir'', simp)
apply (frule is_file_or_dir, simp)
apply (auto dest!:current_has_sec'
simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop')
done
definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"
where
"sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"
definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"
where
"get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"
lemma is_file_has_sfile:
"\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some
(if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,
sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>
(sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"
apply (case_tac f, simp, drule root_is_dir', simp, simp)
apply (frule is_file_in_current)
apply (drule current_file_has_sfile, simp)
apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)
done
lemma is_dir_has_sfile:
"\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of
[] \<Rightarrow> cf2sfile s f = Some sroot
| a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some
(if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,
sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>
(sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"
apply (case_tac f, simp add:sroot_only)
apply (frule is_dir_in_current, frule is_dir_not_file)
apply (drule current_file_has_sfile, simp)
apply (auto simp:cf2sfile_def split:if_splits option.splits)
done
lemma sroot_set:
"valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"
apply (frule root_is_dir)
apply (drule is_dir_has_sec, simp)
apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps
root_type_remains root_user_remains
dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'
split:option.splits)
done
lemma cf2sfile_path_file:
"\<lbrakk>is_file s (f # pf); valid s\<rbrakk>
\<Longrightarrow> cf2sfile s (f # pf) = (
case (cf2sfile s pf) of
Some (pfi, pfsec, psec, asecs) \<Rightarrow>
(case (sectxt_of_obj s (O_file (f # pf))) of
Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})
| None \<Rightarrow> None)
| _ \<Rightarrow> None)"
apply (frule is_file_in_current, drule parentf_is_dir'', simp)
apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
apply (frule sroot_set)
apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+)
done
lemma cf2sfile_path_dir:
"\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>
\<Longrightarrow> cf2sfile s (f # pf) = (
case (cf2sfile s pf) of
Some (pfi, pfsec, psec, asecs) \<Rightarrow>
(case (sectxt_of_obj s (O_dir (f # pf))) of
Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})
| None \<Rightarrow> None)
| _ \<Rightarrow> None)"
apply (frule is_dir_in_current, drule parentf_is_dir'', simp)
apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)
apply (frule_tac f = "pf" in is_dir_has_sfile, simp)
apply (frule sroot_set)
apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+)
done
lemma cf2sfile_path:
"\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
case (cf2sfile s pf) of
Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))
then (case (sectxt_of_obj s (O_file (f # pf))) of
Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})
| None \<Rightarrow> None)
else (case (sectxt_of_obj s (O_dir (f # pf))) of
Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})
| None \<Rightarrow> None) )
| None \<Rightarrow> None)"
apply (drule is_file_or_dir, simp)
apply (erule disjE)
apply (frule cf2sfile_path_file, simp) defer
apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)
apply (auto split:option.splits)
done
lemma cf2sfile_path_file_prop1:
"\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>
\<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) =
Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and>
sectxt_of_obj s (O_file (f # pf)) = Some fsec"
apply (frule is_file_has_sfile, simp)
by (auto simp:cf2sfile_path_file)
lemma cf2sfile_path_file_prop2:
"\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs);
sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) =
Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})"
by (drule cf2sfile_path_file_prop1, auto)
lemma cf2sfile_path_dir_prop1:
"\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>
\<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) =
Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and>
sectxt_of_obj s (O_dir (f # pf)) = Some fsec"
apply (frule is_dir_has_sfile, simp)
by (auto simp:cf2sfile_path_dir)
lemma cf2sfile_path_dir_prop2:
"\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs);
sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) =
Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
else Created, fsec, Some pfsec, asecs \<union> {pfsec})"
by (drule cf2sfile_path_dir_prop1, auto)
(**************** cf2sfile event list simpset ****************)
lemma cf2sfile_open_none':
"valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os)
apply (induct f', simp add:cf2sfile_def)
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps)
done
lemma cf2sfile_open_none:
"valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"
apply (rule ext)
by (simp add:cf2sfile_open_none')
lemma cf2sfile_open_some1:
"\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>
\<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac "f = f'", simp)
apply (induct f', simp add:sroot_only, simp)
apply (frule parentf_in_current', simp+)
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps)
done
lemma cf2sfile_open_some2:
"\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>
\<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_file_in_current)
by (simp add:cf2sfile_open_some1)
lemma cf2sfile_open_some3:
"\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>
\<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_dir_in_current)
by (simp add:cf2sfile_open_some1)
lemma cf2sfile_open_some4:
"valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (
case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac f, simp)
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps)
apply (rule impI, (erule conjE)+)
apply (drule not_deleted_init_file, simp+)
apply (simp add:is_file_in_current)
done
lemma cf2sfile_open:
"\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
\<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (
if (opt = None) then cf2sfile s f'
else if (f' = f)
then (case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)
else cf2sfile s f')"
apply (case_tac opt)
apply (simp add:cf2sfile_open_none)
apply (case_tac "f = f'")
apply (simp add:cf2sfile_open_some4 split:option.splits)
apply (simp add:cf2sfile_open_some1 current_files_simps)
done
lemma cf2sfile_mkdir1:
"\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>
\<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac "f = f'", simp)
apply (induct f', simp add:sroot_only, simp)
apply (frule parentf_in_current', simp+)
apply (case_tac "f = f'", simp)
apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps split:if_splits option.splits)
done
lemma cf2sfile_mkdir2:
"\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>
\<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_file_in_current)
by (simp add:cf2sfile_mkdir1)
lemma cf2sfile_mkdir3:
"\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>
\<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_dir_in_current)
by (simp add:cf2sfile_mkdir1)
lemma cf2sfile_mkdir4:
"valid (Mkdir p f i # s)
\<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac f, simp)
apply (clarsimp simp:os_grant.simps)
apply (simp add:sectxt_of_obj_simps)
apply (frule current_proc_has_sec, simp)
apply (frule is_dir_has_sec, simp)
apply (frule get_pfs_secs_prop, simp)
apply (frule is_dir_not_file)
apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps split:option.splits if_splits
dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current)
done
lemma cf2sfile_mkdir:
"\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>
\<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (
if (f' = f)
then (case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)
else cf2sfile s f')"
apply (case_tac "f = f'")
apply (simp add:cf2sfile_mkdir4 split:option.splits)
apply (simp add:cf2sfile_mkdir1 current_files_simps)
done
lemma cf2sfile_linkhard1:
"\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>
\<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac "f = f'", simp)
apply (induct f', simp add:sroot_only, simp)
apply (frule parentf_in_current', simp+)
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps split:if_splits option.splits)
done
lemma cf2sfile_linkhard2:
"\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>
\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_file_in_current)
by (simp add:cf2sfile_linkhard1)
lemma cf2sfile_linkhard3:
"\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>
\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
apply (frule vd_cons, drule is_dir_in_current)
by (simp add:cf2sfile_linkhard1)
lemma cf2sfile_linkhard4:
"valid (LinkHard p oldf f # s)
\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)"
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
apply (case_tac f, simp)
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
get_parentfs_ctxts_simps)
apply (rule impI, (erule conjE)+)
apply (drule not_deleted_init_file, simp+)
apply (simp add:is_file_in_current)
done
lemma cf2sfile_linkhard:
"\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>
\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (
if (f' = f)
then (case (parent f) of
Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
| None \<Rightarrow> None)
else cf2sfile s f')"
apply (case_tac "f = f'")
apply (simp add:cf2sfile_linkhard4 split:option.splits)
apply (simp add:cf2sfile_linkhard1 current_files_simps)
done
lemma cf2sfile_other:
"\<lbrakk>ff \<in> current_files s;
\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
\<forall> p fd. e \<noteq> CloseFd p fd;
\<forall> p f. e \<noteq> UnLink p f;
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i;
\<forall> p f f'. e \<noteq> LinkHard p f f';
valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
apply (frule vd_cons, frule vt_grant_os)
apply (induct ff, simp add:sroot_only)
apply (frule parentf_in_current', simp+, case_tac e)
apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path
split:if_splits option.splits)
done
lemma cf2sfile_other':
"\<lbrakk>valid (e # s);
\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
\<forall> p fd. e \<noteq> CloseFd p fd;
\<forall> p f. e \<noteq> UnLink p f;
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i;
\<forall> p f f'. e \<noteq> LinkHard p f f';
ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
by (auto intro!:cf2sfile_other)
lemma cf2sfile_unlink:
"\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
\<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os)
apply (simp add:current_files_simps split:if_splits)
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
split:if_splits option.splits)
done
lemma cf2sfile_rmdir:
"\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>
\<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"
apply (frule vd_cons, frule vt_grant_os)
apply (simp add:current_files_simps split:if_splits)
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
split:if_splits option.splits)
done
lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"
apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")
by (simp add:pfdof_simp2, simp)
lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"
apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")
by (simp add:pfdof_simp2, simp)
lemma cf2sfile_closefd:
"\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>
\<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"
apply (frule vd_cons, frule vt_grant_os)
apply (simp add:current_files_simps split:if_splits option.splits)
(* costs too much time, but solved
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
split:if_splits option.splits
dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file
not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
dest!:current_has_sec')
done
*)
sorry
lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd
(*********** cfd2sfd simpset *********)
lemma cfd2sfd_open1:
"valid (Open p f flags fd opt # s)
\<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd =
(case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
(Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
| _ \<Rightarrow> None)"
by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)
lemma cfd2sfd_open_some2:
"\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule file_of_proc_fd_in_curf, simp)
apply (case_tac "f = f'", simp)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)
apply (case_tac "p = p'", simp)
apply (rule conjI, rule impI, simp)
apply (drule cf2sfile_open_some1, simp)
apply (auto split:option.splits)[1]
apply simp
apply (drule cf2sfile_open_some1, simp)
apply (auto split:option.splits)[1]
done
lemma cfd2sfd_open_none2:
"\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule file_of_proc_fd_in_curf, simp)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)
apply (case_tac "p = p'", simp)
apply (rule conjI, rule impI, simp)
apply (drule cf2sfile_open_none)
apply (auto split:option.splits)[1]
apply simp
apply (drule cf2sfile_open_none)
apply (auto split:option.splits)[1]
done
lemma cfd2sfd_open2:
"\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"
apply (case_tac opt)
apply (simp add:cfd2sfd_open_none2)
apply (simp add:cfd2sfd_open_some2)
done
lemma cfd2sfd_open:
"\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then
(case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
(Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
| _ \<Rightarrow> None) else cfd2sfd s p' fd')"
apply (simp split:if_splits)
apply (simp add:cfd2sfd_open1 split:option.splits)
apply (simp add:cfd2sfd_open2)
apply (rule impI, simp)
done
lemma cfd2sfd_closefd:
"\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>
\<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule file_of_proc_fd_in_curf, simp)
apply (frule cf2sfile_closefd, simp)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
apply (auto split:option.splits if_splits)
done
lemma cfd2sfd_clone:
"\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>
\<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (
if (p'' = p') then cfd2sfd s p fd'
else cfd2sfd s p'' fd')"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
apply (frule_tac cf2sfile_other', simp+)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
apply (case_tac "p'' = p'", simp)
apply (auto split:option.splits if_splits)[1]
apply (simp)
apply (auto split:option.splits if_splits)[1]
done
lemma cfd2sfd_execve:
"\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
apply (frule_tac cf2sfile_other', simp+)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
apply (case_tac "p' = p", simp)
apply (auto split:option.splits if_splits)[1]
apply (simp)
apply (auto split:option.splits if_splits)[1]
done
lemma cfd2sfd_kill:
"\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule proc_fd_in_procs, simp)
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
apply (frule_tac cf2sfile_other', simp+)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
apply (auto split:option.splits if_splits)
done
lemma cfd2sfd_exit:
"\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>
\<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule proc_fd_in_procs, simp)
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
apply (frule_tac cf2sfile_other', simp+)
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
apply (auto split:option.splits if_splits)
done
lemma cfd2sfd_other:
"\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>
\<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
apply (frule proc_fd_in_procs, simp)
apply (frule file_of_proc_fd_in_curf, simp)
apply (case_tac e)
apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)
apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)
apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)
done
lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other
(********** cpfd2sfds simpset **********)
lemma current_filefd_has_flags:
"\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"
apply (induct s arbitrary:p)
apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
done
lemma current_filefd_has_flags':
"\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
apply (case_tac "file_of_proc_fd s p fd")
apply (simp, drule current_filefd_has_flags, simp+)
done
lemma current_file_has_sfile':
"\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
by (rule notI, drule current_file_has_sfile, simp+)
lemma current_filefd_has_sfd:
"\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"
by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile'
dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)
lemma current_filefd_has_sfd':
"\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)
lemma cpfd2sfds_open1:
"valid (Open p f flags fd opt # s) \<Longrightarrow>
cpfd2sfds (Open p f flags fd opt # s) p = (
case (cfd2sfd (Open p f flags fd opt # s) p fd) of
Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}
| _ \<Rightarrow> cpfd2sfds s p)"
apply (frule vd_cons, frule vt_grant_os)
apply (split option.splits)
apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)
apply (rule allI, rule impI)
apply (rule set_eqI, rule iffI)
apply (case_tac "x = a", simp)
unfolding cpfd2sfds_def
apply (erule CollectE, (erule conjE|erule exE)+)
apply (simp split:if_splits)
apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
apply (case_tac "x = a", simp)
apply (rule_tac x = fd in exI, simp+)
apply (erule conjE|erule exE)+
apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
apply (rule impI, drule proc_fd_in_fds, simp)
apply (simp split:option.splits)
done
lemma cpfd2sfds_open1':
"valid (Open p f flags fd opt # s) \<Longrightarrow>
cpfd2sfds (Open p f flags fd opt # s) p = (
case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
(Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
| _ \<Rightarrow> cpfd2sfds s p)"
apply (frule cfd2sfd_open1)
apply (auto dest:cpfd2sfds_open1 split:option.splits)
done
lemma cpfd2sfds_open2:
"\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'"
apply (frule vt_grant_os, frule vd_cons)
unfolding cpfd2sfds_def
apply (rule set_eqI, rule iffI)
apply (erule CollectE, (erule exE|erule conjE)+)
apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)
apply (rule CollectI)
apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp)
apply (erule CollectE, (erule exE|erule conjE)+)
apply (simp only:file_of_proc_fd.simps split:if_splits)
apply (rule CollectI)
apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
done
lemma cpfd2sfds_open:
"valid (Open p f flags fd opt # s)
\<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (
case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
(Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
| _ \<Rightarrow> cpfd2sfds s p))"
apply (rule ext)
apply (case_tac "x \<noteq> p")
apply (simp add:cpfd2sfds_open2)
apply (simp add:cpfd2sfds_open1')
done
lemma cpfd2sfds_execve:
"valid (Execve p fds # s)
\<Longrightarrow> cpfd2sfds (Execve p fds # s) = (cpfd2sfds s) (p := "
lemma cpfd2sfds_other:
"\<lbrakk>valid (e # s);
\<forall>
lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other
(******** cp2sproc simpset *********)
lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"
apply (simp add:cp2sproc_def)
by (simp add:cp2sproc_def index_of_proc.simps)
lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"
by (simp add:cp2sproc_nil current_procs.simps)
lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (
if (p'' = p') then SCrea (Suc (length \<tau>))
else cp2sproc \<tau> p'' )"
by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"
apply (case_tac e)
by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other
(******************** ch2sshm simpset **************************)
lemma ch2sshm_nil: "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = SInit h"
by (simp add:ch2sshm_def index_of_shm.simps)
lemma ch2sshm_nil': "h \<in> current_shms [] \<Longrightarrow> ch2sshm [] h = SInit h"
by (simp add:ch2sshm_nil current_shms.simps)
lemma ch2sshm_createshm: "ch2sshm (CreateShM p h # \<tau>) h' = (if (h' = h) then SCrea (Suc (length \<tau>)) else ch2sshm \<tau> h')"
by (simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps)
lemma ch2sshm_other: "\<forall> p h. e \<noteq> CreateShM p h \<Longrightarrow> ch2sshm (e # \<tau>) h' = ch2sshm \<tau> h'"
apply (case_tac e)
by (auto simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps)
lemmas ch2sshm_simps = ch2sshm_nil ch2sshm_nil' ch2sshm_createshm ch2sshm_other
(********************* cm2smsg simpset ***********************)
lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"
by (simp add:cm2smsg_def index_of_msg.simps)
lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"
by (simp add:cm2smsg_nil current_msgs.simps)
lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"
by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)
lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"
apply (case_tac e)
by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)
lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
(********************** cfd2fd_s simpset ******************************)
lemma cfd2fd_s_nil: "fd \<in> init_fds_of_proc p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"
by (simp add:cfd2fd_s_def index_of_fd.simps)
lemma cfd2fd_s_nil': "fd \<in> current_proc_fds [] p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"
by (simp add:cfd2fd_s_nil current_proc_fds.simps)
lemma cfd2fd_s_open: "cfd2fd_s (Open p f flags fd opt # \<tau>) p' fd' = (
if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>))
else cfd2fd_s \<tau> p' fd')
else cfd2fd_s \<tau> p' fd' )"
by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
lemma cfd2fd_s_createsock: "cfd2fd_s (CreateSock p af st fd im # \<tau>) p' fd' = (
if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>))
else cfd2fd_s \<tau> p' fd')
else cfd2fd_s \<tau> p' fd' )"
by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
lemma cfd2fd_s_accept: "cfd2fd_s (Accept p fd addr port fd' im # \<tau>) p' fd'' = (
if (p' = p) then (if (fd'' = fd') then SCrea (Suc (length \<tau>))
else cfd2fd_s \<tau> p' fd'')
else cfd2fd_s \<tau> p' fd'' )"
by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
lemma cfd2fd_s_clone: "cfd2fd_s (Clone p p' # \<tau>) p'' fd = (if (p'' = p') then cfd2fd_s \<tau> p fd else cfd2fd_s \<tau> p'' fd)"
by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
lemma cfd2fd_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p af st fd im. e \<noteq> CreateSock p af st fd im;
\<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im;
\<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> cfd2fd_s (e # \<tau>) p'' fd'' = cfd2fd_s \<tau> p'' fd''"
by (case_tac e, auto simp:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)
lemmas cfd2fd_s_simps = cfd2fd_s_nil cfd2fd_s_nil' cfd2fd_s_open cfd2fd_s_createsock cfd2fd_s_accept cfd2fd_s_clone cfd2fd_s_other
(************* cim2im_s simpset **************************)
(* no such lemma
lemma cim2im_s_nil: "init_itag_of_inum im = Some tag \<Longrightarrow> cim2im_s [] im = SInit im"
by (simp add:cim2im_s_def)
*)
lemma cim2im_s_open: "cim2im_s (Open p f flags fd (Some im) # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
by (simp add:cim2im_s_def)
lemma cim2im_s_open': "cim2im_s (Open p f flags fd None # \<tau>) im = cim2im_s \<tau> im"
by (simp add:cim2im_s_def)
lemma cim2im_s_mkdir: "cim2im_s (Mkdir p f im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
by (simp add:cim2im_s_def)
lemma cim2im_s_createsock: "cim2im_s (CreateSock p sf st fd im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
by (simp add:cim2im_s_def)
lemma cim2im_s_accept: "cim2im_s (Accept p fd addr port fd' im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"
by (simp add:cim2im_s_def)
lemma cim2im_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p f im. e \<noteq> Mkdir p f im;
\<forall> p sf st fd im. e \<noteq> CreateSock p sf st fd im;
\<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im\<rbrakk> \<Longrightarrow> cim2im_s (e # \<tau>) im = cim2im_s \<tau> im"
by (case_tac e, auto simp:cim2im_s_def)
lemmas cim2im_s_simps = cim2im_s_open cim2im_s_open' cim2im_s_mkdir cim2im_s_createsock cim2im_s_accept cim2im_s_other
lemma cig2ig_s_simp: "cig2ig_s (e # \<tau>) tag = cig2ig_s \<tau> tag"
apply (case_tac tag)
by auto
(******************* cobj2sobj no Suc (length \<tau>) ***********************)
lemma cf2sfile_le_len: "\<lbrakk>cf2sfile \<tau> f = SCrea (Suc (length \<tau>)) # spf; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"
apply (case_tac f, (simp add:cf2sfile.simps d2s_aux.simps)+)
apply (case_tac "index_of_file \<tau> (a # list)", (simp add:d2s_aux.simps)+)
by (drule index_of_file_le_length', simp+)
lemma cf2sfile_le_len': "\<lbrakk>SCrea (Suc (length \<tau>)) # spf \<preceq> cf2sfile \<tau> f; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"
apply (induct f)
apply (simp add:no_junior_def cf2sfile.simps d2s_aux.simps)
apply (case_tac "cf2sfile \<tau> (a # f) = SCrea (Suc (length \<tau>)) # spf")
apply (drule_tac f = "a # f" in cf2sfile_le_len, simp+)
apply (simp only:cf2sfile.simps d2s_aux.simps)
apply (drule_tac no_junior_noteq, simp+)
apply (rule impI, erule impE, simp+)
apply (drule parentf_in_current', simp+)
done
lemma cp2sproc_le_len: "cp2sproc \<tau> p = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
apply (simp add:cp2sproc_def, case_tac "index_of_proc \<tau> p")
apply (simp add:d2s_aux.simps)+
by (drule index_of_proc_le_length', simp)
lemma ch2sshm_le_len: "ch2sshm \<tau> h = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
apply (simp add:ch2sshm_def, case_tac "index_of_shm \<tau> h")
apply (simp add:d2s_aux.simps)+
by (drule index_of_shm_le_length', simp)
lemma cm2smsg_le_len: "cm2smsg \<tau> m = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
apply (simp add:cm2smsg_def, case_tac "index_of_msg \<tau> m")
apply (simp add:d2s_aux.simps)+
by (drule index_of_msg_le_length', simp)
lemma cim2im_s_le_len: "cim2im_s \<tau> im = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
apply (simp add:cim2im_s_def, case_tac "inum2ind \<tau> im")
apply (simp add:d2s_aux.simps)+
by (drule inum2ind_le_length', simp)
lemma cfd2fd_s_le_len: "cfd2fd_s \<tau> p fd = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"
apply (simp add:cfd2fd_s_def, case_tac "index_of_fd \<tau> p fd")
apply (simp add:d2s_aux.simps)+
by (drule index_of_fd_le_length', simp)
end
(*<*)
end
(*>*)