theory Deleted_prop

imports Main Flask Flask_type Init_prop Alive_prop

begin

context flask begin

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

by (case_tac e, auto)

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

by (auto dest:deleted_cons_I)

lemma not_deleted_imp_exists:

  "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"

apply (induct s, simp add:init_alive_prop)

apply (frule vd_cons)

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

pr 19

done

lemma cons_app_simp_aux:

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

lemma not_deleted_imp_exists':

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

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

apply (frule not_deleted_cons_D)

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

done

(*

lemma nodel_imp_un_deleted:

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

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

lemma nodel_exists_remains:

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

apply (drule_tac obj = obj in nodel_imp_un_deleted)

by (simp add:not_deleted_imp_exists')

lemma nodel_imp_exists:

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

apply (drule_tac obj = obj in nodel_imp_un_deleted)

by (simp add:not_deleted_imp_exists)

lemma no_del_event_cons_D:

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

by (case_tac e, auto)

*)

end

end