# HG changeset patch
# User paulson
# Date 969718327 -7200
# Node ID ab03cfd6be3a3238ce17a0dca9abb30491445ae7
# Parent  2f5686cf8c9ad7c3a3459529a1d8f10a6f1565d5
tidied, removing obsolete "goal" commands

diff -r 2f5686cf8c9a -r ab03cfd6be3a src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Sat Sep 23 16:11:38 2000 +0200
+++ b/src/HOL/Gfp.ML	Sat Sep 23 16:12:07 2000 +0200
@@ -14,7 +14,7 @@
 by (etac (CollectI RS Union_upper) 1);
 qed "gfp_upperbound";
 
-val prems = goalw (the_context ()) [gfp_def]
+val prems = Goalw [gfp_def]
     "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
 by (REPEAT (ares_tac ([Union_least]@prems) 1));
 by (etac CollectD 1);
@@ -42,13 +42,9 @@
 by Auto_tac;
 qed "weak_coinduct";
 
-val [prem,mono] = goal (the_context ())
-    "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
+Goal "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
 \    X Un gfp(f) <= f(X Un gfp(f))";
-by (rtac (prem RS Un_least) 1);
-by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
-by (rtac (Un_upper2 RS subset_trans) 1);
-by (rtac (mono RS mono_Un) 1);
+by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
 qed "coinduct_lemma";
 
 (*strong version, thanks to Coen & Frost*)
@@ -57,11 +53,8 @@
 by (REPEAT (ares_tac [UnI1, Un_least] 1));
 qed "coinduct";
 
-val [mono,prem] = goal (the_context ())
-    "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
-by (rtac (mono RS mono_Un RS subsetD) 1);
-by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1);
-by (rtac prem 1);
+Goal "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
+by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
 qed "gfp_fun_UnI2";
 
 (***  Even Stronger version of coinduct  [by Martin Coen]
@@ -72,18 +65,18 @@
 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
 qed "coinduct3_mono_lemma";
 
-val [prem,mono] = goal (the_context ())
-    "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
+Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
 \    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
 by (rtac subset_trans 1);
-by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
+by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1);
 by (rtac (Un_least RS Un_least) 1);
 by (rtac subset_refl 1);
-by (rtac prem 1);
-by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
-by (rtac (mono RS monoD) 1);
-by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
-by (rtac Un_upper2 1);
+by (assume_tac 1); 
+by (rtac (gfp_Tarski RS equalityD1 RS subset_trans) 1);
+by (assume_tac 1);
+by (rtac monoD 1 THEN assume_tac 1);
+by (stac (coinduct3_mono_lemma RS lfp_Tarski) 1);
+by Auto_tac;  
 qed "coinduct3_lemma";
 
 Goal
@@ -96,15 +89,12 @@
 
 (** Definition forms of gfp_Tarski and coinduct, to control unfolding **)
 
-val [rew,mono] = goal (the_context ()) "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
-by (rewtac rew);
-by (rtac (mono RS gfp_Tarski) 1);
+Goal "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
+by (auto_tac (claset() addSIs [gfp_Tarski], simpset()));  
 qed "def_gfp_Tarski";
 
-val rew::prems = goal (the_context ())
-    "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
-by (rewtac rew);
-by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
+Goal "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
+by (auto_tac (claset() addSIs [coinduct], simpset()));  
 qed "def_coinduct";
 
 (*The version used in the induction/coinduction package*)
@@ -116,10 +106,9 @@
 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
 qed "def_Collect_coinduct";
 
-val rew::prems = goal (the_context ())
-    "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
-by (rewtac rew);
-by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
+Goal "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] \
+\     ==> a: A";
+by (auto_tac (claset() addSIs [coinduct3], simpset()));  
 qed "def_coinduct3";
 
 (*Monotonicity of gfp!*)
diff -r 2f5686cf8c9a -r ab03cfd6be3a src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Sat Sep 23 16:11:38 2000 +0200
+++ b/src/HOL/Lfp.ML	Sat Sep 23 16:12:07 2000 +0200
@@ -55,9 +55,8 @@
 
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
-val [rew,mono] = goal (the_context ()) "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
-by (rewtac rew);
-by (rtac (mono RS lfp_Tarski) 1);
+Goal "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
+by (auto_tac (claset() addSIs [lfp_Tarski], simpset()));  
 qed "def_lfp_Tarski";
 
 val rew::prems = Goal
diff -r 2f5686cf8c9a -r ab03cfd6be3a src/HOL/WF.ML
--- a/src/HOL/WF.ML	Sat Sep 23 16:11:38 2000 +0200
+++ b/src/HOL/WF.ML	Sat Sep 23 16:12:07 2000 +0200
@@ -342,10 +342,9 @@
 (*---------------------------------------------------------------------------
  * This form avoids giant explosions in proofs.  NOTE USE OF == 
  *---------------------------------------------------------------------------*)
-val rew::prems = goal (the_context ())
-    "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
-by (rewtac rew);
-by (REPEAT (resolve_tac (prems@[wfrec]) 1));
+Goal "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
+by Auto_tac;
+by (blast_tac (claset() addIs [wfrec]) 1);   
 qed "def_wfrec";