69 apply (frule is_dir_in_current, frule is_dir_not_file) |
67 apply (frule is_dir_in_current, frule is_dir_not_file) |
70 apply (drule current_file_has_sfile, simp) |
68 apply (drule current_file_has_sfile, simp) |
71 apply (auto simp:cf2sfile_def split:if_splits option.splits) |
69 apply (auto simp:cf2sfile_def split:if_splits option.splits) |
72 done |
70 done |
73 |
71 |
|
72 lemma sroot_set: |
|
73 "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec" |
|
74 apply (frule root_is_dir) |
|
75 apply (drule is_dir_has_sec, simp) |
|
76 apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps |
|
77 root_type_remains root_user_remains |
|
78 dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user' |
|
79 split:option.splits) |
|
80 done |
|
81 |
|
82 lemma cf2sfile_path_file: |
|
83 "\<lbrakk>is_file s (f # pf); valid s\<rbrakk> |
|
84 \<Longrightarrow> cf2sfile s (f # pf) = ( |
|
85 case (cf2sfile s pf) of |
|
86 Some (pfi, pfsec, psec, asecs) \<Rightarrow> |
|
87 (case (sectxt_of_obj s (O_file (f # pf))) of |
|
88 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
|
89 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
|
90 | None \<Rightarrow> None) |
|
91 | _ \<Rightarrow> None)" |
|
92 apply (frule is_file_in_current, drule parentf_is_dir'', simp) |
|
93 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp) |
|
94 apply (frule sroot_set) |
|
95 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) |
|
96 done |
|
97 |
|
98 lemma cf2sfile_path_dir: |
|
99 "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk> |
|
100 \<Longrightarrow> cf2sfile s (f # pf) = ( |
|
101 case (cf2sfile s pf) of |
|
102 Some (pfi, pfsec, psec, asecs) \<Rightarrow> |
|
103 (case (sectxt_of_obj s (O_dir (f # pf))) of |
|
104 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf) |
|
105 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
|
106 | None \<Rightarrow> None) |
|
107 | _ \<Rightarrow> None)" |
|
108 apply (frule is_dir_in_current, drule parentf_is_dir'', simp) |
|
109 apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp) |
|
110 apply (frule_tac f = "pf" in is_dir_has_sfile, simp) |
|
111 apply (frule sroot_set) |
|
112 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) |
|
113 done |
|
114 |
74 lemma cf2sfile_path: |
115 lemma cf2sfile_path: |
75 "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = ( |
116 "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = ( |
76 case (cf2sfile s pf) of |
117 case (cf2sfile s pf) of |
77 Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf)) |
118 Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf)) |
78 then (case (sectxt_of_obj s (O_file (f # pf))) of |
119 then (case (sectxt_of_obj s (O_file (f # pf))) of |
79 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
120 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
80 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
121 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
81 | None \<Rightarrow> None) |
122 | None \<Rightarrow> None) |
82 else (case (sectxt_of_obj s (O_dir (f # pf))) of |
123 else (case (sectxt_of_obj s (O_dir (f # pf))) of |
83 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
124 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf) |
84 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
125 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
85 | None \<Rightarrow> None) ) |
126 | None \<Rightarrow> None) ) |
86 | None \<Rightarrow> None)" |
127 | None \<Rightarrow> None)" |
|
128 apply (drule is_file_or_dir, simp) |
|
129 apply (erule disjE) |
|
130 apply (frule cf2sfile_path_file, simp) defer |
|
131 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file) |
|
132 apply (auto split:option.splits) |
|
133 done |
|
134 |
|
135 |
|
136 |
|
137 apply simp |
|
138 |
|
139 thm cf2sfile_def |
|
140 apply (simp (no_asm_simp)) |
|
141 apply simp |
|
142 apply (frule cf2sfile_path_file, simp) |
|
143 apply (simp add: cf2sfile_path_file) |
|
144 apply auto |
|
145 apply (simp only:cf2sfile_path_file) |
|
146 by (simp add:cf2sfile_path_file cf2sfile_path_dir) |
87 apply (frule parentf_is_dir'', simp) |
147 apply (frule parentf_is_dir'', simp) |
88 apply (frule parentf_in_current', simp) |
|
89 apply (frule is_file_or_dir, simp) |
148 apply (frule is_file_or_dir, simp) |
90 apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE) |
149 apply (frule sroot_set, erule disjE) |
91 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop |
150 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp) |
92 simp:cf2sfile_def split:option.splits if_splits) |
151 apply (case_tac pf, clarsimp) |
|
152 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps |
|
153 simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] |
|
154 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop |
|
155 simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] |
93 apply (case_tac "is_file s (f # pf)") |
156 apply (case_tac "is_file s (f # pf)") |
94 apply (frule is_file_has_sec, simp) |
157 apply (frule is_file_has_sec, simp) |
95 apply (frule is_dir_has_sec, simp) |
158 apply (frule is_dir_has_sec, simp) |
96 apply (frule is_dir_not_file) |
159 apply (frule is_dir_not_file) |
97 apply (erule exE)+ |
160 apply (erule exE)+ |