theory Corres_C

lemma ccorres_noop_spec:
  assumes  s: "\<forall>s. \<Gamma> \<turnstile> (P s) c (R s), (A s)"
  and    nop: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/F\<^esub> {s} c {t. t may_not_modify_globals s}"
  shows "ccorres_underlying rf_sr \<Gamma> dc xf arrel axf \<top> {s. s \<in> P s} 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 allI) apply (rule HoarePartialProps.Merge_PostConj) apply (rule_tac P = "{s} \<inter> P s" in conseqPre) apply (rule_tac x = s in spec [OF s]) apply clarsimp apply (rule_tac x = s in spec [OF nop]) apply simp apply clarsimp apply clarsimp apply (erule iffD2 [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) {s. s \<in> P s} hs (return ()) c proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s \<in> P 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 \<in> P s. (\<sigma>, s) \<in> rf_sr}. \<Gamma>\<turnstile> ({s} \<inter> {s \<in> P s. (\<sigma>, s) \<in> rf_sr}) c {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>s. s \<in> P s \<and> (\<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. s \<in> P s \<and> (\<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. s \<in> P s \<and> (\<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. s \<in> P s \<and> (\<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 (2 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile> (?P'10 \<sigma> s Z) c (?Q'10 \<sigma> s Z),(?A'10 \<sigma> s Z)
 2. \<And>\<sigma> s. s \<in> P s \<and> (\<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 (5 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile> (?P'10 \<sigma> s Z) c (?Q15 \<sigma> s Z),(?A15 \<sigma> s Z)
 2. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma> s Z\<^esub> (?P'15 \<sigma> s Z) c (?R15 \<sigma> s Z),(?X15 \<sigma> s Z)
 3. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {} \<subseteq> ?G15 \<sigma> s Z
 4. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> ?P'10 \<sigma> s Z \<subseteq> ?P'15 \<sigma> s Z
 5. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> ?P'10 \<sigma> s Z \<and> ?Q15 \<sigma> s Z \<inter> ?R15 \<sigma> s Z \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> ?A15 \<sigma> s Z \<inter> ?X15 \<sigma> s Z \<subseteq> {}) proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile> (?P'20 \<sigma> s Z) c (?Q15 \<sigma> s Z),(?A15 \<sigma> s Z)
 2. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> ?P'20 \<sigma> s Z
 3. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma> s Z\<^esub> (?P'15 \<sigma> s Z) c (?R15 \<sigma> s Z),(?X15 \<sigma> s Z)
 4. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {} \<subseteq> ?G15 \<sigma> s Z
 5. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> ?P'15 \<sigma> s Z
 6. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> ?Q15 \<sigma> s Z \<inter> ?R15 \<sigma> s Z \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> ?A15 \<sigma> s Z \<inter> ?X15 \<sigma> s Z \<subseteq> {}) proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> P s
 2. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma> s Z\<^esub> (?P'15 \<sigma> s Z) c (?R15 \<sigma> s Z),(?X15 \<sigma> s Z)
 3. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {} \<subseteq> ?G15 \<sigma> s Z
 4. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> ?P'15 \<sigma> s Z
 5. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> R s \<inter> ?R15 \<sigma> s Z \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> A s \<inter> ?X15 \<sigma> s Z \<subseteq> {}) proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma> s Z\<^esub> (?P'15 \<sigma> s Z) c (?R15 \<sigma> s Z),(?X15 \<sigma> s Z)
 2. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {} \<subseteq> ?G15 \<sigma> s Z
 3. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> ?P'15 \<sigma> s Z
 4. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> R s \<inter> ?R15 \<sigma> s Z \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> A s \<inter> ?X15 \<sigma> s Z \<subseteq> {}) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {} \<subseteq> F
 2. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> {s}
 3. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> R s \<inter> {t. t may_not_modify_globals s} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> A s \<inter> {} \<subseteq> {}) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> s Z. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> {s} \<inter> P s \<subseteq> {s}
 2. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> R s \<inter> {t. t may_not_modify_globals s} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> A s \<inter> {} \<subseteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s. s \<in> P s \<and> (\<sigma>, s) \<in> rf_sr \<Longrightarrow> \<forall>sa. sa \<in> {s} \<longrightarrow> (\<exists>Z. sa \<in> {s} \<inter> P s \<and> R s \<inter> {t. t may_not_modify_globals s} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr} \<and> A s \<inter> {} \<subseteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s; (\<sigma>, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>, x) \<in> rf_sr proof (prove)
goal (18 subgoals):
 1. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> t_hrs_' (globals x) = t_hrs_' (globals s)
 2. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksReadyQueues_' (globals x) = ksReadyQueues_' (globals s)
 3. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals x) = ksReadyQueuesL1Bitmap_' (globals s)
 4. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals x) = ksReadyQueuesL2Bitmap_' (globals s)
 5. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) = ksSchedulerAction_' (globals s)
 6. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksCurThread_' (globals x) = ksCurThread_' (globals s)
 7. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksIdleThread_' (globals x) = ksIdleThread_' (globals s)
 8. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted_' (globals s)
 9. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> ?intStateIRQNode_'27 \<sigma> s x (globals x) = ?intStateIRQNode_'27 \<sigma> s x (globals s)
 10. \<And>\<sigma> s x. \<lbrakk>x \<in> R s; x may_not_modify_globals s; s \<in> P s\<rbrakk> \<Longrightarrow> intStateIRQTable_' (globals x) = intStateIRQTable_' (globals s)
A total of 18 subgoals... proof (prove)
goal:
No subgoals!