src/HOL/Predicate.thy
changeset 46191 a88546428c2a
parent 46175 48c534b22040
child 46553 50a7e97fe653
equal deleted inserted replaced
46190:a42c5f23109f 46191:a88546428c2a
   134   by (simp add: inf_fun_def)
   134   by (simp add: inf_fun_def)
   135 
   135 
   136 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   136 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   137   by (simp add: inf_fun_def)
   137   by (simp add: inf_fun_def)
   138 
   138 
   139 lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   139 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   140   by (simp add: inf_fun_def)
   140   by (simp add: inf_fun_def)
   141 
   141 
   142 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   142 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   143   by (simp add: inf_fun_def)
   143   by (simp add: inf_fun_def)
   144 
   144