theory Machine_C

lemma cleanCaches_PoU_ccorres:
  "ccorres dc xfdc \<top> UNIV []
           (doMachineOp cleanCaches_PoU)
           (Call cleanCaches_PoU_'proc)" apply cinit' apply (simp add: cleanCaches_PoU_def doMachineOp_bind empty_fail_cond
                   empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: clean_D_PoU_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: invalidate_I_PoU_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply wp+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) UNIV [] (doMachineOp cleanCaches_PoU) (Call cleanCaches_PoU_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q8 ?Q'8 [SKIP] (doMachineOp cleanCaches_PoU) (CALL dsb_'proc();;
(CALL clean_D_PoU_'proc();;
(CALL dsb_'proc();;
(CALL invalidate_I_PoU_'proc();;
CALL dsb_'proc()))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q8 s \<and> s' \<in> ?Q'8 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q8 ?Q'8 [SKIP] (do rv <- doMachineOp dsb;
rv <- doMachineOp clean_D_PoU;
rv <- doMachineOp dsb;
rv <- doMachineOp invalidate_I_PoU;
doMachineOp dsb
od) (CALL dsb_'proc();;
(CALL clean_D_PoU_'proc();;
(CALL dsb_'proc();;
(CALL invalidate_I_PoU_'proc();;
CALL dsb_'proc()))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q8 s \<and> s' \<in> ?Q'8 proof (prove)
goal (3 subgoals):
 1. \<And>rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q17 rv) (?Q'17 rv xfdca) [SKIP] (do rv <- doMachineOp clean_D_PoU;
rv <- doMachineOp dsb;
rv <- doMachineOp invalidate_I_PoU;
doMachineOp dsb
od) (CALL clean_D_PoU_'proc();;
(CALL dsb_'proc();;
(CALL invalidate_I_PoU_'proc();;
CALL dsb_'proc())))
 2. \<lbrace>?R17\<rbrace> doMachineOp dsb \<lbrace>?Q17\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'17 rv (xfdc t)} proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q38 rv xfdca rva) (?Q'38 rv xfdca rva xfdcb) [SKIP] (do rv <- doMachineOp dsb;
rv <- doMachineOp invalidate_I_PoU;
doMachineOp dsb
od) (CALL dsb_'proc();;
(CALL invalidate_I_PoU_'proc();;
CALL dsb_'proc()))
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R40 rv\<rbrace> doMachineOp clean_D_PoU \<lbrace>?Q38 rv xfdc\<rbrace>
 3. \<lbrace>?R17\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R40 rv\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'38 rv (xfdc t) rva (xfdc ta)}} proof (prove)
goal (5 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q62 rv xfdca rva xfdcb rvb) (?Q'62 rv xfdca rva xfdcb rvb xfdcc) [SKIP] (do rv <- doMachineOp invalidate_I_PoU;
doMachineOp dsb
od) (CALL invalidate_I_PoU_'proc();;
CALL dsb_'proc())
 2. \<And>rv xfdca rva xfdc. \<lbrakk>dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R64 rv xfdca rva\<rbrace> doMachineOp dsb \<lbrace>?Q62 rv xfdca rva xfdc\<rbrace>
 3. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R40 rv\<rbrace> doMachineOp clean_D_PoU \<lbrace>\<lambda>rva. (\<lambda>_. True) and ?R64 rv xfdc rva\<rbrace>
 4. \<lbrace>?R17\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R40 rv\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'62 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb)}}} proof (prove)
goal (6 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc rvc xfdcd. \<lbrakk>dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc xfdcd\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q87 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'87 rv xfdca rva xfdcb rvb xfdcc rvc xfdcd) [SKIP] (doMachineOp dsb) (CALL dsb_'proc())
 2. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R89 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp invalidate_I_PoU \<lbrace>?Q87 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 3. \<And>rv xfdca rva xfdc. \<lbrakk>dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R64 rv xfdca rva\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?R89 rv xfdca rva xfdc rvb\<rbrace>
 4. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R40 rv\<rbrace> doMachineOp clean_D_PoU \<lbrace>\<lambda>rva. (\<lambda>_. True) and ?R64 rv xfdc rva\<rbrace>
 5. \<lbrace>?R17\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R40 rv\<rbrace>
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tc rvc. dc rvc (xfdc tc) \<longrightarrow> s'\<lparr>globals := globals tc\<rparr> \<in> ?Q'87 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb) rvc (xfdc tc)}}}} proof (prove)
goal (5 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R89 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp invalidate_I_PoU \<lbrace>\<lambda>rvc _. True\<rbrace>
 2. \<And>rv xfdca rva xfdc. \<lbrakk>dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R64 rv xfdca rva\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?R89 rv xfdca rva xfdc rvb\<rbrace>
 3. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R40 rv\<rbrace> doMachineOp clean_D_PoU \<lbrace>\<lambda>rva. (\<lambda>_. True) and ?R64 rv xfdc rva\<rbrace>
 4. \<lbrace>?R17\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R40 rv\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV}}}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV}}}}} proof (prove)
goal:
No subgoals!