# HG changeset patch
# User haftmann
# Date 1482392610 -3600
# Node ID 5bd30359e46e7df973fb9af00fe528feb7415e20
# Parent  5ebcf6c525f1fa965b3771853e59773197cd5fe7
proper logical constants

diff -r 5ebcf6c525f1 -r 5bd30359e46e NEWS
--- a/NEWS	Wed Dec 21 21:26:26 2016 +0100
+++ b/NEWS	Thu Dec 22 08:43:30 2016 +0100
@@ -19,7 +19,9 @@
 * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
 INCOMPATIBILITY.
 
-* Dropped abbreviation transP; use constant transp instead.
+* Dropped abbreviation transP, antisymP, single_valuedP;
+use constants transp, antisymp, single_valuedp instead.
+INCOMPATIBILITY.
 
 * Swapped orientation of congruence rules mod_add_left_eq,
 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
diff -r 5ebcf6c525f1 -r 5bd30359e46e src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Partial_Function.thy	Thu Dec 22 08:43:30 2016 +0100
@@ -283,8 +283,8 @@
 lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
 by(auto simp add: flat_ord_def)
 
-lemma antisymP_flat_ord: "antisymP (flat_ord a)"
-by(rule antisymI)(auto dest: flat_ord_antisym)
+lemma antisymp_flat_ord: "antisymp (flat_ord a)"
+by(rule antisympI)(auto dest: flat_ord_antisym)
 
 interpretation tailrec:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
diff -r 5ebcf6c525f1 -r 5bd30359e46e src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 22 08:43:30 2016 +0100
@@ -1573,34 +1573,29 @@
   fixes p q :: "'a pmf"
   assumes 1: "rel_pmf R p q"
   assumes 2: "rel_pmf R q p"
-  and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
+  and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R"
   shows "p = q"
 proof -
   from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
   also have "inf R R\<inverse>\<inverse> = op ="
-    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
+    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD)
   finally show ?thesis unfolding pmf.rel_eq .
 qed
 
 lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
-by(blast intro: reflpI rel_pmf_reflI reflpD)
+  by (fact pmf.rel_reflp)
 
-lemma antisymP_rel_pmf:
-  "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
-  \<Longrightarrow> antisymP (rel_pmf R)"
-by(rule antisymI)(blast intro: rel_pmf_antisym)
+lemma antisymp_rel_pmf:
+  "\<lbrakk> reflp R; transp R; antisymp R \<rbrakk>
+  \<Longrightarrow> antisymp (rel_pmf R)"
+by(rule antisympI)(blast intro: rel_pmf_antisym)
 
 lemma transp_rel_pmf:
   assumes "transp R"
   shows "transp (rel_pmf R)"
-proof (rule transpI)
-  fix x y z
-  assume "rel_pmf R x y" and "rel_pmf R y z"
-  hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
-  thus "rel_pmf R x z"
-    using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
-qed
+  using assms by (fact pmf.rel_transp)
 
+    
 subsection \<open> Distributions \<close>
 
 context
diff -r 5ebcf6c525f1 -r 5bd30359e46e src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Probability/SPMF.thy	Thu Dec 22 08:43:30 2016 +0100
@@ -95,8 +95,8 @@
 lemma transp_ord_option: "transp ord \<Longrightarrow> transp (ord_option ord)"
 unfolding transp_def by(blast intro: ord_option_trans)
 
-lemma antisymP_ord_option: "antisymP ord \<Longrightarrow> antisymP (ord_option ord)"
-by(auto intro!: antisymI elim!: ord_option.cases dest: antisymD)
+lemma antisymp_ord_option: "antisymp ord \<Longrightarrow> antisymp (ord_option ord)"
+by(auto intro!: antisympI elim!: ord_option.cases dest: antisympD)
 
 lemma ord_option_chainD:
   "Complete_Partial_Order.chain (ord_option ord) Y
@@ -1508,7 +1508,7 @@
   fix x y
   assume "?R x y" "?R y x"
   thus "x = y"
-    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymP_ord_option)
+    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymp_ord_option)
 next
   fix Y x
   assume "Complete_Partial_Order.chain ?R Y" "x \<in> Y"
diff -r 5ebcf6c525f1 -r 5bd30359e46e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 22 08:43:30 2016 +0100
@@ -321,26 +321,51 @@
 definition antisym :: "'a rel \<Rightarrow> bool"
   where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
 
-abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *)
+definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)"
 
-lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
+lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r"
+  by (simp add: antisym_def antisymp_def)
+
+lemma antisymI [intro?]:
+  "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
   unfolding antisym_def by iprover
 
-lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
+lemma antisympI [intro?]:
+  "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r"
+  by (fact antisymI [to_pred])
+    
+lemma antisymD [dest?]:
+  "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
   unfolding antisym_def by iprover
 
-lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
-  unfolding antisym_def by blast
+lemma antisympD [dest?]:
+  "antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b"
+  by (fact antisymD [to_pred])
 
-lemma antisym_empty [simp]: "antisym {}"
+lemma antisym_subset:
+  "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
   unfolding antisym_def by blast
 
-lemma antisymP_equality [simp]: "antisymP op ="
-  by (auto intro: antisymI)
+lemma antisymp_less_eq:
+  "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
+  by (fact antisym_subset [to_pred])
+    
+lemma antisym_empty [simp]:
+  "antisym {}"
+  unfolding antisym_def by blast
 
-lemma antisym_singleton [simp]: "antisym {x}"
-by (blast intro: antisymI)
+lemma antisym_bot [simp]:
+  "antisymp \<bottom>"
+  by (fact antisym_empty [to_pred])
+    
+lemma antisymp_equality [simp]:
+  "antisymp HOL.eq"
+  by (auto intro: antisympI)
+
+lemma antisym_singleton [simp]:
+  "antisym {x}"
+  by (blast intro: antisymI)
 
 
 subsubsection \<open>Transitivity\<close>
@@ -437,21 +462,45 @@
 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
   where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
 
-abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
-  where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *)
+definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
+
+lemma single_valuedp_single_valued_eq [pred_set_conv]:
+  "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
+  by (simp add: single_valued_def single_valuedp_def)
 
-lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r"
-  unfolding single_valued_def .
+lemma single_valuedI:
+  "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
+  unfolding single_valued_def by blast
 
-lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
+lemma single_valuedpI:
+  "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
+  by (fact single_valuedI [to_pred])
+
+lemma single_valuedD:
+  "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
   by (simp add: single_valued_def)
 
-lemma single_valued_empty[simp]: "single_valued {}"
+lemma single_valuedpD:
+  "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
+  by (fact single_valuedD [to_pred])
+
+lemma single_valued_empty [simp]:
+  "single_valued {}"
   by (simp add: single_valued_def)
 
-lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
+lemma single_valuedp_bot [simp]:
+  "single_valuedp \<bottom>"
+  by (fact single_valued_empty [to_pred])
+
+lemma single_valued_subset:
+  "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
   unfolding single_valued_def by blast
 
+lemma single_valuedp_less_eq:
+  "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r"
+  by (fact single_valued_subset [to_pred])
+
 
 subsection \<open>Relation operations\<close>