# HG changeset patch
# User haftmann
# Date 1467654380 -7200
# Node ID 4c0cc2b356f0b1c04d8fe18c57d97c7819ad5848
# Parent  59803048b0e8adf425e1cc89302ad93c7831f157
default one-step rules for predicates on relations;
clarified status of legacy input abbreviations

diff -r 59803048b0e8 -r 4c0cc2b356f0 src/HOL/Relation.thy
--- 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