src/HOL/Relation.ML
changeset 7007 b46ccfee8e59
parent 6806 43c081a0858d
child 7014 11ee650edcd2
     1.1 --- a/src/HOL/Relation.ML	Wed Jul 14 13:32:21 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Jul 15 10:27:54 1999 +0200
     1.3 @@ -207,14 +207,14 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Domain_iff";
     1.6  
     1.7 -qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)"
     1.8 - (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
     1.9 +Goal "(a,b): r ==> a: Domain(r)";
    1.10 +by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
    1.11 +qed "DomainI";
    1.12  
    1.13 -qed_goal "DomainE" thy
    1.14 -    "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P"
    1.15 - (fn prems=>
    1.16 -  [ (rtac (Domain_iff RS iffD1 RS exE) 1),
    1.17 -    (REPEAT (ares_tac prems 1)) ]);
    1.18 +val prems= Goal "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P";
    1.19 +by (rtac (Domain_iff RS iffD1 RS exE) 1);
    1.20 +by (REPEAT (ares_tac prems 1)) ;
    1.21 +qed "DomainE";
    1.22  
    1.23  AddIs  [DomainI];
    1.24  AddSEs [DomainE];
    1.25 @@ -298,22 +298,23 @@
    1.26  
    1.27  qed_goalw "Image_iff" thy [Image_def]
    1.28      "b : r^^A = (? x:A. (x,b):r)"
    1.29 - (fn _ => [ Blast_tac 1 ]);
    1.30 + (fn _ => [(Blast_tac 1)]);
    1.31  
    1.32  qed_goalw "Image_singleton" thy [Image_def]
    1.33      "r^^{a} = {b. (a,b):r}"
    1.34 - (fn _ => [ Blast_tac 1 ]);
    1.35 + (fn _ => [(Blast_tac 1)]);
    1.36  
    1.37 -qed_goal "Image_singleton_iff" thy
    1.38 -    "(b : r^^{a}) = ((a,b):r)"
    1.39 - (fn _ => [ rtac (Image_iff RS trans) 1,
    1.40 -            Blast_tac 1 ]);
    1.41 +Goal
    1.42 +    "(b : r^^{a}) = ((a,b):r)";
    1.43 +by (rtac (Image_iff RS trans) 1);
    1.44 +by (Blast_tac 1);
    1.45 +qed "Image_singleton_iff";
    1.46  
    1.47  AddIffs [Image_singleton_iff];
    1.48  
    1.49 -qed_goalw "ImageI" thy [Image_def]
    1.50 -    "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
    1.51 - (fn _ => [ (Blast_tac 1)]);
    1.52 +Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r^^A";
    1.53 +by (Blast_tac 1);
    1.54 +qed "ImageI";
    1.55  
    1.56  qed_goalw "ImageE" thy [Image_def]
    1.57      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
    1.58 @@ -327,9 +328,10 @@
    1.59  AddSEs [ImageE];
    1.60  
    1.61  
    1.62 -qed_goal "Image_empty" thy
    1.63 -    "R^^{} = {}"
    1.64 - (fn _ => [ Blast_tac 1 ]);
    1.65 +Goal
    1.66 +    "R^^{} = {}";
    1.67 +by (Blast_tac 1);
    1.68 +qed "Image_empty";
    1.69  
    1.70  Addsimps [Image_empty];
    1.71  
    1.72 @@ -343,17 +345,18 @@
    1.73  
    1.74  Addsimps [Image_Id, Image_diag];
    1.75  
    1.76 -qed_goal "Image_Int_subset" thy
    1.77 -    "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
    1.78 - (fn _ => [ Blast_tac 1 ]);
    1.79 +Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
    1.80 +by (Blast_tac 1);
    1.81 +qed "Image_Int_subset";
    1.82  
    1.83 -qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B"
    1.84 - (fn _ => [ Blast_tac 1 ]);
    1.85 +Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
    1.86 +by (Blast_tac 1);
    1.87 +qed "Image_Un";
    1.88  
    1.89 -qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B"
    1.90 - (fn _ =>
    1.91 -  [ (rtac subsetI 1),
    1.92 -    (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
    1.93 +Goal "r <= A Times B ==> r^^C <= B";
    1.94 +by (rtac subsetI 1);
    1.95 +by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
    1.96 +qed "Image_subset";
    1.97  
    1.98  (*NOT suitable for rewriting*)
    1.99  Goal "r^^B = (UN y: B. r^^{y})";