theory DetSchedAux_AI

lemma typ_at_pred_tcb_at_lift:
  assumes typ_lift: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>r s. P (typ_at T p s)\<rbrace>"
  assumes pred_lift: "\<And>P. \<lbrace>pred_tcb_at proj P t\<rbrace> f \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<not> pred_tcb_at proj P t s\<rbrace> f \<lbrace>\<lambda>r s. \<not> pred_tcb_at proj P t s\<rbrace>" apply (simp add: valid_def obj_at_def pred_tcb_at_def) apply clarsimp apply (case_tac "kheap s t") apply (cut_tac P="\<lambda>x. \<not> x" and p=t and T="ATCB" in typ_lift) apply (simp add: valid_def obj_at_def) apply force apply (cut_tac P="\<lambda>x. x" and p=t and T="a_type aa" in typ_lift) apply (cut_tac P="\<lambda>t. \<not> P t" in pred_lift) apply (simp add: valid_def obj_at_def pred_tcb_at_def) apply (drule_tac x=s in spec) apply simp apply (drule_tac x="(a,b)" in bspec) apply simp apply simp apply (subgoal_tac "a_type aa = ATCB") apply (erule a_type_ATCBE) apply simp apply force apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at proj P t s\<rbrace> f \<lbrace>\<lambda>r s. \<not> pred_tcb_at proj P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<forall>ko. kheap s' t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = None\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = None; \<lbrace>\<lambda>s. \<not> typ_at ATCB t s\<rbrace> f \<lbrace>\<lambda>r s. \<not> typ_at ATCB t s\<rbrace>\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = None; \<forall>s. (\<forall>ko. kheap s t = Some ko \<longrightarrow> a_type ko \<noteq> ATCB) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<forall>ko. kheap s' t = Some ko \<longrightarrow> a_type ko \<noteq> ATCB)\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<lbrace>typ_at (a_type aa) t\<rbrace> f \<lbrace>\<lambda>r. typ_at (a_type aa) t\<rbrace>\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>ko. kheap s t = Some ko \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb))); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<lbrace>typ_at (a_type aa) t\<rbrace> f \<lbrace>\<lambda>r. typ_at (a_type aa) t\<rbrace>; \<lbrace>pred_tcb_at proj (\<lambda>t. \<not> P t) t\<rbrace> f \<lbrace>\<lambda>_. pred_tcb_at proj (\<lambda>t. \<not> P t) t\<rbrace>\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> a_type ko = a_type aa) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> a_type ko = a_type aa); \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb))))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); (\<exists>ko. kheap s t = Some ko \<and> a_type ko = a_type aa) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> a_type ko = a_type aa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); \<forall>(r, s')\<in>fst (f s). \<exists>ko. kheap s' t = Some ko \<and> a_type ko = a_type aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb))))\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (f s)
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); case (a, b) of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> a_type ko = a_type aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); case (a, b) of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> a_type ko = a_type aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa; a_type aa = ATCB\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa\<rbrakk> \<Longrightarrow> a_type aa = ATCB proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb aa tcba. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa; aa = TCB tcba\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa\<rbrakk> \<Longrightarrow> a_type aa = ATCB proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb aa tcba. \<lbrakk>\<not> P (proj (tcb_to_itcb tcba)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some (TCB tcba); \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); aa = TCB tcba\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa\<rbrakk> \<Longrightarrow> a_type aa = ATCB proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb aa. \<lbrakk>\<forall>tcb. aa = TCB tcb \<longrightarrow> \<not> P (proj (tcb_to_itcb tcb)); (a, b) \<in> fst (f s); kheap b t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); kheap s t = Some aa; \<forall>s. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<exists>ko. kheap s' t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb)))); ATCB = a_type aa\<rbrakk> \<Longrightarrow> a_type aa = ATCB proof (prove)
goal:
No subgoals!