theory SR_lemmas_C

lemma null_sched_epD:
  assumes om: "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'"
  shows "map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and>
         map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp'" using om apply - apply (rule conjI) apply (rule ext) apply (erule_tac x = x in map_option_comp_eqE ) apply simp apply (case_tac v, case_tac v') apply (clarsimp simp: tcb_null_sched_ptrs_def) apply (rule ext) apply (erule_tac x = x in map_option_comp_eqE ) apply simp apply (case_tac v, case_tac v') apply (clarsimp simp: tcb_null_sched_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
using this:
map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'

goal (1 subgoal):
 1. map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (1 subgoal):
 1. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (2 subgoals):
 1. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp'
 2. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (2 subgoals):
 1. \<And>x. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> (map_option tcbEPNext_C \<circ> mp) x = (map_option tcbEPNext_C \<circ> mp') x
 2. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>mp x = None; mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcbEPNext_C \<circ> mp) x = (map_option tcbEPNext_C \<circ> mp') x
 2. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcbEPNext_C \<circ> mp) x = (map_option tcbEPNext_C \<circ> mp') x
 3. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcbEPNext_C \<circ> mp) x = (map_option tcbEPNext_C \<circ> mp') x
 2. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (2 subgoals):
 1. \<And>x v v' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'; v = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; v' = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> (map_option tcbEPNext_C \<circ> mp) x = (map_option tcbEPNext_C \<circ> mp') x
 2. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (1 subgoal):
 1. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp' proof (prove)
goal (1 subgoal):
 1. \<And>x. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> (map_option tcbEPPrev_C \<circ> mp) x = (map_option tcbEPPrev_C \<circ> mp') x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>mp x = None; mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcbEPPrev_C \<circ> mp) x = (map_option tcbEPPrev_C \<circ> mp') x
 2. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcbEPPrev_C \<circ> mp) x = (map_option tcbEPPrev_C \<circ> mp') x proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcbEPPrev_C \<circ> mp) x = (map_option tcbEPPrev_C \<circ> mp') x proof (prove)
goal (1 subgoal):
 1. \<And>x v v' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'; v = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; v' = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> (map_option tcbEPPrev_C \<circ> mp) x = (map_option tcbEPPrev_C \<circ> mp') x proof (prove)
goal:
No subgoals!