getting rid of qed_goal
authorpaulson
Mon Jul 19 15:24:35 1999 +0200 (1999-07-19)
changeset 7031972b5f62f476
parent 7030 53934985426a
child 7032 d6efb3b8e669
getting rid of qed_goal
src/HOL/Prod.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Vimage.ML
src/HOL/WF_Rel.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Prod.ML	Mon Jul 19 15:19:11 1999 +0200
     1.2 +++ b/src/HOL/Prod.ML	Mon Jul 19 15:24:35 1999 +0200
     1.3 @@ -61,8 +61,11 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "surjective_pairing";
     1.6  
     1.7 -val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
     1.8 -	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
     1.9 +Goal "? x y. z = (x, y)";
    1.10 +by (rtac exI 1);
    1.11 +by (rtac exI 1);
    1.12 +by (rtac surjective_pairing 1);
    1.13 +qed "surj_pair";
    1.14  Addsimps [surj_pair];
    1.15  
    1.16  
    1.17 @@ -120,17 +123,20 @@
    1.18  qed "Pair_fst_snd_eq";
    1.19  
    1.20  (*Prevents simplification of c: much faster*)
    1.21 -qed_goal "split_weak_cong" Prod.thy
    1.22 -  "p=q ==> split c p = split c q"
    1.23 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.24 +val [prem] = goal Prod.thy
    1.25 +  "p=q ==> split c p = split c q";
    1.26 +by (rtac (prem RS arg_cong) 1);
    1.27 +qed "split_weak_cong";
    1.28  
    1.29 -qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
    1.30 -  (K [rtac ext 1, split_all_tac 1, rtac split 1]);
    1.31 +Goal "(%(x,y). f(x,y)) = f";
    1.32 +by (rtac ext 1);
    1.33 +by (split_all_tac 1);
    1.34 +by (rtac split 1);
    1.35 +qed "split_eta";
    1.36  
    1.37 -qed_goal "cond_split_eta" Prod.thy 
    1.38 -	"!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"
    1.39 -  (K [asm_simp_tac (simpset() addsimps [split_eta]) 1]);
    1.40 -
    1.41 +val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
    1.42 +by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
    1.43 +qed "cond_split_eta";
    1.44  
    1.45  (*simplification procedure for cond_split_eta. 
    1.46    using split_eta a rewrite rule is not general enough, and using 
    1.47 @@ -171,9 +177,9 @@
    1.48  
    1.49  Addsimprocs [split_eta_proc];
    1.50  
    1.51 -
    1.52 -qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
    1.53 -	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    1.54 +Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
    1.55 +by (stac surjective_pairing 1 THEN rtac split 1);
    1.56 +qed "split_beta";
    1.57  
    1.58  (*For use with split_tac and the simplifier*)
    1.59  Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
    1.60 @@ -212,11 +218,12 @@
    1.61  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
    1.62  qed "splitE";
    1.63  
    1.64 -val splitE2 = prove_goal Prod.thy 
    1.65 -"[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
    1.66 -	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    1.67 -	rtac (split_beta RS subst) 1,
    1.68 -	rtac (hd prems) 1]);
    1.69 +val major::prems = goal Prod.thy 
    1.70 +    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
    1.71 +\    |] ==> R";
    1.72 +by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
    1.73 +by (rtac (split_beta RS subst) 1 THEN rtac major 1);
    1.74 +qed "splitE2";
    1.75  
    1.76  Goal "split R (a,b) ==> R a b";
    1.77  by (etac (split RS iffD1) 1);
    1.78 @@ -305,20 +312,20 @@
    1.79  
    1.80  (*** Disjoint union of a family of sets - Sigma ***)
    1.81  
    1.82 -qed_goalw "SigmaI" Prod.thy [Sigma_def]
    1.83 -    "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
    1.84 - (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
    1.85 +Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
    1.86 +by (REPEAT (ares_tac [singletonI,UN_I] 1));
    1.87 +qed "SigmaI";
    1.88  
    1.89  AddSIs [SigmaI];
    1.90  
    1.91  (*The general elimination rule*)
    1.92 -qed_goalw "SigmaE" Prod.thy [Sigma_def]
    1.93 +val major::prems = Goalw [Sigma_def]
    1.94      "[| c: Sigma A B;  \
    1.95  \       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
    1.96 -\    |] ==> P"
    1.97 - (fn major::prems=>
    1.98 -  [ (cut_facts_tac [major] 1),
    1.99 -    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   1.100 +\    |] ==> P";
   1.101 +by (cut_facts_tac [major] 1);
   1.102 +by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
   1.103 +qed "SigmaE";
   1.104  
   1.105  (** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   1.106  
   1.107 @@ -375,8 +382,10 @@
   1.108  
   1.109  (*** Complex rules for Sigma ***)
   1.110  
   1.111 -val Collect_split = prove_goal Prod.thy 
   1.112 -	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
   1.113 +Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
   1.114 +by (Blast_tac 1);
   1.115 +qed "Collect_split";
   1.116 +
   1.117  Addsimps [Collect_split];
   1.118  
   1.119  (*Suggested by Pierre Chartier*)
     2.1 --- a/src/HOL/Relation.ML	Mon Jul 19 15:19:11 1999 +0200
     2.2 +++ b/src/HOL/Relation.ML	Mon Jul 19 15:24:35 1999 +0200
     2.3 @@ -171,15 +171,15 @@
     2.4  qed "converseD";
     2.5  
     2.6  (*More general than converseD, as it "splits" the member of the relation*)
     2.7 -qed_goalw "converseE" thy [converse_def]
     2.8 +
     2.9 +val [major,minor] = Goalw [converse_def]
    2.10      "[| yx : r^-1;  \
    2.11  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
    2.12 -\    |] ==> P"
    2.13 - (fn [major,minor]=>
    2.14 -  [ (rtac (major RS CollectE) 1),
    2.15 -    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    2.16 -    (assume_tac 1) ]);
    2.17 -
    2.18 +\    |] ==> P";
    2.19 +by (rtac (major RS CollectE) 1);
    2.20 +by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
    2.21 +by (assume_tac 1);
    2.22 +qed "converseE";
    2.23  AddSEs [converseE];
    2.24  
    2.25  Goalw [converse_def] "(r^-1)^-1 = r";
    2.26 @@ -252,15 +252,16 @@
    2.27  by (Blast_tac 1);
    2.28  qed "Range_iff";
    2.29  
    2.30 -qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    2.31 - (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    2.32 +Goalw [Range_def] "(a,b): r ==> b : Range(r)";
    2.33 +by (etac (converseI RS DomainI) 1);
    2.34 +qed "RangeI";
    2.35  
    2.36 -qed_goalw "RangeE" thy [Range_def]
    2.37 -    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
    2.38 - (fn major::prems=>
    2.39 -  [ (rtac (major RS DomainE) 1),
    2.40 -    (resolve_tac prems 1),
    2.41 -    (etac converseD 1) ]);
    2.42 +val major::prems = Goalw [Range_def] 
    2.43 +    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P";
    2.44 +by (rtac (major RS DomainE) 1);
    2.45 +by (resolve_tac prems 1);
    2.46 +by (etac converseD 1) ;
    2.47 +qed "RangeE";
    2.48  
    2.49  AddIs  [RangeI];
    2.50  AddSEs [RangeE];
    2.51 @@ -296,16 +297,15 @@
    2.52  
    2.53  overload_1st_set "Relation.op ^^";
    2.54  
    2.55 -qed_goalw "Image_iff" thy [Image_def]
    2.56 -    "b : r^^A = (? x:A. (x,b):r)"
    2.57 - (fn _ => [(Blast_tac 1)]);
    2.58 +Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
    2.59 +by (Blast_tac 1);
    2.60 +qed "Image_iff";
    2.61  
    2.62 -qed_goalw "Image_singleton" thy [Image_def]
    2.63 -    "r^^{a} = {b. (a,b):r}"
    2.64 - (fn _ => [(Blast_tac 1)]);
    2.65 +Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
    2.66 +by (Blast_tac 1);
    2.67 +qed "Image_singleton";
    2.68  
    2.69 -Goal
    2.70 -    "(b : r^^{a}) = ((a,b):r)";
    2.71 +Goal "(b : r^^{a}) = ((a,b):r)";
    2.72  by (rtac (Image_iff RS trans) 1);
    2.73  by (Blast_tac 1);
    2.74  qed "Image_singleton_iff";
    2.75 @@ -316,20 +316,19 @@
    2.76  by (Blast_tac 1);
    2.77  qed "ImageI";
    2.78  
    2.79 -qed_goalw "ImageE" thy [Image_def]
    2.80 -    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
    2.81 - (fn major::prems=>
    2.82 -  [ (rtac (major RS CollectE) 1),
    2.83 -    (Clarify_tac 1),
    2.84 -    (rtac (hd prems) 1),
    2.85 -    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    2.86 +val major::prems = Goalw [Image_def]
    2.87 +    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
    2.88 +by (rtac (major RS CollectE) 1);
    2.89 +by (Clarify_tac 1);
    2.90 +by (rtac (hd prems) 1);
    2.91 +by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
    2.92 +qed "ImageE";
    2.93  
    2.94  AddIs  [ImageI];
    2.95  AddSEs [ImageE];
    2.96  
    2.97  
    2.98 -Goal
    2.99 -    "R^^{} = {}";
   2.100 +Goal "R^^{} = {}";
   2.101  by (Blast_tac 1);
   2.102  qed "Image_empty";
   2.103  
   2.104 @@ -366,11 +365,15 @@
   2.105  
   2.106  section "Univalent";
   2.107  
   2.108 -qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
   2.109 -   "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
   2.110 +Goalw [Univalent_def]
   2.111 +     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
   2.112 +by (assume_tac 1);
   2.113 +qed "UnivalentI";
   2.114  
   2.115 -qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
   2.116 -	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
   2.117 +Goalw [Univalent_def]
   2.118 +     "[| Univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
   2.119 +by Auto_tac;
   2.120 +qed "UnivalentD";
   2.121  
   2.122  
   2.123  (** Graphs of partial functions **)
     3.1 --- a/src/HOL/Set.ML	Mon Jul 19 15:19:11 1999 +0200
     3.2 +++ b/src/HOL/Set.ML	Mon Jul 19 15:24:35 1999 +0200
     3.3 @@ -71,7 +71,7 @@
     3.4  by (Blast_tac 1);
     3.5  qed "rev_bexI";
     3.6  
     3.7 -val prems = goal Set.thy 
     3.8 +val prems = Goal 
     3.9     "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)";
    3.10  by (rtac classical 1);
    3.11  by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ;
    3.12 @@ -223,14 +223,18 @@
    3.13  
    3.14  section "The universal set -- UNIV";
    3.15  
    3.16 -qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
    3.17 -  (fn _ => [rtac CollectI 1, rtac TrueI 1]);
    3.18 +Goalw [UNIV_def] "x : UNIV";
    3.19 +by (rtac CollectI 1);
    3.20 +by (rtac TrueI 1);
    3.21 +qed "UNIV_I";
    3.22  
    3.23  Addsimps [UNIV_I];
    3.24  AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
    3.25  
    3.26 -qed_goal "subset_UNIV" Set.thy "A <= UNIV"
    3.27 -  (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
    3.28 +Goal "A <= UNIV";
    3.29 +by (rtac subsetI 1);
    3.30 +by (rtac UNIV_I 1);
    3.31 +qed "subset_UNIV";
    3.32  
    3.33  (** Eta-contracting these two rules (to remove P) causes them to be ignored
    3.34      because of their interaction with congruence rules. **)
    3.35 @@ -266,7 +270,7 @@
    3.36  (*One effect is to delete the ASSUMPTION {} <= A*)
    3.37  AddIffs [empty_subsetI];
    3.38  
    3.39 -val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}";
    3.40 +val [prem]= Goal "[| !!y. y:A ==> False |] ==> A={}";
    3.41  by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
    3.42  qed "equals0I";
    3.43  
    3.44 @@ -301,11 +305,11 @@
    3.45  
    3.46  AddIffs [Pow_iff]; 
    3.47  
    3.48 -Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)";
    3.49 +Goalw [Pow_def] "A <= B ==> A : Pow(B)";
    3.50  by (etac CollectI 1);
    3.51  qed "PowI";
    3.52  
    3.53 -Goalw [Pow_def] "!!A B. A : Pow(B)  ==>  A<=B";
    3.54 +Goalw [Pow_def] "A : Pow(B)  ==>  A<=B";
    3.55  by (etac CollectD 1);
    3.56  qed "PowD";
    3.57  
    3.58 @@ -316,8 +320,9 @@
    3.59  
    3.60  section "Set complement";
    3.61  
    3.62 -qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
    3.63 - (fn _ => [ (Blast_tac 1) ]);
    3.64 +Goalw [Compl_def] "(c : -A) = (c~:A)";
    3.65 +by (Blast_tac 1);
    3.66 +qed "Compl_iff";
    3.67  
    3.68  Addsimps [Compl_iff];
    3.69  
    3.70 @@ -340,9 +345,9 @@
    3.71  
    3.72  section "Binary union -- Un";
    3.73  
    3.74 -qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
    3.75 - (fn _ => [ Blast_tac 1 ]);
    3.76 -
    3.77 +Goalw [Un_def] "(c : A Un B) = (c:A | c:B)";
    3.78 +by (Blast_tac 1);
    3.79 +qed "Un_iff";
    3.80  Addsimps [Un_iff];
    3.81  
    3.82  Goal "c:A ==> c : A Un B";
    3.83 @@ -355,7 +360,7 @@
    3.84  
    3.85  (*Classical introduction rule: no commitment to A vs B*)
    3.86  
    3.87 -val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B";
    3.88 +val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";
    3.89  by (Simp_tac 1);
    3.90  by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
    3.91  qed "UnCI";
    3.92 @@ -372,9 +377,9 @@
    3.93  
    3.94  section "Binary intersection -- Int";
    3.95  
    3.96 -qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
    3.97 - (fn _ => [ (Blast_tac 1) ]);
    3.98 -
    3.99 +Goalw [Int_def] "(c : A Int B) = (c:A & c:B)";
   3.100 +by (Blast_tac 1);
   3.101 +qed "Int_iff";
   3.102  Addsimps [Int_iff];
   3.103  
   3.104  Goal "[| c:A;  c:B |] ==> c : A Int B";
   3.105 @@ -401,9 +406,9 @@
   3.106  
   3.107  section "Set difference";
   3.108  
   3.109 -qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
   3.110 - (fn _ => [ (Blast_tac 1) ]);
   3.111 -
   3.112 +Goalw [set_diff_def] "(c : A-B) = (c:A & c~:B)";
   3.113 +by (Blast_tac 1);
   3.114 +qed "Diff_iff";
   3.115  Addsimps [Diff_iff];
   3.116  
   3.117  Goal "[| c : A;  c ~: B |] ==> c : A - B";
   3.118 @@ -418,7 +423,7 @@
   3.119  by (Asm_full_simp_tac 1) ;
   3.120  qed "DiffD2";
   3.121  
   3.122 -val prems= goal Set.thy "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
   3.123 +val prems = Goal "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
   3.124  by (resolve_tac prems 1);
   3.125  by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
   3.126  qed "DiffE";
   3.127 @@ -429,12 +434,12 @@
   3.128  
   3.129  section "Augmenting a set -- insert";
   3.130  
   3.131 -qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
   3.132 - (fn _ => [Blast_tac 1]);
   3.133 -
   3.134 +Goalw [insert_def] "a : insert b A = (a=b | a:A)";
   3.135 +by (Blast_tac 1);
   3.136 +qed "insert_iff";
   3.137  Addsimps [insert_iff];
   3.138  
   3.139 -val _ = goal Set.thy "a : insert a B";
   3.140 +Goal "a : insert a B";
   3.141  by (Simp_tac 1);
   3.142  qed "insertI1";
   3.143  
   3.144 @@ -449,7 +454,7 @@
   3.145  qed "insertE";
   3.146  
   3.147  (*Classical introduction rule*)
   3.148 -val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B";
   3.149 +val prems = Goal "(a~:B ==> a=b) ==> a: insert b B";
   3.150  by (Simp_tac 1);
   3.151  by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
   3.152  qed "insertCI";
     4.1 --- a/src/HOL/Sum.ML	Mon Jul 19 15:19:11 1999 +0200
     4.2 +++ b/src/HOL/Sum.ML	Mon Jul 19 15:24:35 1999 +0200
     4.3 @@ -6,8 +6,6 @@
     4.4  The disjoint sum of two types
     4.5  *)
     4.6  
     4.7 -open Sum;
     4.8 -
     4.9  (** Inl_Rep and Inr_Rep: Representations of the constructors **)
    4.10  
    4.11  (*This counts as a non-emptiness result for admitting 'a+'b as a type*)
    4.12 @@ -157,15 +155,16 @@
    4.13  by Auto_tac;
    4.14  qed "split_sum_case";
    4.15  
    4.16 -qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \
    4.17 -\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"
    4.18 -    (K [stac split_sum_case 1,
    4.19 -	Blast_tac 1]);
    4.20 +Goal "P (sum_case f g s) = \
    4.21 +\     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
    4.22 +by (stac split_sum_case 1);
    4.23 +by (Blast_tac 1);
    4.24 +qed "split_sum_case_asm";
    4.25  
    4.26  (*Prevents simplification of f and g: much faster*)
    4.27 -qed_goal "sum_case_weak_cong" Sum.thy
    4.28 -  "s=t ==> sum_case f g s = sum_case f g t"
    4.29 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    4.30 +Goal "s=t ==> sum_case f g s = sum_case f g t";
    4.31 +by (etac arg_cong 1);
    4.32 +qed "sum_case_weak_cong";
    4.33  
    4.34  val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
    4.35    \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
     5.1 --- a/src/HOL/Vimage.ML	Mon Jul 19 15:19:11 1999 +0200
     5.2 +++ b/src/HOL/Vimage.ML	Mon Jul 19 15:24:35 1999 +0200
     5.3 @@ -6,33 +6,32 @@
     5.4  Inverse image of a function
     5.5  *)
     5.6  
     5.7 -open Vimage;
     5.8 -
     5.9  (** Basic rules **)
    5.10  
    5.11 -qed_goalw "vimage_eq" thy [vimage_def]
    5.12 -    "(a : f-``B) = (f a : B)"
    5.13 - (fn _ => [ (Blast_tac 1) ]);
    5.14 +Goalw [vimage_def] "(a : f-``B) = (f a : B)";
    5.15 +by (Blast_tac 1) ;
    5.16 +qed "vimage_eq";
    5.17  
    5.18  Addsimps [vimage_eq];
    5.19  
    5.20 -qed_goal "vimage_singleton_eq" thy
    5.21 -    "(a : f-``{b}) = (f a = b)"
    5.22 - (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
    5.23 +Goal "(a : f-``{b}) = (f a = b)";
    5.24 +by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
    5.25 +qed "vimage_singleton_eq";
    5.26  
    5.27 -qed_goalw "vimageI" thy [vimage_def]
    5.28 -    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
    5.29 - (fn _ => [ (Blast_tac 1) ]);
    5.30 +Goalw [vimage_def]
    5.31 +    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
    5.32 +by (Blast_tac 1) ;
    5.33 +qed "vimageI";
    5.34  
    5.35  Goalw [vimage_def] "f a : A ==> a : f -`` A";
    5.36  by (Fast_tac 1);
    5.37  qed "vimageI2";
    5.38  
    5.39 -qed_goalw "vimageE" thy [vimage_def]
    5.40 -    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P"
    5.41 - (fn major::prems=>
    5.42 -  [ (rtac (major RS CollectE) 1),
    5.43 -    (blast_tac (claset() addIs prems) 1) ]);
    5.44 +val major::prems = Goalw [vimage_def]
    5.45 +    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
    5.46 +by (rtac (major RS CollectE) 1);
    5.47 +by (blast_tac (claset() addIs prems) 1) ;
    5.48 +qed "vimageE";
    5.49  
    5.50  Goalw [vimage_def] "a : f -`` A ==> f a : A";
    5.51  by (Fast_tac 1);
     6.1 --- a/src/HOL/WF_Rel.ML	Mon Jul 19 15:19:11 1999 +0200
     6.2 +++ b/src/HOL/WF_Rel.ML	Mon Jul 19 15:24:35 1999 +0200
     6.3 @@ -115,10 +115,10 @@
     6.4  by (Asm_full_simp_tac 1);
     6.5  qed_spec_mp "finite_acyclic_wf";
     6.6  
     6.7 -qed_goal "finite_acyclic_wf_converse" thy 
     6.8 - "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [
     6.9 -	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
    6.10 -	etac (acyclic_converse RS iffD2) 1]);
    6.11 +Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
    6.12 +by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
    6.13 +by (etac (acyclic_converse RS iffD2) 1);
    6.14 +qed "finite_acyclic_wf_converse";
    6.15  
    6.16  Goal "finite r ==> wf r = acyclic r";
    6.17  by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
     7.1 --- a/src/HOL/simpdata.ML	Mon Jul 19 15:19:11 1999 +0200
     7.2 +++ b/src/HOL/simpdata.ML	Mon Jul 19 15:24:35 1999 +0200
     7.3 @@ -89,12 +89,14 @@
     7.4  end;
     7.5  
     7.6  
     7.7 -qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
     7.8 -  (fn [prem] => [rewtac prem, rtac refl 1]);
     7.9 +val [prem] = goal HOL.thy "x==y ==> x=y";
    7.10 +by (rewtac prem);
    7.11 +by (rtac refl 1);
    7.12 +qed "meta_eq_to_obj_eq";
    7.13  
    7.14  local
    7.15  
    7.16 -  fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
    7.17 +  fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
    7.18  
    7.19  in
    7.20  
    7.21 @@ -156,7 +158,7 @@
    7.22  
    7.23  val imp_cong = impI RSN
    7.24      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    7.25 -        (fn _=> [Blast_tac 1]) RS mp RS mp);
    7.26 +        (fn _=> [(Blast_tac 1)]) RS mp RS mp);
    7.27  
    7.28  (*Miniscoping: pushing in existential quantifiers*)
    7.29  val ex_simps = map prover 
    7.30 @@ -185,7 +187,7 @@
    7.31          (fn prems => [resolve_tac prems 1, etac exI 1]);
    7.32        val lemma2 = prove_goalw HOL.thy [Ex_def]
    7.33          "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
    7.34 -        (fn prems => [REPEAT(resolve_tac prems 1)])
    7.35 +        (fn prems => [(REPEAT(resolve_tac prems 1))])
    7.36    in equal_intr lemma1 lemma2 end;
    7.37  
    7.38  end;
    7.39 @@ -194,11 +196,11 @@
    7.40  
    7.41  val True_implies_equals = prove_goal HOL.thy
    7.42   "(True ==> PROP P) == PROP P"
    7.43 -(K [rtac equal_intr_rule 1, atac 2,
    7.44 +(fn _ => [rtac equal_intr_rule 1, atac 2,
    7.45            METAHYPS (fn prems => resolve_tac prems 1) 1,
    7.46            rtac TrueI 1]);
    7.47  
    7.48 -fun prove nm thm  = qed_goal nm HOL.thy thm (K [Blast_tac 1]);
    7.49 +fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
    7.50  
    7.51  prove "conj_commute" "(P&Q) = (Q&P)";
    7.52  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    7.53 @@ -255,19 +257,19 @@
    7.54  
    7.55  let val th = prove_goal HOL.thy 
    7.56                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
    7.57 -                (fn _=> [Blast_tac 1])
    7.58 +                (fn _=> [(Blast_tac 1)])
    7.59  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    7.60  
    7.61  let val th = prove_goal HOL.thy 
    7.62                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
    7.63 -                (fn _=> [Blast_tac 1])
    7.64 +                (fn _=> [(Blast_tac 1)])
    7.65  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    7.66  
    7.67  (* '|' congruence rule: not included by default! *)
    7.68  
    7.69  let val th = prove_goal HOL.thy 
    7.70                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    7.71 -                (fn _=> [Blast_tac 1])
    7.72 +                (fn _=> [(Blast_tac 1)])
    7.73  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    7.74  
    7.75  prove "eq_sym_conv" "(x=y) = (y=x)";
    7.76 @@ -275,48 +277,58 @@
    7.77  
    7.78  (** if-then-else rules **)
    7.79  
    7.80 -qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
    7.81 - (K [Blast_tac 1]);
    7.82 +Goalw [if_def] "(if True then x else y) = x";
    7.83 +by (Blast_tac 1);
    7.84 +qed "if_True";
    7.85  
    7.86 -qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
    7.87 - (K [Blast_tac 1]);
    7.88 +Goalw [if_def] "(if False then x else y) = y";
    7.89 +by (Blast_tac 1);
    7.90 +qed "if_False";
    7.91  
    7.92 -qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
    7.93 - (K [Blast_tac 1]);
    7.94 +Goalw [if_def] "!!P. P ==> (if P then x else y) = x";
    7.95 +by (Blast_tac 1);
    7.96 +qed "if_P";
    7.97  
    7.98 -qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
    7.99 - (K [Blast_tac 1]);
   7.100 +Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y";
   7.101 +by (Blast_tac 1);
   7.102 +qed "if_not_P";
   7.103  
   7.104 -qed_goal "split_if" HOL.thy
   7.105 -    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
   7.106 -	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
   7.107 -         stac if_P 2,
   7.108 -         stac if_not_P 1,
   7.109 -         ALLGOALS (Blast_tac)]);
   7.110 +Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))";
   7.111 +by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1);
   7.112 +by (stac if_P 2);
   7.113 +by (stac if_not_P 1);
   7.114 +by (ALLGOALS (Blast_tac));
   7.115 +qed "split_if";
   7.116 +
   7.117  (* for backwards compatibility: *)
   7.118  val expand_if = split_if;
   7.119  
   7.120 -qed_goal "split_if_asm" HOL.thy
   7.121 -    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
   7.122 -    (K [stac split_if 1,
   7.123 -	Blast_tac 1]);
   7.124 +Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
   7.125 +by (stac split_if 1);
   7.126 +by (Blast_tac 1);
   7.127 +qed "split_if_asm";
   7.128  
   7.129 -qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   7.130 -  (K [stac split_if 1, Blast_tac 1]);
   7.131 +Goal "(if c then x else x) = x";
   7.132 +by (stac split_if 1);
   7.133 +by (Blast_tac 1);
   7.134 +qed "if_cancel";
   7.135  
   7.136 -qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   7.137 -  (K [stac split_if 1, Blast_tac 1]);
   7.138 +Goal "(if x = y then y else x) = x";
   7.139 +by (stac split_if 1);
   7.140 +by (Blast_tac 1);
   7.141 +qed "if_eq_cancel";
   7.142  
   7.143  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   7.144 -qed_goal "if_bool_eq_conj" HOL.thy
   7.145 -    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   7.146 -    (K [rtac split_if 1]);
   7.147 +Goal
   7.148 +    "(if P then Q else R) = ((P-->Q) & (~P-->R))";
   7.149 +by (rtac split_if 1);
   7.150 +qed "if_bool_eq_conj";
   7.151  
   7.152  (*And this form is useful for expanding IFs on the LEFT*)
   7.153 -qed_goal "if_bool_eq_disj" HOL.thy
   7.154 -    "(if P then Q else R) = ((P&Q) | (~P&R))"
   7.155 -    (K [stac split_if 1,
   7.156 -	Blast_tac 1]);
   7.157 +Goal "(if P then Q else R) = ((P&Q) | (~P&R))";
   7.158 +by (stac split_if 1);
   7.159 +by (Blast_tac 1);
   7.160 +qed "if_bool_eq_disj";
   7.161  
   7.162  
   7.163  (*** make simplification procedures for quantifier elimination ***)
   7.164 @@ -453,18 +465,18 @@
   7.165  qed "if_cong";
   7.166  
   7.167  (*Prevents simplification of x and y: much faster*)
   7.168 -qed_goal "if_weak_cong" HOL.thy
   7.169 -  "b=c ==> (if b then x else y) = (if c then x else y)"
   7.170 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   7.171 +Goal "b=c ==> (if b then x else y) = (if c then x else y)";
   7.172 +by (etac arg_cong 1);
   7.173 +qed "if_weak_cong";
   7.174  
   7.175  (*Prevents simplification of t: much faster*)
   7.176 -qed_goal "let_weak_cong" HOL.thy
   7.177 -  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
   7.178 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   7.179 +Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))";
   7.180 +by (etac arg_cong 1);
   7.181 +qed "let_weak_cong";
   7.182  
   7.183 -qed_goal "if_distrib" HOL.thy
   7.184 -  "f(if c then x else y) = (if c then f x else f y)" 
   7.185 -  (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
   7.186 +Goal "f(if c then x else y) = (if c then f x else f y)";
   7.187 +by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
   7.188 +qed "if_distrib";
   7.189  
   7.190  
   7.191  (*For expand_case_tac*)