modernized definitions
authorhaftmann
Thu Oct 13 22:56:19 2011 +0200 (2011-10-13)
changeset 451376e422d180de8
parent 45136 2afb928c71ca
child 45138 ba618e9288b8
modernized definitions
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     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)