--- a/src/HOL/Relation.thy Mon Jul 04 19:46:20 2016 +0200
+++ b/src/HOL/Relation.thy Mon Jul 04 19:46:20 2016 +0200
@@ -51,6 +51,7 @@
declare Sup2_E [elim!]
declare SUP2_E [elim!]
+
subsection \<open>Fundamental\<close>
subsubsection \<open>Relations as sets of pairs\<close>
@@ -141,6 +142,7 @@
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)"
by (simp add: fun_eq_iff)
+
subsection \<open>Properties of relations\<close>
subsubsection \<open>Reflexivity\<close>
@@ -161,7 +163,7 @@
"reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
by (simp add: refl_on_def reflp_def)
-lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
+lemma refl_onI [intro?]: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
by (unfold refl_on_def) (iprover intro!: ballI)
lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
@@ -173,7 +175,7 @@
lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
by (unfold refl_on_def) blast
-lemma reflpI:
+lemma reflpI [intro?]:
"(\<And>x. r x x) \<Longrightarrow> reflp r"
by (auto intro: refl_onI simp add: reflp_def)
@@ -182,7 +184,7 @@
obtains "r x x"
using assms by (auto dest: refl_onD simp add: reflp_def)
-lemma reflpD:
+lemma reflpD [dest?]:
assumes "reflp r"
shows "r x x"
using assms by (auto elim: reflpE)
@@ -222,6 +224,7 @@
lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
by(auto intro: reflpI dest: reflpD)
+
subsubsection \<open>Irreflexivity\<close>
definition irrefl :: "'a rel \<Rightarrow> bool"
@@ -236,11 +239,11 @@
"irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R"
by (simp add: irrefl_def irreflp_def)
-lemma irreflI:
+lemma irreflI [intro?]:
"(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
by (simp add: irrefl_def)
-lemma irreflpI:
+lemma irreflpI [intro?]:
"(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
by (fact irreflI [to_pred])
@@ -278,11 +281,11 @@
"symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
by (simp add: sym_def symp_def)
-lemma symI:
+lemma symI [intro?]:
"(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
by (unfold sym_def) iprover
-lemma sympI:
+lemma sympI [intro?]:
"(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
by (fact symI [to_pred])
@@ -296,12 +299,12 @@
obtains "r a b"
using assms by (rule symE [to_pred])
-lemma symD:
+lemma symD [dest?]:
assumes "sym r" and "(b, a) \<in> r"
shows "(a, b) \<in> r"
using assms by (rule symE)
-lemma sympD:
+lemma sympD [dest?]:
assumes "symp r" and "r b a"
shows "r a b"
using assms by (rule symD [to_pred])
@@ -346,14 +349,14 @@
"antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-where
+where -- \<open>FIXME proper logical operation\<close>
"antisymP r \<equiv> antisym {(x, y). r x y}"
-lemma antisymI:
+lemma antisymI [intro?]:
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
by (unfold antisym_def) iprover
-lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
+lemma antisymD [dest?]: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
by (unfold antisym_def) iprover
lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
@@ -365,6 +368,7 @@
lemma antisymP_equality [simp]: "antisymP op ="
by(auto intro: antisymI)
+
subsubsection \<open>Transitivity\<close>
definition trans :: "'a rel \<Rightarrow> bool"
@@ -379,15 +383,11 @@
"transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
by (simp add: trans_def transp_def)
-abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-where \<comment> \<open>FIXME drop\<close>
- "transP r \<equiv> trans {(x, y). r x y}"
-
-lemma transI:
+lemma transI [intro?]:
"(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
by (unfold trans_def) iprover
-lemma transpI:
+lemma transpI [intro?]:
"(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
by (fact transI [to_pred])
@@ -401,12 +401,12 @@
obtains "r x z"
using assms by (rule transE [to_pred])
-lemma transD:
+lemma transD [dest?]:
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
shows "(x, z) \<in> r"
using assms by (rule transE)
-lemma transpD:
+lemma transpD [dest?]:
assumes "transp r" and "r x y" and "r y z"
shows "r x z"
using assms by (rule transD [to_pred])
@@ -436,6 +436,7 @@
lemma transp_equality [simp]: "transp op ="
by(auto intro: transpI)
+
subsubsection \<open>Totality\<close>
definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
@@ -454,7 +455,8 @@
where
"single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
-abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+where -- \<open>FIXME proper logical operation\<close>
"single_valuedP r \<equiv> single_valued {(x, y). r x y}"
lemma single_valuedI:
@@ -518,6 +520,7 @@
lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
by force
+
subsubsection \<open>Diagonal: identity over a set\<close>
definition Id_on :: "'a set \<Rightarrow> 'a rel"
@@ -684,6 +687,7 @@
lemma OO_eq: "R OO op = = R"
by blast
+
subsubsection \<open>Converse\<close>
inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999)
@@ -838,8 +842,6 @@
where
DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r"
-abbreviation (input) "DomainP \<equiv> Domainp"
-
lemmas DomainPI = Domainp.DomainI
inductive_cases DomainE [elim!]: "a \<in> Domain r"
@@ -850,8 +852,6 @@
where
RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r"
-abbreviation (input) "RangeP \<equiv> Rangep"
-
lemmas RangePI = Rangep.RangeI
inductive_cases RangeE [elim!]: "b \<in> Range r"
@@ -1079,6 +1079,7 @@
lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
by auto
+
subsubsection \<open>Inverse image\<close>
definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
@@ -1122,6 +1123,7 @@
lemmas Powp_mono [mono] = Pow_mono [to_pred]
+
subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close>
lemma Id_on_fold:
@@ -1196,4 +1198,17 @@
(auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
cong: if_cong)
+text \<open>Misc\<close>
+
+abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+where \<comment> \<open>FIXME drop\<close>
+ "transP r \<equiv> trans {(x, y). r x y}"
+
+abbreviation (input)
+ "RangeP \<equiv> Rangep"
+
+abbreviation (input)
+ "DomainP \<equiv> Domainp"
+
+
end