author haftmann Thu Dec 22 08:43:30 2016 +0100 (2016-12-22) changeset 64634 5bd30359e46e parent 64633 5ebcf6c525f1 child 64635 255741c5f862
proper logical constants
 NEWS file | annotate | diff | revisions src/HOL/Partial_Function.thy file | annotate | diff | revisions src/HOL/Probability/Probability_Mass_Function.thy file | annotate | diff | revisions src/HOL/Probability/SPMF.thy file | annotate | diff | revisions src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/NEWS	Wed Dec 21 21:26:26 2016 +0100
1.2 +++ b/NEWS	Thu Dec 22 08:43:30 2016 +0100
1.3 @@ -19,7 +19,9 @@
1.4  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
1.5  INCOMPATIBILITY.
1.6
1.7 -* Dropped abbreviation transP; use constant transp instead.
1.8 +* Dropped abbreviation transP, antisymP, single_valuedP;
1.9 +use constants transp, antisymp, single_valuedp instead.
1.10 +INCOMPATIBILITY.
1.11
1.12  * Swapped orientation of congruence rules mod_add_left_eq,
```
```     2.1 --- a/src/HOL/Partial_Function.thy	Wed Dec 21 21:26:26 2016 +0100
2.2 +++ b/src/HOL/Partial_Function.thy	Thu Dec 22 08:43:30 2016 +0100
2.3 @@ -283,8 +283,8 @@
2.4  lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
2.5  by(auto simp add: flat_ord_def)
2.6
2.7 -lemma antisymP_flat_ord: "antisymP (flat_ord a)"
2.8 -by(rule antisymI)(auto dest: flat_ord_antisym)
2.9 +lemma antisymp_flat_ord: "antisymp (flat_ord a)"
2.10 +by(rule antisympI)(auto dest: flat_ord_antisym)
2.11
2.12  interpretation tailrec:
2.13    partial_function_definitions "flat_ord undefined" "flat_lub undefined"
```
```     3.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Dec 21 21:26:26 2016 +0100
3.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 22 08:43:30 2016 +0100
3.3 @@ -1573,34 +1573,29 @@
3.4    fixes p q :: "'a pmf"
3.5    assumes 1: "rel_pmf R p q"
3.6    assumes 2: "rel_pmf R q p"
3.7 -  and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
3.8 +  and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R"
3.9    shows "p = q"
3.10  proof -
3.11    from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
3.12    also have "inf R R\<inverse>\<inverse> = op ="
3.13 -    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
3.14 +    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD)
3.15    finally show ?thesis unfolding pmf.rel_eq .
3.16  qed
3.17
3.18  lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
3.19 -by(blast intro: reflpI rel_pmf_reflI reflpD)
3.20 +  by (fact pmf.rel_reflp)
3.21
3.22 -lemma antisymP_rel_pmf:
3.23 -  "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
3.24 -  \<Longrightarrow> antisymP (rel_pmf R)"
3.25 -by(rule antisymI)(blast intro: rel_pmf_antisym)
3.26 +lemma antisymp_rel_pmf:
3.27 +  "\<lbrakk> reflp R; transp R; antisymp R \<rbrakk>
3.28 +  \<Longrightarrow> antisymp (rel_pmf R)"
3.29 +by(rule antisympI)(blast intro: rel_pmf_antisym)
3.30
3.31  lemma transp_rel_pmf:
3.32    assumes "transp R"
3.33    shows "transp (rel_pmf R)"
3.34 -proof (rule transpI)
3.35 -  fix x y z
3.36 -  assume "rel_pmf R x y" and "rel_pmf R y z"
3.37 -  hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
3.38 -  thus "rel_pmf R x z"
3.39 -    using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
3.40 -qed
3.41 +  using assms by (fact pmf.rel_transp)
3.42
3.43 +
3.44  subsection \<open> Distributions \<close>
3.45
3.46  context
```
```     4.1 --- a/src/HOL/Probability/SPMF.thy	Wed Dec 21 21:26:26 2016 +0100
4.2 +++ b/src/HOL/Probability/SPMF.thy	Thu Dec 22 08:43:30 2016 +0100
4.3 @@ -95,8 +95,8 @@
4.4  lemma transp_ord_option: "transp ord \<Longrightarrow> transp (ord_option ord)"
4.5  unfolding transp_def by(blast intro: ord_option_trans)
4.6
4.7 -lemma antisymP_ord_option: "antisymP ord \<Longrightarrow> antisymP (ord_option ord)"
4.8 -by(auto intro!: antisymI elim!: ord_option.cases dest: antisymD)
4.9 +lemma antisymp_ord_option: "antisymp ord \<Longrightarrow> antisymp (ord_option ord)"
4.10 +by(auto intro!: antisympI elim!: ord_option.cases dest: antisympD)
4.11
4.12  lemma ord_option_chainD:
4.13    "Complete_Partial_Order.chain (ord_option ord) Y
4.14 @@ -1508,7 +1508,7 @@
4.15    fix x y
4.16    assume "?R x y" "?R y x"
4.17    thus "x = y"
4.18 -    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymP_ord_option)
4.19 +    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymp_ord_option)
4.20  next
4.21    fix Y x
4.22    assume "Complete_Partial_Order.chain ?R Y" "x \<in> Y"
```
```     5.1 --- a/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
5.2 +++ b/src/HOL/Relation.thy	Thu Dec 22 08:43:30 2016 +0100
5.3 @@ -321,26 +321,51 @@
5.4  definition antisym :: "'a rel \<Rightarrow> bool"
5.5    where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
5.6
5.7 -abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
5.8 -  where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *)
5.9 +definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
5.10 +  where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)"
5.11
5.12 -lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
5.13 +lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r"
5.14 +  by (simp add: antisym_def antisymp_def)
5.15 +
5.16 +lemma antisymI [intro?]:
5.17 +  "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
5.18    unfolding antisym_def by iprover
5.19
5.20 -lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
5.21 +lemma antisympI [intro?]:
5.22 +  "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r"
5.23 +  by (fact antisymI [to_pred])
5.24 +
5.25 +lemma antisymD [dest?]:
5.26 +  "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
5.27    unfolding antisym_def by iprover
5.28
5.29 -lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
5.30 -  unfolding antisym_def by blast
5.31 +lemma antisympD [dest?]:
5.32 +  "antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b"
5.33 +  by (fact antisymD [to_pred])
5.34
5.35 -lemma antisym_empty [simp]: "antisym {}"
5.36 +lemma antisym_subset:
5.37 +  "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
5.38    unfolding antisym_def by blast
5.39
5.40 -lemma antisymP_equality [simp]: "antisymP op ="
5.41 -  by (auto intro: antisymI)
5.42 +lemma antisymp_less_eq:
5.43 +  "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
5.44 +  by (fact antisym_subset [to_pred])
5.45 +
5.46 +lemma antisym_empty [simp]:
5.47 +  "antisym {}"
5.48 +  unfolding antisym_def by blast
5.49
5.50 -lemma antisym_singleton [simp]: "antisym {x}"
5.51 -by (blast intro: antisymI)
5.52 +lemma antisym_bot [simp]:
5.53 +  "antisymp \<bottom>"
5.54 +  by (fact antisym_empty [to_pred])
5.55 +
5.56 +lemma antisymp_equality [simp]:
5.57 +  "antisymp HOL.eq"
5.58 +  by (auto intro: antisympI)
5.59 +
5.60 +lemma antisym_singleton [simp]:
5.61 +  "antisym {x}"
5.62 +  by (blast intro: antisymI)
5.63
5.64
5.65  subsubsection \<open>Transitivity\<close>
5.66 @@ -437,21 +462,45 @@
5.67  definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
5.68    where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
5.69
5.70 -abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
5.71 -  where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *)
5.72 +definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
5.73 +  where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
5.74 +
5.75 +lemma single_valuedp_single_valued_eq [pred_set_conv]:
5.76 +  "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
5.77 +  by (simp add: single_valued_def single_valuedp_def)
5.78
5.79 -lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r"
5.80 -  unfolding single_valued_def .
5.81 +lemma single_valuedI:
5.82 +  "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
5.83 +  unfolding single_valued_def by blast
5.84
5.85 -lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
5.86 +lemma single_valuedpI:
5.87 +  "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
5.88 +  by (fact single_valuedI [to_pred])
5.89 +
5.90 +lemma single_valuedD:
5.91 +  "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
5.92    by (simp add: single_valued_def)
5.93
5.94 -lemma single_valued_empty[simp]: "single_valued {}"
5.95 +lemma single_valuedpD:
5.96 +  "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
5.97 +  by (fact single_valuedD [to_pred])
5.98 +
5.99 +lemma single_valued_empty [simp]:
5.100 +  "single_valued {}"
5.101    by (simp add: single_valued_def)
5.102
5.103 -lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
5.104 +lemma single_valuedp_bot [simp]:
5.105 +  "single_valuedp \<bottom>"
5.106 +  by (fact single_valued_empty [to_pred])
5.107 +
5.108 +lemma single_valued_subset:
5.109 +  "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
5.110    unfolding single_valued_def by blast
5.111
5.112 +lemma single_valuedp_less_eq:
5.113 +  "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r"
5.114 +  by (fact single_valued_subset [to_pred])
5.115 +
5.116
5.117  subsection \<open>Relation operations\<close>
5.118
```