theory Arch_IF

lemma get_object_revrv':
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
   (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv')
   \<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 add: equiv_for_def) apply (wpsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (\<lambda>_. True) (get_object ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (\<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>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?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>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?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 or aag_can_affect aag l) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?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 or aag_can_affect aag l) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?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 or aag_can_affect aag l) 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>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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> aag_can_read aag ptr \<longrightarrow> the (rv ptr) = the (rv' ptr)
 2. \<And>rv rv'. equiv_for (aag_can_read aag or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. aag_can_read aag ptr \<longrightarrow> the (rv ptr) = the (rv' ptr)) (?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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) id rv rv' \<Longrightarrow> aag_can_read aag ptr \<longrightarrow> the (rv ptr) = the (rv' ptr)
 2. \<And>rv rv'. equiv_for (aag_can_read aag or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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 or aag_can_affect aag l) 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!