Additional Hoare logic laws and a fix

UTP/ITree_CSP.thy

@@ -267,6 +267,7 @@ friend_of_corec extchoice :: "('e, 's) itree \<Rightarrow> ('e, 's) itree \<Righ
    )"
     apply (cases P; cases Q)
             apply (auto simp add: extcheq_def genchoice.ctr extchoice_itree_def)
+
    apply transfer_prover
   apply transfer_prover
   done
@@ -621,7 +622,7 @@ lemma hide_Sil [simp]: "(\<tau> P) \<setminus> A = \<tau> (P \<setminus> A)"
 lemma hide_sync: "(sync a \<bind> P) \<setminus> {build\<^bsub>a\<^esub> ()} = \<tau> (P ()) \<setminus> {build\<^bsub>a\<^esub> ()}"
   by (simp add: sync_def hide.code)
 
-lemma hide_sync_loop_diverge: "hide (iter (sync a)) {build\<^bsub>a\<^esub> ()} = diverge"
+lemma hide_sync_loop_diverge: "hide (loop (\<lambda> _. sync a) ()) {build\<^bsub>a\<^esub> ()} = diverge"
   apply (coinduction rule:itree_coind, auto)
   apply (simp add: iterate.code, simp add: sync_def)
   apply (metis One_nat_def hide_sync is_Sil_hide itree.disc(5) iterate.code)

UTP/ITree_Hoare.thy

@@ -85,6 +85,12 @@ corollary hl_disj_post:
   shows "\<^bold>{P\<^bold>} S \<^bold>{Q\<^sub>1 \<or> Q2\<^bold>}"
   by (rule hl_strengthen[OF assms], simp)
 
+lemma hl_pre_false [hoare_safe]: "\<^bold>{False\<^bold>} S \<^bold>{P\<^bold>}"
+  by (simp add: hoare_alt_def)
+
+lemma hl_post_true [hoare_safe]: "\<^bold>{P\<^bold>} S \<^bold>{True\<^bold>}"
+  by (simp add: hoare_alt_def)
+
 lemma hl_conj:
   assumes "\<^bold>{P\<^sub>1\<^bold>} S \<^bold>{Q\<^sub>1\<^bold>}" "\<^bold>{P\<^sub>2\<^bold>} S \<^bold>{Q\<^sub>2\<^bold>}"
   shows "\<^bold>{P\<^sub>1 \<and> P\<^sub>2\<^bold>} S \<^bold>{Q\<^sub>1 \<and> Q\<^sub>2\<^bold>}"