1 theory Valid_prop

     2 imports Main Flask Flask_type My_list_prefix

     3 begin

     4 

     5 context flask begin

     6 

     7 lemma vd_cons'[rule_format]: "valid s' \<Longrightarrow> e # s = s' \<longrightarrow> valid s"

     8 by (erule valid.induct, auto)

     9 

    10 lemma vd_cons: "valid (e # s) \<Longrightarrow> valid s"

    11 by (simp only:vd_cons')

    12 

    13 lemma vd_appd: " valid (\<tau>' @ \<tau>) \<Longrightarrow> valid \<tau>"

    14 apply (induct \<tau>')

    15 by (auto simp:vd_cons)

    16 

    17 lemma vd_preceq: "\<lbrakk>\<tau>' \<preceq> \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid \<tau>'"

    18 apply (erule no_juniorE)

    19 by (simp only:vd_appd)

    20 

    21 lemma vd_prec: "\<lbrakk>\<tau>' \<prec> \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid \<tau>'"

    22 apply (drule is_ancestor_no_junior)

    23 by (simp only:vd_preceq)

    24 

    25 lemma vt_grant_os: "valid (e # \<tau>) \<Longrightarrow> os_grant \<tau> e"

    26 by (erule valid.cases, simp+)

    27 

    28 lemma vt_grant: "valid (e # \<tau>) \<Longrightarrow> grant \<tau> e"

    29 by (erule valid.cases, simp+)

    30 

    31 end

    32 

    33 end