tidied

--- a/src/HOL/HOL_lemmas.ML	Mon Mar 20 18:24:11 2000 +0100
+++ b/src/HOL/HOL_lemmas.ML	Mon Mar 20 18:25:35 2000 +0100
@@ -131,13 +131,16 @@
 (** Universal quantifier **)
 section "!";
 
-qed_goalw "allI" (the_context ()) [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
+val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ! x. P(x)";
+by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
+qed "allI";
 
-qed_goalw "spec" (the_context ()) [All_def] "! x::'a. P(x) ==> P(x)"
- (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
+Goalw [All_def] "! x::'a. P(x) ==> P(x)";
+by (rtac eqTrueE 1);
+by (etac fun_cong 1);
+qed "spec";
 
-val major::prems= goal (the_context ()) "[| !x. P(x);  P(x) ==> R |] ==> R";
+val major::prems= goal (the_context ()) "[| ! x. P(x);  P(x) ==> R |] ==> R";
 by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
 qed "allE";
 
@@ -151,32 +154,45 @@
              before quantifiers! **)
 section "False";
 
-qed_goalw "FalseE" (the_context ()) [False_def] "False ==> P"
- (fn [major] => [rtac (major RS spec) 1]);
+Goalw [False_def] "False ==> P";
+by (etac spec 1);
+qed "FalseE";
 
-qed_goal "False_neq_True" (the_context ()) "False=True ==> P"
- (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
+Goal "False=True ==> P";
+by (etac (eqTrueE RS FalseE) 1);
+qed "False_neq_True";
 
 
 (** Negation **)
 section "~";
 
-qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P"
- (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
+val prems = Goalw [not_def] "(P ==> False) ==> ~P";
+by (rtac impI 1);
+by (eresolve_tac prems 1);
+qed "notI";
 
-qed_goal "False_not_True" (the_context ()) "False ~= True"
-  (fn _ => [rtac notI 1, etac False_neq_True 1]);
+Goal "False ~= True";
+by (rtac notI 1);
+by (etac False_neq_True 1);
+qed "False_not_True";
 
-qed_goal "True_not_False" (the_context ()) "True ~= False"
-  (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
+Goal "True ~= False";
+by (rtac notI 1);
+by (dtac sym 1);
+by (etac False_neq_True 1);
+qed "True_not_False";
 
-qed_goalw "notE" (the_context ()) [not_def] "[| ~P;  P |] ==> R"
- (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
+Goalw [not_def] "[| ~P;  P |] ==> R";
+by (etac (mp RS FalseE) 1);
+by (assume_tac 1);
+qed "notE";
 
 bind_thm ("classical2", notE RS notI);
 
-qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R"
- (fn _ => [REPEAT (ares_tac [notE] 1)]);
+Goal "[| P; ~P |] ==> R";
+by (etac notE 1);
+by (assume_tac 1);
+qed "rev_notE";
 
 
 (** Implication **)
@@ -208,61 +224,80 @@
 (** Existential quantifier **)
 section "?";
 
-qed_goalw "exI" (the_context ()) [Ex_def] "P x ==> ? x::'a. P x"
- (fn prems => [rtac selectI 1, resolve_tac prems 1]);
+Goalw [Ex_def] "P x ==> ? x::'a. P x";
+by (etac selectI 1) ;
+qed "exI";
 
-qed_goalw "exE" (the_context ()) [Ex_def]
-  "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
-  (fn prems => [REPEAT(resolve_tac prems 1)]);
+val [major,minor] = 
+Goalw [Ex_def] "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
+by (rtac (major RS minor) 1);
+qed "exE";
 
 
 (** Conjunction **)
 section "&";
 
-qed_goalw "conjI" (the_context ()) [and_def] "[| P; Q |] ==> P&Q"
- (fn prems =>
-  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
+Goalw [and_def] "[| P; Q |] ==> P&Q";
+by (rtac (impI RS allI) 1);
+by (etac (mp RS mp) 1);
+by (REPEAT (assume_tac 1));
+qed "conjI";
 
-qed_goalw "conjunct1" (the_context ()) [and_def] "[| P & Q |] ==> P"
- (fn prems =>
-   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
+Goalw [and_def] "[| P & Q |] ==> P";
+by (dtac spec 1) ;
+by (etac mp 1);
+by (REPEAT (ares_tac [impI] 1));
+qed "conjunct1";
 
-qed_goalw "conjunct2" (the_context ()) [and_def] "[| P & Q |] ==> Q"
- (fn prems =>
-   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
+Goalw [and_def] "[| P & Q |] ==> Q";
+by (dtac spec 1) ;
+by (etac mp 1);
+by (REPEAT (ares_tac [impI] 1));
+qed "conjunct2";
 
-qed_goal "conjE" (the_context ()) "[| P&Q;  [| P; Q |] ==> R |] ==> R"
- (fn prems =>
-         [cut_facts_tac prems 1, resolve_tac prems 1,
-          etac conjunct1 1, etac conjunct2 1]);
+val [major,minor] =
+Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
+by (rtac minor 1);
+by (rtac (major RS conjunct1) 1);
+by (rtac (major RS conjunct2) 1);
+qed "conjE";
 
-qed_goal "context_conjI" (the_context ())  "[| P; P ==> Q |] ==> P & Q"
- (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
+val prems =
+Goal "[| P; P ==> Q |] ==> P & Q";
+by (REPEAT (resolve_tac (conjI::prems) 1));
+qed "context_conjI";
 
 
 (** Disjunction *)
 section "|";
 
-qed_goalw "disjI1" (the_context ()) [or_def] "P ==> P|Q"
- (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+Goalw [or_def] "P ==> P|Q";
+by (REPEAT (resolve_tac [allI,impI] 1));
+by (etac mp 1 THEN assume_tac 1);
+qed "disjI1";
 
-qed_goalw "disjI2" (the_context ()) [or_def] "Q ==> P|Q"
- (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+Goalw [or_def] "Q ==> P|Q";
+by (REPEAT (resolve_tac [allI,impI] 1));
+by (etac mp 1 THEN assume_tac 1);
+qed "disjI2";
 
-qed_goalw "disjE" (the_context ()) [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
- (fn [a1,a2,a3] =>
-        [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
-         rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
+val [major,minorP,minorQ] =
+Goalw [or_def]  "[| P | Q; P ==> R; Q ==> R |] ==> R";
+by (rtac (major RS spec RS mp RS mp) 1);
+by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));
+qed "disjE";
 
 
 (** CCONTR -- classical logic **)
 section "classical logic";
 
-qed_goalw "classical" (the_context ()) [not_def]  "(~P ==> P) ==> P"
- (fn [prem] =>
-   [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
-    rtac (impI RS prem RS eqTrueI) 1,
-    etac subst 1,  assume_tac 1]);
+val [prem] = Goal  "(~P ==> P) ==> P";
+by (rtac (True_or_False RS disjE RS eqTrueE) 1);
+by (assume_tac 1);
+by (rtac (notI RS prem RS eqTrueI) 1);
+by (etac subst 1);
+by (assume_tac 1);
+qed "classical";
 
 bind_thm ("ccontr", FalseE RS classical);
 
@@ -290,22 +325,22 @@
 (** Unique existence **)
 section "?!";
 
-qed_goalw "ex1I" (the_context ()) [Ex1_def]
-            "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
- (fn prems =>
-  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
+val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)";
+by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
+qed "ex1I";
 
 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
-val [ex,eq] = Goal
+val [ex_prem,eq] = Goal
     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
-by (rtac (ex RS exE) 1);
+by (rtac (ex_prem RS exE) 1);
 by (REPEAT (ares_tac [ex1I,eq] 1)) ;
 qed "ex_ex1I";
 
-qed_goalw "ex1E" (the_context ()) [Ex1_def]
-    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
- (fn major::prems =>
-  [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
+val major::prems = Goalw [Ex1_def]
+    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R";
+by (rtac (major RS exE) 1);
+by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
+qed "ex1E";
 
 Goal "?! x. P x ==> ? x. P x";
 by (etac ex1E 1);
@@ -326,9 +361,10 @@
 qed "selectI2";
 
 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
-qed_goal "selectI2EX" (the_context ())
-  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
-(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
+val [major,minor] = Goal "[| ? a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
+by (rtac (major RS exE) 1);
+by (etac selectI2 1 THEN etac minor 1);
+qed "selectI2EX";
 
 val prems = Goal
     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
@@ -418,9 +454,11 @@
 
 (* case distinction *)
 
-qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q"
-  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
-                  etac p2 1, etac p1 1]);
+val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
+by (rtac (excluded_middle RS disjE) 1);
+by (etac prem2 1);
+by (etac prem1 1);
+qed "case_split_thm";
 
 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
 

--- a/src/HOL/Map.ML	Mon Mar 20 18:24:11 2000 +0100
+++ b/src/HOL/Map.ML	Mon Mar 20 18:25:35 2000 +0100
@@ -16,9 +16,10 @@
 
 section "map_upd";
 
-qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t(k|->x) = t"
-	(K [rtac ext 1, Asm_simp_tac 1]);
-(*Addsimps [map_upd_triv];*)
+Goal "t k = Some x ==> t(k|->x) = t";
+by (rtac ext 1);
+by (Asm_simp_tac 1);
+qed "map_upd_triv";
 
 Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
 by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
@@ -44,10 +45,14 @@
 
 section "chg_map";
 
-qed_goalw "chg_map_new" thy [chg_map_def]
-	"!!s. m a = None   ==> chg_map f a m = m"          (K [Auto_tac]);
-qed_goalw "chg_map_upd" thy [chg_map_def]
-	"!!s. m a = Some b ==> chg_map f a m = m(a|->f b)" (K [Auto_tac]);
+Goalw [chg_map_def] "m a = None   ==> chg_map f a m = m";
+by Auto_tac;
+qed "chg_map_new";
+
+Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a|->f b)";
+by Auto_tac;
+qed "chg_map_upd";
+
 Addsimps[chg_map_new, chg_map_upd];
 
 
@@ -78,12 +83,16 @@
 
 section "option_map related";
 
-qed_goal "option_map_o_empty" thy 
-         "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
+Goal "option_map f o empty = empty";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "option_map_o_empty";
 
-qed_goal "option_map_o_map_upd" thy 
-	 "option_map f o m(a|->b) = (option_map f o m)(a|->f b)" 
-	(K [rtac ext 1, Simp_tac 1]);
+Goal "option_map f o m(a|->b) = (option_map f o m)(a|->f b)";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "option_map_o_map_upd";
+
 Addsimps[option_map_o_empty, option_map_o_map_upd];
 
 section "++";
@@ -168,15 +177,14 @@
 qed "dom_map_upd";
 Addsimps [dom_map_upd];
 
-qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
-	induct_tac "l" 1,
-	 ALLGOALS Simp_tac,
-	stac (insert_Collect RS sym) 1,
-	Asm_full_simp_tac 1]);
+Goalw [dom_def] "finite (dom (map_of l))";
+by (induct_tac "l" 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [insert_Collect RS sym]));
+qed "finite_dom_map_of";
 
 Goalw [dom_def] "dom(m++n) = dom n Un dom m";
-by (Simp_tac 1);
-by (Blast_tac 1);
+by Auto_tac;
 qed "dom_override";
 Addsimps [dom_override];
 

--- a/src/HOL/Ord.ML	Mon Mar 20 18:24:11 2000 +0100
+++ b/src/HOL/Ord.ML	Mon Mar 20 18:25:35 2000 +0100
@@ -164,10 +164,13 @@
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_max_iff_disj";
 
-qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y" 
-	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);
-qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y" 
-	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);
+Goal "(x::'a::linorder) <= max x y";
+by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
+qed "le_maxI1";
+
+Goal "(y::'a::linorder) <= max x y";
+by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
+qed "le_maxI2";
 (*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)
 
 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";