--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Valid_prop.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,33 @@
+theory Valid_prop
+imports Main Flask Flask_type My_list_prefix
+begin
+
+context flask begin
+
+lemma vd_cons'[rule_format]: "valid s' \<Longrightarrow> e # s = s' \<longrightarrow> valid s"
+by (erule valid.induct, auto)
+
+lemma vd_cons: "valid (e # s) \<Longrightarrow> valid s"
+by (simp only:vd_cons')
+
+lemma vd_appd: " valid (\<tau>' @ \<tau>) \<Longrightarrow> valid \<tau>"
+apply (induct \<tau>')
+by (auto simp:vd_cons)
+
+lemma vd_preceq: "\<lbrakk>\<tau>' \<preceq> \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid \<tau>'"
+apply (erule no_juniorE)
+by (simp only:vd_appd)
+
+lemma vd_prec: "\<lbrakk>\<tau>' \<prec> \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid \<tau>'"
+apply (drule is_ancestor_no_junior)
+by (simp only:vd_preceq)
+
+lemma vt_grant_os: "valid (e # \<tau>) \<Longrightarrow> os_grant \<tau> e"
+by (erule valid.cases, simp+)
+
+lemma vt_grant: "valid (e # \<tau>) \<Longrightarrow> grant \<tau> e"
+by (erule valid.cases, simp+)
+
+end
+
+end
\ No newline at end of file