theory ADT_C

lemma cpspace_user_data_relation_unique:
  "\<lbrakk>cmap_relation (heap_to_user_data ah bh) (clift ch) Ptr cuser_user_data_relation;
    cmap_relation (heap_to_user_data ah' bh')(clift ch) Ptr cuser_user_data_relation\<rbrakk>
   \<Longrightarrow> map_to_user_data ah' = map_to_user_data 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_user_data ah bh)") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) apply (clarsimp simp add: cuser_user_data_relation_def heap_to_user_data_def) apply (rule ccontr) apply (case_tac z, case_tac za) apply simp apply (fastforce simp: dom_def heap_to_user_data_def Collect_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_user_data_relation ah bh ch; cpspace_user_data_relation ah' bh' ch\<rbrakk> \<Longrightarrow> map_to_user_data ah' = map_to_user_data ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PTR(user_data_C) ` dom (heap_to_user_data ah bh) = dom (clift ch); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); PTR(user_data_C) ` dom (heap_to_user_data ah' bh') = dom (clift ch); \<forall>x\<in>dom (heap_to_user_data ah' bh'). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> map_to_user_data ah' = map_to_user_data ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah' bh'). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah' bh')\<rbrakk> \<Longrightarrow> map_to_user_data ah' = map_to_user_data ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' = map_to_user_data ah proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<in> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<in> dom (heap_to_user_data ah bh); cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x)))\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv PTR(user_data_C) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. heap_to_user_data ah bh a = Some y}; \<exists>y. heap_to_user_data ah bh x = Some y; cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); (\<exists>y. heap_to_user_data ah' bh' x = Some y) = (\<exists>y. heap_to_user_data ah bh x = Some y)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR(user_data_C) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data ah a = Some z}; \<forall>off. byte_to_word_heap bh x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; \<forall>off. byte_to_word_heap bh' x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; map_to_user_data ah x = Some z; map_to_user_data ah' x = Some za\<rbrakk> \<Longrightarrow> za = z
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR(user_data_C) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data ah a = Some z}; \<forall>off. byte_to_word_heap bh x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; \<forall>off. byte_to_word_heap bh' x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; map_to_user_data ah x = Some z; map_to_user_data ah' x = Some za; za \<noteq> z\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (2 subgoals):
 1. \<And>x z za. \<lbrakk>inv PTR(user_data_C) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>z. map_to_user_data ah a = Some z}; \<forall>off. byte_to_word_heap bh x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; \<forall>off. byte_to_word_heap bh' x off = user_data_C.words_C (the (clift ch (PTR(user_data_C) x))).[unat off]; map_to_user_data ah x = Some z; map_to_user_data ah' x = Some za; za \<noteq> z; z = UserData; za = UserData\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah bh x)) (the (clift ch (PTR(user_data_C) x))); \<forall>x\<in>dom (heap_to_user_data ah bh). cuser_user_data_relation (the (heap_to_user_data ah' bh' x)) (the (clift ch (PTR(user_data_C) x))); dom (heap_to_user_data ah' bh') = dom (heap_to_user_data ah bh); inv PTR(user_data_C) ` dom (clift ch) = dom (heap_to_user_data ah bh); x \<notin> dom (heap_to_user_data ah bh)\<rbrakk> \<Longrightarrow> map_to_user_data ah' x = map_to_user_data ah x proof (prove)
goal:
No subgoals!