theory Invocation_DP

lemma sep_nonimpact_valid_lift:
  assumes non_intent_impact:
   "\<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
    f \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>"
  assumes non_irq_node_impact:
   "\<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> f \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace>"
  shows
   "\<lbrace>\<lambda>s. < Q >  s\<rbrace> f \<lbrace>\<lambda>rv s. < Q > s\<rbrace>" apply (clarsimp simp: valid_def sep_state_projection_def Let_def
                        sep_state_add_def sep_disj_sep_state_def
                        sep_state_disj_def
                        map_option_case
                 split: if_split_asm option.splits sep_state.splits) apply (erule rsubst [where P=Q]) apply clarsimp apply (rule conjI) apply (rule ext)+ apply (clarsimp split:option.splits) apply (intro conjI impI allI) apply (drule_tac P1 ="\<lambda>x. True" and A1 = "\<lambda>x. \<not>x" in use_valid[OF _ non_intent_impact]) apply (simp add:object_at_def)+ apply (drule_tac P1 ="\<lambda>x. True" and A1 = "\<lambda>x. x" in use_valid[OF _ non_intent_impact]) apply (fastforce simp:object_at_def)+ apply (drule_tac P1 ="\<lambda>x. object_clean x = object_clean x2" and
                    A1 = "\<lambda>x. x" in use_valid[OF _ non_intent_impact]) apply (fastforce simp:object_at_def) apply (clarsimp simp: object_at_def object_slots_object_clean
                         object_project_def
                  split: cdl_component_id.splits) apply (rule ext)+ apply (clarsimp split:option.splits) apply (drule_tac A1 = "\<lambda>x. x = (cdl_irq_node s)" in use_valid[OF _ non_irq_node_impact]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift Q\<rbrace> f \<lbrace>\<lambda>rv. cdl.lift Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>Q (SepState (\<lambda>(obj_id, comp_id). case cdl_objects s obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) (\<lambda>irq. Some (cdl_irq_node s irq))); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q (SepState (\<lambda>(obj_id, comp_id). case cdl_objects b obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) (\<lambda>irq. Some (cdl_irq_node b irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> SepState (\<lambda>(obj_id, comp_id). case cdl_objects s obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) (\<lambda>irq. Some (cdl_irq_node s irq)) = SepState (\<lambda>(obj_id, comp_id). case cdl_objects b obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>(obj_id, comp_id). case cdl_objects s obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) = (\<lambda>(obj_id, comp_id). case cdl_objects b obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) \<and> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>(obj_id, comp_id). case cdl_objects s obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) = (\<lambda>(obj_id, comp_id). case cdl_objects b obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x))
 2. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. (a, b) \<in> fst (f s) \<Longrightarrow> (case x of (obj_id, comp_id) \<Rightarrow> case cdl_objects s obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x)) = (case x of (obj_id, comp_id) \<Rightarrow> case cdl_objects b obj_id of None \<Rightarrow> None | Some x \<Rightarrow> Some (object_project comp_id x))
 2. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. (a, b) \<in> fst (f s) \<Longrightarrow> (cdl_objects s aa = None \<longrightarrow> cdl_objects b aa = None) \<and> (\<forall>x2. cdl_objects s aa = Some x2 \<longrightarrow> (\<exists>y. cdl_objects b aa = Some y) \<and> (\<forall>x2a. cdl_objects b aa = Some x2a \<longrightarrow> object_project ba x2 = object_project ba x2a))
 2. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (4 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = None\<rbrakk> \<Longrightarrow> cdl_objects b aa = None
 2. \<And>s a b aa ba x2. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects b aa = Some y
 3. \<And>s a b aa ba x2 x2a. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 4. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (5 subgoals):
 1. \<And>s a b aa ba. cdl_objects s aa = None \<Longrightarrow> \<not> object_at (\<lambda>obj. True) (?ptr34 s a b aa ba) s
 2. \<And>s a b aa ba. \<lbrakk>cdl_objects s aa = None; \<not> object_at (\<lambda>obj. True) (?ptr34 s a b aa ba) b\<rbrakk> \<Longrightarrow> cdl_objects b aa = None
 3. \<And>s a b aa ba x2. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects b aa = Some y
 4. \<And>s a b aa ba x2 x2a. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 5. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa x2. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects b aa = Some y
 2. \<And>s a b aa ba x2 x2a. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 3. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (4 subgoals):
 1. \<And>s a b aa x2. cdl_objects s aa = Some x2 \<Longrightarrow> object_at (\<lambda>obj. True) (?ptr39 s a b aa x2) s
 2. \<And>s a b aa x2. \<lbrakk>cdl_objects s aa = Some x2; object_at (\<lambda>obj. True) (?ptr39 s a b aa x2) b\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects b aa = Some y
 3. \<And>s a b aa ba x2 x2a. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 4. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba x2 x2a. \<lbrakk>(a, b) \<in> fst (f s); cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 2. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba x2 x2a. \<lbrakk>cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a\<rbrakk> \<Longrightarrow> object_at (\<lambda>obj. object_clean (object_clean obj) = object_clean x2) (?ptr49 s a b aa ba x2 x2a) s
 2. \<And>s a b aa ba x2 x2a. \<lbrakk>cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a; object_at (\<lambda>obj. object_clean (object_clean obj) = object_clean x2) (?ptr49 s a b aa ba x2 x2a) b\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 3. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba x2 x2a. \<lbrakk>cdl_objects s aa = Some x2; cdl_objects b aa = Some x2a; object_at (\<lambda>obj. object_clean (object_clean obj) = object_clean x2) aa b\<rbrakk> \<Longrightarrow> object_project ba x2 = object_project ba x2a
 2. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>irq. Some (cdl_irq_node b irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. (a, b) \<in> fst (f s) \<Longrightarrow> Some (cdl_irq_node s irq) = Some (cdl_irq_node b irq) proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. (a, b) \<in> fst (f s) \<Longrightarrow> cdl_irq_node s irq = cdl_irq_node b irq proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. cdl_irq_node s = cdl_irq_node s
 2. \<And>s a b irq. cdl_irq_node b = cdl_irq_node s \<Longrightarrow> cdl_irq_node s irq = cdl_irq_node b irq proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. cdl_irq_node b = cdl_irq_node s \<Longrightarrow> cdl_irq_node s irq = cdl_irq_node b irq proof (prove)
goal:
No subgoals!