src/HOL/Relation.ML
changeset 7031 972b5f62f476
parent 7014 11ee650edcd2
child 7083 9663eb2bce05
     1.1 --- a/src/HOL/Relation.ML	Mon Jul 19 15:19:11 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Jul 19 15:24:35 1999 +0200
     1.3 @@ -171,15 +171,15 @@
     1.4  qed "converseD";
     1.5  
     1.6  (*More general than converseD, as it "splits" the member of the relation*)
     1.7 -qed_goalw "converseE" thy [converse_def]
     1.8 +
     1.9 +val [major,minor] = Goalw [converse_def]
    1.10      "[| yx : r^-1;  \
    1.11  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
    1.12 -\    |] ==> P"
    1.13 - (fn [major,minor]=>
    1.14 -  [ (rtac (major RS CollectE) 1),
    1.15 -    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    1.16 -    (assume_tac 1) ]);
    1.17 -
    1.18 +\    |] ==> P";
    1.19 +by (rtac (major RS CollectE) 1);
    1.20 +by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
    1.21 +by (assume_tac 1);
    1.22 +qed "converseE";
    1.23  AddSEs [converseE];
    1.24  
    1.25  Goalw [converse_def] "(r^-1)^-1 = r";
    1.26 @@ -252,15 +252,16 @@
    1.27  by (Blast_tac 1);
    1.28  qed "Range_iff";
    1.29  
    1.30 -qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    1.31 - (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    1.32 +Goalw [Range_def] "(a,b): r ==> b : Range(r)";
    1.33 +by (etac (converseI RS DomainI) 1);
    1.34 +qed "RangeI";
    1.35  
    1.36 -qed_goalw "RangeE" thy [Range_def]
    1.37 -    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
    1.38 - (fn major::prems=>
    1.39 -  [ (rtac (major RS DomainE) 1),
    1.40 -    (resolve_tac prems 1),
    1.41 -    (etac converseD 1) ]);
    1.42 +val major::prems = Goalw [Range_def] 
    1.43 +    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P";
    1.44 +by (rtac (major RS DomainE) 1);
    1.45 +by (resolve_tac prems 1);
    1.46 +by (etac converseD 1) ;
    1.47 +qed "RangeE";
    1.48  
    1.49  AddIs  [RangeI];
    1.50  AddSEs [RangeE];
    1.51 @@ -296,16 +297,15 @@
    1.52  
    1.53  overload_1st_set "Relation.op ^^";
    1.54  
    1.55 -qed_goalw "Image_iff" thy [Image_def]
    1.56 -    "b : r^^A = (? x:A. (x,b):r)"
    1.57 - (fn _ => [(Blast_tac 1)]);
    1.58 +Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
    1.59 +by (Blast_tac 1);
    1.60 +qed "Image_iff";
    1.61  
    1.62 -qed_goalw "Image_singleton" thy [Image_def]
    1.63 -    "r^^{a} = {b. (a,b):r}"
    1.64 - (fn _ => [(Blast_tac 1)]);
    1.65 +Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
    1.66 +by (Blast_tac 1);
    1.67 +qed "Image_singleton";
    1.68  
    1.69 -Goal
    1.70 -    "(b : r^^{a}) = ((a,b):r)";
    1.71 +Goal "(b : r^^{a}) = ((a,b):r)";
    1.72  by (rtac (Image_iff RS trans) 1);
    1.73  by (Blast_tac 1);
    1.74  qed "Image_singleton_iff";
    1.75 @@ -316,20 +316,19 @@
    1.76  by (Blast_tac 1);
    1.77  qed "ImageI";
    1.78  
    1.79 -qed_goalw "ImageE" thy [Image_def]
    1.80 -    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
    1.81 - (fn major::prems=>
    1.82 -  [ (rtac (major RS CollectE) 1),
    1.83 -    (Clarify_tac 1),
    1.84 -    (rtac (hd prems) 1),
    1.85 -    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    1.86 +val major::prems = Goalw [Image_def]
    1.87 +    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
    1.88 +by (rtac (major RS CollectE) 1);
    1.89 +by (Clarify_tac 1);
    1.90 +by (rtac (hd prems) 1);
    1.91 +by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
    1.92 +qed "ImageE";
    1.93  
    1.94  AddIs  [ImageI];
    1.95  AddSEs [ImageE];
    1.96  
    1.97  
    1.98 -Goal
    1.99 -    "R^^{} = {}";
   1.100 +Goal "R^^{} = {}";
   1.101  by (Blast_tac 1);
   1.102  qed "Image_empty";
   1.103  
   1.104 @@ -366,11 +365,15 @@
   1.105  
   1.106  section "Univalent";
   1.107  
   1.108 -qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
   1.109 -   "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
   1.110 +Goalw [Univalent_def]
   1.111 +     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
   1.112 +by (assume_tac 1);
   1.113 +qed "UnivalentI";
   1.114  
   1.115 -qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
   1.116 -	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
   1.117 +Goalw [Univalent_def]
   1.118 +     "[| Univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
   1.119 +by Auto_tac;
   1.120 +qed "UnivalentD";
   1.121  
   1.122  
   1.123  (** Graphs of partial functions **)