moved diag (diagonal relation) from Univ to Relation
authorpaulson
Fri Nov 27 10:40:29 1998 +0100 (1998-11-27)
changeset 5978fa2c2dd74f8c
parent 5977 9f0c8869cf71
child 5979 11cbf236ca16
moved diag (diagonal relation) from Univ to Relation
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Univ.ML
src/HOL/Univ.thy
     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.4  Addsimps [pair_in_Id_conv];
     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.26 +AddSIs [diagI];
    1.27 +AddSEs [diagE];
    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.44  Addsimps [Domain_Id];
    1.45  
    1.46 +Goal "Domain (diag A) = A";
    1.47 +by Auto_tac;
    1.48 +qed "Domain_diag";
    1.49 +Addsimps [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.31 +AddSIs [uprodI, dprodI];
    3.32 +AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
    3.33 +AddSEs [uprodE, dprodE, usumE, dsumE];
    3.34  
    3.35 -AddSIs [diagI, uprodI, dprodI];
    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  
    3.67 -Addsimps [Domain_diag, Domain_dprod, Domain_dsum];
    3.68 +Addsimps [Domain_dprod, Domain_dsum];
     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