fix trailing whitespace errors squash

Signed-off-by: Michael McInerney <[email protected]>

proof/crefine/AARCH64/IpcCancel_C.thy

@@ -30,7 +30,7 @@ qed
 
 lemmas cready_queues_index_to_C_in_range =
   cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
-                              
+
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';
      prio \<le> maxPriority; prio' \<le> maxPriority \<rbrakk> \<Longrightarrow> prio = prio' \<and> qdom = qdom'"
@@ -670,7 +670,7 @@ lemma tcb_queue_prepend_ccorres:
      (\<lbrace>ctcb_queue_relation queue \<acute>queue\<rbrace> \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace>) hs
      (tcbQueuePrepend queue tcbPtr) (Call tcb_queue_prepend_'proc)"
   (is "ccorres _ _ ?abs _ _ _ _")
-  supply if_split[split del]  
+  supply if_split[split del]
   apply (cinit lift: tcb_')
    \<comment> \<open>cinit is not able to lift queue_' because queue_' is later modified in the C program\<close>
    apply (rule_tac xf'=queue_' in ccorres_abstract, ceqv, rename_tac cqueue)

proof/crefine/AARCH64/Refine_C.thy

@@ -433,7 +433,7 @@ lemma handleSyscall_ccorres:
       apply (wpsimp wp: hoare_drop_imps)
      apply (simp
           | wpc
-          | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs'               
+          | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs'
           | strengthen ct_active_not_idle'_strengthen invs_valid_objs_strengthen)+
       apply (rule_tac  Q="\<lambda>rv. invs' and ct_active'" in hoare_post_imp, simp)
       apply (wp hy_invs')

proof/crefine/AARCH64/Schedule_C.thy

@@ -105,7 +105,7 @@ lemma Arch_switchToThread_ccorres:
 lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_aligned':
   "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> pspace_aligned' s"
   by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)
- 
+
 lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_distinct':
   "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> pspace_distinct' s"
   by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)

proof/refine/X64/Interrupt_R.thy

@@ -759,7 +759,7 @@ lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified]
 
 lemma handleInterrupt_corres:
   "corres dc
-     einvs 
+     einvs
      (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive))
      (handle_interrupt irq) (handleInterrupt irq)"
   (is "corres dc ?P ?P' ?f ?g")

proof/refine/X64/Ipc_R.thy

@@ -2201,14 +2201,14 @@ lemma doReplyTransfer_corres:
                               in corres_inst)
                 apply (case_tac rvb, simp_all)[1]
                  apply (rule corres_guard_imp)
-                   apply (rule corres_split[OF setThreadState_corres])  
+                   apply (rule corres_split[OF setThreadState_corres])
                       apply simp
                      apply (fold dc_def, rule possibleSwitchTo_corres)
                     apply simp
                     apply (wp hoare_weak_lift_imp hoare_weak_lift_imp_conj
                               set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
                               sts_st_tcb' sts_valid_objs'
-                           | simp 
+                           | simp
                            | force simp: valid_sched_def valid_sched_action_def
                                          valid_tcb_state'_def)+
                 apply (rule corres_guard_imp)

proof/refine/X64/Schedule_R.thy

@@ -1383,7 +1383,7 @@ lemma guarded_switch_to_corres:
       apply (rule switchToThread_corres)
      apply (force simp: st_tcb_at_tcb_at)
     apply (wp gts_st_tcb_at)
-   apply (force simp: st_tcb_at_tcb_at)+ 
+   apply (force simp: st_tcb_at_tcb_at)+
   done
 
 abbreviation "enumPrio \<equiv> [0.e.maxPriority]"