theory Invariants_AI

lemma refs_of_live:
  "refs_of ko \<noteq> {} \<Longrightarrow> live ko" apply (cases ko, simp_all) apply (rename_tac tcb_ext) apply (case_tac "tcb_state tcb_ext", simp_all add: live_def) apply (fastforce simp: tcb_bound_refs_def)+ apply (rename_tac notification) apply (case_tac "ntfn_obj notification", simp_all) apply (fastforce simp: ntfn_bound_refs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refs_of ko \<noteq> {} \<Longrightarrow> live ko proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>tcb_st_refs_of (tcb_state x2) = {} \<longrightarrow> tcb_bound_refs (tcb_bound_notification x2) \<noteq> {}; ko = TCB x2\<rbrakk> \<Longrightarrow> live (TCB x2)
 2. \<And>x3. \<lbrakk>ep_q_refs_of x3 \<noteq> {}; ko = Endpoint x3\<rbrakk> \<Longrightarrow> live (Endpoint x3)
 3. \<And>x4. \<lbrakk>ntfn_q_refs_of (ntfn_obj x4) = {} \<longrightarrow> ntfn_bound_refs (ntfn_bound_tcb x4) \<noteq> {}; ko = Notification x4\<rbrakk> \<Longrightarrow> live (Notification x4) proof (prove)
goal (3 subgoals):
 1. \<And>tcb_ext. \<lbrakk>tcb_st_refs_of (tcb_state tcb_ext) = {} \<longrightarrow> tcb_bound_refs (tcb_bound_notification tcb_ext) \<noteq> {}; ko = TCB tcb_ext\<rbrakk> \<Longrightarrow> live (TCB tcb_ext)
 2. \<And>x3. \<lbrakk>ep_q_refs_of x3 \<noteq> {}; ko = Endpoint x3\<rbrakk> \<Longrightarrow> live (Endpoint x3)
 3. \<And>x4. \<lbrakk>ntfn_q_refs_of (ntfn_obj x4) = {} \<longrightarrow> ntfn_bound_refs (ntfn_bound_tcb x4) \<noteq> {}; ko = Notification x4\<rbrakk> \<Longrightarrow> live (Notification x4) proof (prove)
goal (4 subgoals):
 1. \<And>tcb_ext. \<lbrakk>tcb_bound_refs (tcb_bound_notification tcb_ext) \<noteq> {}; ko = TCB tcb_ext; inactive (tcb_state tcb_ext)\<rbrakk> \<Longrightarrow> (\<exists>y. tcb_bound_notification tcb_ext = Some y) \<or> hyp_live (TCB tcb_ext)
 2. \<And>tcb_ext. \<lbrakk>tcb_bound_refs (tcb_bound_notification tcb_ext) \<noteq> {}; ko = TCB tcb_ext; idle (tcb_state tcb_ext)\<rbrakk> \<Longrightarrow> (\<exists>y. tcb_bound_notification tcb_ext = Some y) \<or> hyp_live (TCB tcb_ext)
 3. \<And>x3. \<lbrakk>ep_q_refs_of x3 \<noteq> {}; ko = Endpoint x3\<rbrakk> \<Longrightarrow> x3 \<noteq> IdleEP
 4. \<And>x4. \<lbrakk>ntfn_q_refs_of (ntfn_obj x4) = {} \<longrightarrow> ntfn_bound_refs (ntfn_bound_tcb x4) \<noteq> {}; ko = Notification x4\<rbrakk> \<Longrightarrow> (\<exists>y. ntfn_bound_tcb x4 = Some y) \<or> (\<exists>ts. ntfn_obj x4 = WaitingNtfn ts) proof (prove)
goal (1 subgoal):
 1. \<And>x4. \<lbrakk>ntfn_q_refs_of (ntfn_obj x4) = {} \<longrightarrow> ntfn_bound_refs (ntfn_bound_tcb x4) \<noteq> {}; ko = Notification x4\<rbrakk> \<Longrightarrow> (\<exists>y. ntfn_bound_tcb x4 = Some y) \<or> (\<exists>ts. ntfn_obj x4 = WaitingNtfn ts) proof (prove)
goal (1 subgoal):
 1. \<And>notification. \<lbrakk>ntfn_q_refs_of (ntfn_obj notification) = {} \<longrightarrow> ntfn_bound_refs (ntfn_bound_tcb notification) \<noteq> {}; ko = Notification notification\<rbrakk> \<Longrightarrow> (\<exists>y. ntfn_bound_tcb notification = Some y) \<or> (\<exists>ts. ntfn_obj notification = WaitingNtfn ts) proof (prove)
goal (2 subgoals):
 1. \<And>notification. \<lbrakk>ntfn_bound_refs (ntfn_bound_tcb notification) \<noteq> {}; ko = Notification notification; ntfn_obj notification = IdleNtfn\<rbrakk> \<Longrightarrow> \<exists>y. ntfn_bound_tcb notification = Some y
 2. \<And>notification x3. \<lbrakk>ntfn_bound_refs (ntfn_bound_tcb notification) \<noteq> {}; ko = Notification notification; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<exists>y. ntfn_bound_tcb notification = Some y proof (prove)
goal:
No subgoals!