theory PageTableDuplicates

lemma activate_sch_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
     activateThread \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: activateThread_def getCurThread_def
             cong: if_cong Structures_H.thread_state.case_cong) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_seq_ext[where B="\<lambda>st s.  (runnable' or idle') st
    \<and> vs_valid_duplicates' (ksPSpace s)"]) apply (rule hoare_pre) apply (wp | wpc | simp add: setThreadState_runnable_simp)+ apply (clarsimp simp: ct_in_state'_def cur_tcb'_def pred_tcb_at'
                 elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace> activateThread \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace> do thread <- gets ksCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>(\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> do state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread state. \<lbrace>\<lambda>s. (runnable' or idle') state \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace> case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>thread. \<lbrace>(\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> getThreadState thread \<lbrace>\<lambda>st s. (runnable' or idle') st \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread state. \<lbrace>?Q18 thread state\<rbrace> case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>thread state s. (runnable' or idle') state \<and> vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q18 thread state s
 3. \<And>thread. \<lbrace>(\<lambda>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> getThreadState thread \<lbrace>\<lambda>st s. (runnable' or idle') st \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state' activatable' s \<and> vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> st_tcb_at' activatable' (ksCurThread s) s proof (prove)
goal:
No subgoals!