author haftmann Thu Oct 13 22:56:19 2011 +0200 (2011-10-13) changeset 45137 6e422d180de8 parent 45136 2afb928c71ca child 45138 ba618e9288b8
modernized definitions
 src/HOL/Relation.thy file | annotate | diff | revisions src/HOL/Transitive_Closure.thy file | annotate | diff | revisions src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Relation.thy	Thu Oct 13 22:50:35 2011 +0200
1.2 +++ b/src/HOL/Relation.thy	Thu Oct 13 22:56:19 2011 +0200
1.3 @@ -14,7 +14,7 @@
1.4  definition
1.5    converse :: "('a * 'b) set => ('b * 'a) set"
1.6      ("(_^-1)" [1000] 999) where
1.7 -  "r^-1 == {(y, x). (x, y) : r}"
1.8 +  "r^-1 = {(y, x). (x, y) : r}"
1.9
1.10  notation (xsymbols)
1.11    converse  ("(_\<inverse>)" [1000] 999)
1.12 @@ -22,70 +22,70 @@
1.13  definition
1.14    rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
1.15      (infixr "O" 75) where
1.16 -  "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
1.17 +  "r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}"
1.18
1.19  definition
1.20    Image :: "[('a * 'b) set, 'a set] => 'b set"
1.21      (infixl "``" 90) where
1.22 -  "r `` s == {y. EX x:s. (x,y):r}"
1.23 +  "r `` s = {y. EX x:s. (x,y):r}"
1.24
1.25  definition
1.26    Id :: "('a * 'a) set" where -- {* the identity relation *}
1.27 -  "Id == {p. EX x. p = (x,x)}"
1.28 +  "Id = {p. EX x. p = (x,x)}"
1.29
1.30  definition
1.31    Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
1.32 -  "Id_on A == \<Union>x\<in>A. {(x,x)}"
1.33 +  "Id_on A = (\<Union>x\<in>A. {(x,x)})"
1.34
1.35  definition
1.36    Domain :: "('a * 'b) set => 'a set" where
1.37 -  "Domain r == {x. EX y. (x,y):r}"
1.38 +  "Domain r = {x. EX y. (x,y):r}"
1.39
1.40  definition
1.41    Range  :: "('a * 'b) set => 'b set" where
1.42 -  "Range r == Domain(r^-1)"
1.43 +  "Range r = Domain(r^-1)"
1.44
1.45  definition
1.46    Field :: "('a * 'a) set => 'a set" where
1.47 -  "Field r == Domain r \<union> Range r"
1.48 +  "Field r = Domain r \<union> Range r"
1.49
1.50  definition
1.51    refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
1.52 -  "refl_on A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
1.53 +  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
1.54
1.55  abbreviation
1.56    refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
1.57 -  "refl == refl_on UNIV"
1.58 +  "refl \<equiv> refl_on UNIV"
1.59
1.60  definition
1.61    sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
1.62 -  "sym r == ALL x y. (x,y): r --> (y,x): r"
1.63 +  "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
1.64
1.65  definition
1.66    antisym :: "('a * 'a) set => bool" where -- {* antisymmetry predicate *}
1.67 -  "antisym r == ALL x y. (x,y):r --> (y,x):r --> x=y"
1.68 +  "antisym r \<longleftrightarrow> (ALL x y. (x,y):r --> (y,x):r --> x=y)"
1.69
1.70  definition
1.71    trans :: "('a * 'a) set => bool" where -- {* transitivity predicate *}
1.72 -  "trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.73 +  "trans r \<longleftrightarrow> (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.74
1.75  definition
1.76 -irrefl :: "('a * 'a) set => bool" where
1.77 -"irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
1.78 +  irrefl :: "('a * 'a) set => bool" where
1.79 +  "irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)"
1.80
1.81  definition
1.82 -total_on :: "'a set => ('a * 'a) set => bool" where
1.83 -"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"
1.84 +  total_on :: "'a set => ('a * 'a) set => bool" where
1.85 +  "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)"
1.86
1.87  abbreviation "total \<equiv> total_on UNIV"
1.88
1.89  definition
1.90    single_valued :: "('a * 'b) set => bool" where
1.91 -  "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
1.92 +  "single_valued r \<longleftrightarrow> (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))"
1.93
1.94  definition
1.95    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
1.96 -  "inv_image r f == {(x, y). (f x, f y) : r}"
1.97 +  "inv_image r f = {(x, y). (f x, f y) : r}"
1.98
1.99
1.100  subsection {* The identity relation *}
```
```     2.1 --- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:50:35 2011 +0200
2.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:56:19 2011 +0200
2.3 @@ -44,11 +44,11 @@
2.4
2.5  abbreviation
2.6    reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
2.7 -  "r^== == sup r op ="
2.8 +  "r^== \<equiv> sup r op ="
2.9
2.10  abbreviation
2.11    reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
2.12 -  "r^= == r \<union> Id"
2.13 +  "r^= \<equiv> r \<union> Id"
2.14
2.15  notation (xsymbols)
2.16    rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
```
```     3.1 --- a/src/HOL/Wellfounded.thy	Thu Oct 13 22:50:35 2011 +0200
3.2 +++ b/src/HOL/Wellfounded.thy	Thu Oct 13 22:56:19 2011 +0200
3.3 @@ -15,10 +15,10 @@
3.4  subsection {* Basic Definitions *}
3.5
3.6  definition wf :: "('a * 'a) set => bool" where
3.7 -  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
3.8 +  "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
3.9
3.10  definition wfP :: "('a => 'a => bool) => bool" where
3.11 -  "wfP r == wf {(x, y). r x y}"
3.12 +  "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
3.13
3.14  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
3.15    by (simp add: wfP_def)
3.16 @@ -382,10 +382,10 @@
3.17  subsection {* Acyclic relations *}
3.18
3.19  definition acyclic :: "('a * 'a) set => bool" where
3.20 -  "acyclic r == !x. (x,x) ~: r^+"
3.21 +  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
3.22
3.23  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
3.24 -  "acyclicP r == acyclic {(x, y). r x y}"
3.25 +  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
3.26
3.27  lemma acyclic_irrefl:
3.28    "acyclic r \<longleftrightarrow> irrefl (r^+)"
3.29 @@ -515,11 +515,11 @@
3.30
3.31  abbreviation
3.32    termip :: "('a => 'a => bool) => 'a => bool" where
3.33 -  "termip r == accp (r\<inverse>\<inverse>)"
3.34 +  "termip r \<equiv> accp (r\<inverse>\<inverse>)"
3.35
3.36  abbreviation
3.37    termi :: "('a * 'a) set => 'a set" where
3.38 -  "termi r == acc (r\<inverse>)"
3.39 +  "termi r \<equiv> acc (r\<inverse>)"
3.40
3.41  lemmas accpI = accp.accI
3.42
3.43 @@ -672,7 +672,7 @@
3.44  text {* Measure functions into @{typ nat} *}
3.45
3.46  definition measure :: "('a => nat) => ('a * 'a)set"
3.47 -where "measure == inv_image less_than"
3.48 +where "measure = inv_image less_than"
3.49
3.50  lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
3.51    by (simp add:measure_def)
3.52 @@ -735,7 +735,7 @@
3.53  text {* proper subset relation on finite sets *}
3.54
3.55  definition finite_psubset  :: "('a set * 'a set) set"
3.56 -where "finite_psubset == {(A,B). A < B & finite B}"
3.57 +where "finite_psubset = {(A,B). A < B & finite B}"
3.58
3.59  lemma wf_finite_psubset[simp]: "wf(finite_psubset)"
3.60  apply (unfold finite_psubset_def)
```