theory ADT_C

lemma cpspace_device_data_relation_unique:
  "\<lbrakk>cmap_relation (heap_to_device_data ah bh) (clift ch) Ptr cuser_device_data_relation;
    cmap_relation (heap_to_device_data ah' bh')(clift ch) Ptr cuser_device_data_relation\<rbrakk>
   \<Longrightarrow> map_to_user_data_device ah' = map_to_user_data_device ah" apply (clarsimp simp add: cmap_relation_def) apply (drule inj_image_inv[OF inj_Ptr])+ apply simp apply (rule ext) apply (case_tac "x:dom (heap_to_device_data ah bh)") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) apply (clarsimp simp add: heap_to_device_data_def) apply (rule ccontr) apply (case_tac z, case_tac za) apply simp apply (fastforce simp: dom_def heap_to_device_data_def Collect_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (heap_to_device_data ah bh) (clift ch) PTR('a) cuser_device_data_relation; cmap_relation (heap_to_device_data ah' bh') (clift ch) PTR('a) cuser_device_data_relation\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' = map_to_user_data_device ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PTR('a) ` dom (heap_to_device_data ah bh) = dom (clift ch); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); PTR('a) ` dom (heap_to_device_data ah' bh') = dom (clift ch); \<forall>x\<in>dom (heap_to_device_data ah' bh'). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x)))\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' = map_to_user_data_device ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah' bh'). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah' bh')\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' = map_to_user_data_device ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' = map_to_user_data_device ah proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<in> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<in> dom (heap_to_device_data ah bh); cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x)))\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv PTR('a) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. heap_to_device_data ah bh a = Some y}; \<exists>y. heap_to_device_data ah bh x = Some y; cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); (\<exists>y. heap_to_device_data ah' bh' x = Some y) = (\<exists>y. heap_to_device_data ah bh x = Some y)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR('a) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data_device ah a = Some z}; cuser_device_data_relation (byte_to_word_heap bh x) (the (clift ch (PTR('a) x))); cuser_device_data_relation (byte_to_word_heap bh' x) (the (clift ch (PTR('a) x))); map_to_user_data_device ah x = Some z; map_to_user_data_device ah' x = Some za\<rbrakk> \<Longrightarrow> za = z
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR('a) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data_device ah a = Some z}; cuser_device_data_relation (byte_to_word_heap bh x) (the (clift ch (PTR('a) x))); cuser_device_data_relation (byte_to_word_heap bh' x) (the (clift ch (PTR('a) x))); map_to_user_data_device ah x = Some z; map_to_user_data_device ah' x = Some za; za \<noteq> z\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR('a) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data_device ah a = Some z}; cuser_device_data_relation (byte_to_word_heap bh x) (the (clift ch (PTR('a) x))); cuser_device_data_relation (byte_to_word_heap bh' x) (the (clift ch (PTR('a) x))); map_to_user_data_device ah x = Some z; map_to_user_data_device ah' x = Some za; za \<noteq> z; z = UserDataDevice; za = UserDataDevice\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah bh x)) (the (clift ch (PTR('a) x))); \<forall>x\<in>dom (heap_to_device_data ah bh). cuser_device_data_relation (the (heap_to_device_data ah' bh' x)) (the (clift ch (PTR('a) x))); dom (heap_to_device_data ah' bh') = dom (heap_to_device_data ah bh); inv PTR('a) ` dom (clift ch) = dom (heap_to_device_data ah bh); x \<notin> dom (heap_to_device_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data_device ah' x = map_to_user_data_device ah x proof (prove)
goal:
No subgoals!