theory ADT_C

lemma csch_act_rel_to_H:
  "(\<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits) \<Longrightarrow>
   cscheduler_action_relation a p \<longleftrightarrow> cscheduler_action_to_H p = a" apply (cases a) apply (simp_all add: cscheduler_action_relation_def
                         cscheduler_action_to_H_def) apply safe apply (simp_all add: tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def
                          ctcb_offset_defs is_aligned_mask mask_def
                          objBits_defs) apply (word_bitwise, simp) apply (word_bitwise, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits \<Longrightarrow> cscheduler_action_relation a p = (cscheduler_action_to_H p = a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits; a = ResumeCurrentThread\<rbrakk> \<Longrightarrow> cscheduler_action_relation a p = (cscheduler_action_to_H p = a)
 2. \<lbrakk>\<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits; a = ChooseNewThread\<rbrakk> \<Longrightarrow> cscheduler_action_relation a p = (cscheduler_action_to_H p = a)
 3. \<And>x3. \<lbrakk>\<forall>t. a = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits; a = SwitchToThread x3\<rbrakk> \<Longrightarrow> cscheduler_action_relation a p = (cscheduler_action_to_H p = a) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>is_aligned x3 tcbBlockSizeBits; a = SwitchToThread x3\<rbrakk> \<Longrightarrow> (p = tcb_Ptr 1 \<longrightarrow> tcb_Ptr 1 \<noteq> tcb_ptr_to_ctcb_ptr x3) \<and> (p \<noteq> tcb_Ptr 1 \<longrightarrow> (p = NULL \<longrightarrow> NULL \<noteq> tcb_ptr_to_ctcb_ptr x3) \<and> (p \<noteq> NULL \<longrightarrow> (p = tcb_ptr_to_ctcb_ptr x3) = (ctcb_ptr_to_tcb_ptr p = x3))) proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>is_aligned x3 tcbBlockSizeBits; a = SwitchToThread x3; p = tcb_Ptr 1; tcb_Ptr 1 = tcb_ptr_to_ctcb_ptr x3\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>is_aligned x3 tcbBlockSizeBits; a = SwitchToThread x3; p = NULL; 0 \<noteq> 1; NULL = tcb_ptr_to_ctcb_ptr x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>is_aligned x3 tcbBlockSizeBits; a = SwitchToThread x3; tcb_ptr_to_ctcb_ptr x3 \<noteq> tcb_Ptr 1; tcb_ptr_to_ctcb_ptr x3 \<noteq> NULL; p = tcb_ptr_to_ctcb_ptr x3\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x3) = x3
 4. \<And>x3. \<lbrakk>is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits; a = SwitchToThread (ctcb_ptr_to_tcb_ptr p); p \<noteq> tcb_Ptr 1; p \<noteq> NULL\<rbrakk> \<Longrightarrow> p = tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr p) proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>x3 && 0x1FF = 0; a = SwitchToThread x3; p = tcb_Ptr (x3 + 0x100); 0xFF + x3 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>x3 && 0x1FF = 0; a = SwitchToThread x3; p = NULL; x3 + 0x100 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>x3 && 0x1FF = 0; a = SwitchToThread x3; p = NULL; x3 + 0x100 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!