1 theory Deleted_prop

     2 imports Main Flask Flask_type Init_prop Alive_prop

     3 begin

     4 

     5 context flask 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; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"

    15 apply (induct s, simp add:init_alive_prop)

    16 apply (frule vd_cons)

    17 apply (case_tac a, auto simp:alive_simps split:t_object.splits)

    18 pr 19

    19 done

    20 

    21 lemma cons_app_simp_aux:

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

    23 

    24 lemma not_deleted_imp_exists':

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

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

    27 apply (frule not_deleted_cons_D)

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

    29 done

    30 

    31 (*

    32 

    33 lemma nodel_imp_un_deleted:

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

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

    36 

    37 lemma nodel_exists_remains:

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

    39 apply (drule_tac obj = obj in nodel_imp_un_deleted)

    40 by (simp add:not_deleted_imp_exists')

    41 

    42 lemma nodel_imp_exists:

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

    44 apply (drule_tac obj = obj in nodel_imp_un_deleted)

    45 by (simp add:not_deleted_imp_exists)

    46 

    47 lemma no_del_event_cons_D:

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

    49 by (case_tac e, auto)

    50 *)

    51 end

    52 

    53 end