src/HOL/Relation.thy
changeset 61799 4cf66f21b764
parent 61630 608520e0e8e2
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Relation.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -57,11 +57,11 @@
     1.4  
     1.5  type_synonym 'a rel = "('a * 'a) set"
     1.6  
     1.7 -lemma subrelI: -- \<open>Version of @{thm [source] subsetI} for binary relations\<close>
     1.8 +lemma subrelI: \<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close>
     1.9    "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
    1.10    by auto
    1.11  
    1.12 -lemma lfp_induct2: -- \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
    1.13 +lemma lfp_induct2: \<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
    1.14    "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
    1.15      (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
    1.16    using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
    1.17 @@ -150,7 +150,7 @@
    1.18    "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
    1.19  
    1.20  abbreviation refl :: "'a rel \<Rightarrow> bool"
    1.21 -where -- \<open>reflexivity over a type\<close>
    1.22 +where \<comment> \<open>reflexivity over a type\<close>
    1.23    "refl \<equiv> refl_on UNIV"
    1.24  
    1.25  definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.26 @@ -380,7 +380,7 @@
    1.27    by (simp add: trans_def transp_def)
    1.28  
    1.29  abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.30 -where -- \<open>FIXME drop\<close>
    1.31 +where \<comment> \<open>FIXME drop\<close>
    1.32    "transP r \<equiv> trans {(x, y). r x y}"
    1.33  
    1.34  lemma transI:
    1.35 @@ -494,7 +494,7 @@
    1.36    by (simp add: refl_on_def)
    1.37  
    1.38  lemma antisym_Id: "antisym Id"
    1.39 -  -- \<open>A strange result, since @{text Id} is also symmetric.\<close>
    1.40 +  \<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close>
    1.41    by (simp add: antisym_def)
    1.42  
    1.43  lemma sym_Id: "sym Id"
    1.44 @@ -533,7 +533,7 @@
    1.45  
    1.46  lemma Id_onE [elim!]:
    1.47    "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.48 -  -- \<open>The general elimination rule.\<close>
    1.49 +  \<comment> \<open>The general elimination rule.\<close>
    1.50    by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
    1.51  
    1.52  lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
    1.53 @@ -715,7 +715,7 @@
    1.54    by (fact converseD [to_pred])
    1.55  
    1.56  lemma converseE [elim!]:
    1.57 -  -- \<open>More general than @{text converseD}, as it ``splits'' the member of the relation.\<close>
    1.58 +  \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close>
    1.59    "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
    1.60    by (cases yx) (simp, erule converse.cases, iprover)
    1.61  
    1.62 @@ -1008,7 +1008,7 @@
    1.63    by (unfold Image_def) (iprover elim!: CollectE bexE)
    1.64  
    1.65  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
    1.66 -  -- \<open>This version's more effective when we already have the required @{text a}\<close>
    1.67 +  \<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close>
    1.68    by blast
    1.69  
    1.70  lemma Image_empty [simp]: "R``{} = {}"
    1.71 @@ -1037,7 +1037,7 @@
    1.72    by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
    1.73  
    1.74  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
    1.75 -  -- \<open>NOT suitable for rewriting\<close>
    1.76 +  \<comment> \<open>NOT suitable for rewriting\<close>
    1.77    by blast
    1.78  
    1.79  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"