theory Finalise_DR

lemma remain_pd_either_section_relation:
  "\<lbrakk>\<forall>y \<in> set ys. is_aligned y 2;ptr\<notin> set ys;is_aligned ptr 2\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in> set ys. (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
    pd_section_relation (y && ~~ mask pd_bits) pg_id y s) \<rbrace>
    store_pde ptr ARM_A.pde.InvalidPDE
   \<lbrace>\<lambda>r s. \<forall>y\<in>set ys.
     (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
     pd_section_relation (y && ~~ mask pd_bits) pg_id y s)\<rbrace>" including no_pre apply (rule hoare_vcg_const_Ball_lift) apply (wp hoare_vcg_disj_lift) apply (rule hoare_strengthen_post[OF remain_pd_super_section_relation]; fastforce) apply (rule hoare_strengthen_post[OF remain_pd_section_relation]; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>set ys. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>r s. \<forall>y\<in>set ys. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>set ys. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>r s. \<forall>y\<in>set ys. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2; y \<in> set ys\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>rv s. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> pd_section_relation (y && ~~ mask pd_bits) pg_id y s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2; y \<in> set ys\<rbrakk> \<Longrightarrow> \<lbrace>pd_super_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>rv. pd_super_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace>
 2. \<And>y. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2; y \<in> set ys\<rbrakk> \<Longrightarrow> \<lbrace>pd_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>rv. pd_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>y\<in>set ys. is_aligned y 2; ptr \<notin> set ys; is_aligned ptr 2; y \<in> set ys\<rbrakk> \<Longrightarrow> \<lbrace>pd_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace> store_pde ptr InvalidPDE \<lbrace>\<lambda>rv. pd_section_relation (y && ~~ mask pd_bits) pg_id y\<rbrace> proof (prove)
goal:
No subgoals!