# HG changeset patch
# User lcp
# Date 767976947 -7200
# Node ID edf1ffedf13933e778d8c653408b7a24b969048f
# Parent  b5030aaca2abee4704aadb99bcab6548d615d9e1
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw

diff -r b5030aaca2ab -r edf1ffedf139 src/CTT/Arith.ML
--- a/src/CTT/Arith.ML	Tue May 03 15:14:54 1994 +0200
+++ b/src/CTT/Arith.ML	Tue May 03 16:55:47 1994 +0200
@@ -17,108 +17,86 @@
 
 (*typing of add: short and long versions*)
 
-val add_typing = prove_goal Arith.thy 
+val add_typing = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> a #+ b : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (typechk_tac prems) ]);
+ (fn prems=> [ (typechk_tac prems) ]);
 
-val add_typingL = prove_goal Arith.thy 
+val add_typingL = prove_goalw Arith.thy arith_defs
     "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (equal_tac prems) ]);
+ (fn prems=> [ (equal_tac prems) ]);
 
 
 (*computation for add: 0 and successor cases*)
 
-val addC0 = prove_goal Arith.thy 
+val addC0 = prove_goalw Arith.thy arith_defs
     "b:N ==> 0 #+ b = b : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (rew_tac prems) ]);
+ (fn prems=> [ (rew_tac prems) ]);
 
-val addC_succ = prove_goal Arith.thy 
+val addC_succ = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (rew_tac prems) ]); 
+ (fn prems=> [ (rew_tac prems) ]); 
 
 
 (** Multiplication *)
 
 (*typing of mult: short and long versions*)
 
-val mult_typing = prove_goal Arith.thy 
+val mult_typing = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> a #* b : N"
  (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (typechk_tac([add_typing]@prems)) ]);
+  [ (typechk_tac([add_typing]@prems)) ]);
 
-val mult_typingL = prove_goal Arith.thy 
+val mult_typingL = prove_goalw Arith.thy arith_defs
     "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
  (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (equal_tac (prems@[add_typingL])) ]);
+  [ (equal_tac (prems@[add_typingL])) ]);
 
 (*computation for mult: 0 and successor cases*)
 
-val multC0 = prove_goal Arith.thy 
+val multC0 = prove_goalw Arith.thy arith_defs
     "b:N ==> 0 #* b = 0 : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (rew_tac prems) ]);
+ (fn prems=> [ (rew_tac prems) ]);
 
-val multC_succ = prove_goal Arith.thy 
+val multC_succ = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (rew_tac prems) ]);
+ (fn prems=> [ (rew_tac prems) ]);
 
 
 (** Difference *)
 
 (*typing of difference*)
 
-val diff_typing = prove_goal Arith.thy 
+val diff_typing = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> a - b : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (typechk_tac prems) ]);
+ (fn prems=> [ (typechk_tac prems) ]);
 
-val diff_typingL = prove_goal Arith.thy 
+val diff_typingL = prove_goalw Arith.thy arith_defs
     "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (equal_tac prems) ]);
+ (fn prems=> [ (equal_tac prems) ]);
 
 
 
 (*computation for difference: 0 and successor cases*)
 
-val diffC0 = prove_goal Arith.thy 
+val diffC0 = prove_goalw Arith.thy arith_defs
     "a:N ==> a - 0 = a : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (rew_tac prems) ]);
+ (fn prems=> [ (rew_tac prems) ]);
 
 (*Note: rec(a, 0, %z w.z) is pred(a). *)
 
-val diff_0_eq_0 = prove_goal Arith.thy 
+val diff_0_eq_0 = prove_goalw Arith.thy arith_defs
     "b:N ==> 0 - b = 0 : N"
  (fn prems=>
   [ (NE_tac "b" 1),
-    (rewrite_goals_tac arith_defs),
     (hyp_rew_tac prems) ]);
 
 
 (*Essential to simplify FIRST!!  (Else we get a critical pair)
   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
-val diff_succ_succ = prove_goal Arith.thy 
+val diff_succ_succ = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
  (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (hyp_rew_tac prems),
+  [ (hyp_rew_tac prems),
     (NE_tac "b" 1),
     (hyp_rew_tac prems) ]);
 
@@ -305,40 +283,33 @@
 
 (*typing of absolute difference: short and long versions*)
 
-val absdiff_typing = prove_goal Arith.thy 
+val absdiff_typing = prove_goalw Arith.thy arith_defs
     "[| a:N;  b:N |] ==> a |-| b : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (typechk_tac prems) ]);
+ (fn prems=> [ (typechk_tac prems) ]);
 
-val absdiff_typingL = prove_goal Arith.thy 
+val absdiff_typingL = prove_goalw Arith.thy arith_defs
     "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
- (fn prems=>
-  [ (rewrite_goals_tac arith_defs),
-    (equal_tac prems) ]);
+ (fn prems=> [ (equal_tac prems) ]);
 
-val absdiff_self_eq_0 = prove_goal Arith.thy 
+val absdiff_self_eq_0 = prove_goalw Arith.thy [absdiff_def]
     "a:N ==> a |-| a = 0 : N"
  (fn prems=>
-  [ (rewrite_goals_tac [absdiff_def]),
-    (arith_rew_tac (prems@[diff_self_eq_0])) ]);
+  [ (arith_rew_tac (prems@[diff_self_eq_0])) ]);
 
-val absdiffC0 = prove_goal Arith.thy 
+val absdiffC0 = prove_goalw Arith.thy [absdiff_def]
     "a:N ==> 0 |-| a = a : N"
  (fn prems=>
-  [ (rewrite_goals_tac [absdiff_def]),
-    (hyp_arith_rew_tac prems) ]);
+  [ (hyp_arith_rew_tac prems) ]);
 
 
-val absdiff_succ_succ = prove_goal Arith.thy 
+val absdiff_succ_succ = prove_goalw Arith.thy [absdiff_def]
     "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
  (fn prems=>
-  [ (rewrite_goals_tac [absdiff_def]),
-    (hyp_arith_rew_tac prems) ]);
+  [ (hyp_arith_rew_tac prems) ]);
 
 (*Note how easy using commutative laws can be?  ...not always... *)
-val prems = goal Arith.thy "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
-by (rewrite_goals_tac [absdiff_def]);
+val prems = goalw Arith.thy [absdiff_def]
+    "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
 by (resolve_tac [add_commute] 1);
 by (typechk_tac ([diff_typing]@prems));
 val absdiff_commute = result();
@@ -366,7 +337,7 @@
 val add_eq0 = result();
 
 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-val prems = goal Arith.thy
+val prems = goalw Arith.thy [absdiff_def]
     "[| a:N;  b:N;  a |-| b = 0 : N |] ==> \
 \    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
 by (intr_tac[]);
@@ -374,7 +345,7 @@
 by (resolve_tac [add_eq0] 2);
 by (resolve_tac [add_eq0] 1);
 by (resolve_tac [add_commute RS trans_elem] 6);
-by (typechk_tac (diff_typing:: map (rewrite_rule [absdiff_def]) prems));
+by (typechk_tac (diff_typing::prems));
 val absdiff_eq0_lem = result();
 
 (*if  a |-| b = 0  then  a = b  
@@ -396,62 +367,54 @@
 
 (*typing of remainder: short and long versions*)
 
-val mod_typing = prove_goal Arith.thy
+val mod_typing = prove_goalw Arith.thy [mod_def]
     "[| a:N;  b:N |] ==> a mod b : N"
  (fn prems=>
-  [ (rewrite_goals_tac [mod_def]),
-    (typechk_tac (absdiff_typing::prems)) ]);
+  [ (typechk_tac (absdiff_typing::prems)) ]);
  
-val mod_typingL = prove_goal Arith.thy
+val mod_typingL = prove_goalw Arith.thy [mod_def]
     "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
  (fn prems=>
-  [ (rewrite_goals_tac [mod_def]),
-    (equal_tac (prems@[absdiff_typingL])) ]);
+  [ (equal_tac (prems@[absdiff_typingL])) ]);
  
 
 (*computation for  mod : 0 and successor cases*)
 
-val modC0 = prove_goal Arith.thy "b:N ==> 0 mod b = 0 : N"
+val modC0 = prove_goalw Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
  (fn prems=>
-  [ (rewrite_goals_tac [mod_def]),
-    (rew_tac(absdiff_typing::prems)) ]);
+  [ (rew_tac(absdiff_typing::prems)) ]);
 
-val modC_succ = prove_goal Arith.thy 
+val modC_succ = prove_goalw Arith.thy [mod_def] 
 "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
  (fn prems=>
-  [ (rewrite_goals_tac [mod_def]),
-    (rew_tac(absdiff_typing::prems)) ]);
+  [ (rew_tac(absdiff_typing::prems)) ]);
 
 
 (*typing of quotient: short and long versions*)
 
-val div_typing = prove_goal Arith.thy "[| a:N;  b:N |] ==> a div b : N"
+val div_typing = prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
  (fn prems=>
-  [ (rewrite_goals_tac [div_def]),
-    (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
+  [ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
 
-val div_typingL = prove_goal Arith.thy
+val div_typingL = prove_goalw Arith.thy [div_def]
    "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
  (fn prems=>
-  [ (rewrite_goals_tac [div_def]),
-    (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
+  [ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
 
 val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
 
 
 (*computation for quotient: 0 and successor cases*)
 
-val divC0 = prove_goal Arith.thy "b:N ==> 0 div b = 0 : N"
+val divC0 = prove_goalw Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
  (fn prems=>
-  [ (rewrite_goals_tac [div_def]),
-    (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
+  [ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
 
 val divC_succ =
-prove_goal Arith.thy "[| a:N;  b:N |] ==> succ(a) div b = \
+prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> succ(a) div b = \
 \    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
  (fn prems=>
-  [ (rewrite_goals_tac [div_def]),
-    (rew_tac([mod_typing]@prems)) ]);
+  [ (rew_tac([mod_typing]@prems)) ]);
 
 
 (*Version of above with same condition as the  mod  one*)