theory VSpace_R

lemma pdeCheckIfMapped_corres:
  "corres (=) (pde_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (pde_check_if_mapped slot) (pdeCheckIfMapped slot)" apply (simp add: pde_check_if_mapped_def pdeCheckIfMapped_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_master_pde_corres', simplified]) apply (rule corres_return[where P="pde_at slot" and
                          P'="pspace_aligned' and pspace_distinct'", THEN iffD2]) apply (clarsimp simp: pte_relation'_def split: ) apply (case_tac pd, simp_all)[1] apply wp+ apply (clarsimp simp: pte_relation_aligned_def split: if_split_asm) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (pde_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (pde_check_if_mapped slot) (pdeCheckIfMapped slot) proof (prove)
goal (1 subgoal):
 1. corres (=) (pde_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (do pd <- get_master_pde slot;
return (pd \<noteq> ARM_A.InvalidPDE)
od) (do pd <- getObject slot;
return (pd \<noteq> ARM_H.InvalidPDE)
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do pd <- get_master_pde slot;
return (pd \<noteq> ARM_A.InvalidPDE)
od) (do pd <- getObject slot;
return (pd \<noteq> ARM_H.InvalidPDE)
od)
 2. \<And>s. pde_at slot s \<Longrightarrow> ?Q s
 3. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>pd pda. pde_relation' pd pda \<Longrightarrow> corres (=) (?R4 pd) (?R'4 pda) (return (pd \<noteq> ARM_A.InvalidPDE)) (return (pda \<noteq> ARM_H.InvalidPDE))
 2. \<lbrace>?Q4\<rbrace> get_master_pde slot \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>?R'4\<rbrace>
 4. \<And>s. pde_at slot s \<Longrightarrow> (pde_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>pd pda. pde_relation' pd pda \<Longrightarrow> (\<exists>s s'. pde_at slot s \<and> (pspace_aligned' and pspace_distinct') s' \<and> (s, s') \<in> state_relation) \<longrightarrow> (pd \<noteq> ARM_A.InvalidPDE) = (pda \<noteq> ARM_H.InvalidPDE)
 2. \<lbrace>?Q4\<rbrace> get_master_pde slot \<lbrace>\<lambda>pd. pde_at slot\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pda. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. pde_at slot s \<Longrightarrow> (pde_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>pd pda s s'. \<lbrakk>pde_relation' pd pda; pde_at slot s; pspace_aligned' s'; pspace_distinct' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pd = ARM_A.InvalidPDE) = (pda = ARM_H.InvalidPDE)
 2. \<lbrace>?Q4\<rbrace> get_master_pde slot \<lbrace>\<lambda>pd. pde_at slot\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pda. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. pde_at slot s \<Longrightarrow> (pde_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_master_pde slot \<lbrace>\<lambda>pd. pde_at slot\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pda. pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. pde_at slot s \<Longrightarrow> (pde_at slot and ?Q4) s
 4. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. pde_at slot s \<Longrightarrow> (pde_at slot and pde_at slot) s
 2. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct')) s proof (prove)
goal:
No subgoals!