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