Conditional laws

isabelle-utp · Oct 17, 2023 · d915bac · d915bac
1 parent 1033c5c
commit d915bac
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/utp_des_core.thy b/utp_des_core.thy
@@ -37,7 +37,7 @@ abbreviation drop_desr ("\<lfloor>_\<rfloor>\<^sub>D")
 where "\<lfloor>P\<rfloor>\<^sub>D \<equiv> P \<down> (\<^bold>v\<^sub>D \<times> \<^bold>v\<^sub>D)"
 
 abbreviation dcond :: "('\<alpha>, '\<beta>) des_rel \<Rightarrow> '\<alpha> pred \<Rightarrow> ('\<alpha>, '\<beta>) des_rel \<Rightarrow> ('\<alpha>, '\<beta>) des_rel" 
-where "dcond P b Q \<equiv> P \<triangleleft> \<lceil>b\<rceil>\<^sub>D\<^sub>< \<triangleright> Q"
+where "dcond P b Q \<equiv> P \<lhd> (b \<up> \<^bold>v\<^sub>D) \<rhd> Q"
 
 syntax "_dcond" :: "logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("(3_ \<triangleleft> _ \<triangleright>\<^sub>D/ _)" [52,0,53] 52)
 translations "_dcond P b Q" == "CONST dcond P (b)\<^sub>e Q"

diff --git a/utp_des_laws.thy b/utp_des_laws.thy
@@ -302,7 +302,7 @@ theorem design_condr:
   by (pred_auto)
 
 theorem ndesign_dcond [ndes_simp]:
-  shows "((p\<^sub>1 \<turnstile>\<^sub>n P\<^sub>2) \<triangleleft> b\<^sup>< \<up> more\<^sub>L\<^sup>2 \<triangleright> (q\<^sub>1 \<turnstile>\<^sub>n Q\<^sub>2)) = ((p\<^sub>1 \<triangleleft> b \<triangleright> q\<^sub>1) \<turnstile>\<^sub>n (P\<^sub>2 \<triangleleft> b\<^sup>< \<triangleright> Q\<^sub>2))"
+  shows "(dcond (p\<^sub>1 \<turnstile>\<^sub>n P\<^sub>2) b (q\<^sub>1 \<turnstile>\<^sub>n Q\<^sub>2)) = ((p\<^sub>1 \<triangleleft> b \<triangleright> q\<^sub>1) \<turnstile>\<^sub>n (P\<^sub>2 \<triangleleft> b\<^sup>< \<triangleright> Q\<^sub>2))"
   by (pred_auto)
 
 lemma design_UINF_mem: