src/HOL/Relation.thy
changeset 60758 d8d85a8172b5
parent 60057 86fa63ce8156
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Relation.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Relation.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Relations -- as sets of pairs, and binary predicates *}
     1.8 +section \<open>Relations -- as sets of pairs, and binary predicates\<close>
     1.9  
    1.10  theory Relation
    1.11  imports Finite_Set
    1.12  begin
    1.13  
    1.14 -text {* A preliminary: classical rules for reasoning on predicates *}
    1.15 +text \<open>A preliminary: classical rules for reasoning on predicates\<close>
    1.16  
    1.17  declare predicate1I [Pure.intro!, intro!]
    1.18  declare predicate1D [Pure.dest, dest]
    1.19 @@ -51,23 +51,23 @@
    1.20  declare Sup2_E [elim!]
    1.21  declare SUP2_E [elim!]
    1.22  
    1.23 -subsection {* Fundamental *}
    1.24 +subsection \<open>Fundamental\<close>
    1.25  
    1.26 -subsubsection {* Relations as sets of pairs *}
    1.27 +subsubsection \<open>Relations as sets of pairs\<close>
    1.28  
    1.29  type_synonym 'a rel = "('a * 'a) set"
    1.30  
    1.31 -lemma subrelI: -- {* Version of @{thm [source] subsetI} for binary relations *}
    1.32 +lemma subrelI: -- \<open>Version of @{thm [source] subsetI} for binary relations\<close>
    1.33    "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
    1.34    by auto
    1.35  
    1.36 -lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
    1.37 +lemma lfp_induct2: -- \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
    1.38    "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
    1.39      (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
    1.40    using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
    1.41  
    1.42  
    1.43 -subsubsection {* Conversions between set and predicate relations *}
    1.44 +subsubsection \<open>Conversions between set and predicate relations\<close>
    1.45  
    1.46  lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S"
    1.47    by (simp add: set_eq_iff fun_eq_iff)
    1.48 @@ -141,16 +141,16 @@
    1.49  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.50    by (simp add: fun_eq_iff)
    1.51  
    1.52 -subsection {* Properties of relations *}
    1.53 +subsection \<open>Properties of relations\<close>
    1.54  
    1.55 -subsubsection {* Reflexivity *}
    1.56 +subsubsection \<open>Reflexivity\<close>
    1.57  
    1.58  definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
    1.59  where
    1.60    "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
    1.61  
    1.62  abbreviation refl :: "'a rel \<Rightarrow> bool"
    1.63 -where -- {* reflexivity over a type *}
    1.64 +where -- \<open>reflexivity over a type\<close>
    1.65    "refl \<equiv> refl_on UNIV"
    1.66  
    1.67  definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.68 @@ -219,7 +219,7 @@
    1.69  lemma reflp_equality [simp]: "reflp op ="
    1.70  by(simp add: reflp_def)
    1.71  
    1.72 -subsubsection {* Irreflexivity *}
    1.73 +subsubsection \<open>Irreflexivity\<close>
    1.74  
    1.75  definition irrefl :: "'a rel \<Rightarrow> bool"
    1.76  where
    1.77 @@ -246,7 +246,7 @@
    1.78    by (auto simp add: irrefl_def)
    1.79  
    1.80  
    1.81 -subsubsection {* Asymmetry *}
    1.82 +subsubsection \<open>Asymmetry\<close>
    1.83  
    1.84  inductive asym :: "'a rel \<Rightarrow> bool"
    1.85  where
    1.86 @@ -261,7 +261,7 @@
    1.87    by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
    1.88  
    1.89  
    1.90 -subsubsection {* Symmetry *}
    1.91 +subsubsection \<open>Symmetry\<close>
    1.92  
    1.93  definition sym :: "'a rel \<Rightarrow> bool"
    1.94  where
    1.95 @@ -336,7 +336,7 @@
    1.96    by (fact sym_UNION [to_pred])
    1.97  
    1.98  
    1.99 -subsubsection {* Antisymmetry *}
   1.100 +subsubsection \<open>Antisymmetry\<close>
   1.101  
   1.102  definition antisym :: "'a rel \<Rightarrow> bool"
   1.103  where
   1.104 @@ -362,7 +362,7 @@
   1.105  lemma antisymP_equality [simp]: "antisymP op ="
   1.106  by(auto intro: antisymI)
   1.107  
   1.108 -subsubsection {* Transitivity *}
   1.109 +subsubsection \<open>Transitivity\<close>
   1.110  
   1.111  definition trans :: "'a rel \<Rightarrow> bool"
   1.112  where
   1.113 @@ -377,7 +377,7 @@
   1.114    by (simp add: trans_def transp_def)
   1.115  
   1.116  abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   1.117 -where -- {* FIXME drop *}
   1.118 +where -- \<open>FIXME drop\<close>
   1.119    "transP r \<equiv> trans {(x, y). r x y}"
   1.120  
   1.121  lemma transI:
   1.122 @@ -433,7 +433,7 @@
   1.123  lemma transp_equality [simp]: "transp op ="
   1.124  by(auto intro: transpI)
   1.125  
   1.126 -subsubsection {* Totality *}
   1.127 +subsubsection \<open>Totality\<close>
   1.128  
   1.129  definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   1.130  where
   1.131 @@ -445,7 +445,7 @@
   1.132    by (simp add: total_on_def)
   1.133  
   1.134  
   1.135 -subsubsection {* Single valued relations *}
   1.136 +subsubsection \<open>Single valued relations\<close>
   1.137  
   1.138  definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
   1.139  where
   1.140 @@ -470,9 +470,9 @@
   1.141    by (unfold single_valued_def) blast
   1.142  
   1.143  
   1.144 -subsection {* Relation operations *}
   1.145 +subsection \<open>Relation operations\<close>
   1.146  
   1.147 -subsubsection {* The identity relation *}
   1.148 +subsubsection \<open>The identity relation\<close>
   1.149  
   1.150  definition Id :: "'a rel"
   1.151  where
   1.152 @@ -491,7 +491,7 @@
   1.153    by (simp add: refl_on_def)
   1.154  
   1.155  lemma antisym_Id: "antisym Id"
   1.156 -  -- {* A strange result, since @{text Id} is also symmetric. *}
   1.157 +  -- \<open>A strange result, since @{text Id} is also symmetric.\<close>
   1.158    by (simp add: antisym_def)
   1.159  
   1.160  lemma sym_Id: "sym Id"
   1.161 @@ -513,7 +513,7 @@
   1.162    by (simp add: total_on_def)
   1.163  
   1.164  
   1.165 -subsubsection {* Diagonal: identity over a set *}
   1.166 +subsubsection \<open>Diagonal: identity over a set\<close>
   1.167  
   1.168  definition Id_on  :: "'a set \<Rightarrow> 'a rel"
   1.169  where
   1.170 @@ -530,7 +530,7 @@
   1.171  
   1.172  lemma Id_onE [elim!]:
   1.173    "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   1.174 -  -- {* The general elimination rule. *}
   1.175 +  -- \<open>The general elimination rule.\<close>
   1.176    by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
   1.177  
   1.178  lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
   1.179 @@ -559,7 +559,7 @@
   1.180    by (unfold single_valued_def) blast
   1.181  
   1.182  
   1.183 -subsubsection {* Composition *}
   1.184 +subsubsection \<open>Composition\<close>
   1.185  
   1.186  inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
   1.187    for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
   1.188 @@ -570,10 +570,10 @@
   1.189  
   1.190  lemmas relcomppI = relcompp.intros
   1.191  
   1.192 -text {*
   1.193 +text \<open>
   1.194    For historic reasons, the elimination rules are not wholly corresponding.
   1.195    Feel free to consolidate this.
   1.196 -*}
   1.197 +\<close>
   1.198  
   1.199  inductive_cases relcompEpair: "(a, c) \<in> r O s"
   1.200  inductive_cases relcomppE [elim!]: "(r OO s) a c"
   1.201 @@ -677,7 +677,7 @@
   1.202  by blast
   1.203  
   1.204  
   1.205 -subsubsection {* Converse *}
   1.206 +subsubsection \<open>Converse\<close>
   1.207  
   1.208  inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^-1)" [1000] 999)
   1.209    for r :: "('a \<times> 'b) set"
   1.210 @@ -710,7 +710,7 @@
   1.211    by (fact converseD [to_pred])
   1.212  
   1.213  lemma converseE [elim!]:
   1.214 -  -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   1.215 +  -- \<open>More general than @{text converseD}, as it ``splits'' the member of the relation.\<close>
   1.216    "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
   1.217    by (cases yx) (simp, erule converse.cases, iprover)
   1.218  
   1.219 @@ -826,7 +826,7 @@
   1.220    by (simp add: set_eq_iff)
   1.221  
   1.222  
   1.223 -subsubsection {* Domain, range and field *}
   1.224 +subsubsection \<open>Domain, range and field\<close>
   1.225  
   1.226  inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set"
   1.227    for r :: "('a \<times> 'b) set"
   1.228 @@ -980,7 +980,7 @@
   1.229    by blast
   1.230  
   1.231  
   1.232 -subsubsection {* Image of a set under a relation *}
   1.233 +subsubsection \<open>Image of a set under a relation\<close>
   1.234  
   1.235  definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90)
   1.236  where
   1.237 @@ -1003,7 +1003,7 @@
   1.238    by (unfold Image_def) (iprover elim!: CollectE bexE)
   1.239  
   1.240  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   1.241 -  -- {* This version's more effective when we already have the required @{text a} *}
   1.242 +  -- \<open>This version's more effective when we already have the required @{text a}\<close>
   1.243    by blast
   1.244  
   1.245  lemma Image_empty [simp]: "R``{} = {}"
   1.246 @@ -1032,7 +1032,7 @@
   1.247    by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.248  
   1.249  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   1.250 -  -- {* NOT suitable for rewriting *}
   1.251 +  -- \<open>NOT suitable for rewriting\<close>
   1.252    by blast
   1.253  
   1.254  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
   1.255 @@ -1047,7 +1047,7 @@
   1.256  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
   1.257    by blast
   1.258  
   1.259 -text{*Converse inclusion requires some assumptions*}
   1.260 +text\<open>Converse inclusion requires some assumptions\<close>
   1.261  lemma Image_INT_eq:
   1.262       "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
   1.263  apply (rule equalityI)
   1.264 @@ -1067,7 +1067,7 @@
   1.265  lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
   1.266    by auto
   1.267  
   1.268 -subsubsection {* Inverse image *}
   1.269 +subsubsection \<open>Inverse image\<close>
   1.270  
   1.271  definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
   1.272  where
   1.273 @@ -1099,7 +1099,7 @@
   1.274    by (simp add: inv_imagep_def)
   1.275  
   1.276  
   1.277 -subsubsection {* Powerset *}
   1.278 +subsubsection \<open>Powerset\<close>
   1.279  
   1.280  definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   1.281  where
   1.282 @@ -1110,7 +1110,7 @@
   1.283  
   1.284  lemmas Powp_mono [mono] = Pow_mono [to_pred]
   1.285  
   1.286 -subsubsection {* Expressing relation operations via @{const Finite_Set.fold} *}
   1.287 +subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close>
   1.288  
   1.289  lemma Id_on_fold:
   1.290    assumes "finite A"
   1.291 @@ -1152,7 +1152,7 @@
   1.292    qed
   1.293    have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI)
   1.294    show ?thesis unfolding *
   1.295 -  using `finite S` by (induct S) (auto split: prod.split)
   1.296 +  using \<open>finite S\<close> by (induct S) (auto split: prod.split)
   1.297  qed
   1.298  
   1.299  lemma insert_relcomp_fold: