theory Invariants_AI

lemma only_idle_lift:
  assumes T: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
  assumes s: "\<And>P t. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>"
  assumes i: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
  shows "\<lbrace>only_idle\<rbrace> f \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: only_idle_def) apply (rule hoare_vcg_all_lift) apply (subst imp_conv_disj not_pred_tcb)+ apply (rule hoare_vcg_disj_lift)+ apply (simp add: tcb_at_typ) apply (rule T) apply (rule s) apply (rule hoare_lift_Pf [where f="idle_thread"]) apply (rule assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> f \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>\<lambda>s. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>\<lambda>s. (\<not> tcb_at t s \<or> st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t s) \<or> t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. (\<not> tcb_at t s \<or> st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t s) \<or> t = idle_thread s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>\<lambda>s. \<not> tcb_at t s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> tcb_at t s\<rbrace>
 2. \<And>t. \<lbrace>st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace>
 3. \<And>t. \<lbrace>\<lambda>s. t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = idle_thread s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>\<lambda>s. \<not> typ_at ATCB t s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at ATCB t s\<rbrace>
 2. \<And>t. \<lbrace>st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace>
 3. \<And>t. \<lbrace>\<lambda>s. t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = idle_thread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>a. a \<noteq> IdleThreadState) t\<rbrace>
 2. \<And>t. \<lbrace>\<lambda>s. t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = idle_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>\<lambda>s. t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = idle_thread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t x. \<lbrace>\<lambda>s. t = x\<rbrace> f \<lbrace>\<lambda>_ a. t = x\<rbrace>
 2. \<And>t P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!