theory KHeap_DR

lemma dcorres_revoke_cap_simple_helper:
  "\<lbrakk> dcorres r P P'
    (do descendants \<leftarrow> gets $ KHeap_D.descendants_of victim;
      assert (finite descendants);
      non_null \<leftarrow> gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
      non_null_descendants \<leftarrow> return (descendants \<inter> non_null);
      if non_null_descendants \<noteq> {}
      then do a \<leftarrow> select non_null_descendants;
              y \<leftarrow> delete_cap_simple a;
              revoke_cap_simple victim
           od
      else return ()
     od)
     h \<rbrakk> \<Longrightarrow> dcorres r P P' (revoke_cap_simple victim) h" apply (rule corres_dummy_get_pl) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:corres_underlying_def) apply (rename_tac s' a b) apply (subst revoke_cap_simple.simps) apply (erule_tac x=s' in allE, simp) apply (clarsimp cong: if_cong) apply (drule_tac x="(a,b)" in bspec) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (do descendants <- gets $ KHeap_D.descendants_of victim;
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) h \<Longrightarrow> dcorres r P P' (revoke_cap_simple victim) h proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (do descendants <- gets $ KHeap_D.descendants_of victim;
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) h \<Longrightarrow> dcorres r P P' (do s <- get;
revoke_cap_simple victim
od) h proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>dcorres r P P' (do descendants <- gets $ KHeap_D.descendants_of victim;
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) h; P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') (revoke_cap_simple victim) h proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>\<forall>b. P (transform b) \<and> P' b \<longrightarrow> (\<forall>x\<in>fst (h b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform b)). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'); P (transform s'); P' s'; (a, b) \<in> fst (h s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (revoke_cap_simple victim (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>\<forall>b. P (transform b) \<and> P' b \<longrightarrow> (\<forall>x\<in>fst (h b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform b)). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'); P (transform s'); P' s'; (a, b) \<in> fst (h s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (revoke_cap_simple victim (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>\<forall>b. P (transform b) \<and> P' b \<longrightarrow> (\<forall>x\<in>fst (h b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform b)). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'); P (transform s'); P' s'; (a, b) \<in> fst (h s')\<rbrakk> \<Longrightarrow> \<exists>(ra, t)\<in>fst ((do descendants <- gets $ KHeap_D.descendants_of victim;
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). transform b = t \<and> r () a proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>P (transform s'); P' s'; (a, b) \<in> fst (h s'); \<forall>(r', t')\<in>fst (h s'). \<exists>(ra, t)\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). transform t' = t \<and> r () r'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>P (transform s'); P' s'; (a, b) \<in> fst (h s'); \<forall>x\<in>fst (h s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>P (transform s'); P' s'; (a, b) \<in> fst (h s')\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (h s')
 2. \<And>s' a b. \<lbrakk>P (transform s'); P' s'; (a, b) \<in> fst (h s'); case (a, b) of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>P (transform s'); P' s'; (a, b) \<in> fst (h s'); case (a, b) of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform t' = t \<and> r () r'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do descendants <- gets (KHeap_D.descendants_of victim);
y <- assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
if descendants \<inter> non_null \<noteq> {} then do a <- select (descendants \<inter> non_null);
y <- delete_cap_simple a;
revoke_cap_simple victim
od else return ()
od) (transform s')). case x of (ra, t) \<Rightarrow> transform b = t \<and> r () a proof (prove)
goal:
No subgoals!