theory Invariants_H

lemma refs_of_live':
  "refs_of' ko \<noteq> {} \<Longrightarrow> live' ko" apply (cases ko, simp_all) apply clarsimp apply (rename_tac notification) apply (case_tac "ntfnObj notification"; simp) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refs_of' ko \<noteq> {} \<Longrightarrow> live' ko proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>ep_q_refs_of' x1 \<noteq> {}; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> x1 \<noteq> Structures_H.endpoint.IdleEP
 2. \<And>x2. \<lbrakk>ntfn_q_refs_of' (ntfnObj x2) = {} \<longrightarrow> ntfn_bound_refs' (ntfnBoundTCB x2) \<noteq> {}; ko = KONotification x2\<rbrakk> \<Longrightarrow> (\<exists>y. ntfnBoundTCB x2 = Some y) \<or> (\<exists>ts. ntfnObj x2 = Structures_H.ntfn.WaitingNtfn ts)
 3. \<And>x6. \<lbrakk>tcb_st_refs_of' (tcbState x6) = {} \<longrightarrow> tcb_bound_refs' (tcbBoundNotification x6) \<noteq> {}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>y. tcbBoundNotification x6 = Some y) \<or> tcbState x6 \<noteq> Structures_H.thread_state.Inactive \<and> tcbState x6 \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued x6 proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>ntfn_q_refs_of' (ntfnObj x2) = {} \<longrightarrow> ntfn_bound_refs' (ntfnBoundTCB x2) \<noteq> {}; ko = KONotification x2\<rbrakk> \<Longrightarrow> (\<exists>y. ntfnBoundTCB x2 = Some y) \<or> (\<exists>ts. ntfnObj x2 = Structures_H.ntfn.WaitingNtfn ts)
 2. \<And>x6. \<lbrakk>tcb_st_refs_of' (tcbState x6) = {} \<longrightarrow> tcb_bound_refs' (tcbBoundNotification x6) \<noteq> {}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>y. tcbBoundNotification x6 = Some y) \<or> tcbState x6 \<noteq> Structures_H.thread_state.Inactive \<and> tcbState x6 \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued x6 proof (prove)
goal (2 subgoals):
 1. \<And>notification. \<lbrakk>ntfn_q_refs_of' (ntfnObj notification) = {} \<longrightarrow> ntfn_bound_refs' (ntfnBoundTCB notification) \<noteq> {}; ko = KONotification notification\<rbrakk> \<Longrightarrow> (\<exists>y. ntfnBoundTCB notification = Some y) \<or> (\<exists>ts. ntfnObj notification = Structures_H.ntfn.WaitingNtfn ts)
 2. \<And>x6. \<lbrakk>tcb_st_refs_of' (tcbState x6) = {} \<longrightarrow> tcb_bound_refs' (tcbBoundNotification x6) \<noteq> {}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>y. tcbBoundNotification x6 = Some y) \<or> tcbState x6 \<noteq> Structures_H.thread_state.Inactive \<and> tcbState x6 \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued x6 proof (prove)
goal (3 subgoals):
 1. \<And>notification. \<lbrakk>ntfn_bound_refs' (ntfnBoundTCB notification) \<noteq> {}; ko = KONotification notification; ntfnObj notification = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> \<exists>y. ntfnBoundTCB notification = Some y
 2. \<And>notification x2. \<lbrakk>ntfn_bound_refs' (ntfnBoundTCB notification) \<noteq> {}; ko = KONotification notification; ntfnObj notification = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> \<exists>y. ntfnBoundTCB notification = Some y
 3. \<And>x6. \<lbrakk>tcb_st_refs_of' (tcbState x6) = {} \<longrightarrow> tcb_bound_refs' (tcbBoundNotification x6) \<noteq> {}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>y. tcbBoundNotification x6 = Some y) \<or> tcbState x6 \<noteq> Structures_H.thread_state.Inactive \<and> tcbState x6 \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued x6 proof (prove)
goal:
No subgoals!