moved inv_image to Relation
authoroheimb
Thu Feb 15 16:00:40 2001 +0100 (2001-02-15)
changeset 11136e34e7f6d9b57
parent 11135 8fd0dea26286
child 11137 9265b6415d76
moved inv_image to Relation
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/Relation.ML	Thu Feb 15 16:00:38 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Thu Feb 15 16:00:40 2001 +0100
     1.3 @@ -468,3 +468,13 @@
     1.4  by (atac 1);
     1.5  by (atac 1);
     1.6  qed "fun_rel_comp_unique";
     1.7 +
     1.8 +
     1.9 +section "inverse image";
    1.10 +
    1.11 +Goalw [trans_def,inv_image_def]
    1.12 +    "!!r. trans r ==> trans (inv_image r f)";
    1.13 +by (Simp_tac 1);
    1.14 +by (Blast_tac 1);
    1.15 +qed "trans_inv_image";
    1.16 +
     2.1 --- a/src/HOL/Relation.thy	Thu Feb 15 16:00:38 2001 +0100
     2.2 +++ b/src/HOL/Relation.thy	Thu Feb 15 16:00:40 2001 +0100
     2.3 @@ -13,47 +13,50 @@
     2.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
     2.5  
     2.6  constdefs
     2.7 -  comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
     2.8 +  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     2.9      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    2.10  
    2.11 -  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
    2.12 +  Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
    2.13      "r `` s == {y. ? x:s. (x,y):r}"
    2.14  
    2.15 -  Id    :: "('a * 'a)set"                            (*the identity relation*)
    2.16 +  Id    :: "('a * 'a) set"                            (*the identity relation*)
    2.17      "Id == {p. ? x. p = (x,x)}"
    2.18  
    2.19 -  diag  :: "'a set => ('a * 'a)set"          (*diagonal: identity over a set*)
    2.20 +  diag  :: "'a set => ('a * 'a) set"          (*diagonal: identity over a set*)
    2.21      "diag(A) == UN x:A. {(x,x)}"
    2.22    
    2.23 -  Domain :: "('a*'b) set => 'a set"
    2.24 +  Domain :: "('a * 'b) set => 'a set"
    2.25      "Domain(r) == {x. ? y. (x,y):r}"
    2.26  
    2.27 -  Range  :: "('a*'b) set => 'b set"
    2.28 +  Range  :: "('a * 'b) set => 'b set"
    2.29      "Range(r) == Domain(r^-1)"
    2.30  
    2.31 -  Field :: "('a*'a)set=>'a set"
    2.32 +  Field :: "('a * 'a) set => 'a set"
    2.33      "Field r == Domain r Un Range r"
    2.34  
    2.35 -  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    2.36 +  refl   :: "['a set, ('a * 'a) set] => bool" (*reflexivity over a set*)
    2.37      "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    2.38  
    2.39 -  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
    2.40 +  sym    :: "('a * 'a) set => bool"             (*symmetry predicate*)
    2.41      "sym(r) == ALL x y. (x,y): r --> (y,x): r"
    2.42  
    2.43 -  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
    2.44 +  antisym:: "('a * 'a) set => bool"          (*antisymmetry predicate*)
    2.45      "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
    2.46  
    2.47 -  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
    2.48 +  trans  :: "('a * 'a) set => bool"          (*transitivity predicate*)
    2.49      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    2.50  
    2.51 -  single_valued :: "('a * 'b)set => bool"
    2.52 +  single_valued :: "('a * 'b) set => bool"
    2.53      "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    2.54  
    2.55    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    2.56      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
    2.57  
    2.58 +  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
    2.59 +    "inv_image r f == {(x,y). (f(x), f(y)) : r}"
    2.60 +
    2.61  syntax
    2.62 -  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
    2.63 +  reflexive :: "('a * 'a) set => bool"       (*reflexivity over a type*)
    2.64  translations
    2.65    "reflexive" == "refl UNIV"
    2.66  
     3.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:38 2001 +0100
     3.2 +++ b/src/HOL/Wellfounded_Relations.thy	Thu Feb 15 16:00:40 2001 +0100
     3.3 @@ -21,9 +21,6 @@
     3.4   less_than :: "(nat*nat)set"
     3.5  "less_than == trancl pred_nat"
     3.6  
     3.7 - inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
     3.8 -"inv_image r f == {(x,y). (f(x), f(y)) : r}"
     3.9 -
    3.10   measure   :: "('a => nat) => ('a * 'a)set"
    3.11  "measure == inv_image less_than"
    3.12