Removed Inf_apply and variants from [simp] as they break proof abstraction in UTP.

Author: simondfoster

utp_pred.thy

@@ -161,6 +161,18 @@ end
 
 unbundle utp_lattice_syntax
 
+text \<open> The laws for applying functional infimum hamper proof automation. We therefore remove these
+  laws from the simplifer, and instead add their definitional equations to the predicate laws. \<close>
+
+declare Inf_apply [simp del]
+declare INF_apply [simp del]
+
+declare Sup_apply [simp del]
+declare SUP_apply [simp del]
+
+declare Inf_fun_def [pred]
+declare Sup_fun_def [pred]
+
 subsection \<open> Substitution Laws \<close>
 
 lemma subst_pred [usubst]:

utp_rel_laws.thy

@@ -508,15 +508,15 @@ lemma ustar_rep_eq [rel]: "\<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>U = \<lbrakk>
 proof 
   have "((a, b) \<in> \<lbrakk>P\<rbrakk>\<^sub>U\<^sup>*) \<Longrightarrow> (a,b) \<in> \<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>U" for a b
     apply (induct rule: rtrancl.induct)
-     apply (simp_all add: pred_rel_def ustar_def)
+     apply (simp_all add: pred_rel_def ustar_def Sup_apply)
      apply (metis (full_types) power.power.power_0 prod.simps(2) skip_def)
     apply (metis (mono_tags, lifting) case_prodI upred_semiring.power_Suc2 utp_rel.seq_def)
     done
   then show "\<lbrakk>P\<rbrakk>\<^sub>U\<^sup>* \<subseteq> \<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>U"
     by auto
 next
   have "((a, b) \<in> \<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>U) \<Longrightarrow> (a,b) \<in> \<lbrakk>P\<rbrakk>\<^sub>U\<^sup>*" for a b
-    apply (simp add: ustar_def pred_rel_def)
+    apply (simp add: ustar_def pred_rel_def Sup_apply)
     apply (metis mem_Collect_eq pred_rel_def rtrancl_power upower_interp)
     done
   then show "\<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>U \<subseteq> \<lbrakk>P\<rbrakk>\<^sub>U\<^sup>*"