author paulson Wed Jul 05 18:27:55 2000 +0200 (2000-07-05) changeset 9251 bd57acd44fc1 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 file | annotate | diff | revisions src/CTT/Bool.ML file | annotate | diff | revisions src/CTT/CTT.ML file | annotate | diff | revisions src/CTT/ex/elim.ML file | annotate | diff | revisions src/CTT/ex/equal.ML file | annotate | diff | revisions src/CTT/ex/synth.ML file | annotate | diff | revisions src/CTT/ex/typechk.ML file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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.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.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.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.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();
```