# HG changeset patch
# User oheimb
# Date 982249240 -3600
# Node ID e34e7f6d9b571e2c903d8e012c8044da368970cb
# Parent  8fd0dea26286eb8872eae54d0c0f5dbf04e67b14
moved inv_image to Relation

diff -r 8fd0dea26286 -r e34e7f6d9b57 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Feb 15 16:00:38 2001 +0100
+++ b/src/HOL/Relation.ML	Thu Feb 15 16:00:40 2001 +0100
@@ -468,3 +468,13 @@
 by (atac 1);
 by (atac 1);
 qed "fun_rel_comp_unique";
+
+
+section "inverse image";
+
+Goalw [trans_def,inv_image_def]
+    "!!r. trans r ==> trans (inv_image r f)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_inv_image";
+
diff -r 8fd0dea26286 -r e34e7f6d9b57 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Feb 15 16:00:38 2001 +0100
+++ b/src/HOL/Relation.thy	Thu Feb 15 16:00:40 2001 +0100
@@ -13,47 +13,50 @@
   converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
 
 constdefs
-  comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
+  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
 
-  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
+  Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
     "r `` s == {y. ? x:s. (x,y):r}"
 
-  Id    :: "('a * 'a)set"                            (*the identity relation*)
+  Id    :: "('a * 'a) set"                            (*the identity relation*)
     "Id == {p. ? x. p = (x,x)}"
 
-  diag  :: "'a set => ('a * 'a)set"          (*diagonal: identity over a set*)
+  diag  :: "'a set => ('a * 'a) set"          (*diagonal: identity over a set*)
     "diag(A) == UN x:A. {(x,x)}"
   
-  Domain :: "('a*'b) set => 'a set"
+  Domain :: "('a * 'b) set => 'a set"
     "Domain(r) == {x. ? y. (x,y):r}"
 
-  Range  :: "('a*'b) set => 'b set"
+  Range  :: "('a * 'b) set => 'b set"
     "Range(r) == Domain(r^-1)"
 
-  Field :: "('a*'a)set=>'a set"
+  Field :: "('a * 'a) set => 'a set"
     "Field r == Domain r Un Range r"
 
-  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
+  refl   :: "['a set, ('a * 'a) set] => bool" (*reflexivity over a set*)
     "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
 
-  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
+  sym    :: "('a * 'a) set => bool"             (*symmetry predicate*)
     "sym(r) == ALL x y. (x,y): r --> (y,x): r"
 
-  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
+  antisym:: "('a * 'a) set => bool"          (*antisymmetry predicate*)
     "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
 
-  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
+  trans  :: "('a * 'a) set => bool"          (*transitivity predicate*)
     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
 
-  single_valued :: "('a * 'b)set => bool"
+  single_valued :: "('a * 'b) set => bool"
     "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
 
   fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
     "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
 
+  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
+    "inv_image r f == {(x,y). (f(x), f(y)) : r}"
+
 syntax
-  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
+  reflexive :: "('a * 'a) set => bool"       (*reflexivity over a type*)
 translations
   "reflexive" == "refl UNIV"
 
diff -r 8fd0dea26286 -r e34e7f6d9b57 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:38 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:40 2001 +0100
@@ -21,9 +21,6 @@
  less_than :: "(nat*nat)set"
 "less_than == trancl pred_nat"
 
- inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
-"inv_image r f == {(x,y). (f(x), f(y)) : r}"
-
  measure   :: "('a => nat) => ('a * 'a)set"
 "measure == inv_image less_than"