theory Finalise_IF

lemma get_simple_ko_revrv:
  "inj C \<Longrightarrow> reads_equiv_valid_rv_inv R aag (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t
                                                            \<and> R s t \<and> P s \<and> P t
                                                            \<and> ko_at (C obj) ptr s
                                                            \<and> ko_at (C obj') ptr t)
                                      P (get_simple_ko C ptr)" apply (simp add: get_simple_ko_def) apply (rule_tac Q="\<lambda> rv. ko_at rv ptr and P" in equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp[OF equiv_valid_rv_trivial]) apply wpsimp+ apply (clarsimp simp add: assert_def fail_ev2_l fail_ev2_r
                   simp del: imp_disjL split: option.split) apply (rule return_ev2) apply (auto simp: proj_inj)[1] apply (rule hoare_strengthen_post[OF get_object_sp]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj C \<Longrightarrow> reads_equiv_valid_rv_inv R aag (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) P (get_simple_ko C ptr) proof (prove)
goal (1 subgoal):
 1. inj C \<Longrightarrow> reads_equiv_valid_rv_inv R aag (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) P (do kobj <- get_object ptr;
y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv C kobj of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od) proof (prove)
goal (3 subgoals):
 1. inj C \<Longrightarrow> reads_equiv_valid_rv_inv R aag ?W4 P (get_object ptr)
 2. \<And>rv rv'. \<lbrakk>inj C; ?W4 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) R R (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) (ko_at rv ptr and P) (ko_at rv' ptr and P) (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
case partial_inv C rv of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
case partial_inv C rv' of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od)
 3. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. \<lbrakk>inj C; P s\<rbrakk> \<Longrightarrow> True
 3. \<And>rv rv'. \<lbrakk>inj C; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) R R (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) (ko_at rv ptr and P) (ko_at rv' ptr and P) (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
case partial_inv C rv of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
case partial_inv C rv' of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od)
 4. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. inj C \<Longrightarrow> equiv_valid_2 (reads_equiv aag) R R (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) (ko_at rv ptr and P) (ko_at rv' ptr and P) (do y <- assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN);
case partial_inv C rv of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od) (do y <- assert (a_type rv' = AEndpoint \<or> a_type rv' = ANTFN);
case partial_inv C rv' of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2
od)
 2. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' x2 x2a. \<lbrakk>inj C; partial_inv C rv = Some x2; partial_inv C rv' = Some x2a; a_type rv = AEndpoint \<or> a_type rv = ANTFN; a_type rv' = AEndpoint \<or> a_type rv' = ANTFN\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) R R (\<lambda>obj obj'. \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C obj) ptr s \<and> ko_at (C obj') ptr t) (ko_at rv ptr and P) (ko_at rv' ptr and P) (return x2) (return x2a)
 2. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' x2 x2a s t. \<lbrakk>inj C; partial_inv C rv = Some x2; partial_inv C rv' = Some x2a; a_type rv = AEndpoint \<or> a_type rv = ANTFN; a_type rv' = AEndpoint \<or> a_type rv' = ANTFN; (ko_at rv ptr and P) s; (ko_at rv' ptr and P) t; reads_equiv aag s t; R s t\<rbrakk> \<Longrightarrow> \<exists>s t. reads_equiv aag s t \<and> R s t \<and> P s \<and> P t \<and> ko_at (C x2) ptr s \<and> ko_at (C x2a) ptr t
 2. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. inj C \<Longrightarrow> \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>rv. ko_at rv ptr and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>inj C; (P and ko_at rv ptr) s\<rbrakk> \<Longrightarrow> (ko_at rv ptr and P) s proof (prove)
goal:
No subgoals!