--- 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*)