# HG changeset patch
# User paulson
# Date 962814475 -7200
# Node ID bd57acd44fc17c0b948f5a6b9b716718403a7f72
# Parent  0a85dbc4206ff42d89af226cc0b60cfe812f2484
more tidying.  also generalized some tactics to prove "Type A" and
"a = b : A" judgements

diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/Arith.ML
--- a/src/CTT/Arith.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/Arith.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -1,10 +1,8 @@
-(*  Title:      CTT/arith
+(*  Title:      CTT/Arith
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Theorems for arith.thy (Arithmetic operators)
-
 Proofs about elementary arithmetic: addition, multiplication, etc.
 Tests definitions and simplifier.
 *)
@@ -16,27 +14,23 @@
 
 (*typing of add: short and long versions*)
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> a #+ b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> a #+ b : N";
+by (typechk_tac []) ;
 qed "add_typing";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
+by (equal_tac []) ;
 qed "add_typingL";
 
 
 (*computation for add: 0 and successor cases*)
 
-val prems= goalw Arith.thy arith_defs 
-    "b:N ==> 0 #+ b = b : N";
-by (rew_tac prems) ;
+Goalw arith_defs "b:N ==> 0 #+ b = b : N";
+by (rew_tac []) ;
 qed "addC0";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
-by (rew_tac prems) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
+by (rew_tac []) ;
 qed "addC_succ"; 
 
 
@@ -44,26 +38,22 @@
 
 (*typing of mult: short and long versions*)
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> a #* b : N";
-by (typechk_tac([add_typing]@prems)) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> a #* b : N";
+by (typechk_tac [add_typing]) ;
 qed "mult_typing";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
-by (equal_tac (prems@[add_typingL])) ;
+Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
+by (equal_tac [add_typingL]) ;
 qed "mult_typingL";
 
 (*computation for mult: 0 and successor cases*)
 
-val prems= goalw Arith.thy arith_defs 
-    "b:N ==> 0 #* b = 0 : N";
-by (rew_tac prems) ;
+Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
+by (rew_tac []) ;
 qed "multC0";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
-by (rew_tac prems) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
+by (rew_tac []) ;
 qed "multC_succ";
 
 
@@ -71,41 +61,36 @@
 
 (*typing of difference*)
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> a - b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> a - b : N";
+by (typechk_tac []) ;
 qed "diff_typing";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
+by (equal_tac []) ;
 qed "diff_typingL";
 
 
 
 (*computation for difference: 0 and successor cases*)
 
-val prems= goalw Arith.thy arith_defs 
-    "a:N ==> a - 0 = a : N";
-by (rew_tac prems) ;
+Goalw arith_defs "a:N ==> a - 0 = a : N";
+by (rew_tac []) ;
 qed "diffC0";
 
 (*Note: rec(a, 0, %z w.z) is pred(a). *)
 
-val prems= goalw Arith.thy arith_defs 
-    "b:N ==> 0 - b = 0 : N";
+Goalw arith_defs "b:N ==> 0 - b = 0 : N";
 by (NE_tac "b" 1);
-by (hyp_rew_tac prems) ;
+by (hyp_rew_tac []) ;
 qed "diff_0_eq_0";
 
 
 (*Essential to simplify FIRST!!  (Else we get a critical pair)
   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
-by (hyp_rew_tac prems);
+Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
+by (hyp_rew_tac []);
 by (NE_tac "b" 1);
-by (hyp_rew_tac prems) ;
+by (hyp_rew_tac []) ;
 qed "diff_succ_succ";
 
 
@@ -152,23 +137,21 @@
  **********)
 
 (*Associative law for addition*)
-val prems= goal Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
+Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
 qed "add_assoc";
 
 
 (*Commutative law for addition.  Can be proved using three inductions.
   Must simplify after first induction!  Orientation of rewrites is delicate*)  
-val prems= goal Arith.thy 
-    "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
+Goal "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems);
+by (hyp_arith_rew_tac []);
 by (NE_tac "b" 2);
 by (rtac sym_elem 1);
 by (NE_tac "b" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
 qed "add_commute";
 
 
@@ -177,52 +160,48 @@
  ****************)
 
 (*Commutative law for multiplication
-val prems= goal Arith.thy 
-    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
+Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems);
+by (hyp_arith_rew_tac []);
 by (NE_tac "b" 2);
 by (rtac sym_elem 1);
 by (NE_tac "b" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
 qed "mult_commute";   NEEDS COMMUTATIVE MATCHING
 ***************)
 
 (*right annihilation in product*)
-val prems= goal Arith.thy 
-    "a:N ==> a #* 0 = 0 : N";
+Goal "a:N ==> a #* 0 = 0 : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
 qed "mult_0_right";
 
 (*right successor law for multiplication*)
-val prems= goal Arith.thy 
-    "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
+Goal "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem]));
-by (REPEAT (assume_tac 1  ORELSE resolve_tac (prems@[add_commute,mult_typingL,add_typingL]@ intrL_rls@[refl_elem])   1)) ;
+by (hyp_arith_rew_tac [add_assoc RS sym_elem]);
+by (REPEAT (assume_tac 1
+     ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@
+			 [refl_elem])   1)) ;
 qed "mult_succ_right";
 
 (*Commutative law for multiplication*)
-val prems= goal Arith.thy 
-    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
+Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ;
+by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
 qed "mult_commute";
 
 (*addition distributes over multiplication*)
-val prems= goal Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
+Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ;
+by (hyp_arith_rew_tac [add_assoc RS sym_elem]) ;
 qed "add_mult_distrib";
 
 
 (*Associative law for multiplication*)
-val prems= goal Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
+Goal "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ;
+by (hyp_arith_rew_tac [add_mult_distrib]) ;
 qed "mult_assoc";
 
 
@@ -233,10 +212,9 @@
 Difference on natural numbers, without negative numbers
   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
 
-val prems= goal Arith.thy 
-    "a:N ==> a - a = 0 : N";
+Goal "a:N ==> a - a = 0 : N";
 by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
 qed "diff_self_eq_0";
 
 
@@ -246,9 +224,7 @@
 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   An example of induction over a quantified formula (a product).
   Uses rewriting with a quantified, implicative inductive hypothesis.*)
-val prems =
-goal Arith.thy 
-    "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
+Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
 by (NE_tac "b" 1);
 (*strip one "universal quantifier" but not the "implication"*)
 by (resolve_tac intr_rls 3);  
@@ -258,11 +234,11 @@
 (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
 by (rtac replace_type 5);
 by (rtac replace_type 4);
-by (arith_rew_tac prems); 
+by (arith_rew_tac []); 
 (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   Both follow by rewriting, (2) using quantified induction hyp*)
 by (intr_tac[]);  (*strips remaining PRODs*)
-by (hyp_arith_rew_tac (prems@[add_0_right]));  
+by (hyp_arith_rew_tac [add_0_right]);  
 by (assume_tac 1);
 qed "add_diff_inverse_lemma";
 
@@ -271,11 +247,10 @@
   Using ProdE does not work -- for ?B(?a) is ambiguous.
   Instead, add_diff_inverse_lemma states the desired induction scheme;
     the use of RS below instantiates Vars in ProdE automatically. *)
-val prems =
-goal Arith.thy "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
+Goal "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
 by (rtac EqE 1);
 by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
-by (REPEAT (resolve_tac (prems@[EqI]) 1));
+by (REPEAT (ares_tac [EqI] 1));
 qed "add_diff_inverse";
 
 
@@ -285,63 +260,55 @@
 
 (*typing of absolute difference: short and long versions*)
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a:N;  b:N |] ==> a |-| b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N;  b:N |] ==> a |-| b : N";
+by (typechk_tac []) ;
 qed "absdiff_typing";
 
-val prems= goalw Arith.thy arith_defs 
-    "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
+by (equal_tac []) ;
 qed "absdiff_typingL";
 
-Goalw [absdiff_def]  
-    "a:N ==> a |-| a = 0 : N";
-by (arith_rew_tac (prems@[diff_self_eq_0])) ;
+Goalw [absdiff_def] "a:N ==> a |-| a = 0 : N";
+by (arith_rew_tac [diff_self_eq_0]) ;
 qed "absdiff_self_eq_0";
 
-Goalw [absdiff_def]  
-    "a:N ==> 0 |-| a = a : N";
+Goalw [absdiff_def] "a:N ==> 0 |-| a = a : N";
 by (hyp_arith_rew_tac []);
 qed "absdiffC0";
 
 
-Goalw [absdiff_def]  
-    "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
+Goalw [absdiff_def] "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
 by (hyp_arith_rew_tac []) ;
 qed "absdiff_succ_succ";
 
 (*Note how easy using commutative laws can be?  ...not always... *)
-val prems = goalw Arith.thy [absdiff_def]
-    "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
+Goalw [absdiff_def] "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
 by (rtac add_commute 1);
-by (typechk_tac ([diff_typing]@prems));
+by (typechk_tac [diff_typing]);
 qed "absdiff_commute";
 
 (*If a+b=0 then a=0.   Surprisingly tedious*)
-val prems =
-goal Arith.thy "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
+Goal "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
 by (NE_tac "a" 1);
 by (rtac replace_type 3);
-by (arith_rew_tac prems);
+by (arith_rew_tac []);
 by (intr_tac[]);  (*strips remaining PRODs*)
 by (resolve_tac [ zero_ne_succ RS FE ] 2);
 by (etac (EqE RS sym_elem) 3);
-by (typechk_tac ([add_typing] @prems));
+by (typechk_tac [add_typing]);
 qed "add_eq0_lemma";
 
 (*Version of above with the premise  a+b=0.
   Again, resolution instantiates variables in ProdE *)
-val prems =
-goal Arith.thy "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
+Goal "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
 by (rtac EqE 1);
 by (resolve_tac [add_eq0_lemma RS ProdE] 1);
 by (rtac EqI 3);
-by (ALLGOALS (resolve_tac prems));
+by (typechk_tac []) ;
 qed "add_eq0";
 
 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-val prems = goalw Arith.thy [absdiff_def]
+Goalw [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[]);
@@ -349,20 +316,19 @@
 by (rtac add_eq0 2);
 by (rtac add_eq0 1);
 by (resolve_tac [add_commute RS trans_elem] 6);
-by (typechk_tac (diff_typing::prems));
+by (typechk_tac [diff_typing]);
 qed "absdiff_eq0_lem";
 
 (*if  a |-| b = 0  then  a = b  
   proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
-val prems =
-goal Arith.thy "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
+Goal "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
 by (rtac EqE 1);
 by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
-by (TRYALL (resolve_tac prems));
+by (TRYALL assume_tac);
 by eqintr_tac;
 by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
 by (rtac EqE 3  THEN  assume_tac 3);
-by (hyp_arith_rew_tac (prems@[add_0_right]));
+by (hyp_arith_rew_tac [add_0_right]);
 qed "absdiff_eq0";
 
 (***********************
@@ -371,40 +337,35 @@
 
 (*typing of remainder: short and long versions*)
 
-Goalw [mod_def]  
-    "[| a:N;  b:N |] ==> a mod b : N";
-by (typechk_tac (absdiff_typing::prems)) ;
+Goalw [mod_def] "[| a:N;  b:N |] ==> a mod b : N";
+by (typechk_tac [absdiff_typing]) ;
 qed "mod_typing";
  
-Goalw [mod_def]  
-    "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
+Goalw [mod_def] "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
 by (equal_tac [absdiff_typingL]) ;
-by (ALLGOALS assume_tac);
 qed "mod_typingL";
  
 
 (*computation for  mod : 0 and successor cases*)
 
 Goalw [mod_def]   "b:N ==> 0 mod b = 0 : N";
-by (rew_tac(absdiff_typing::prems)) ;
+by (rew_tac [absdiff_typing]) ;
 qed "modC0";
 
 Goalw [mod_def]   
 "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
-by (rew_tac(absdiff_typing::prems)) ;
+by (rew_tac [absdiff_typing]) ;
 qed "modC_succ";
 
 
 (*typing of quotient: short and long versions*)
 
 Goalw [div_def]   "[| a:N;  b:N |] ==> a div b : N";
-by (typechk_tac ([absdiff_typing,mod_typing]@prems)) ;
+by (typechk_tac [absdiff_typing,mod_typing]) ;
 qed "div_typing";
 
-Goalw [div_def]  
-   "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
+Goalw [div_def] "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
 by (equal_tac [absdiff_typingL, mod_typingL]);
-by (ALLGOALS assume_tac);
 qed "div_typingL";
 
 val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
@@ -413,54 +374,51 @@
 (*computation for quotient: 0 and successor cases*)
 
 Goalw [div_def]   "b:N ==> 0 div b = 0 : N";
-by (rew_tac([mod_typing, absdiff_typing] @ prems)) ;
+by (rew_tac [mod_typing, absdiff_typing]) ;
 qed "divC0";
 
 Goalw [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";
-by (rew_tac([mod_typing]@prems)) ;
+by (rew_tac [mod_typing]) ;
 qed "divC_succ";
 
 
 (*Version of above with same condition as the  mod  one*)
-val prems= goal Arith.thy
-    "[| a:N;  b:N |] ==> \
+Goal "[| a:N;  b:N |] ==> \
 \    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N";
 by (resolve_tac [ divC_succ RS trans_elem ] 1);
-by (rew_tac(div_typing_rls @ prems @ [modC_succ]));
+by (rew_tac(div_typing_rls @ [modC_succ]));
 by (NE_tac "succ(a mod b)|-|b" 1);
-by (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ;
+by (rew_tac [mod_typing, div_typing, absdiff_typing]);
 qed "divC_succ2";
 
 (*for case analysis on whether a number is 0 or a successor*)
-val prems= goal Arith.thy
-    "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
+Goal "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
 \                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))";
 by (NE_tac "a" 1);
 by (rtac PlusI_inr 3);
 by (rtac PlusI_inl 2);
 by eqintr_tac;
-by (equal_tac prems) ;
+by (equal_tac []) ;
 qed "iszero_decidable";
 
 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
-val prems =
-goal Arith.thy "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
+Goal "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
 by (NE_tac "a" 1);
-by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); 
+by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); 
 by (rtac EqE 1);
 (*case analysis on   succ(u mod b)|-|b  *)
 by (res_inst_tac [("a1", "succ(u mod b) |-| b")] 
                  (iszero_decidable RS PlusE) 1);
 by (etac SumE 3);
-by (hyp_arith_rew_tac (prems @ div_typing_rls @
+by (hyp_arith_rew_tac (div_typing_rls @
         [modC0,modC_succ, divC0, divC_succ2])); 
 (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
 by (resolve_tac [ add_typingL RS trans_elem ] 1);
 by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
 by (rtac refl_elem 3);
-by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
+by (hyp_arith_rew_tac (div_typing_rls)); 
 qed "mod_div_equality";
 
 writeln"Reached end of file.";
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/Bool.ML
--- a/src/CTT/Bool.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/Bool.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title:      CTT/bool
+(*  Title:      CTT/Bool
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Theorems for bool.thy (booleans and conditionals)
+The two-element type (booleans and conditionals)
 *)
 
 val bool_defs = [Bool_def,true_def,false_def,cond_def];
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/CTT.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title:      CTT/ctt.ML
+(*  Title:      CTT/CTT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Tactics and lemmas for ctt.thy (Constructive Type Theory)
+Tactics and derived rules for Constructive Type Theory
 *)
 
 (*Formation rules*)
@@ -33,30 +33,30 @@
 val basic_defs = [fst_def,snd_def];
 
 (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-val prems= goal CTT.thy
-    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
+Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
 by (rtac sym_elem 1);
 by (rtac SumIL 1);
 by (ALLGOALS (rtac sym_elem ));
-by (ALLGOALS (resolve_tac prems)) ;
+by (ALLGOALS assume_tac) ;
 qed "SumIL2";
 
 val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
 
 (*Exploit p:Prod(A,B) to create the assumption z:B(a).  
   A more natural form of product elimination. *)
-val prems= goal CTT.thy
-    "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
+val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
 \    |] ==> c(p`a): C(p`a)";
-by (REPEAT (resolve_tac (prems@[ProdE]) 1)) ;
+by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
 qed "subst_prodE";
 
 (** Tactics for type checking **)
 
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))
+fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
+  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
+  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
   | is_rigid_elem _ = false;
 
-(*Try solving a:A by assumption provided a is rigid!*) 
+(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
 val test_assume_tac = SUBGOAL(fn (prem,i) =>
     if is_rigid_elem (Logic.strip_assums_concl prem)
     then  assume_tac i  else  no_tac);
@@ -72,7 +72,7 @@
 
 
 (*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
+val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
 
 
 (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
@@ -98,16 +98,15 @@
 (*** Simplification ***)
 
 (*To simplify the type in a goal*)
-val prems= goal CTT.thy
-    "[| B = A;  a : A |] ==> a : B";
+Goal "[| B = A;  a : A |] ==> a : B";
 by (rtac equal_types 1);
 by (rtac sym_type 2);
-by (ALLGOALS (resolve_tac prems)) ;
+by (ALLGOALS assume_tac) ;
 qed "replace_type";
 
 (*Simplify the parameter of a unary type operator.*)
-val prems= goal CTT.thy
-    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)";
+val prems = Goal
+     "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
 by (rtac subst_typeL 1);
 by (rtac refl_type 2);
 by (ALLGOALS (resolve_tac prems));
@@ -175,14 +174,13 @@
 
 (** The elimination rules for fst/snd **)
 
-val [major] = goalw CTT.thy basic_defs
-    "p : Sum(A,B) ==> fst(p) : A";
-by (rtac (major RS SumE) 1);
-by (assume_tac 1) ;
+Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
+by (etac SumE 1);
+by (assume_tac 1);
 qed "SumE_fst";
 
 (*The first premise must be p:Sum(A,B) !!*)
-val major::prems= goalw CTT.thy basic_defs
+val major::prems= Goalw basic_defs
     "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
 \    |] ==> snd(p) : B(fst(p))";
 by (rtac (major RS SumE) 1);
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/elim.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -15,8 +15,8 @@
 
 
 writeln"This finds the functions fst and snd!"; 
-val prems = goal CTT.thy "A type ==> ?a : (A*A) --> A";
-by (pc_tac prems 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
+Goal "A type ==> ?a : (A*A) --> A";
+by (pc_tac [] 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
 result();
 writeln"first solution is fst;  backtracking gives snd";
 back(); 
@@ -24,47 +24,43 @@
 
 
 writeln"Double negation of the Excluded Middle";
-val prems = goal CTT.thy "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
-by (intr_tac prems);
+Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
+by (intr_tac []);
 by (rtac ProdE 1);
 by (assume_tac 1);
-by (pc_tac prems 1);
+by (pc_tac [] 1);
 result();
 
-val prems = goal CTT.thy 
-    "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
-by (pc_tac prems 1);
+Goal "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
+by (pc_tac [] 1);
 result();
 (*The sequent version (ITT) could produce an interesting alternative
   by backtracking.  No longer.*)
 
 writeln"Binary sums and products";
-val prems = goal CTT.thy
-   "[| A type;  B type;  C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
+by (pc_tac [] 1);
 result();
 
 (*A distributive law*)
-val prems = goal CTT.thy 
-    "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
-by (pc_tac prems 1);
+Goal "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
+by (pc_tac [] 1);
 result();
 
 (*more general version, same proof*)
-val prems = goal CTT.thy 
-    "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
-\    ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
+val prems = Goal
+   "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
+\      ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
 by (pc_tac prems 1);
 result();
 
 writeln"Construction of the currying functional";
-val prems = goal CTT.thy 
-    "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
-by (pc_tac prems 1);
+Goal "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
+by (pc_tac [] 1);
 result();
 
 (*more general goal with same proof*)
-val prems = goal CTT.thy
+val prems = Goal
     "[| A type; !!x. x:A ==> B(x) type;                         \
 \               !!z. z: (SUM x:A. B(x)) ==> C(z) type           \
 \    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).    \
@@ -73,27 +69,25 @@
 result();
 
 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
-val prems = goal CTT.thy 
-    "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
-by (pc_tac prems 1);
+Goal "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
+by (pc_tac [] 1);
 result();
 
 (*more general goal with same proof*)
-val prems = goal CTT.thy 
-  "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \
+val prems = Goal 
+ "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \
 \  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
 \       --> (PROD z : (SUM x:A . B(x)) . C(z))";
 by (pc_tac prems 1);
 result();
 
 writeln"Function application";
-val prems = goal CTT.thy  
-    "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
-by (pc_tac prems 1);
+Goal "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
+by (pc_tac [] 1);
 result();
 
 writeln"Basic test of quantifier reasoning";
-val prems = goal CTT.thy  
+val prems = Goal  
     "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
 \    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
 \         --> (PROD x:A . SUM y:B . C(x,y))";
@@ -105,7 +99,7 @@
 by (pc_tac prems 1);        ...fails!!  *)
 
 writeln"Martin-Lof (1984) pages 36-7: the combinator S";
-val prems = goal CTT.thy  
+val prems = Goal  
     "[| A type;  !!x. x:A ==> B(x) type;  \
 \       !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
 \    ==> ?a :    (PROD x:A. PROD y:B(x). C(x,y)) \
@@ -114,7 +108,7 @@
 result();
 
 writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
-val prems = goal CTT.thy
+val prems = Goal
     "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
 \    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
 \         --> (PROD z: A+B. C(z))";
@@ -122,15 +116,14 @@
 result();
 
 (*towards AXIOM OF CHOICE*)
-val prems = goal CTT.thy  
-  "[| A type;  B type;  C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
+by (pc_tac [] 1);
 by (fold_tac basic_defs);   (*puts in fst and snd*)
 result();
 
 (*Martin-Lof (1984) page 50*)
-writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
-val prems = goal CTT.thy   
+writeln"AXIOM OF CHOICE!  Delicate use of elimination rules";
+val prems = Goal   
     "[| A type;  !!x. x:A ==> B(x) type;                        \
 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
@@ -147,7 +140,7 @@
 result();
 
 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
-val prems = goal CTT.thy   
+val prems = Goal   
     "[| A type;  !!x. x:A ==> B(x) type;                         \
 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
@@ -172,7 +165,7 @@
 writeln"Example of sequent_style deduction"; 
 (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
     lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
-val prems = goal CTT.thy   
+val prems = Goal   
     "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
 \    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
 by (resolve_tac intr_rls 1);
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/ex/equal.ML
--- a/src/CTT/ex/equal.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/equal.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -6,78 +6,68 @@
 Equality reasoning by rewriting.
 *)
 
-val prems =
-goal CTT.thy "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
+Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
 by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1  THEN  assume_tac 1);
+by (rew_tac []);
 qed "split_eq";
 
-val prems =
-goal CTT.thy
-    "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
+Goal "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
 by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1  THEN  assume_tac 1);
+by (rew_tac []);
+by (ALLGOALS assume_tac);
 qed "when_eq";
 
 
 (*in the "rec" formulation of addition, 0+n=n *)
-val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
+Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
 by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1  THEN  assume_tac 1);
+by (rew_tac []);
 result();
 
 
 (*the harder version, n+0=n: recursive, uses induction hypothesis*)
-val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
+Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
 by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
-by (hyp_rew_tac prems);
+by (resolve_tac elim_rls 1  THEN  assume_tac 1);
+by (hyp_rew_tac []);
 result();
 
 
 (*Associativity of addition*)
-val prems =
-goal CTT.thy
-   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
-\                   rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
+Goal "[| a:N;  b:N;  c:N |] \
+\     ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
+\         rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
 by (NE_tac "a" 1);
-by (hyp_rew_tac prems);
+by (hyp_rew_tac []);
 result();
 
 
 (*Martin-Lof (1984) page 62: pairing is surjective*)
-val prems =
-goal CTT.thy
-    "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
+Goal "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
 by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
-by (DEPTH_SOLVE_1 (rew_tac prems));   (*!!!!!!!*)
+by (resolve_tac elim_rls 1  THEN  assume_tac 1);
+by (DEPTH_SOLVE_1 (rew_tac []));   (*!!!!!!!*)
 result();
 
 
-val prems =
-goal CTT.thy "[| a : A;  b : B |] ==> \
+Goal "[| a : A;  b : B |] ==> \
 \    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
-by (rew_tac prems);
+by (rew_tac []);
 result();
 
 
 (*a contrived, complicated simplication, requires sum-elimination also*)
-val prems =
-goal CTT.thy
-   "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
+Goal "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
 \     lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)";
 by (resolve_tac reduction_rls 1);
 by (resolve_tac intrL_rls 3);
 by (rtac EqE 4);
 by (rtac SumE 4  THEN  assume_tac 4);
 (*order of unifiers is essential here*)
-by (rew_tac prems);
+by (rew_tac []);
 result();
 
 writeln"Reached end of file.";
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/ex/synth.ML
--- a/src/CTT/ex/synth.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/synth.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -6,9 +6,10 @@
 
 writeln"Synthesis examples, using a crude form of narrowing";
 
+context Arith.thy;
 
 writeln"discovery of predecessor function";
-goal CTT.thy 
+Goal 
  "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
 \                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
 by (intr_tac[]);
@@ -19,24 +20,22 @@
 result();
 
 writeln"the function fst as an element of a function type";
-val prems = goal CTT.thy 
-    "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
-by (intr_tac prems);
+Goal "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
+by (intr_tac []);
 by eqintr_tac;
 by (resolve_tac reduction_rls 2);
 by (resolve_tac comp_rls 4);
-by (typechk_tac prems);
+by (typechk_tac []);
 writeln"now put in A everywhere";
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
 by (fold_tac basic_defs);
 result();
 
 writeln"An interesting use of the eliminator, when";
 (*The early implementation of unification caused non-rigid path in occur check
   See following example.*)
-goal CTT.thy 
-    "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
-\                 * Eq(?A, ?b(inr(i)), <succ(0), i>)";
+Goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
+\                  * Eq(?A, ?b(inr(i)), <succ(0), i>)";
 by (intr_tac[]);
 by eqintr_tac;
 by (resolve_tac comp_rls 1);
@@ -47,13 +46,12 @@
  This prevents the cycle in the first unification (no longer needed).  
  Requires flex-flex to preserve the dependence.
  Simpler still: make ?A into a constant type N*N.*)
-goal CTT.thy 
-    "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
-\                *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
+Goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
+\                 *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
 
 writeln"A tricky combination of when and split";
 (*Now handled easily, but caused great problems once*)
-goal CTT.thy 
+Goal 
     "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
 \                          *  Eq(?A, ?b(inr(<i,j>)), j)";
 by (intr_tac[]); 
@@ -67,20 +65,17 @@
 uresult();
 
 (*similar but allows the type to depend on i and j*)
-goal CTT.thy 
-    "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
+Goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
 \                         *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
 
 (*similar but specifying the type N simplifies the unification problems*)
-goal CTT.thy
-    "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
+Goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
 \                         *   Eq(N, ?b(inr(<i,j>)), j)";
 
 
 writeln"Deriving the addition operator";
-goal Arith.thy 
-   "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
-\               *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
+Goal "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
+\                 *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
 by (intr_tac[]);
 by eqintr_tac;
 by (resolve_tac comp_rls 1);
@@ -89,7 +84,7 @@
 result();
 
 writeln"The addition function -- using explicit lambdas";
-goal Arith.thy 
+Goal
   "?c : SUM plus : ?A .  \
 \        PROD x:N. Eq(N, plus`0`x, x)  \
 \               *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
diff -r 0a85dbc4206f -r bd57acd44fc1 src/CTT/ex/typechk.ML
--- a/src/CTT/ex/typechk.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/typechk.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -8,7 +8,7 @@
 
 writeln"Single-step proofs: verifying that a type is well-formed";
 
-goal CTT.thy "?A type";
+Goal "?A type";
 by (resolve_tac form_rls 1);
 result(); 
 writeln"getting a second solution";
@@ -17,7 +17,7 @@
 by (resolve_tac form_rls 1);
 result(); 
 
-goal CTT.thy "PROD z:?A . N + ?B(z) type";
+Goal "PROD z:?A . N + ?B(z) type";
 by (resolve_tac form_rls 1);
 by (resolve_tac form_rls 1);
 by (resolve_tac form_rls 1);
@@ -28,34 +28,34 @@
 
 writeln"Multi-step proofs: Type inference";
 
-goal CTT.thy "PROD w:N. N + N type";
+Goal "PROD w:N. N + N type";
 by form_tac;
 result(); 
 
-goal CTT.thy "<0, succ(0)> : ?A";
+Goal "<0, succ(0)> : ?A";
 by (intr_tac[]);
 result(); 
 
-goal CTT.thy "PROD w:N . Eq(?A,w,w) type";
+Goal "PROD w:N . Eq(?A,w,w) type";
 by (typechk_tac[]);
 result(); 
 
-goal CTT.thy "PROD x:N . PROD y:N . Eq(?A,x,y) type";
+Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking an application of fst";
-goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
+Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the predecessor function";
-goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
+Goal "lam n. rec(n, 0, %x y. x) : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the addition function";
-goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
+Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
 by (typechk_tac[]);
 result(); 
 
@@ -63,18 +63,18 @@
   For concreteness, every type variable left over is forced to be N*)
 val N_tac = TRYALL (rtac NF);
 
-goal CTT.thy "lam w. <w,w> : ?A";
+Goal "lam w. <w,w> : ?A";
 by (typechk_tac[]);
 by N_tac;
 result(); 
 
-goal CTT.thy "lam x. lam y. x : ?A";
+Goal "lam x. lam y. x : ?A";
 by (typechk_tac[]);
 by N_tac;
 result(); 
 
 writeln"typechecking fst (as a function object) ";
-goal CTT.thy "lam i. split(i, %j k. j) : ?A";
+Goal "lam i. split(i, %j k. j) : ?A";
 by (typechk_tac[]);
 by N_tac;
 result();