--- 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,
--- 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"
--- 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
--- 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"
--- 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>