theory Corres_C

lemma ccorres_noop:
  assumes nop: "\<forall>s. \<Gamma> \<turnstile> {s} c {t. t may_not_modify_globals s}"
  shows "ccorres_underlying rf_sr \<Gamma> dc xf arrel axf \<top> UNIV hs (return ()) c" apply (rule ccorres_from_vcg, rule allI, simp add: return_def) apply (rule HoarePartial.conseq_exploit_pre) apply simp apply (intro allI impI) apply (rule HoarePartial.conseq) apply (rule nop) apply clarsimp apply (erule iffD1 [OF rf_sr_upd, rotated -1]) apply (clarsimp simp: meq_def mex_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> dc xf arrel axf (\<lambda>_. True) UNIV hs (return ()) c proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} c {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>s\<in>{s. (\<sigma>, s) \<in> rf_sr}. \<Gamma>\<turnstile> ({s} \<inter> {s. (\<sigma>, s) \<in> rf_sr}) c {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>s. (\<sigma>, s) \<in> rf_sr \<longrightarrow> \<Gamma>\<turnstile> {s} c {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile> {s} c {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>Z. \<Gamma>\<turnstile> (?P'10 \<sigma> s Z) c (?Q'10 \<sigma> s Z),(?A'10 \<sigma> s Z)
 2. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> ?P'10 \<sigma> s Z \<and> ?Q'10 \<sigma> s Z \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> ?A'10 \<sigma> s Z \<subseteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {Z} \<and> {t. t may_not_modify_globals Z} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> {} \<subseteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; x may_not_modify_globals s\<rbrakk> \<Longrightarrow> (\<sigma>, x) \<in> rf_sr proof (prove)
goal (18 subgoals):
 1. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> t_hrs_' (globals s) = t_hrs_' (globals x)
 2. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksReadyQueues_' (globals s) = ksReadyQueues_' (globals x)
 3. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s) = ksReadyQueuesL1Bitmap_' (globals x)
 4. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s) = ksReadyQueuesL2Bitmap_' (globals x)
 5. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksSchedulerAction_' (globals s) = ksSchedulerAction_' (globals x)
 6. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksCurThread_' (globals s) = ksCurThread_' (globals x)
 7. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksIdleThread_' (globals s) = ksIdleThread_' (globals x)
 8. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted_' (globals x)
 9. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> ?intStateIRQNode_'17 \<sigma> s x (globals s) = ?intStateIRQNode_'17 \<sigma> s x (globals x)
 10. \<And>\<sigma> s x. x may_not_modify_globals s \<Longrightarrow> intStateIRQTable_' (globals s) = intStateIRQTable_' (globals x)
A total of 18 subgoals... proof (prove)
goal:
No subgoals!