theory Finalise_IF

lemma set_simple_ko_reads_respects:
  "reads_respects aag l \<top> (set_simple_ko f ptr ep)" unfolding set_simple_ko_def apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp) apply (rule get_object_revrv) apply (simp, simp) apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (subst equiv_valid_def2[symmetric]) apply (rule set_object_reads_respects) apply (rule assert_ev2) apply (simp) apply (rule assert_inv)+ apply (rule assert_ev2) apply (simp) apply (rule assert_inv)+ apply (simp) apply (wp get_object_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_simple_ko f ptr ep) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. partial_inv f obj = Some y);
set_object ptr (f ep)
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W (\<lambda>_. True) (get_object ptr)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q rv) (?Q rv') (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
y <- assert (\<exists>y. partial_inv f rv = Some y);
set_object ptr (f ep)
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
y <- assert (\<exists>y. partial_inv f rv' = Some y);
set_object ptr (f ep)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W ?P4 (get_object ptr)
 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) (=) (?Q rv) (?Q rv') (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
y <- assert (\<exists>y. partial_inv f rv = Some y);
set_object ptr (f ep)
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
y <- assert (\<exists>y. partial_inv f rv' = Some y);
set_object ptr (f ep)
od)
 4. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q rv) (?Q rv') (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
y <- assert (\<exists>y. partial_inv f rv = Some y);
set_object ptr (f ep)
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
y <- assert (\<exists>y. partial_inv f rv' = Some y);
set_object ptr (f ep)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q rv) (?Q rv') (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
y <- assert (\<exists>y. partial_inv f rv = Some y);
set_object ptr (f ep)
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
y <- assert (\<exists>y. partial_inv f rv' = Some y);
set_object ptr (f ep)
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q8 rv rv' rva) (?Q'8 rv rv' rv'a) (do y <- assert (\<exists>y. partial_inv f rv = Some y);
set_object ptr (f ep)
od) (do y <- assert (\<exists>y. partial_inv f rv' = Some y);
set_object ptr (f ep)
od)
 2. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 3. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>?Q8 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>?Q'8 rv rv'\<rbrace>
 5. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q14 rv rv' rva rv'a rvb) (?Q'14 rv rv' rva rv'a rv'b) (set_object ptr (f ep)) (set_object ptr (f ep))
 2. \<And>rv rv' rva rv'a. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P16 rv rv' rva) (?P'18 rv rv' rv'a) (assert (\<exists>y. partial_inv f rv = Some y)) (assert (\<exists>y. partial_inv f rv' = Some y))
 3. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S17 rv rv' rva\<rbrace> assert (\<exists>y. partial_inv f rv = Some y) \<lbrace>?Q14 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S'19 rv rv' rv'a\<rbrace> assert (\<exists>y. partial_inv f rv' = Some y) \<lbrace>?Q'14 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 6. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> ?S17 rv rv' rva s\<rbrace>
 7. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> ?S'19 rv rv' rv'a s\<rbrace>
 8. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>a. ?Q'23 rv rv' rva rv'a) (set_object ptr (f ep))
 2. \<And>rv rv' rva rv'a. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P16 rv rv' rva) (?P'18 rv rv' rv'a) (assert (\<exists>y. partial_inv f rv = Some y)) (assert (\<exists>y. partial_inv f rv' = Some y))
 3. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S17 rv rv' rva\<rbrace> assert (\<exists>y. partial_inv f rv = Some y) \<lbrace>\<lambda>rvb a. ?Q'23 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S'19 rv rv' rv'a\<rbrace> assert (\<exists>y. partial_inv f rv' = Some y) \<lbrace>\<lambda>rv'b a. ?Q'23 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 6. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> ?S17 rv rv' rva s\<rbrace>
 7. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> ?S'19 rv rv' rv'a s\<rbrace>
 8. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P16 rv rv' rva) (?P'18 rv rv' rv'a) (assert (\<exists>y. partial_inv f rv = Some y)) (assert (\<exists>y. partial_inv f rv' = Some y))
 2. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S17 rv rv' rva\<rbrace> assert (\<exists>y. partial_inv f rv = Some y) \<lbrace>\<lambda>rvb a. True\<rbrace>
 3. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S'19 rv rv' rv'a\<rbrace> assert (\<exists>y. partial_inv f rv' = Some y) \<lbrace>\<lambda>rv'b a. True\<rbrace>
 4. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 5. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> ?S17 rv rv' rva s\<rbrace>
 6. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> ?S'19 rv rv' rv'a s\<rbrace>
 7. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a. True \<Longrightarrow> True
 2. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S17 rv rv' rva\<rbrace> assert (\<exists>y. partial_inv f rv = Some y) \<lbrace>\<lambda>rvb a. True\<rbrace>
 3. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S'19 rv rv' rv'a\<rbrace> assert (\<exists>y. partial_inv f rv' = Some y) \<lbrace>\<lambda>rv'b a. True\<rbrace>
 4. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 5. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> ?S17 rv rv' rva s\<rbrace>
 6. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> ?S'19 rv rv' rv'a s\<rbrace>
 7. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S17 rv rv' rva\<rbrace> assert (\<exists>y. partial_inv f rv = Some y) \<lbrace>\<lambda>rvb a. True\<rbrace>
 2. \<And>rv rv' rva rv'a. True \<Longrightarrow> \<lbrace>?S'19 rv rv' rv'a\<rbrace> assert (\<exists>y. partial_inv f rv' = Some y) \<lbrace>\<lambda>rv'b a. True\<rbrace>
 3. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 4. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> ?S17 rv rv' rva s\<rbrace>
 5. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> ?S'19 rv rv' rv'a s\<rbrace>
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P'12 rv) (?P'12 rv') (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) (assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN))
 2. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> True\<rbrace>
 3. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> True\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. True
 2. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> True\<rbrace>
 3. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> True\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrace>?S'13 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva s. ?P16 rv rv' rva s \<and> True\<rbrace>
 2. \<And>rv rv'. \<lbrace>?S'13 rv'\<rbrace> assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN) \<lbrace>\<lambda>rv'a s. ?P'18 rv rv' rv'a s \<and> True\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?S'13 rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?P'35 rv s \<and> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>\<lambda>rv s. ?P'12 rv s \<and> ?P'35 rv s\<rbrace> proof (prove)
goal:
No subgoals!