theory Arch_IF

lemma get_object_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag \<top>\<top> \<top> (get_object ptr)" unfolding get_object_def apply (rule equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp) apply (rule gets_kheap_revrv') apply (simp, simp) apply (rule equiv_valid_2_bind) apply (rule return_ev2) apply (simp) apply (rule assert_ev2) apply (simp) apply (wpsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) (get_object ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) (do kh <- gets kheap;
assert (kh ptr \<noteq> None);
return $ the $ kh ptr
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W (\<lambda>_. True) (gets kheap)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (do assert (rv ptr \<noteq> None);
return $ the $ rv ptr
od) (do assert (rv' ptr \<noteq> None);
return $ the $ rv' ptr
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W ?P4 (gets kheap)
 2. \<And>s. True \<Longrightarrow> ?P4 s
 3. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (do assert (rv ptr \<noteq> None);
return $ the $ rv ptr
od) (do assert (rv' ptr \<noteq> None);
return $ the $ rv' ptr
od)
 4. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (do assert (rv ptr \<noteq> None);
return $ the $ rv ptr
od) (do assert (rv' ptr \<noteq> None);
return $ the $ rv' ptr
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (do y <- assert (\<exists>y. rv ptr = Some y);
return (the (rv ptr))
od) (do y <- assert (\<exists>y. rv' ptr = Some y);
return (the (rv' ptr))
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>?Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>equiv_for (aag_can_read aag) id rv rv'; ?R'8 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q8 rv rv' rva) (?Q'8 rv rv' rv'a) (return (the (rv ptr))) (return (the (rv' ptr)))
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'8 rv rv') (?P'11 rv) (?P'11 rv') (assert (\<exists>y. rv ptr = Some y)) (assert (\<exists>y. rv' ptr = Some y))
 3. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv\<rbrace> assert (\<exists>y. rv ptr = Some y) \<lbrace>?Q8 rv rv'\<rbrace>
 4. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv'\<rbrace> assert (\<exists>y. rv' ptr = Some y) \<lbrace>?Q'8 rv rv'\<rbrace>
 5. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>\<lambda>rv s. ?P'11 rv s \<and> ?S'12 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a s t. \<lbrakk>equiv_for (aag_can_read aag) id rv rv'; ?R'8 rv rv' rva rv'a; ?Q8 rv rv' rva s; ?Q'8 rv rv' rv'a t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> True
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'8 rv rv') (?P'11 rv) (?P'11 rv') (assert (\<exists>y. rv ptr = Some y)) (assert (\<exists>y. rv' ptr = Some y))
 3. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv\<rbrace> assert (\<exists>y. rv ptr = Some y) \<lbrace>?Q8 rv rv'\<rbrace>
 4. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv'\<rbrace> assert (\<exists>y. rv' ptr = Some y) \<lbrace>?Q'8 rv rv'\<rbrace>
 5. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>\<lambda>rv s. ?P'11 rv s \<and> ?S'12 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'8 rv rv') (?P'11 rv) (?P'11 rv') (assert (\<exists>y. rv ptr = Some y)) (assert (\<exists>y. rv' ptr = Some y))
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv\<rbrace> assert (\<exists>y. rv ptr = Some y) \<lbrace>?Q8 rv rv'\<rbrace>
 3. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv'\<rbrace> assert (\<exists>y. rv' ptr = Some y) \<lbrace>?Q'8 rv rv'\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>\<lambda>rv s. ?P'11 rv s \<and> ?S'12 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> ?R'8 rv rv' () ()
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv\<rbrace> assert (\<exists>y. rv ptr = Some y) \<lbrace>?Q8 rv rv'\<rbrace>
 3. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv'\<rbrace> assert (\<exists>y. rv' ptr = Some y) \<lbrace>?Q'8 rv rv'\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>\<lambda>rv s. ?P'11 rv s \<and> ?S'12 rv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv\<rbrace> assert (\<exists>y. rv ptr = Some y) \<lbrace>?Q8 rv rv'\<rbrace>
 2. \<And>rv rv'. equiv_for (aag_can_read aag) id rv rv' \<Longrightarrow> \<lbrace>?S'12 rv'\<rbrace> assert (\<exists>y. rv' ptr = Some y) \<lbrace>?Q'8 rv rv'\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> gets kheap \<lbrace>\<lambda>rv s. ?P'11 rv s \<and> ?S'12 rv s\<rbrace> proof (prove)
goal:
No subgoals!