proper logical constants
authorhaftmann
Thu Dec 22 08:43:30 2016 +0100 (2016-12-22)
changeset 646345bd30359e46e
parent 64633 5ebcf6c525f1
child 64635 255741c5f862
proper logical constants
NEWS
src/HOL/Partial_Function.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/SPMF.thy
src/HOL/Relation.thy
     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,
    1.13  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_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