1 theory deleted_prop

     2 imports Main rc_theory os_rc

     3 begin

     4 

     5 context tainting begin

     6 

     7 lemma deleted_cons_I: "deleted obj s \<Longrightarrow> deleted obj (e # s)"

     8 by (case_tac e, auto)

     9 

    10 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" 

    11 by (auto dest:deleted_cons_I)

    12 

    13 lemma not_deleted_imp_exists:

    14   "\<lbrakk>\<not> deleted obj s; exists [] obj\<rbrakk> \<Longrightarrow> exists s obj"

    15 apply (induct s, simp)

    16 apply (case_tac a, case_tac [!] obj, auto)

    17 done

    18 

    19 lemma cons_app_simp_aux:

    20   "(a # b) @ c = a # (b @ c)" by auto

    21 

    22 lemma not_deleted_imp_exists':

    23   "\<lbrakk>\<not> deleted obj (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"

    24 apply (induct s', simp, simp only:cons_app_simp_aux)

    25 apply (frule not_deleted_cons_D)

    26 apply (case_tac a, case_tac [!] obj, auto)

    27 done

    28 

    29 lemma nodel_imp_un_deleted:

    30   "no_del_event s \<Longrightarrow> \<not> deleted obj s"

    31 by (induct s, simp, case_tac a,auto)

    32 

    33 lemma nodel_exists_remains:

    34   "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"

    35 apply (drule_tac obj = obj in nodel_imp_un_deleted)

    36 by (simp add:not_deleted_imp_exists')

    37 

    38 lemma nodel_imp_exists:

    39   "\<lbrakk>no_del_event s; exists [] obj\<rbrakk> \<Longrightarrow> exists s obj"

    40 apply (drule_tac obj = obj in nodel_imp_un_deleted)

    41 by (simp add:not_deleted_imp_exists)

    42 

    43 lemma no_del_event_cons_D:

    44   "no_del_event (e # s) \<Longrightarrow> no_del_event s"

    45 by (case_tac e, auto)

    46 

    47 end

    48 

    49 end