theory Dpolicy

lemma cdl_cdt_transform_rev:
  "\<lbrakk> invs s; cdl_cdt (transform s) slot' = Some slot \<rbrakk> \<Longrightarrow>
     \<exists>ptr' ptr. slot' = transform_cslot_ptr ptr' \<and> slot = transform_cslot_ptr ptr \<and>
                cdt s ptr' = Some ptr" apply (clarsimp simp:cdt_transform map_lift_over_def split:if_split_asm) apply (rule_tac x=a in exI, rule_tac x=b in exI) apply (subst (asm) inv_into_f_f) apply (rule subset_inj_on) apply (simp add:dom_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> \<exists>ptr' ptr. slot' = transform_cslot_ptr ptr' \<and> slot = transform_cslot_ptr ptr \<and> cdt s ptr' = Some ptr proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ab ba bb. \<lbrakk>invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (transform_cslot_ptr (a, b))) = Some (aa, bb); slot = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> \<exists>ab ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, ba) \<and> (\<exists>a b. transform_cslot_ptr (aa, bb) = transform_cslot_ptr (a, b) \<and> cdt s (ab, ba) = Some (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ab ba bb. \<lbrakk>invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (transform_cslot_ptr (a, b))) = Some (aa, bb); slot = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (a, b) \<and> (\<exists>ab ba. transform_cslot_ptr (aa, bb) = transform_cslot_ptr (ab, ba) \<and> cdt s (a, b) = Some (ab, ba)) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>slot = transform_cslot_ptr (aa, bb); invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba)\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (dom (cdt s))
 2. \<And>a b aa ab ba bb. \<lbrakk>slot = transform_cslot_ptr (aa, bb); invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba)\<rbrakk> \<Longrightarrow> (a, b) \<in> dom (cdt s)
 3. \<And>a b aa ab ba bb. \<lbrakk>invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba); cdt s (a, b) = Some (aa, bb); slot = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (a, b) \<and> (\<exists>ab ba. transform_cslot_ptr (aa, bb) = transform_cslot_ptr (ab, ba) \<and> cdt s (a, b) = Some (ab, ba)) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>slot = transform_cslot_ptr (aa, bb); invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba)\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (?B47 a b aa ab ba bb)
 2. \<And>a b aa ab ba bb. \<lbrakk>slot = transform_cslot_ptr (aa, bb); invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba)\<rbrakk> \<Longrightarrow> dom (cdt s) \<subseteq> ?B47 a b aa ab ba bb
 3. \<And>a b aa ab ba bb. \<lbrakk>slot = transform_cslot_ptr (aa, bb); invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba)\<rbrakk> \<Longrightarrow> (a, b) \<in> dom (cdt s)
 4. \<And>a b aa ab ba bb. \<lbrakk>invs s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); slot' = transform_cslot_ptr (a, b); cdt s (a, b) = Some (ab, ba); cdt s (a, b) = Some (aa, bb); slot = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (a, b) \<and> (\<exists>ab ba. transform_cslot_ptr (aa, bb) = transform_cslot_ptr (ab, ba) \<and> cdt s (a, b) = Some (ab, ba)) proof (prove)
goal:
No subgoals!