more tidying. also generalized some tactics to prove "Type A" and
authorpaulson
Wed Jul 05 18:27:55 2000 +0200 (2000-07-05)
changeset 9251bd57acd44fc1
parent 9250 0a85dbc4206f
child 9252 83060e826e02
more tidying. also generalized some tactics to prove "Type A" and
"a = b : A" judgements
src/CTT/Arith.ML
src/CTT/Bool.ML
src/CTT/CTT.ML
src/CTT/ex/elim.ML
src/CTT/ex/equal.ML
src/CTT/ex/synth.ML
src/CTT/ex/typechk.ML
     1.1 --- a/src/CTT/Arith.ML	Wed Jul 05 17:52:24 2000 +0200
     1.2 +++ b/src/CTT/Arith.ML	Wed Jul 05 18:27:55 2000 +0200
     1.3 @@ -1,10 +1,8 @@
     1.4 -(*  Title:      CTT/arith
     1.5 +(*  Title:      CTT/Arith
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9  
    1.10 -Theorems for arith.thy (Arithmetic operators)
    1.11 -
    1.12  Proofs about elementary arithmetic: addition, multiplication, etc.
    1.13  Tests definitions and simplifier.
    1.14  *)
    1.15 @@ -16,27 +14,23 @@
    1.16  
    1.17  (*typing of add: short and long versions*)
    1.18  
    1.19 -val prems= goalw Arith.thy arith_defs 
    1.20 -    "[| a:N;  b:N |] ==> a #+ b : N";
    1.21 -by (typechk_tac prems) ;
    1.22 +Goalw arith_defs "[| a:N;  b:N |] ==> a #+ b : N";
    1.23 +by (typechk_tac []) ;
    1.24  qed "add_typing";
    1.25  
    1.26 -val prems= goalw Arith.thy arith_defs 
    1.27 -    "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
    1.28 -by (equal_tac prems) ;
    1.29 +Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
    1.30 +by (equal_tac []) ;
    1.31  qed "add_typingL";
    1.32  
    1.33  
    1.34  (*computation for add: 0 and successor cases*)
    1.35  
    1.36 -val prems= goalw Arith.thy arith_defs 
    1.37 -    "b:N ==> 0 #+ b = b : N";
    1.38 -by (rew_tac prems) ;
    1.39 +Goalw arith_defs "b:N ==> 0 #+ b = b : N";
    1.40 +by (rew_tac []) ;
    1.41  qed "addC0";
    1.42  
    1.43 -val prems= goalw Arith.thy arith_defs 
    1.44 -    "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
    1.45 -by (rew_tac prems) ;
    1.46 +Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
    1.47 +by (rew_tac []) ;
    1.48  qed "addC_succ"; 
    1.49  
    1.50  
    1.51 @@ -44,26 +38,22 @@
    1.52  
    1.53  (*typing of mult: short and long versions*)
    1.54  
    1.55 -val prems= goalw Arith.thy arith_defs 
    1.56 -    "[| a:N;  b:N |] ==> a #* b : N";
    1.57 -by (typechk_tac([add_typing]@prems)) ;
    1.58 +Goalw arith_defs "[| a:N;  b:N |] ==> a #* b : N";
    1.59 +by (typechk_tac [add_typing]) ;
    1.60  qed "mult_typing";
    1.61  
    1.62 -val prems= goalw Arith.thy arith_defs 
    1.63 -    "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
    1.64 -by (equal_tac (prems@[add_typingL])) ;
    1.65 +Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
    1.66 +by (equal_tac [add_typingL]) ;
    1.67  qed "mult_typingL";
    1.68  
    1.69  (*computation for mult: 0 and successor cases*)
    1.70  
    1.71 -val prems= goalw Arith.thy arith_defs 
    1.72 -    "b:N ==> 0 #* b = 0 : N";
    1.73 -by (rew_tac prems) ;
    1.74 +Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
    1.75 +by (rew_tac []) ;
    1.76  qed "multC0";
    1.77  
    1.78 -val prems= goalw Arith.thy arith_defs 
    1.79 -    "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
    1.80 -by (rew_tac prems) ;
    1.81 +Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
    1.82 +by (rew_tac []) ;
    1.83  qed "multC_succ";
    1.84  
    1.85  
    1.86 @@ -71,41 +61,36 @@
    1.87  
    1.88  (*typing of difference*)
    1.89  
    1.90 -val prems= goalw Arith.thy arith_defs 
    1.91 -    "[| a:N;  b:N |] ==> a - b : N";
    1.92 -by (typechk_tac prems) ;
    1.93 +Goalw arith_defs "[| a:N;  b:N |] ==> a - b : N";
    1.94 +by (typechk_tac []) ;
    1.95  qed "diff_typing";
    1.96  
    1.97 -val prems= goalw Arith.thy arith_defs 
    1.98 -    "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
    1.99 -by (equal_tac prems) ;
   1.100 +Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
   1.101 +by (equal_tac []) ;
   1.102  qed "diff_typingL";
   1.103  
   1.104  
   1.105  
   1.106  (*computation for difference: 0 and successor cases*)
   1.107  
   1.108 -val prems= goalw Arith.thy arith_defs 
   1.109 -    "a:N ==> a - 0 = a : N";
   1.110 -by (rew_tac prems) ;
   1.111 +Goalw arith_defs "a:N ==> a - 0 = a : N";
   1.112 +by (rew_tac []) ;
   1.113  qed "diffC0";
   1.114  
   1.115  (*Note: rec(a, 0, %z w.z) is pred(a). *)
   1.116  
   1.117 -val prems= goalw Arith.thy arith_defs 
   1.118 -    "b:N ==> 0 - b = 0 : N";
   1.119 +Goalw arith_defs "b:N ==> 0 - b = 0 : N";
   1.120  by (NE_tac "b" 1);
   1.121 -by (hyp_rew_tac prems) ;
   1.122 +by (hyp_rew_tac []) ;
   1.123  qed "diff_0_eq_0";
   1.124  
   1.125  
   1.126  (*Essential to simplify FIRST!!  (Else we get a critical pair)
   1.127    succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
   1.128 -val prems= goalw Arith.thy arith_defs 
   1.129 -    "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
   1.130 -by (hyp_rew_tac prems);
   1.131 +Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
   1.132 +by (hyp_rew_tac []);
   1.133  by (NE_tac "b" 1);
   1.134 -by (hyp_rew_tac prems) ;
   1.135 +by (hyp_rew_tac []) ;
   1.136  qed "diff_succ_succ";
   1.137  
   1.138  
   1.139 @@ -152,23 +137,21 @@
   1.140   **********)
   1.141  
   1.142  (*Associative law for addition*)
   1.143 -val prems= goal Arith.thy 
   1.144 -    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
   1.145 +Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
   1.146  by (NE_tac "a" 1);
   1.147 -by (hyp_arith_rew_tac prems) ;
   1.148 +by (hyp_arith_rew_tac []) ;
   1.149  qed "add_assoc";
   1.150  
   1.151  
   1.152  (*Commutative law for addition.  Can be proved using three inductions.
   1.153    Must simplify after first induction!  Orientation of rewrites is delicate*)  
   1.154 -val prems= goal Arith.thy 
   1.155 -    "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
   1.156 +Goal "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
   1.157  by (NE_tac "a" 1);
   1.158 -by (hyp_arith_rew_tac prems);
   1.159 +by (hyp_arith_rew_tac []);
   1.160  by (NE_tac "b" 2);
   1.161  by (rtac sym_elem 1);
   1.162  by (NE_tac "b" 1);
   1.163 -by (hyp_arith_rew_tac prems) ;
   1.164 +by (hyp_arith_rew_tac []) ;
   1.165  qed "add_commute";
   1.166  
   1.167  
   1.168 @@ -177,52 +160,48 @@
   1.169   ****************)
   1.170  
   1.171  (*Commutative law for multiplication
   1.172 -val prems= goal Arith.thy 
   1.173 -    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.174 +Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.175  by (NE_tac "a" 1);
   1.176 -by (hyp_arith_rew_tac prems);
   1.177 +by (hyp_arith_rew_tac []);
   1.178  by (NE_tac "b" 2);
   1.179  by (rtac sym_elem 1);
   1.180  by (NE_tac "b" 1);
   1.181 -by (hyp_arith_rew_tac prems) ;
   1.182 +by (hyp_arith_rew_tac []) ;
   1.183  qed "mult_commute";   NEEDS COMMUTATIVE MATCHING
   1.184  ***************)
   1.185  
   1.186  (*right annihilation in product*)
   1.187 -val prems= goal Arith.thy 
   1.188 -    "a:N ==> a #* 0 = 0 : N";
   1.189 +Goal "a:N ==> a #* 0 = 0 : N";
   1.190  by (NE_tac "a" 1);
   1.191 -by (hyp_arith_rew_tac prems) ;
   1.192 +by (hyp_arith_rew_tac []) ;
   1.193  qed "mult_0_right";
   1.194  
   1.195  (*right successor law for multiplication*)
   1.196 -val prems= goal Arith.thy 
   1.197 -    "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
   1.198 +Goal "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
   1.199  by (NE_tac "a" 1);
   1.200 -by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem]));
   1.201 -by (REPEAT (assume_tac 1  ORELSE resolve_tac (prems@[add_commute,mult_typingL,add_typingL]@ intrL_rls@[refl_elem])   1)) ;
   1.202 +by (hyp_arith_rew_tac [add_assoc RS sym_elem]);
   1.203 +by (REPEAT (assume_tac 1
   1.204 +     ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@
   1.205 +			 [refl_elem])   1)) ;
   1.206  qed "mult_succ_right";
   1.207  
   1.208  (*Commutative law for multiplication*)
   1.209 -val prems= goal Arith.thy 
   1.210 -    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.211 +Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.212  by (NE_tac "a" 1);
   1.213 -by (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ;
   1.214 +by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
   1.215  qed "mult_commute";
   1.216  
   1.217  (*addition distributes over multiplication*)
   1.218 -val prems= goal Arith.thy 
   1.219 -    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
   1.220 +Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
   1.221  by (NE_tac "a" 1);
   1.222 -by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ;
   1.223 +by (hyp_arith_rew_tac [add_assoc RS sym_elem]) ;
   1.224  qed "add_mult_distrib";
   1.225  
   1.226  
   1.227  (*Associative law for multiplication*)
   1.228 -val prems= goal Arith.thy 
   1.229 -    "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
   1.230 +Goal "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
   1.231  by (NE_tac "a" 1);
   1.232 -by (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ;
   1.233 +by (hyp_arith_rew_tac [add_mult_distrib]) ;
   1.234  qed "mult_assoc";
   1.235  
   1.236  
   1.237 @@ -233,10 +212,9 @@
   1.238  Difference on natural numbers, without negative numbers
   1.239    a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
   1.240  
   1.241 -val prems= goal Arith.thy 
   1.242 -    "a:N ==> a - a = 0 : N";
   1.243 +Goal "a:N ==> a - a = 0 : N";
   1.244  by (NE_tac "a" 1);
   1.245 -by (hyp_arith_rew_tac prems) ;
   1.246 +by (hyp_arith_rew_tac []) ;
   1.247  qed "diff_self_eq_0";
   1.248  
   1.249  
   1.250 @@ -246,9 +224,7 @@
   1.251  (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   1.252    An example of induction over a quantified formula (a product).
   1.253    Uses rewriting with a quantified, implicative inductive hypothesis.*)
   1.254 -val prems =
   1.255 -goal Arith.thy 
   1.256 -    "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
   1.257 +Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
   1.258  by (NE_tac "b" 1);
   1.259  (*strip one "universal quantifier" but not the "implication"*)
   1.260  by (resolve_tac intr_rls 3);  
   1.261 @@ -258,11 +234,11 @@
   1.262  (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   1.263  by (rtac replace_type 5);
   1.264  by (rtac replace_type 4);
   1.265 -by (arith_rew_tac prems); 
   1.266 +by (arith_rew_tac []); 
   1.267  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   1.268    Both follow by rewriting, (2) using quantified induction hyp*)
   1.269  by (intr_tac[]);  (*strips remaining PRODs*)
   1.270 -by (hyp_arith_rew_tac (prems@[add_0_right]));  
   1.271 +by (hyp_arith_rew_tac [add_0_right]);  
   1.272  by (assume_tac 1);
   1.273  qed "add_diff_inverse_lemma";
   1.274  
   1.275 @@ -271,11 +247,10 @@
   1.276    Using ProdE does not work -- for ?B(?a) is ambiguous.
   1.277    Instead, add_diff_inverse_lemma states the desired induction scheme;
   1.278      the use of RS below instantiates Vars in ProdE automatically. *)
   1.279 -val prems =
   1.280 -goal Arith.thy "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
   1.281 +Goal "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
   1.282  by (rtac EqE 1);
   1.283  by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
   1.284 -by (REPEAT (resolve_tac (prems@[EqI]) 1));
   1.285 +by (REPEAT (ares_tac [EqI] 1));
   1.286  qed "add_diff_inverse";
   1.287  
   1.288  
   1.289 @@ -285,63 +260,55 @@
   1.290  
   1.291  (*typing of absolute difference: short and long versions*)
   1.292  
   1.293 -val prems= goalw Arith.thy arith_defs 
   1.294 -    "[| a:N;  b:N |] ==> a |-| b : N";
   1.295 -by (typechk_tac prems) ;
   1.296 +Goalw arith_defs "[| a:N;  b:N |] ==> a |-| b : N";
   1.297 +by (typechk_tac []) ;
   1.298  qed "absdiff_typing";
   1.299  
   1.300 -val prems= goalw Arith.thy arith_defs 
   1.301 -    "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
   1.302 -by (equal_tac prems) ;
   1.303 +Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
   1.304 +by (equal_tac []) ;
   1.305  qed "absdiff_typingL";
   1.306  
   1.307 -Goalw [absdiff_def]  
   1.308 -    "a:N ==> a |-| a = 0 : N";
   1.309 -by (arith_rew_tac (prems@[diff_self_eq_0])) ;
   1.310 +Goalw [absdiff_def] "a:N ==> a |-| a = 0 : N";
   1.311 +by (arith_rew_tac [diff_self_eq_0]) ;
   1.312  qed "absdiff_self_eq_0";
   1.313  
   1.314 -Goalw [absdiff_def]  
   1.315 -    "a:N ==> 0 |-| a = a : N";
   1.316 +Goalw [absdiff_def] "a:N ==> 0 |-| a = a : N";
   1.317  by (hyp_arith_rew_tac []);
   1.318  qed "absdiffC0";
   1.319  
   1.320  
   1.321 -Goalw [absdiff_def]  
   1.322 -    "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
   1.323 +Goalw [absdiff_def] "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
   1.324  by (hyp_arith_rew_tac []) ;
   1.325  qed "absdiff_succ_succ";
   1.326  
   1.327  (*Note how easy using commutative laws can be?  ...not always... *)
   1.328 -val prems = goalw Arith.thy [absdiff_def]
   1.329 -    "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
   1.330 +Goalw [absdiff_def] "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
   1.331  by (rtac add_commute 1);
   1.332 -by (typechk_tac ([diff_typing]@prems));
   1.333 +by (typechk_tac [diff_typing]);
   1.334  qed "absdiff_commute";
   1.335  
   1.336  (*If a+b=0 then a=0.   Surprisingly tedious*)
   1.337 -val prems =
   1.338 -goal Arith.thy "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
   1.339 +Goal "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
   1.340  by (NE_tac "a" 1);
   1.341  by (rtac replace_type 3);
   1.342 -by (arith_rew_tac prems);
   1.343 +by (arith_rew_tac []);
   1.344  by (intr_tac[]);  (*strips remaining PRODs*)
   1.345  by (resolve_tac [ zero_ne_succ RS FE ] 2);
   1.346  by (etac (EqE RS sym_elem) 3);
   1.347 -by (typechk_tac ([add_typing] @prems));
   1.348 +by (typechk_tac [add_typing]);
   1.349  qed "add_eq0_lemma";
   1.350  
   1.351  (*Version of above with the premise  a+b=0.
   1.352    Again, resolution instantiates variables in ProdE *)
   1.353 -val prems =
   1.354 -goal Arith.thy "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
   1.355 +Goal "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
   1.356  by (rtac EqE 1);
   1.357  by (resolve_tac [add_eq0_lemma RS ProdE] 1);
   1.358  by (rtac EqI 3);
   1.359 -by (ALLGOALS (resolve_tac prems));
   1.360 +by (typechk_tac []) ;
   1.361  qed "add_eq0";
   1.362  
   1.363  (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   1.364 -val prems = goalw Arith.thy [absdiff_def]
   1.365 +Goalw [absdiff_def]
   1.366      "[| a:N;  b:N;  a |-| b = 0 : N |] ==> \
   1.367  \    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
   1.368  by (intr_tac[]);
   1.369 @@ -349,20 +316,19 @@
   1.370  by (rtac add_eq0 2);
   1.371  by (rtac add_eq0 1);
   1.372  by (resolve_tac [add_commute RS trans_elem] 6);
   1.373 -by (typechk_tac (diff_typing::prems));
   1.374 +by (typechk_tac [diff_typing]);
   1.375  qed "absdiff_eq0_lem";
   1.376  
   1.377  (*if  a |-| b = 0  then  a = b  
   1.378    proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   1.379 -val prems =
   1.380 -goal Arith.thy "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
   1.381 +Goal "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
   1.382  by (rtac EqE 1);
   1.383  by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
   1.384 -by (TRYALL (resolve_tac prems));
   1.385 +by (TRYALL assume_tac);
   1.386  by eqintr_tac;
   1.387  by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
   1.388  by (rtac EqE 3  THEN  assume_tac 3);
   1.389 -by (hyp_arith_rew_tac (prems@[add_0_right]));
   1.390 +by (hyp_arith_rew_tac [add_0_right]);
   1.391  qed "absdiff_eq0";
   1.392  
   1.393  (***********************
   1.394 @@ -371,40 +337,35 @@
   1.395  
   1.396  (*typing of remainder: short and long versions*)
   1.397  
   1.398 -Goalw [mod_def]  
   1.399 -    "[| a:N;  b:N |] ==> a mod b : N";
   1.400 -by (typechk_tac (absdiff_typing::prems)) ;
   1.401 +Goalw [mod_def] "[| a:N;  b:N |] ==> a mod b : N";
   1.402 +by (typechk_tac [absdiff_typing]) ;
   1.403  qed "mod_typing";
   1.404   
   1.405 -Goalw [mod_def]  
   1.406 -    "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
   1.407 +Goalw [mod_def] "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
   1.408  by (equal_tac [absdiff_typingL]) ;
   1.409 -by (ALLGOALS assume_tac);
   1.410  qed "mod_typingL";
   1.411   
   1.412  
   1.413  (*computation for  mod : 0 and successor cases*)
   1.414  
   1.415  Goalw [mod_def]   "b:N ==> 0 mod b = 0 : N";
   1.416 -by (rew_tac(absdiff_typing::prems)) ;
   1.417 +by (rew_tac [absdiff_typing]) ;
   1.418  qed "modC0";
   1.419  
   1.420  Goalw [mod_def]   
   1.421  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
   1.422 -by (rew_tac(absdiff_typing::prems)) ;
   1.423 +by (rew_tac [absdiff_typing]) ;
   1.424  qed "modC_succ";
   1.425  
   1.426  
   1.427  (*typing of quotient: short and long versions*)
   1.428  
   1.429  Goalw [div_def]   "[| a:N;  b:N |] ==> a div b : N";
   1.430 -by (typechk_tac ([absdiff_typing,mod_typing]@prems)) ;
   1.431 +by (typechk_tac [absdiff_typing,mod_typing]) ;
   1.432  qed "div_typing";
   1.433  
   1.434 -Goalw [div_def]  
   1.435 -   "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
   1.436 +Goalw [div_def] "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
   1.437  by (equal_tac [absdiff_typingL, mod_typingL]);
   1.438 -by (ALLGOALS assume_tac);
   1.439  qed "div_typingL";
   1.440  
   1.441  val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
   1.442 @@ -413,54 +374,51 @@
   1.443  (*computation for quotient: 0 and successor cases*)
   1.444  
   1.445  Goalw [div_def]   "b:N ==> 0 div b = 0 : N";
   1.446 -by (rew_tac([mod_typing, absdiff_typing] @ prems)) ;
   1.447 +by (rew_tac [mod_typing, absdiff_typing]) ;
   1.448  qed "divC0";
   1.449  
   1.450  Goalw [div_def] 
   1.451   "[| a:N;  b:N |] ==> succ(a) div b = \
   1.452  \    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N";
   1.453 -by (rew_tac([mod_typing]@prems)) ;
   1.454 +by (rew_tac [mod_typing]) ;
   1.455  qed "divC_succ";
   1.456  
   1.457  
   1.458  (*Version of above with same condition as the  mod  one*)
   1.459 -val prems= goal Arith.thy
   1.460 -    "[| a:N;  b:N |] ==> \
   1.461 +Goal "[| a:N;  b:N |] ==> \
   1.462  \    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N";
   1.463  by (resolve_tac [ divC_succ RS trans_elem ] 1);
   1.464 -by (rew_tac(div_typing_rls @ prems @ [modC_succ]));
   1.465 +by (rew_tac(div_typing_rls @ [modC_succ]));
   1.466  by (NE_tac "succ(a mod b)|-|b" 1);
   1.467 -by (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ;
   1.468 +by (rew_tac [mod_typing, div_typing, absdiff_typing]);
   1.469  qed "divC_succ2";
   1.470  
   1.471  (*for case analysis on whether a number is 0 or a successor*)
   1.472 -val prems= goal Arith.thy
   1.473 -    "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
   1.474 +Goal "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
   1.475  \                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))";
   1.476  by (NE_tac "a" 1);
   1.477  by (rtac PlusI_inr 3);
   1.478  by (rtac PlusI_inl 2);
   1.479  by eqintr_tac;
   1.480 -by (equal_tac prems) ;
   1.481 +by (equal_tac []) ;
   1.482  qed "iszero_decidable";
   1.483  
   1.484  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   1.485 -val prems =
   1.486 -goal Arith.thy "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
   1.487 +Goal "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
   1.488  by (NE_tac "a" 1);
   1.489 -by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); 
   1.490 +by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); 
   1.491  by (rtac EqE 1);
   1.492  (*case analysis on   succ(u mod b)|-|b  *)
   1.493  by (res_inst_tac [("a1", "succ(u mod b) |-| b")] 
   1.494                   (iszero_decidable RS PlusE) 1);
   1.495  by (etac SumE 3);
   1.496 -by (hyp_arith_rew_tac (prems @ div_typing_rls @
   1.497 +by (hyp_arith_rew_tac (div_typing_rls @
   1.498          [modC0,modC_succ, divC0, divC_succ2])); 
   1.499  (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   1.500  by (resolve_tac [ add_typingL RS trans_elem ] 1);
   1.501  by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
   1.502  by (rtac refl_elem 3);
   1.503 -by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
   1.504 +by (hyp_arith_rew_tac (div_typing_rls)); 
   1.505  qed "mod_div_equality";
   1.506  
   1.507  writeln"Reached end of file.";
     2.1 --- a/src/CTT/Bool.ML	Wed Jul 05 17:52:24 2000 +0200
     2.2 +++ b/src/CTT/Bool.ML	Wed Jul 05 18:27:55 2000 +0200
     2.3 @@ -1,9 +1,9 @@
     2.4 -(*  Title:      CTT/bool
     2.5 +(*  Title:      CTT/Bool
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1991  University of Cambridge
     2.9  
    2.10 -Theorems for bool.thy (booleans and conditionals)
    2.11 +The two-element type (booleans and conditionals)
    2.12  *)
    2.13  
    2.14  val bool_defs = [Bool_def,true_def,false_def,cond_def];
     3.1 --- a/src/CTT/CTT.ML	Wed Jul 05 17:52:24 2000 +0200
     3.2 +++ b/src/CTT/CTT.ML	Wed Jul 05 18:27:55 2000 +0200
     3.3 @@ -1,9 +1,9 @@
     3.4 -(*  Title:      CTT/ctt.ML
     3.5 +(*  Title:      CTT/CTT.ML
     3.6      ID:         $Id$
     3.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8      Copyright   1991  University of Cambridge
     3.9  
    3.10 -Tactics and lemmas for ctt.thy (Constructive Type Theory)
    3.11 +Tactics and derived rules for Constructive Type Theory
    3.12  *)
    3.13  
    3.14  (*Formation rules*)
    3.15 @@ -33,30 +33,30 @@
    3.16  val basic_defs = [fst_def,snd_def];
    3.17  
    3.18  (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    3.19 -val prems= goal CTT.thy
    3.20 -    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
    3.21 +Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
    3.22  by (rtac sym_elem 1);
    3.23  by (rtac SumIL 1);
    3.24  by (ALLGOALS (rtac sym_elem ));
    3.25 -by (ALLGOALS (resolve_tac prems)) ;
    3.26 +by (ALLGOALS assume_tac) ;
    3.27  qed "SumIL2";
    3.28  
    3.29  val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
    3.30  
    3.31  (*Exploit p:Prod(A,B) to create the assumption z:B(a).  
    3.32    A more natural form of product elimination. *)
    3.33 -val prems= goal CTT.thy
    3.34 -    "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    3.35 +val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    3.36  \    |] ==> c(p`a): C(p`a)";
    3.37 -by (REPEAT (resolve_tac (prems@[ProdE]) 1)) ;
    3.38 +by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
    3.39  qed "subst_prodE";
    3.40  
    3.41  (** Tactics for type checking **)
    3.42  
    3.43 -fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))
    3.44 +fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
    3.45 +  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
    3.46 +  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
    3.47    | is_rigid_elem _ = false;
    3.48  
    3.49 -(*Try solving a:A by assumption provided a is rigid!*) 
    3.50 +(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
    3.51  val test_assume_tac = SUBGOAL(fn (prem,i) =>
    3.52      if is_rigid_elem (Logic.strip_assums_concl prem)
    3.53      then  assume_tac i  else  no_tac);
    3.54 @@ -72,7 +72,7 @@
    3.55  
    3.56  
    3.57  (*Solve all subgoals "A type" using formation rules. *)
    3.58 -val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
    3.59 +val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
    3.60  
    3.61  
    3.62  (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    3.63 @@ -98,16 +98,15 @@
    3.64  (*** Simplification ***)
    3.65  
    3.66  (*To simplify the type in a goal*)
    3.67 -val prems= goal CTT.thy
    3.68 -    "[| B = A;  a : A |] ==> a : B";
    3.69 +Goal "[| B = A;  a : A |] ==> a : B";
    3.70  by (rtac equal_types 1);
    3.71  by (rtac sym_type 2);
    3.72 -by (ALLGOALS (resolve_tac prems)) ;
    3.73 +by (ALLGOALS assume_tac) ;
    3.74  qed "replace_type";
    3.75  
    3.76  (*Simplify the parameter of a unary type operator.*)
    3.77 -val prems= goal CTT.thy
    3.78 -    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)";
    3.79 +val prems = Goal
    3.80 +     "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
    3.81  by (rtac subst_typeL 1);
    3.82  by (rtac refl_type 2);
    3.83  by (ALLGOALS (resolve_tac prems));
    3.84 @@ -175,14 +174,13 @@
    3.85  
    3.86  (** The elimination rules for fst/snd **)
    3.87  
    3.88 -val [major] = goalw CTT.thy basic_defs
    3.89 -    "p : Sum(A,B) ==> fst(p) : A";
    3.90 -by (rtac (major RS SumE) 1);
    3.91 -by (assume_tac 1) ;
    3.92 +Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
    3.93 +by (etac SumE 1);
    3.94 +by (assume_tac 1);
    3.95  qed "SumE_fst";
    3.96  
    3.97  (*The first premise must be p:Sum(A,B) !!*)
    3.98 -val major::prems= goalw CTT.thy basic_defs
    3.99 +val major::prems= Goalw basic_defs
   3.100      "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
   3.101  \    |] ==> snd(p) : B(fst(p))";
   3.102  by (rtac (major RS SumE) 1);
     4.1 --- a/src/CTT/ex/elim.ML	Wed Jul 05 17:52:24 2000 +0200
     4.2 +++ b/src/CTT/ex/elim.ML	Wed Jul 05 18:27:55 2000 +0200
     4.3 @@ -15,8 +15,8 @@
     4.4  
     4.5  
     4.6  writeln"This finds the functions fst and snd!"; 
     4.7 -val prems = goal CTT.thy "A type ==> ?a : (A*A) --> A";
     4.8 -by (pc_tac prems 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
     4.9 +Goal "A type ==> ?a : (A*A) --> A";
    4.10 +by (pc_tac [] 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
    4.11  result();
    4.12  writeln"first solution is fst;  backtracking gives snd";
    4.13  back(); 
    4.14 @@ -24,47 +24,43 @@
    4.15  
    4.16  
    4.17  writeln"Double negation of the Excluded Middle";
    4.18 -val prems = goal CTT.thy "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
    4.19 -by (intr_tac prems);
    4.20 +Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
    4.21 +by (intr_tac []);
    4.22  by (rtac ProdE 1);
    4.23  by (assume_tac 1);
    4.24 -by (pc_tac prems 1);
    4.25 +by (pc_tac [] 1);
    4.26  result();
    4.27  
    4.28 -val prems = goal CTT.thy 
    4.29 -    "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
    4.30 -by (pc_tac prems 1);
    4.31 +Goal "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
    4.32 +by (pc_tac [] 1);
    4.33  result();
    4.34  (*The sequent version (ITT) could produce an interesting alternative
    4.35    by backtracking.  No longer.*)
    4.36  
    4.37  writeln"Binary sums and products";
    4.38 -val prems = goal CTT.thy
    4.39 -   "[| A type;  B type;  C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
    4.40 -by (pc_tac prems 1);
    4.41 +Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
    4.42 +by (pc_tac [] 1);
    4.43  result();
    4.44  
    4.45  (*A distributive law*)
    4.46 -val prems = goal CTT.thy 
    4.47 -    "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
    4.48 -by (pc_tac prems 1);
    4.49 +Goal "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
    4.50 +by (pc_tac [] 1);
    4.51  result();
    4.52  
    4.53  (*more general version, same proof*)
    4.54 -val prems = goal CTT.thy 
    4.55 -    "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
    4.56 -\    ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
    4.57 +val prems = Goal
    4.58 +   "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
    4.59 +\      ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
    4.60  by (pc_tac prems 1);
    4.61  result();
    4.62  
    4.63  writeln"Construction of the currying functional";
    4.64 -val prems = goal CTT.thy 
    4.65 -    "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
    4.66 -by (pc_tac prems 1);
    4.67 +Goal "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
    4.68 +by (pc_tac [] 1);
    4.69  result();
    4.70  
    4.71  (*more general goal with same proof*)
    4.72 -val prems = goal CTT.thy
    4.73 +val prems = Goal
    4.74      "[| A type; !!x. x:A ==> B(x) type;                         \
    4.75  \               !!z. z: (SUM x:A. B(x)) ==> C(z) type           \
    4.76  \    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).    \
    4.77 @@ -73,27 +69,25 @@
    4.78  result();
    4.79  
    4.80  writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
    4.81 -val prems = goal CTT.thy 
    4.82 -    "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
    4.83 -by (pc_tac prems 1);
    4.84 +Goal "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
    4.85 +by (pc_tac [] 1);
    4.86  result();
    4.87  
    4.88  (*more general goal with same proof*)
    4.89 -val prems = goal CTT.thy 
    4.90 -  "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \
    4.91 +val prems = Goal 
    4.92 + "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \
    4.93  \  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
    4.94  \       --> (PROD z : (SUM x:A . B(x)) . C(z))";
    4.95  by (pc_tac prems 1);
    4.96  result();
    4.97  
    4.98  writeln"Function application";
    4.99 -val prems = goal CTT.thy  
   4.100 -    "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
   4.101 -by (pc_tac prems 1);
   4.102 +Goal "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
   4.103 +by (pc_tac [] 1);
   4.104  result();
   4.105  
   4.106  writeln"Basic test of quantifier reasoning";
   4.107 -val prems = goal CTT.thy  
   4.108 +val prems = Goal  
   4.109      "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
   4.110  \    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
   4.111  \         --> (PROD x:A . SUM y:B . C(x,y))";
   4.112 @@ -105,7 +99,7 @@
   4.113  by (pc_tac prems 1);        ...fails!!  *)
   4.114  
   4.115  writeln"Martin-Lof (1984) pages 36-7: the combinator S";
   4.116 -val prems = goal CTT.thy  
   4.117 +val prems = Goal  
   4.118      "[| A type;  !!x. x:A ==> B(x) type;  \
   4.119  \       !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
   4.120  \    ==> ?a :    (PROD x:A. PROD y:B(x). C(x,y)) \
   4.121 @@ -114,7 +108,7 @@
   4.122  result();
   4.123  
   4.124  writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
   4.125 -val prems = goal CTT.thy
   4.126 +val prems = Goal
   4.127      "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
   4.128  \    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
   4.129  \         --> (PROD z: A+B. C(z))";
   4.130 @@ -122,15 +116,14 @@
   4.131  result();
   4.132  
   4.133  (*towards AXIOM OF CHOICE*)
   4.134 -val prems = goal CTT.thy  
   4.135 -  "[| A type;  B type;  C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
   4.136 -by (pc_tac prems 1);
   4.137 +Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
   4.138 +by (pc_tac [] 1);
   4.139  by (fold_tac basic_defs);   (*puts in fst and snd*)
   4.140  result();
   4.141  
   4.142  (*Martin-Lof (1984) page 50*)
   4.143 -writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
   4.144 -val prems = goal CTT.thy   
   4.145 +writeln"AXIOM OF CHOICE!  Delicate use of elimination rules";
   4.146 +val prems = Goal   
   4.147      "[| A type;  !!x. x:A ==> B(x) type;                        \
   4.148  \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
   4.149  \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
   4.150 @@ -147,7 +140,7 @@
   4.151  result();
   4.152  
   4.153  writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
   4.154 -val prems = goal CTT.thy   
   4.155 +val prems = Goal   
   4.156      "[| A type;  !!x. x:A ==> B(x) type;                         \
   4.157  \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
   4.158  \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
   4.159 @@ -172,7 +165,7 @@
   4.160  writeln"Example of sequent_style deduction"; 
   4.161  (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   4.162      lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
   4.163 -val prems = goal CTT.thy   
   4.164 +val prems = Goal   
   4.165      "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
   4.166  \    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
   4.167  by (resolve_tac intr_rls 1);
     5.1 --- a/src/CTT/ex/equal.ML	Wed Jul 05 17:52:24 2000 +0200
     5.2 +++ b/src/CTT/ex/equal.ML	Wed Jul 05 18:27:55 2000 +0200
     5.3 @@ -6,78 +6,68 @@
     5.4  Equality reasoning by rewriting.
     5.5  *)
     5.6  
     5.7 -val prems =
     5.8 -goal CTT.thy "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
     5.9 +Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
    5.10  by (rtac EqE 1);
    5.11 -by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    5.12 -by (rew_tac prems);
    5.13 +by (resolve_tac elim_rls 1  THEN  assume_tac 1);
    5.14 +by (rew_tac []);
    5.15  qed "split_eq";
    5.16  
    5.17 -val prems =
    5.18 -goal CTT.thy
    5.19 -    "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
    5.20 +Goal "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
    5.21  by (rtac EqE 1);
    5.22 -by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    5.23 -by (rew_tac prems);
    5.24 +by (resolve_tac elim_rls 1  THEN  assume_tac 1);
    5.25 +by (rew_tac []);
    5.26 +by (ALLGOALS assume_tac);
    5.27  qed "when_eq";
    5.28  
    5.29  
    5.30  (*in the "rec" formulation of addition, 0+n=n *)
    5.31 -val prems =
    5.32 -goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
    5.33 +Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
    5.34  by (rtac EqE 1);
    5.35 -by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    5.36 -by (rew_tac prems);
    5.37 +by (resolve_tac elim_rls 1  THEN  assume_tac 1);
    5.38 +by (rew_tac []);
    5.39  result();
    5.40  
    5.41  
    5.42  (*the harder version, n+0=n: recursive, uses induction hypothesis*)
    5.43 -val prems =
    5.44 -goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
    5.45 +Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
    5.46  by (rtac EqE 1);
    5.47 -by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    5.48 -by (hyp_rew_tac prems);
    5.49 +by (resolve_tac elim_rls 1  THEN  assume_tac 1);
    5.50 +by (hyp_rew_tac []);
    5.51  result();
    5.52  
    5.53  
    5.54  (*Associativity of addition*)
    5.55 -val prems =
    5.56 -goal CTT.thy
    5.57 -   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
    5.58 -\                   rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
    5.59 +Goal "[| a:N;  b:N;  c:N |] \
    5.60 +\     ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
    5.61 +\         rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
    5.62  by (NE_tac "a" 1);
    5.63 -by (hyp_rew_tac prems);
    5.64 +by (hyp_rew_tac []);
    5.65  result();
    5.66  
    5.67  
    5.68  (*Martin-Lof (1984) page 62: pairing is surjective*)
    5.69 -val prems =
    5.70 -goal CTT.thy
    5.71 -    "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
    5.72 +Goal "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
    5.73  by (rtac EqE 1);
    5.74 -by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    5.75 -by (DEPTH_SOLVE_1 (rew_tac prems));   (*!!!!!!!*)
    5.76 +by (resolve_tac elim_rls 1  THEN  assume_tac 1);
    5.77 +by (DEPTH_SOLVE_1 (rew_tac []));   (*!!!!!!!*)
    5.78  result();
    5.79  
    5.80  
    5.81 -val prems =
    5.82 -goal CTT.thy "[| a : A;  b : B |] ==> \
    5.83 +Goal "[| a : A;  b : B |] ==> \
    5.84  \    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
    5.85 -by (rew_tac prems);
    5.86 +by (rew_tac []);
    5.87  result();
    5.88  
    5.89  
    5.90  (*a contrived, complicated simplication, requires sum-elimination also*)
    5.91 -val prems =
    5.92 -goal CTT.thy
    5.93 -   "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
    5.94 +Goal "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
    5.95  \     lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)";
    5.96  by (resolve_tac reduction_rls 1);
    5.97  by (resolve_tac intrL_rls 3);
    5.98  by (rtac EqE 4);
    5.99  by (rtac SumE 4  THEN  assume_tac 4);
   5.100  (*order of unifiers is essential here*)
   5.101 -by (rew_tac prems);
   5.102 +by (rew_tac []);
   5.103  result();
   5.104  
   5.105  writeln"Reached end of file.";
     6.1 --- a/src/CTT/ex/synth.ML	Wed Jul 05 17:52:24 2000 +0200
     6.2 +++ b/src/CTT/ex/synth.ML	Wed Jul 05 18:27:55 2000 +0200
     6.3 @@ -6,9 +6,10 @@
     6.4  
     6.5  writeln"Synthesis examples, using a crude form of narrowing";
     6.6  
     6.7 +context Arith.thy;
     6.8  
     6.9  writeln"discovery of predecessor function";
    6.10 -goal CTT.thy 
    6.11 +Goal 
    6.12   "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
    6.13  \                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
    6.14  by (intr_tac[]);
    6.15 @@ -19,24 +20,22 @@
    6.16  result();
    6.17  
    6.18  writeln"the function fst as an element of a function type";
    6.19 -val prems = goal CTT.thy 
    6.20 -    "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
    6.21 -by (intr_tac prems);
    6.22 +Goal "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
    6.23 +by (intr_tac []);
    6.24  by eqintr_tac;
    6.25  by (resolve_tac reduction_rls 2);
    6.26  by (resolve_tac comp_rls 4);
    6.27 -by (typechk_tac prems);
    6.28 +by (typechk_tac []);
    6.29  writeln"now put in A everywhere";
    6.30 -by (REPEAT (resolve_tac prems 1));
    6.31 +by (REPEAT (assume_tac 1));
    6.32  by (fold_tac basic_defs);
    6.33  result();
    6.34  
    6.35  writeln"An interesting use of the eliminator, when";
    6.36  (*The early implementation of unification caused non-rigid path in occur check
    6.37    See following example.*)
    6.38 -goal CTT.thy 
    6.39 -    "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
    6.40 -\                 * Eq(?A, ?b(inr(i)), <succ(0), i>)";
    6.41 +Goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
    6.42 +\                  * Eq(?A, ?b(inr(i)), <succ(0), i>)";
    6.43  by (intr_tac[]);
    6.44  by eqintr_tac;
    6.45  by (resolve_tac comp_rls 1);
    6.46 @@ -47,13 +46,12 @@
    6.47   This prevents the cycle in the first unification (no longer needed).  
    6.48   Requires flex-flex to preserve the dependence.
    6.49   Simpler still: make ?A into a constant type N*N.*)
    6.50 -goal CTT.thy 
    6.51 -    "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
    6.52 -\                *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
    6.53 +Goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
    6.54 +\                 *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
    6.55  
    6.56  writeln"A tricky combination of when and split";
    6.57  (*Now handled easily, but caused great problems once*)
    6.58 -goal CTT.thy 
    6.59 +Goal 
    6.60      "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
    6.61  \                          *  Eq(?A, ?b(inr(<i,j>)), j)";
    6.62  by (intr_tac[]); 
    6.63 @@ -67,20 +65,17 @@
    6.64  uresult();
    6.65  
    6.66  (*similar but allows the type to depend on i and j*)
    6.67 -goal CTT.thy 
    6.68 -    "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
    6.69 +Goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
    6.70  \                         *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
    6.71  
    6.72  (*similar but specifying the type N simplifies the unification problems*)
    6.73 -goal CTT.thy
    6.74 -    "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
    6.75 +Goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
    6.76  \                         *   Eq(N, ?b(inr(<i,j>)), j)";
    6.77  
    6.78  
    6.79  writeln"Deriving the addition operator";
    6.80 -goal Arith.thy 
    6.81 -   "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
    6.82 -\               *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
    6.83 +Goal "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
    6.84 +\                 *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
    6.85  by (intr_tac[]);
    6.86  by eqintr_tac;
    6.87  by (resolve_tac comp_rls 1);
    6.88 @@ -89,7 +84,7 @@
    6.89  result();
    6.90  
    6.91  writeln"The addition function -- using explicit lambdas";
    6.92 -goal Arith.thy 
    6.93 +Goal
    6.94    "?c : SUM plus : ?A .  \
    6.95  \        PROD x:N. Eq(N, plus`0`x, x)  \
    6.96  \               *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
     7.1 --- a/src/CTT/ex/typechk.ML	Wed Jul 05 17:52:24 2000 +0200
     7.2 +++ b/src/CTT/ex/typechk.ML	Wed Jul 05 18:27:55 2000 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  
     7.5  writeln"Single-step proofs: verifying that a type is well-formed";
     7.6  
     7.7 -goal CTT.thy "?A type";
     7.8 +Goal "?A type";
     7.9  by (resolve_tac form_rls 1);
    7.10  result(); 
    7.11  writeln"getting a second solution";
    7.12 @@ -17,7 +17,7 @@
    7.13  by (resolve_tac form_rls 1);
    7.14  result(); 
    7.15  
    7.16 -goal CTT.thy "PROD z:?A . N + ?B(z) type";
    7.17 +Goal "PROD z:?A . N + ?B(z) type";
    7.18  by (resolve_tac form_rls 1);
    7.19  by (resolve_tac form_rls 1);
    7.20  by (resolve_tac form_rls 1);
    7.21 @@ -28,34 +28,34 @@
    7.22  
    7.23  writeln"Multi-step proofs: Type inference";
    7.24  
    7.25 -goal CTT.thy "PROD w:N. N + N type";
    7.26 +Goal "PROD w:N. N + N type";
    7.27  by form_tac;
    7.28  result(); 
    7.29  
    7.30 -goal CTT.thy "<0, succ(0)> : ?A";
    7.31 +Goal "<0, succ(0)> : ?A";
    7.32  by (intr_tac[]);
    7.33  result(); 
    7.34  
    7.35 -goal CTT.thy "PROD w:N . Eq(?A,w,w) type";
    7.36 +Goal "PROD w:N . Eq(?A,w,w) type";
    7.37  by (typechk_tac[]);
    7.38  result(); 
    7.39  
    7.40 -goal CTT.thy "PROD x:N . PROD y:N . Eq(?A,x,y) type";
    7.41 +Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
    7.42  by (typechk_tac[]);
    7.43  result(); 
    7.44  
    7.45  writeln"typechecking an application of fst";
    7.46 -goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
    7.47 +Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
    7.48  by (typechk_tac[]);
    7.49  result(); 
    7.50  
    7.51  writeln"typechecking the predecessor function";
    7.52 -goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
    7.53 +Goal "lam n. rec(n, 0, %x y. x) : ?A";
    7.54  by (typechk_tac[]);
    7.55  result(); 
    7.56  
    7.57  writeln"typechecking the addition function";
    7.58 -goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
    7.59 +Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
    7.60  by (typechk_tac[]);
    7.61  result(); 
    7.62  
    7.63 @@ -63,18 +63,18 @@
    7.64    For concreteness, every type variable left over is forced to be N*)
    7.65  val N_tac = TRYALL (rtac NF);
    7.66  
    7.67 -goal CTT.thy "lam w. <w,w> : ?A";
    7.68 +Goal "lam w. <w,w> : ?A";
    7.69  by (typechk_tac[]);
    7.70  by N_tac;
    7.71  result(); 
    7.72  
    7.73 -goal CTT.thy "lam x. lam y. x : ?A";
    7.74 +Goal "lam x. lam y. x : ?A";
    7.75  by (typechk_tac[]);
    7.76  by N_tac;
    7.77  result(); 
    7.78  
    7.79  writeln"typechecking fst (as a function object) ";
    7.80 -goal CTT.thy "lam i. split(i, %j k. j) : ?A";
    7.81 +Goal "lam i. split(i, %j k. j) : ?A";
    7.82  by (typechk_tac[]);
    7.83  by N_tac;
    7.84  result();