src/HOL/Relation.thy
changeset 63376 4c0cc2b356f0
parent 62343 24106dc44def
child 63404 a95e7432d86c
     1.1 --- a/src/HOL/Relation.thy	Mon Jul 04 19:46:20 2016 +0200
     1.2 +++ b/src/HOL/Relation.thy	Mon Jul 04 19:46:20 2016 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4  declare Sup2_E [elim!]
     1.5  declare SUP2_E [elim!]
     1.6  
     1.7 +
     1.8  subsection \<open>Fundamental\<close>
     1.9  
    1.10  subsubsection \<open>Relations as sets of pairs\<close>
    1.11 @@ -141,6 +142,7 @@
    1.12  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
    1.13    by (simp add: fun_eq_iff)
    1.14  
    1.15 +
    1.16  subsection \<open>Properties of relations\<close>
    1.17  
    1.18  subsubsection \<open>Reflexivity\<close>
    1.19 @@ -161,7 +163,7 @@
    1.20    "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r" 
    1.21    by (simp add: refl_on_def reflp_def)
    1.22  
    1.23 -lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
    1.24 +lemma refl_onI [intro?]: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
    1.25    by (unfold refl_on_def) (iprover intro!: ballI)
    1.26  
    1.27  lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
    1.28 @@ -173,7 +175,7 @@
    1.29  lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
    1.30    by (unfold refl_on_def) blast
    1.31  
    1.32 -lemma reflpI:
    1.33 +lemma reflpI [intro?]:
    1.34    "(\<And>x. r x x) \<Longrightarrow> reflp r"
    1.35    by (auto intro: refl_onI simp add: reflp_def)
    1.36  
    1.37 @@ -182,7 +184,7 @@
    1.38    obtains "r x x"
    1.39    using assms by (auto dest: refl_onD simp add: reflp_def)
    1.40  
    1.41 -lemma reflpD:
    1.42 +lemma reflpD [dest?]:
    1.43    assumes "reflp r"
    1.44    shows "r x x"
    1.45    using assms by (auto elim: reflpE)
    1.46 @@ -222,6 +224,7 @@
    1.47  lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
    1.48  by(auto intro: reflpI dest: reflpD)
    1.49  
    1.50 +
    1.51  subsubsection \<open>Irreflexivity\<close>
    1.52  
    1.53  definition irrefl :: "'a rel \<Rightarrow> bool"
    1.54 @@ -236,11 +239,11 @@
    1.55    "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 
    1.56    by (simp add: irrefl_def irreflp_def)
    1.57  
    1.58 -lemma irreflI:
    1.59 +lemma irreflI [intro?]:
    1.60    "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
    1.61    by (simp add: irrefl_def)
    1.62  
    1.63 -lemma irreflpI:
    1.64 +lemma irreflpI [intro?]:
    1.65    "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
    1.66    by (fact irreflI [to_pred])
    1.67  
    1.68 @@ -278,11 +281,11 @@
    1.69    "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" 
    1.70    by (simp add: sym_def symp_def)
    1.71  
    1.72 -lemma symI:
    1.73 +lemma symI [intro?]:
    1.74    "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
    1.75    by (unfold sym_def) iprover
    1.76  
    1.77 -lemma sympI:
    1.78 +lemma sympI [intro?]:
    1.79    "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
    1.80    by (fact symI [to_pred])
    1.81  
    1.82 @@ -296,12 +299,12 @@
    1.83    obtains "r a b"
    1.84    using assms by (rule symE [to_pred])
    1.85  
    1.86 -lemma symD:
    1.87 +lemma symD [dest?]:
    1.88    assumes "sym r" and "(b, a) \<in> r"
    1.89    shows "(a, b) \<in> r"
    1.90    using assms by (rule symE)
    1.91  
    1.92 -lemma sympD:
    1.93 +lemma sympD [dest?]:
    1.94    assumes "symp r" and "r b a"
    1.95    shows "r a b"
    1.96    using assms by (rule symD [to_pred])
    1.97 @@ -346,14 +349,14 @@
    1.98    "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
    1.99  
   1.100  abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   1.101 -where
   1.102 +where -- \<open>FIXME proper logical operation\<close>
   1.103    "antisymP r \<equiv> antisym {(x, y). r x y}"
   1.104  
   1.105 -lemma antisymI:
   1.106 +lemma antisymI [intro?]:
   1.107    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   1.108    by (unfold antisym_def) iprover
   1.109  
   1.110 -lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   1.111 +lemma antisymD [dest?]: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   1.112    by (unfold antisym_def) iprover
   1.113  
   1.114  lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
   1.115 @@ -365,6 +368,7 @@
   1.116  lemma antisymP_equality [simp]: "antisymP op ="
   1.117  by(auto intro: antisymI)
   1.118  
   1.119 +
   1.120  subsubsection \<open>Transitivity\<close>
   1.121  
   1.122  definition trans :: "'a rel \<Rightarrow> bool"
   1.123 @@ -379,15 +383,11 @@
   1.124    "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" 
   1.125    by (simp add: trans_def transp_def)
   1.126  
   1.127 -abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   1.128 -where \<comment> \<open>FIXME drop\<close>
   1.129 -  "transP r \<equiv> trans {(x, y). r x y}"
   1.130 -
   1.131 -lemma transI:
   1.132 +lemma transI [intro?]:
   1.133    "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
   1.134    by (unfold trans_def) iprover
   1.135  
   1.136 -lemma transpI:
   1.137 +lemma transpI [intro?]:
   1.138    "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   1.139    by (fact transI [to_pred])
   1.140  
   1.141 @@ -401,12 +401,12 @@
   1.142    obtains "r x z"
   1.143    using assms by (rule transE [to_pred])
   1.144  
   1.145 -lemma transD:
   1.146 +lemma transD [dest?]:
   1.147    assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
   1.148    shows "(x, z) \<in> r"
   1.149    using assms by (rule transE)
   1.150  
   1.151 -lemma transpD:
   1.152 +lemma transpD [dest?]:
   1.153    assumes "transp r" and "r x y" and "r y z"
   1.154    shows "r x z"
   1.155    using assms by (rule transD [to_pred])
   1.156 @@ -436,6 +436,7 @@
   1.157  lemma transp_equality [simp]: "transp op ="
   1.158  by(auto intro: transpI)
   1.159  
   1.160 +
   1.161  subsubsection \<open>Totality\<close>
   1.162  
   1.163  definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   1.164 @@ -454,7 +455,8 @@
   1.165  where
   1.166    "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
   1.167  
   1.168 -abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.169 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   1.170 +where -- \<open>FIXME proper logical operation\<close>
   1.171    "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   1.172  
   1.173  lemma single_valuedI:
   1.174 @@ -518,6 +520,7 @@
   1.175  lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
   1.176    by force
   1.177  
   1.178 +
   1.179  subsubsection \<open>Diagonal: identity over a set\<close>
   1.180  
   1.181  definition Id_on  :: "'a set \<Rightarrow> 'a rel"
   1.182 @@ -684,6 +687,7 @@
   1.183  lemma OO_eq: "R OO op = = R"
   1.184  by blast
   1.185  
   1.186 +
   1.187  subsubsection \<open>Converse\<close>
   1.188  
   1.189  inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  ("(_\<inverse>)" [1000] 999)
   1.190 @@ -838,8 +842,6 @@
   1.191  where
   1.192    DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r"
   1.193  
   1.194 -abbreviation (input) "DomainP \<equiv> Domainp"
   1.195 -
   1.196  lemmas DomainPI = Domainp.DomainI
   1.197  
   1.198  inductive_cases DomainE [elim!]: "a \<in> Domain r"
   1.199 @@ -850,8 +852,6 @@
   1.200  where
   1.201    RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r"
   1.202  
   1.203 -abbreviation (input) "RangeP \<equiv> Rangep"
   1.204 -
   1.205  lemmas RangePI = Rangep.RangeI
   1.206  
   1.207  inductive_cases RangeE [elim!]: "b \<in> Range r"
   1.208 @@ -1079,6 +1079,7 @@
   1.209  lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
   1.210    by auto
   1.211  
   1.212 +
   1.213  subsubsection \<open>Inverse image\<close>
   1.214  
   1.215  definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
   1.216 @@ -1122,6 +1123,7 @@
   1.217  
   1.218  lemmas Powp_mono [mono] = Pow_mono [to_pred]
   1.219  
   1.220 +
   1.221  subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close>
   1.222  
   1.223  lemma Id_on_fold:
   1.224 @@ -1196,4 +1198,17 @@
   1.225      (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
   1.226        cong: if_cong)
   1.227  
   1.228 +text \<open>Misc\<close>
   1.229 +
   1.230 +abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   1.231 +where \<comment> \<open>FIXME drop\<close>
   1.232 +  "transP r \<equiv> trans {(x, y). r x y}"
   1.233 +
   1.234 +abbreviation (input)
   1.235 +  "RangeP \<equiv> Rangep"
   1.236 +
   1.237 +abbreviation (input)
   1.238 +  "DomainP \<equiv> Domainp"
   1.239 +
   1.240 +
   1.241  end