--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Delete_prop.thy	Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,53 @@
+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
\ No newline at end of file