Additional predicate laws

isabelle-utp · Jan 10, 2025 · c628a5c · c628a5c
1 parent 3fc0d62
commit c628a5c
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/utp_pred.thy b/utp_pred.thy
@@ -99,6 +99,12 @@ lemma pred_ref_iff_le: "(f :: 's pred) \<sqsubseteq> g \<longleftrightarrow> g \
 lemma pred_refine_as_impl: "(P \<sqsubseteq> Q) \<longleftrightarrow> `Q \<longrightarrow> P`"
   by (simp add: pred_refine_iff taut_def)
 
+lemma pred_ref_monoI:
+  fixes F :: "'\<alpha> pred \<Rightarrow> '\<beta> pred"
+  assumes "(\<And>P Q. P \<sqsubseteq> Q \<Longrightarrow> F P \<sqsubseteq> F Q)"
+  shows "mono F"
+  using assms by (simp add: monoI pred_ref_iff_le)
+
 lemma pred_ref_monoD: 
   fixes P Q :: "'a pred" and F :: "'a pred \<Rightarrow> 'b pred"
   assumes "mono F" "P \<sqsubseteq> Q" 
@@ -110,6 +116,9 @@ method pred_auto uses assms add = (insert assms, (simp add: pred expr_simps add)
 
 declare expr_if_def [pred]
 
+lemma expr_if_cond_def: "P \<triangleleft> B \<triangleright> Q = ((B \<and> P)\<^sub>e \<or> (\<not> B \<and> Q)\<^sub>e)"
+  by pred_auto
+
 subsection \<open> Algebraic Structures \<close>
 
 interpretation pred_ba: boolean_algebra diff_pred not_pred conj_pred "(\<sqsupseteq>)" "(\<sqsupset>)"

diff --git a/utp_pred_laws.thy b/utp_pred_laws.thy
@@ -29,4 +29,8 @@ lemma not_INF:
   shows "(\<not> (\<Squnion> x\<in>A. P x)) = (\<Sqinter> x\<in>A. \<not> P x)"
   by pred_simp
 
+lemma ex_pred_simps [simp]:
+  "(\<exists> x \<Zspot> true) = true" "(\<exists> x \<Zspot> false) = false"
+  by (pred_auto+)
+
 end