src/HOL/Relation.ML
changeset 10797 028d22926a41
parent 10786 04ee73606993
child 10832 e33b47e4246d
     1.1 --- a/src/HOL/Relation.ML	Fri Jan 05 18:33:47 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Fri Jan 05 18:48:18 2001 +0100
     1.3 @@ -333,27 +333,27 @@
     1.4  
     1.5  overload_1st_set "Relation.Image";
     1.6  
     1.7 -Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
     1.8 +Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)";
     1.9  by (Blast_tac 1);
    1.10  qed "Image_iff";
    1.11  
    1.12 -Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
    1.13 +Goalw [Image_def] "r```{a} = {b. (a,b):r}";
    1.14  by (Blast_tac 1);
    1.15  qed "Image_singleton";
    1.16  
    1.17 -Goal "(b : r^^{a}) = ((a,b):r)";
    1.18 +Goal "(b : r```{a}) = ((a,b):r)";
    1.19  by (rtac (Image_iff RS trans) 1);
    1.20  by (Blast_tac 1);
    1.21  qed "Image_singleton_iff";
    1.22  
    1.23  AddIffs [Image_singleton_iff];
    1.24  
    1.25 -Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r^^A";
    1.26 +Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r```A";
    1.27  by (Blast_tac 1);
    1.28  qed "ImageI";
    1.29  
    1.30  val major::prems = Goalw [Image_def]
    1.31 -    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
    1.32 +    "[| b: r```A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
    1.33  by (rtac (major RS CollectE) 1);
    1.34  by (Clarify_tac 1);
    1.35  by (rtac (hd prems) 1);
    1.36 @@ -364,72 +364,72 @@
    1.37  AddSEs [ImageE];
    1.38  
    1.39  (*This version's more effective when we already have the required "a"*)
    1.40 -Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
    1.41 +Goal  "[| a:A;  (a,b): r |] ==> b : r```A";
    1.42  by (Blast_tac 1);
    1.43  qed "rev_ImageI";
    1.44  
    1.45 -Goal "R^^{} = {}";
    1.46 +Goal "R```{} = {}";
    1.47  by (Blast_tac 1);
    1.48  qed "Image_empty";
    1.49  
    1.50  Addsimps [Image_empty];
    1.51  
    1.52 -Goal "Id ^^ A = A";
    1.53 +Goal "Id ``` A = A";
    1.54  by (Blast_tac 1);
    1.55  qed "Image_Id";
    1.56  
    1.57 -Goal "diag A ^^ B = A Int B";
    1.58 +Goal "diag A ``` B = A Int B";
    1.59  by (Blast_tac 1);
    1.60  qed "Image_diag";
    1.61  
    1.62  Addsimps [Image_Id, Image_diag];
    1.63  
    1.64 -Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
    1.65 +Goal "R ``` (A Int B) <= R ``` A Int R ``` B";
    1.66  by (Blast_tac 1);
    1.67  qed "Image_Int_subset";
    1.68  
    1.69 -Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
    1.70 +Goal "R ``` (A Un B) = R ``` A Un R ``` B";
    1.71  by (Blast_tac 1);
    1.72  qed "Image_Un";
    1.73  
    1.74 -Goal "r <= A <*> B ==> r^^C <= B";
    1.75 +Goal "r <= A <*> B ==> r```C <= B";
    1.76  by (rtac subsetI 1);
    1.77  by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
    1.78  qed "Image_subset";
    1.79  
    1.80  (*NOT suitable for rewriting*)
    1.81 -Goal "r^^B = (UN y: B. r^^{y})";
    1.82 +Goal "r```B = (UN y: B. r```{y})";
    1.83  by (Blast_tac 1);
    1.84  qed "Image_eq_UN";
    1.85  
    1.86 -Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
    1.87 +Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)";
    1.88  by (Blast_tac 1);
    1.89  qed "Image_mono";
    1.90  
    1.91 -Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
    1.92 +Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))";
    1.93  by (Blast_tac 1);
    1.94  qed "Image_UN";
    1.95  
    1.96  (*Converse inclusion fails*)
    1.97 -Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
    1.98 +Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))";
    1.99  by (Blast_tac 1);
   1.100  qed "Image_INT_subset";
   1.101  
   1.102 -Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
   1.103 +Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))";
   1.104  by (Blast_tac 1);
   1.105  qed "Image_subset_eq";
   1.106  
   1.107 -section "univalent";
   1.108 +section "single_valued";
   1.109  
   1.110 -Goalw [univalent_def]
   1.111 -     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r";
   1.112 +Goalw [single_valued_def]
   1.113 +     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r";
   1.114  by (assume_tac 1);
   1.115 -qed "univalentI";
   1.116 +qed "single_valuedI";
   1.117  
   1.118 -Goalw [univalent_def]
   1.119 -     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
   1.120 +Goalw [single_valued_def]
   1.121 +     "[| single_valued r;  (x,y):r;  (x,z):r|] ==> y=z";
   1.122  by Auto_tac;
   1.123 -qed "univalentD";
   1.124 +qed "single_valuedD";
   1.125  
   1.126  
   1.127  (** Graphs given by Collect **)
   1.128 @@ -442,7 +442,7 @@
   1.129  by Auto_tac; 
   1.130  qed "Range_Collect_split";
   1.131  
   1.132 -Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}";
   1.133 +Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}";
   1.134  by Auto_tac; 
   1.135  qed "Image_Collect_split";
   1.136