src/HOL/Relation.thy
changeset 46664 1f6c140f9c72
parent 46638 fc315796794e
child 46689 f559866a7aa2
     1.1 --- a/src/HOL/Relation.thy	Fri Feb 24 22:46:16 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Feb 24 22:46:44 2012 +0100
     1.3 @@ -1,15 +1,107 @@
     1.4  (*  Title:      HOL/Relation.thy
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   1996  University of Cambridge
     1.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     1.8  *)
     1.9  
    1.10 -header {* Relations *}
    1.11 +header {* Relations – as sets of pairs, and binary predicates *}
    1.12  
    1.13  theory Relation
    1.14  imports Datatype Finite_Set
    1.15  begin
    1.16  
    1.17 -subsection {* Definitions *}
    1.18 +notation
    1.19 +  bot ("\<bottom>") and
    1.20 +  top ("\<top>") and
    1.21 +  inf (infixl "\<sqinter>" 70) and
    1.22 +  sup (infixl "\<squnion>" 65) and
    1.23 +  Inf ("\<Sqinter>_" [900] 900) and
    1.24 +  Sup ("\<Squnion>_" [900] 900)
    1.25 +
    1.26 +syntax (xsymbols)
    1.27 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.28 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.29 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.30 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.31 +
    1.32 +
    1.33 +subsection {* Classical rules for reasoning on predicates *}
    1.34 +
    1.35 +declare predicate1D [Pure.dest?, dest?]
    1.36 +declare predicate2I [Pure.intro!, intro!]
    1.37 +declare predicate2D [Pure.dest, dest]
    1.38 +declare bot1E [elim!]
    1.39 +declare bot2E [elim!]
    1.40 +declare top1I [intro!]
    1.41 +declare top2I [intro!]
    1.42 +declare inf1I [intro!]
    1.43 +declare inf2I [intro!]
    1.44 +declare inf1E [elim!]
    1.45 +declare inf2E [elim!]
    1.46 +declare sup1I1 [intro?]
    1.47 +declare sup2I1 [intro?]
    1.48 +declare sup1I2 [intro?]
    1.49 +declare sup2I2 [intro?]
    1.50 +declare sup1E [elim!]
    1.51 +declare sup2E [elim!]
    1.52 +declare sup1CI [intro!]
    1.53 +declare sup2CI [intro!]
    1.54 +declare INF1_I [intro!]
    1.55 +declare INF2_I [intro!]
    1.56 +declare INF1_D [elim]
    1.57 +declare INF2_D [elim]
    1.58 +declare INF1_E [elim]
    1.59 +declare INF2_E [elim]
    1.60 +declare SUP1_I [intro]
    1.61 +declare SUP2_I [intro]
    1.62 +declare SUP1_E [elim!]
    1.63 +declare SUP2_E [elim!]
    1.64 +
    1.65 +
    1.66 +subsection {* Conversions between set and predicate relations *}
    1.67 +
    1.68 +lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    1.69 +  by (simp add: set_eq_iff fun_eq_iff)
    1.70 +
    1.71 +lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
    1.72 +  by (simp add: set_eq_iff fun_eq_iff)
    1.73 +
    1.74 +lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    1.75 +  by (simp add: subset_iff le_fun_def)
    1.76 +
    1.77 +lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    1.78 +  by (simp add: subset_iff le_fun_def)
    1.79 +
    1.80 +lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    1.81 +  by (auto simp add: fun_eq_iff)
    1.82 +
    1.83 +lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.84 +  by (auto simp add: fun_eq_iff)
    1.85 +
    1.86 +lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.87 +  by (simp add: inf_fun_def)
    1.88 +
    1.89 +lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
    1.90 +  by (simp add: inf_fun_def)
    1.91 +
    1.92 +lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    1.93 +  by (simp add: sup_fun_def)
    1.94 +
    1.95 +lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
    1.96 +  by (simp add: sup_fun_def)
    1.97 +
    1.98 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    1.99 +  by (simp add: INF_apply fun_eq_iff)
   1.100 +
   1.101 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   1.102 +  by (simp add: INF_apply fun_eq_iff)
   1.103 +
   1.104 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   1.105 +  by (simp add: SUP_apply fun_eq_iff)
   1.106 +
   1.107 +lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
   1.108 +  by (simp add: SUP_apply fun_eq_iff)
   1.109 +
   1.110 +
   1.111 +subsection {* Relations as sets of pairs *}
   1.112  
   1.113  type_synonym 'a rel = "('a * 'a) set"
   1.114  
   1.115 @@ -90,7 +182,7 @@
   1.116    "inv_image r f = {(x, y). (f x, f y) : r}"
   1.117  
   1.118  
   1.119 -subsection {* The identity relation *}
   1.120 +subsubsection {* The identity relation *}
   1.121  
   1.122  lemma IdI [intro]: "(a, a) : Id"
   1.123  by (simp add: Id_def)
   1.124 @@ -115,7 +207,7 @@
   1.125  by (simp add: trans_def)
   1.126  
   1.127  
   1.128 -subsection {* Diagonal: identity over a set *}
   1.129 +subsubsection {* Diagonal: identity over a set *}
   1.130  
   1.131  lemma Id_on_empty [simp]: "Id_on {} = {}"
   1.132  by (simp add: Id_on_def) 
   1.133 @@ -142,7 +234,7 @@
   1.134  by blast
   1.135  
   1.136  
   1.137 -subsection {* Composition of two relations *}
   1.138 +subsubsection {* Composition of two relations *}
   1.139  
   1.140  lemma rel_compI [intro]:
   1.141    "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
   1.142 @@ -194,7 +286,7 @@
   1.143  by auto
   1.144  
   1.145  
   1.146 -subsection {* Reflexivity *}
   1.147 +subsubsection {* Reflexivity *}
   1.148  
   1.149  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
   1.150  by (unfold refl_on_def) (iprover intro!: ballI)
   1.151 @@ -232,7 +324,8 @@
   1.152    "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
   1.153  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
   1.154  
   1.155 -subsection {* Antisymmetry *}
   1.156 +
   1.157 +subsubsection {* Antisymmetry *}
   1.158  
   1.159  lemma antisymI:
   1.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   1.161 @@ -251,7 +344,7 @@
   1.162  by (unfold antisym_def) blast
   1.163  
   1.164  
   1.165 -subsection {* Symmetry *}
   1.166 +subsubsection {* Symmetry *}
   1.167  
   1.168  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   1.169  by (unfold sym_def) iprover
   1.170 @@ -275,7 +368,7 @@
   1.171  by (rule symI) clarify
   1.172  
   1.173  
   1.174 -subsection {* Transitivity *}
   1.175 +subsubsection {* Transitivity *}
   1.176  
   1.177  lemma trans_join [code]:
   1.178    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
   1.179 @@ -300,7 +393,8 @@
   1.180  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
   1.181  unfolding antisym_def trans_def by blast
   1.182  
   1.183 -subsection {* Irreflexivity *}
   1.184 +
   1.185 +subsubsection {* Irreflexivity *}
   1.186  
   1.187  lemma irrefl_distinct [code]:
   1.188    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
   1.189 @@ -310,7 +404,7 @@
   1.190  by(simp add:irrefl_def)
   1.191  
   1.192  
   1.193 -subsection {* Totality *}
   1.194 +subsubsection {* Totality *}
   1.195  
   1.196  lemma total_on_empty[simp]: "total_on {} r"
   1.197  by(simp add:total_on_def)
   1.198 @@ -318,7 +412,8 @@
   1.199  lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
   1.200  by(simp add: total_on_def)
   1.201  
   1.202 -subsection {* Converse *}
   1.203 +
   1.204 +subsubsection {* Converse *}
   1.205  
   1.206  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   1.207  by (simp add: converse_def)
   1.208 @@ -383,7 +478,7 @@
   1.209  by (auto simp: total_on_def)
   1.210  
   1.211  
   1.212 -subsection {* Domain *}
   1.213 +subsubsection {* Domain *}
   1.214  
   1.215  declare Domain_def [no_atp]
   1.216  
   1.217 @@ -444,7 +539,7 @@
   1.218  by auto
   1.219  
   1.220  
   1.221 -subsection {* Range *}
   1.222 +subsubsection {* Range *}
   1.223  
   1.224  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   1.225  by (simp add: Domain_def Range_def)
   1.226 @@ -493,7 +588,7 @@
   1.227    by force
   1.228  
   1.229  
   1.230 -subsection {* Field *}
   1.231 +subsubsection {* Field *}
   1.232  
   1.233  lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   1.234  by(auto simp:Field_def Domain_def Range_def)
   1.235 @@ -514,7 +609,7 @@
   1.236  by(auto simp:Field_def)
   1.237  
   1.238  
   1.239 -subsection {* Image of a set under a relation *}
   1.240 +subsubsection {* Image of a set under a relation *}
   1.241  
   1.242  declare Image_def [no_atp]
   1.243  
   1.244 @@ -588,7 +683,7 @@
   1.245  by blast
   1.246  
   1.247  
   1.248 -subsection {* Single valued relations *}
   1.249 +subsubsection {* Single valued relations *}
   1.250  
   1.251  lemma single_valuedI:
   1.252    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   1.253 @@ -613,7 +708,7 @@
   1.254  by (unfold single_valued_def) blast
   1.255  
   1.256  
   1.257 -subsection {* Graphs given by @{text Collect} *}
   1.258 +subsubsection {* Graphs given by @{text Collect} *}
   1.259  
   1.260  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
   1.261  by auto
   1.262 @@ -625,7 +720,7 @@
   1.263  by auto
   1.264  
   1.265  
   1.266 -subsection {* Inverse image *}
   1.267 +subsubsection {* Inverse image *}
   1.268  
   1.269  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   1.270  by (unfold sym_def inv_image_def) blast
   1.271 @@ -643,7 +738,7 @@
   1.272  unfolding inv_image_def converse_def by auto
   1.273  
   1.274  
   1.275 -subsection {* Finiteness *}
   1.276 +subsubsection {* Finiteness *}
   1.277  
   1.278  lemma finite_converse [iff]: "finite (r^-1) = finite r"
   1.279    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   1.280 @@ -671,7 +766,7 @@
   1.281    done
   1.282  
   1.283  
   1.284 -subsection {* Miscellaneous *}
   1.285 +subsubsection {* Miscellaneous *}
   1.286  
   1.287  text {* Version of @{thm[source] lfp_induct} for binary relations *}
   1.288  
   1.289 @@ -683,4 +778,171 @@
   1.290  lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
   1.291  by auto
   1.292  
   1.293 +
   1.294 +subsection {* Relations as binary predicates *}
   1.295 +
   1.296 +subsubsection {* Composition *}
   1.297 +
   1.298 +inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   1.299 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
   1.300 +  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   1.301 +
   1.302 +inductive_cases pred_compE [elim!]: "(r OO s) a c"
   1.303 +
   1.304 +lemma pred_comp_rel_comp_eq [pred_set_conv]:
   1.305 +  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   1.306 +  by (auto simp add: fun_eq_iff)
   1.307 +
   1.308 +
   1.309 +subsubsection {* Converse *}
   1.310 +
   1.311 +inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   1.312 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.313 +  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   1.314 +
   1.315 +notation (xsymbols)
   1.316 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   1.317 +
   1.318 +lemma conversepD:
   1.319 +  assumes ab: "r^--1 a b"
   1.320 +  shows "r b a" using ab
   1.321 +  by cases simp
   1.322 +
   1.323 +lemma conversep_iff [iff]: "r^--1 a b = r b a"
   1.324 +  by (iprover intro: conversepI dest: conversepD)
   1.325 +
   1.326 +lemma conversep_converse_eq [pred_set_conv]:
   1.327 +  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   1.328 +  by (auto simp add: fun_eq_iff)
   1.329 +
   1.330 +lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   1.331 +  by (iprover intro: order_antisym conversepI dest: conversepD)
   1.332 +
   1.333 +lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.334 +  by (iprover intro: order_antisym conversepI pred_compI
   1.335 +    elim: pred_compE dest: conversepD)
   1.336 +
   1.337 +lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   1.338 +  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   1.339 +
   1.340 +lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   1.341 +  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   1.342 +
   1.343 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   1.344 +  by (auto simp add: fun_eq_iff)
   1.345 +
   1.346 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
   1.347 +  by (auto simp add: fun_eq_iff)
   1.348 +
   1.349 +
   1.350 +subsubsection {* Domain *}
   1.351 +
   1.352 +inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.353 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.354 +  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   1.355 +
   1.356 +inductive_cases DomainPE [elim!]: "DomainP r a"
   1.357 +
   1.358 +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   1.359 +  by (blast intro!: Orderings.order_antisym predicate1I)
   1.360 +
   1.361 +
   1.362 +subsubsection {* Range *}
   1.363 +
   1.364 +inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   1.365 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.366 +  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   1.367 +
   1.368 +inductive_cases RangePE [elim!]: "RangeP r b"
   1.369 +
   1.370 +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   1.371 +  by (blast intro!: Orderings.order_antisym predicate1I)
   1.372 +
   1.373 +
   1.374 +subsubsection {* Inverse image *}
   1.375 +
   1.376 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   1.377 +  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
   1.378 +
   1.379 +lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
   1.380 +  by (simp add: inv_image_def inv_imagep_def)
   1.381 +
   1.382 +lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   1.383 +  by (simp add: inv_imagep_def)
   1.384 +
   1.385 +
   1.386 +subsubsection {* Powerset *}
   1.387 +
   1.388 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.389 +  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
   1.390 +
   1.391 +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   1.392 +  by (auto simp add: Powp_def fun_eq_iff)
   1.393 +
   1.394 +lemmas Powp_mono [mono] = Pow_mono [to_pred]
   1.395 +
   1.396 +
   1.397 +subsubsection {* Properties of predicate relations *}
   1.398 +
   1.399 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.400 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
   1.401 +
   1.402 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.403 +  "transP r \<equiv> trans {(x, y). r x y}"
   1.404 +
   1.405 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.406 +  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   1.407 +
   1.408 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   1.409 +
   1.410 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.411 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
   1.412 +
   1.413 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.414 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   1.415 +
   1.416 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.417 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   1.418 +
   1.419 +lemma reflpI:
   1.420 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
   1.421 +  by (auto intro: refl_onI simp add: reflp_def)
   1.422 +
   1.423 +lemma reflpE:
   1.424 +  assumes "reflp r"
   1.425 +  obtains "r x x"
   1.426 +  using assms by (auto dest: refl_onD simp add: reflp_def)
   1.427 +
   1.428 +lemma sympI:
   1.429 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   1.430 +  by (auto intro: symI simp add: symp_def)
   1.431 +
   1.432 +lemma sympE:
   1.433 +  assumes "symp r" and "r x y"
   1.434 +  obtains "r y x"
   1.435 +  using assms by (auto dest: symD simp add: symp_def)
   1.436 +
   1.437 +lemma transpI:
   1.438 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   1.439 +  by (auto intro: transI simp add: transp_def)
   1.440 +  
   1.441 +lemma transpE:
   1.442 +  assumes "transp r" and "r x y" and "r y z"
   1.443 +  obtains "r x z"
   1.444 +  using assms by (auto dest: transD simp add: transp_def)
   1.445 +
   1.446 +no_notation
   1.447 +  bot ("\<bottom>") and
   1.448 +  top ("\<top>") and
   1.449 +  inf (infixl "\<sqinter>" 70) and
   1.450 +  sup (infixl "\<squnion>" 65) and
   1.451 +  Inf ("\<Sqinter>_" [900] 900) and
   1.452 +  Sup ("\<Squnion>_" [900] 900)
   1.453 +
   1.454 +no_syntax (xsymbols)
   1.455 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   1.456 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   1.457 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   1.458 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   1.459 +
   1.460  end