theory DetSchedSchedule_AI

lemma valid_blocked_except_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. st_tcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at Q t s\<rbrace>"
  assumes t: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T t s)\<rbrace>"
      and c: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
      and e: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
      and d: "\<And>P. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>"
    shows "\<lbrace>valid_blocked_except thread\<rbrace> f \<lbrace>\<lambda>rv. valid_blocked_except thread\<rbrace>" apply (rule hoare_pre) apply (wps c e d) apply (simp add: valid_blocked_except_def) apply (wp hoare_weak_lift_imp hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_conj_lift a) apply (rule hoare_convert_imp) apply (rule typ_at_st_tcb_at_lift) apply (wp a t)+ apply (simp add: valid_blocked_except_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked_except thread\<rbrace> f \<lbrace>\<lambda>rv. valid_blocked_except thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv. valid_blocked_except thread\<rbrace>
 2. \<And>s. valid_blocked_except thread s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. valid_blocked_except_2 thread (ready_queues prev_s) (kheap s') (scheduler_action prev_s) (cur_thread prev_s)\<rbrace>
 2. \<And>s. valid_blocked_except thread s \<Longrightarrow> ?P3 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. \<forall>t. t \<noteq> thread \<longrightarrow> not_queued t prev_s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s' \<longrightarrow> t \<noteq> cur_thread prev_s \<longrightarrow> scheduler_action prev_s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrace>
 2. \<And>s. valid_blocked_except thread s \<Longrightarrow> ?P3 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s t st. \<lbrace>?P21 prev_s t st\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread prev_s \<longrightarrow> scheduler_action prev_s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrace>
 2. \<And>s. valid_blocked_except thread s \<Longrightarrow> \<forall>x. x \<noteq> thread \<longrightarrow> not_queued x s \<longrightarrow> (\<forall>xa. ?P21 s x xa s) proof (prove)
goal (3 subgoals):
 1. \<And>prev_s t st. \<lbrace>\<lambda>s. \<not> ?P23 prev_s t st s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> st_tcb_at ((=) st) t s\<rbrace>
 2. \<And>prev_s t st. \<lbrace>?R23 prev_s t st\<rbrace> f \<lbrace>\<lambda>rv s. t \<noteq> cur_thread prev_s \<longrightarrow> scheduler_action prev_s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrace>
 3. \<And>s. valid_blocked_except thread s \<Longrightarrow> \<forall>x. x \<noteq> thread \<longrightarrow> not_queued x s \<longrightarrow> (\<forall>xa. ?P23 s x xa s \<longrightarrow> ?R23 s x xa s) proof (prove)
goal (4 subgoals):
 1. \<And>prev_s t st P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 2. \<And>prev_s t st P. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>
 3. \<And>prev_s t st. \<lbrace>?R23 prev_s t st\<rbrace> f \<lbrace>\<lambda>rv s. t \<noteq> cur_thread prev_s \<longrightarrow> scheduler_action prev_s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrace>
 4. \<And>s. valid_blocked_except thread s \<Longrightarrow> \<forall>x. x \<noteq> thread \<longrightarrow> not_queued x s \<longrightarrow> (\<forall>xa. st_tcb_at ((=) xa) x s \<longrightarrow> ?R23 s x xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked_except thread s \<Longrightarrow> \<forall>x. x \<noteq> thread \<longrightarrow> not_queued x s \<longrightarrow> (\<forall>xa. st_tcb_at ((=) xa) x s \<longrightarrow> x \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread x \<longrightarrow> xa \<noteq> Running \<and> xa \<noteq> Restart) proof (prove)
goal:
No subgoals!