# HG changeset patch
# User haftmann
# Date 1318539379 -7200
# Node ID 6e422d180de80a9cdd5012fbac9885ce39e699e0
# Parent  2afb928c71ca8545c410f75163a1e1c09bbeda09
modernized definitions

diff -r 2afb928c71ca -r 6e422d180de8 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 13 22:50:35 2011 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 13 22:56:19 2011 +0200
@@ -14,7 +14,7 @@
 definition
   converse :: "('a * 'b) set => ('b * 'a) set"
     ("(_^-1)" [1000] 999) where
-  "r^-1 == {(y, x). (x, y) : r}"
+  "r^-1 = {(y, x). (x, y) : r}"
 
 notation (xsymbols)
   converse  ("(_\<inverse>)" [1000] 999)
@@ -22,70 +22,70 @@
 definition
   rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
     (infixr "O" 75) where
-  "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
+  "r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}"
 
 definition
   Image :: "[('a * 'b) set, 'a set] => 'b set"
     (infixl "``" 90) where
-  "r `` s == {y. EX x:s. (x,y):r}"
+  "r `` s = {y. EX x:s. (x,y):r}"
 
 definition
   Id :: "('a * 'a) set" where -- {* the identity relation *}
-  "Id == {p. EX x. p = (x,x)}"
+  "Id = {p. EX x. p = (x,x)}"
 
 definition
   Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
-  "Id_on A == \<Union>x\<in>A. {(x,x)}"
+  "Id_on A = (\<Union>x\<in>A. {(x,x)})"
 
 definition
   Domain :: "('a * 'b) set => 'a set" where
-  "Domain r == {x. EX y. (x,y):r}"
+  "Domain r = {x. EX y. (x,y):r}"
 
 definition
   Range  :: "('a * 'b) set => 'b set" where
-  "Range r == Domain(r^-1)"
+  "Range r = Domain(r^-1)"
 
 definition
   Field :: "('a * 'a) set => 'a set" where
-  "Field r == Domain r \<union> Range r"
+  "Field r = Domain r \<union> Range r"
 
 definition
   refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
-  "refl_on A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
+  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
 
 abbreviation
   refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
-  "refl == refl_on UNIV"
+  "refl \<equiv> refl_on UNIV"
 
 definition
   sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
-  "sym r == ALL x y. (x,y): r --> (y,x): r"
+  "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
 
 definition
   antisym :: "('a * 'a) set => bool" where -- {* antisymmetry predicate *}
-  "antisym r == ALL x y. (x,y):r --> (y,x):r --> x=y"
+  "antisym r \<longleftrightarrow> (ALL x y. (x,y):r --> (y,x):r --> x=y)"
 
 definition
   trans :: "('a * 'a) set => bool" where -- {* transitivity predicate *}
-  "trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
+  "trans r \<longleftrightarrow> (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
 
 definition
-irrefl :: "('a * 'a) set => bool" where
-"irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
+  irrefl :: "('a * 'a) set => bool" where
+  "irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)"
 
 definition
-total_on :: "'a set => ('a * 'a) set => bool" where
-"total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
+  total_on :: "'a set => ('a * 'a) set => bool" where
+  "total_on A r \<longleftrightarrow> (\<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r)"
 
 abbreviation "total \<equiv> total_on UNIV"
 
 definition
   single_valued :: "('a * 'b) set => bool" where
-  "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
+  "single_valued r \<longleftrightarrow> (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))"
 
 definition
   inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
-  "inv_image r f == {(x, y). (f x, f y) : r}"
+  "inv_image r f = {(x, y). (f x, f y) : r}"
 
 
 subsection {* The identity relation *}
diff -r 2afb928c71ca -r 6e422d180de8 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:50:35 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:56:19 2011 +0200
@@ -44,11 +44,11 @@
 
 abbreviation
   reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
-  "r^== == sup r op ="
+  "r^== \<equiv> sup r op ="
 
 abbreviation
   reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
-  "r^= == r \<union> Id"
+  "r^= \<equiv> r \<union> Id"
 
 notation (xsymbols)
   rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
diff -r 2afb928c71ca -r 6e422d180de8 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Oct 13 22:50:35 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Oct 13 22:56:19 2011 +0200
@@ -15,10 +15,10 @@
 subsection {* Basic Definitions *}
 
 definition wf :: "('a * 'a) set => bool" where
-  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
+  "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
 
 definition wfP :: "('a => 'a => bool) => bool" where
-  "wfP r == wf {(x, y). r x y}"
+  "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
 
 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   by (simp add: wfP_def)
@@ -382,10 +382,10 @@
 subsection {* Acyclic relations *}
 
 definition acyclic :: "('a * 'a) set => bool" where
-  "acyclic r == !x. (x,x) ~: r^+"
+  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
 
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
-  "acyclicP r == acyclic {(x, y). r x y}"
+  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
 
 lemma acyclic_irrefl:
   "acyclic r \<longleftrightarrow> irrefl (r^+)"
@@ -515,11 +515,11 @@
 
 abbreviation
   termip :: "('a => 'a => bool) => 'a => bool" where
-  "termip r == accp (r\<inverse>\<inverse>)"
+  "termip r \<equiv> accp (r\<inverse>\<inverse>)"
 
 abbreviation
   termi :: "('a * 'a) set => 'a set" where
-  "termi r == acc (r\<inverse>)"
+  "termi r \<equiv> acc (r\<inverse>)"
 
 lemmas accpI = accp.accI
 
@@ -672,7 +672,7 @@
 text {* Measure functions into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"
-where "measure == inv_image less_than"
+where "measure = inv_image less_than"
 
 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   by (simp add:measure_def)
@@ -735,7 +735,7 @@
 text {* proper subset relation on finite sets *}
 
 definition finite_psubset  :: "('a set * 'a set) set"
-where "finite_psubset == {(A,B). A < B & finite B}"
+where "finite_psubset = {(A,B). A < B & finite B}"
 
 lemma wf_finite_psubset[simp]: "wf(finite_psubset)"
 apply (unfold finite_psubset_def)