author paulson Fri Nov 27 10:40:29 1998 +0100 (1998-11-27) changeset 5978 fa2c2dd74f8c parent 5977 9f0c8869cf71 child 5979 11cbf236ca16
moved diag (diagonal relation) from Univ to Relation
 src/HOL/Relation.ML file | annotate | diff | revisions src/HOL/Relation.thy file | annotate | diff | revisions src/HOL/Univ.ML file | annotate | diff | revisions src/HOL/Univ.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Relation.ML	Thu Nov 26 17:40:10 1998 +0100
1.2 +++ b/src/HOL/Relation.ML	Fri Nov 27 10:40:29 1998 +0100
1.3 @@ -26,6 +26,38 @@
1.5
1.6
1.7 +(** Diagonal relation: indentity restricted to some set **)
1.8 +
1.9 +(*** Equality : the diagonal relation ***)
1.10 +
1.11 +Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
1.12 +by (Blast_tac 1);
1.13 +qed "diag_eqI";
1.14 +
1.15 +val diagI = refl RS diag_eqI |> standard;
1.16 +
1.17 +(*The general elimination rule*)
1.18 +val major::prems = Goalw [diag_def]
1.19 +    "[| c : diag(A);  \
1.20 +\       !!x y. [| x:A;  c = (x,x) |] ==> P \
1.21 +\    |] ==> P";
1.22 +by (rtac (major RS UN_E) 1);
1.23 +by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
1.24 +qed "diagE";
1.25 +
1.28 +
1.29 +Goal "((x,y) : diag A) = (x=y & x : A)";
1.30 +by (Blast_tac 1);
1.31 +qed "diag_iff";
1.32 +
1.33 +Goal "diag(A) <= A Times A";
1.34 +by (Blast_tac 1);
1.35 +qed "diag_subset_Sigma";
1.36 +
1.37 +
1.38 +
1.39  (** Composition of two relations **)
1.40
1.41  Goalw [comp_def]
1.42 @@ -152,6 +184,11 @@
1.43  qed "Domain_Id";
1.45
1.46 +Goal "Domain (diag A) = A";
1.47 +by Auto_tac;
1.48 +qed "Domain_diag";
1.50 +
1.51  Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
1.52  by (Blast_tac 1);
1.53  qed "Domain_Un_eq";
```
```     2.1 --- a/src/HOL/Relation.thy	Thu Nov 26 17:40:10 1998 +0100
2.2 +++ b/src/HOL/Relation.thy	Fri Nov 27 10:40:29 1998 +0100
2.3 @@ -5,22 +5,34 @@
2.4  *)
2.5
2.6  Relation = Prod +
2.7 +
2.8  consts
2.9 -    Id          :: "('a * 'a)set"               (*the identity relation*)
2.10 -    O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
2.11 -    converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
2.12 -    "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
2.13 -    Domain      :: "('a*'b) set => 'a set"
2.14 -    Range       :: "('a*'b) set => 'b set"
2.15 -    trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
2.16 -    Univalent   :: "('a * 'b)set => bool"
2.17 +  O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
2.18 +  converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
2.19 +  "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
2.20 +
2.21  defs
2.22 -    Id_def        "Id == {p. ? x. p = (x,x)}"
2.23 -    comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
2.24 -    converse_def   "r^-1 == {(y,x). (x,y):r}"
2.25 -    Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
2.26 -    Range_def     "Range(r) == Domain(r^-1)"
2.27 -    Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
2.28 -    trans_def     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
2.29 -    Univalent_def "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
2.30 +  comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
2.31 +  converse_def  "r^-1 == {(y,x). (x,y):r}"
2.32 +  Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
2.33 +
2.34 +constdefs
2.35 +  Id          :: "('a * 'a)set"               (*the identity relation*)
2.36 +      "Id == {p. ? x. p = (x,x)}"
2.37 +
2.38 +  diag   :: "'a set => ('a * 'a)set"
2.39 +    "diag(A) == UN x:A. {(x,x)}"
2.40 +
2.41 +  Domain      :: "('a*'b) set => 'a set"
2.42 +    "Domain(r) == {x. ? y. (x,y):r}"
2.43 +
2.44 +  Range       :: "('a*'b) set => 'b set"
2.45 +    "Range(r) == Domain(r^-1)"
2.46 +
2.47 +  trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
2.48 +    "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
2.49 +
2.50 +  Univalent   :: "('a * 'b)set => bool"
2.51 +    "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
2.52 +
2.53  end
```
```     3.1 --- a/src/HOL/Univ.ML	Thu Nov 26 17:40:10 1998 +0100
3.2 +++ b/src/HOL/Univ.ML	Fri Nov 27 10:40:29 1998 +0100
3.3 @@ -465,23 +465,6 @@
3.4  qed "In1_UN1";
3.5
3.6
3.7 -(*** Equality : the diagonal relation ***)
3.8 -
3.9 -Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
3.10 -by (Blast_tac 1);
3.11 -qed "diag_eqI";
3.12 -
3.13 -val diagI = refl RS diag_eqI |> standard;
3.14 -
3.15 -(*The general elimination rule*)
3.16 -val major::prems = Goalw [diag_def]
3.17 -    "[| c : diag(A);  \
3.18 -\       !!x y. [| x:A;  c = (x,x) |] ==> P \
3.19 -\    |] ==> P";
3.20 -by (rtac (major RS UN_E) 1);
3.21 -by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
3.22 -qed "diagE";
3.23 -
3.24  (*** Equality for Cartesian Product ***)
3.25
3.26  Goalw [dprod_def]
3.27 @@ -520,10 +503,10 @@
3.28  by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
3.29  qed "dsumE";
3.30
3.32 +AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
3.33 +AddSEs [uprodE, dprodE, usumE, dsumE];
3.34
3.36 -AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
3.37 -AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
3.38
3.39  (*** Monotonicity ***)
3.40
3.41 @@ -538,10 +521,6 @@
3.42
3.43  (*** Bounding theorems ***)
3.44
3.45 -Goal "diag(A) <= A Times A";
3.46 -by (Blast_tac 1);
3.47 -qed "diag_subset_Sigma";
3.48 -
3.49  Goal "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
3.50  by (Blast_tac 1);
3.51  qed "dprod_Sigma";
3.52 @@ -564,10 +543,6 @@
3.53
3.54  (*** Domain ***)
3.55
3.56 -Goal "Domain (diag A) = A";
3.57 -by Auto_tac;
3.58 -qed "Domain_diag";
3.59 -
3.60  Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)";
3.61  by Auto_tac;
3.62  qed "Domain_dprod";
3.63 @@ -576,4 +551,4 @@
3.64  by Auto_tac;
3.65  qed "Domain_dsum";
3.66
```
```     4.1 --- a/src/HOL/Univ.thy	Thu Nov 26 17:40:10 1998 +0100
4.2 +++ b/src/HOL/Univ.thy	Fri Nov 27 10:40:29 1998 +0100
4.3 @@ -42,7 +42,6 @@
4.4    Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
4.5    Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
4.6
4.7 -  diag   :: "'a set => ('a * 'a)set"
4.8    "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
4.9             => ('a item * 'a item)set" (infixr 80)
4.10    "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
4.11 @@ -88,13 +87,11 @@
4.12                                | (? y . M = In1(y) & u = d(y))"
4.13
4.14
4.15 -  (** diagonal sets and equality for the "universe" **)
4.16 -
4.17 -  diag_def   "diag(A) == UN x:A. {(x,x)}"
4.18 +  (** equality for the "universe" **)
4.19
4.20    dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
4.21
4.22    dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
4.23 -                       (UN (y,y'):s. {(In1(y),In1(y'))})"
4.24 +                        (UN (y,y'):s. {(In1(y),In1(y'))})"
4.25
4.26  end
```