src/HOL/Relation.ML
changeset 5069 3ea049f7979d
parent 4830 bd73675adbed
child 5143 b94cd208f073
     1.1 --- a/src/HOL/Relation.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  (** Identity relation **)
     1.6  
     1.7 -goalw thy [id_def] "(a,a) : id";  
     1.8 +Goalw [id_def] "(a,a) : id";  
     1.9  by (Blast_tac 1);
    1.10  qed "idI";
    1.11  
    1.12 @@ -20,7 +20,7 @@
    1.13  by (eresolve_tac prems 1);
    1.14  qed "idE";
    1.15  
    1.16 -goalw thy [id_def] "(a,b):id = (a=b)";
    1.17 +Goalw [id_def] "(a,b):id = (a=b)";
    1.18  by (Blast_tac 1);
    1.19  qed "pair_in_id_conv";
    1.20  Addsimps [pair_in_id_conv];
    1.21 @@ -28,7 +28,7 @@
    1.22  
    1.23  (** Composition of two relations **)
    1.24  
    1.25 -goalw thy [comp_def]
    1.26 +Goalw [comp_def]
    1.27      "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.28  by (Blast_tac 1);
    1.29  qed "compI";
    1.30 @@ -54,25 +54,25 @@
    1.31  AddIs [compI, idI];
    1.32  AddSEs [compE, idE];
    1.33  
    1.34 -goal thy "R O id = R";
    1.35 +Goal "R O id = R";
    1.36  by (Fast_tac 1);
    1.37  qed "R_O_id";
    1.38  
    1.39 -goal thy "id O R = R";
    1.40 +Goal "id O R = R";
    1.41  by (Fast_tac 1);
    1.42  qed "id_O_R";
    1.43  
    1.44  Addsimps [R_O_id,id_O_R];
    1.45  
    1.46 -goal thy "(R O S) O T = R O (S O T)";
    1.47 +Goal "(R O S) O T = R O (S O T)";
    1.48  by (Blast_tac 1);
    1.49  qed "O_assoc";
    1.50  
    1.51 -goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.52 +Goal "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.53  by (Blast_tac 1);
    1.54  qed "comp_mono";
    1.55  
    1.56 -goal thy
    1.57 +Goal
    1.58      "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    1.59  by (Blast_tac 1);
    1.60  qed "comp_subset_Sigma";
    1.61 @@ -84,24 +84,24 @@
    1.62  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.63  qed "transI";
    1.64  
    1.65 -goalw thy [trans_def]
    1.66 +Goalw [trans_def]
    1.67      "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.68  by (Blast_tac 1);
    1.69  qed "transD";
    1.70  
    1.71  (** Natural deduction for r^-1 **)
    1.72  
    1.73 -goalw thy [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    1.74 +Goalw [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    1.75  by (Simp_tac 1);
    1.76  qed "converse_iff";
    1.77  
    1.78  AddIffs [converse_iff];
    1.79  
    1.80 -goalw thy [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    1.81 +Goalw [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    1.82  by (Simp_tac 1);
    1.83  qed "converseI";
    1.84  
    1.85 -goalw thy [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    1.86 +Goalw [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    1.87  by (Blast_tac 1);
    1.88  qed "converseD";
    1.89  
    1.90 @@ -117,16 +117,16 @@
    1.91  
    1.92  AddSEs [converseE];
    1.93  
    1.94 -goalw thy [converse_def] "(r^-1)^-1 = r";
    1.95 +Goalw [converse_def] "(r^-1)^-1 = r";
    1.96  by (Blast_tac 1);
    1.97  qed "converse_converse";
    1.98  Addsimps [converse_converse];
    1.99  
   1.100 -goal thy "(r O s)^-1 = s^-1 O r^-1";
   1.101 +Goal "(r O s)^-1 = s^-1 O r^-1";
   1.102  by (Blast_tac 1);
   1.103  qed "converse_comp";
   1.104  
   1.105 -goal thy "id^-1 = id";
   1.106 +Goal "id^-1 = id";
   1.107  by (Blast_tac 1);
   1.108  qed "converse_id";
   1.109  Addsimps [converse_id];
   1.110 @@ -149,7 +149,7 @@
   1.111  AddIs  [DomainI];
   1.112  AddSEs [DomainE];
   1.113  
   1.114 -goal thy "Domain id = UNIV";
   1.115 +Goal "Domain id = UNIV";
   1.116  by (Blast_tac 1);
   1.117  qed "Domain_id";
   1.118  Addsimps [Domain_id];
   1.119 @@ -169,7 +169,7 @@
   1.120  AddIs  [RangeI];
   1.121  AddSEs [RangeE];
   1.122  
   1.123 -goal thy "Range id = UNIV";
   1.124 +Goal "Range id = UNIV";
   1.125  by (Blast_tac 1);
   1.126  qed "Range_id";
   1.127  Addsimps [Range_id];
   1.128 @@ -213,7 +213,7 @@
   1.129  
   1.130  Addsimps [Image_empty];
   1.131  
   1.132 -goal thy "id ^^ A = A";
   1.133 +Goal "id ^^ A = A";
   1.134  by (Blast_tac 1);
   1.135  qed "Image_id";
   1.136  
   1.137 @@ -232,7 +232,7 @@
   1.138      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
   1.139  
   1.140  (*NOT suitable for rewriting*)
   1.141 -goal thy "r^^B = (UN y: B. r^^{y})";
   1.142 +Goal "r^^B = (UN y: B. r^^{y})";
   1.143  by (Blast_tac 1);
   1.144  qed "Image_eq_UN";
   1.145