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