# HG changeset patch
# User wenzelm
# Date 1149264938 -7200
# Node ID 5cd82054c2c696037a40c95dcd27983c97543610
# Parent  c7e9cc10acc852484a472ad1609593e29e6595a1
removed obsolete ML files;

diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/Arith.ML
--- a/src/CTT/Arith.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(*  Title:      CTT/Arith.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
-Tests definitions and simplifier.
-*)
-
-val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
-
-
-(** Addition *)
-
-(*typing of add: short and long versions*)
-
-Goalw arith_defs "[| a:N;  b:N |] ==> a #+ b : N";
-by (typechk_tac []) ;
-qed "add_typing";
-
-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*)
-
-Goalw arith_defs "b:N ==> 0 #+ b = b : N";
-by (rew_tac []) ;
-qed "addC0";
-
-Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
-by (rew_tac []) ;
-qed "addC_succ";
-
-
-(** Multiplication *)
-
-(*typing of mult: short and long versions*)
-
-Goalw arith_defs "[| a:N;  b:N |] ==> a #* b : N";
-by (typechk_tac [add_typing]) ;
-qed "mult_typing";
-
-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*)
-
-Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
-by (rew_tac []) ;
-qed "multC0";
-
-Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
-by (rew_tac []) ;
-qed "multC_succ";
-
-
-(** Difference *)
-
-(*typing of difference*)
-
-Goalw arith_defs "[| a:N;  b:N |] ==> a - b : N";
-by (typechk_tac []) ;
-qed "diff_typing";
-
-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*)
-
-Goalw arith_defs "a:N ==> a - 0 = a : N";
-by (rew_tac []) ;
-qed "diffC0";
-
-(*Note: rec(a, 0, %z w.z) is pred(a). *)
-
-Goalw arith_defs "b:N ==> 0 - b = 0 : N";
-by (NE_tac "b" 1);
-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)  *)
-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 []) ;
-qed "diff_succ_succ";
-
-
-
-(*** Simplification *)
-
-val arith_typing_rls =
-  [add_typing, mult_typing, diff_typing];
-
-val arith_congr_rls =
-  [add_typingL, mult_typingL, diff_typingL];
-
-val congr_rls = arith_congr_rls@standard_congr_rls;
-
-val arithC_rls =
-  [addC0, addC_succ,
-   multC0, multC_succ,
-   diffC0, diff_0_eq_0, diff_succ_succ];
-
-
-structure Arith_simp_data: TSIMP_DATA =
-  struct
-  val refl              = refl_elem
-  val sym               = sym_elem
-  val trans             = trans_elem
-  val refl_red          = refl_red
-  val trans_red         = trans_red
-  val red_if_equal      = red_if_equal
-  val default_rls       = arithC_rls @ comp_rls
-  val routine_tac       = routine_tac (arith_typing_rls @ routine_rls)
-  end;
-
-structure Arith_simp = TSimpFun (Arith_simp_data);
-
-fun arith_rew_tac prems = make_rew_tac
-    (Arith_simp.norm_tac(congr_rls, prems));
-
-fun hyp_arith_rew_tac prems = make_rew_tac
-    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));
-
-
-(**********
-  Addition
- **********)
-
-(*Associative law for addition*)
-Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
-by (NE_tac "a" 1);
-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*)
-Goal "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
-by (NE_tac "a" 1);
-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 []) ;
-qed "add_commute";
-
-
-(****************
-  Multiplication
- ****************)
-
-(*Commutative law for multiplication
-Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
-by (NE_tac "a" 1);
-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 []) ;
-qed "mult_commute";   NEEDS COMMUTATIVE MATCHING
-***************)
-
-(*right annihilation in product*)
-Goal "a:N ==> a #* 0 = 0 : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac []) ;
-qed "mult_0_right";
-
-(*right successor law for multiplication*)
-Goal "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
-by (NE_tac "a" 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*)
-Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
-qed "mult_commute";
-
-(*addition distributes over multiplication*)
-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 [add_assoc RS sym_elem]) ;
-qed "add_mult_distrib";
-
-
-(*Associative law for multiplication*)
-Goal "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac [add_mult_distrib]) ;
-qed "mult_assoc";
-
-
-(************
-  Difference
- ************
-
-Difference on natural numbers, without negative numbers
-  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
-
-Goal "a:N ==> a - a = 0 : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac []) ;
-qed "diff_self_eq_0";
-
-
-(*  [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N  *)
-val add_0_right = addC0 RSN (3, add_commute RS trans_elem);
-
-(*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.*)
-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);
-(*case analysis on x in
-    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-by (NE_tac "x" 4 THEN assume_tac 4);
-(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
-by (rtac replace_type 5);
-by (rtac replace_type 4);
-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 [add_0_right]);
-by (assume_tac 1);
-qed "add_diff_inverse_lemma";
-
-
-(*Version of above with premise   b-a=0   i.e.    a >= b.
-  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. *)
-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 (ares_tac [EqI] 1));
-qed "add_diff_inverse";
-
-
-(********************
-  Absolute difference
- ********************)
-
-(*typing of absolute difference: short and long versions*)
-
-Goalw arith_defs "[| a:N;  b:N |] ==> a |-| b : N";
-by (typechk_tac []) ;
-qed "absdiff_typing";
-
-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 [diff_self_eq_0]) ;
-qed "absdiff_self_eq_0";
-
-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";
-by (hyp_arith_rew_tac []) ;
-qed "absdiff_succ_succ";
-
-(*Note how easy using commutative laws can be?  ...not always... *)
-Goalw [absdiff_def] "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
-by (rtac add_commute 1);
-by (typechk_tac [diff_typing]);
-qed "absdiff_commute";
-
-(*If a+b=0 then a=0.   Surprisingly tedious*)
-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 []);
-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]);
-qed "add_eq0_lemma";
-
-(*Version of above with the premise  a+b=0.
-  Again, resolution instantiates variables in ProdE *)
-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 (typechk_tac []) ;
-qed "add_eq0";
-
-(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-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[]);
-by eqintr_tac;
-by (rtac add_eq0 2);
-by (rtac add_eq0 1);
-by (resolve_tac [add_commute RS trans_elem] 6);
-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*)
-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 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 [add_0_right]);
-qed "absdiff_eq0";
-
-(***********************
-  Remainder and Quotient
- ***********************)
-
-(*typing of remainder: short and long versions*)
-
-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";
-by (equal_tac [absdiff_typingL]) ;
-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]) ;
-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]) ;
-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]) ;
-qed "div_typing";
-
-Goalw [div_def] "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
-by (equal_tac [absdiff_typingL, mod_typingL]);
-qed "div_typingL";
-
-val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
-
-
-(*computation for quotient: 0 and successor cases*)
-
-Goalw [div_def]   "b:N ==> 0 div b = 0 : N";
-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]) ;
-qed "divC_succ";
-
-
-(*Version of above with same condition as the  mod  one*)
-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 @ [modC_succ]));
-by (NE_tac "succ(a mod b)|-|b" 1);
-by (rew_tac [mod_typing, div_typing, absdiff_typing]);
-qed "divC_succ2";
-
-(*for case analysis on whether a number is 0 or a successor*)
-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 []) ;
-qed "iszero_decidable";
-
-(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
-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@[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 (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 (div_typing_rls));
-qed "mod_div_equality";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -4,16 +4,13 @@
     Copyright   1991  University of Cambridge
 *)
 
-header {* Arithmetic operators and their definitions *}
+header {* Elementary arithmetic *}
 
 theory Arith
 imports Bool
 begin
 
-text {*
-  Proves about elementary arithmetic: addition, multiplication, etc.
-  Tests definitions and simplifier.
-*}
+subsection {* Arithmetic operators and their definitions *}
 
 consts
   "#+"  :: "[i,i]=>i"   (infixr 65)
@@ -37,6 +34,426 @@
   mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
   div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
+
+
+subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *}
+
+(** Addition *)
+
+(*typing of add: short and long versions*)
+
+lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+
+(*computation for add: 0 and successor cases*)
+
+lemma addC0: "b:N ==> 0 #+ b = b : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+
+(** Multiplication *)
+
+(*typing of mult: short and long versions*)
+
+lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
+apply (unfold arith_defs)
+apply (tactic {* typechk_tac [thm "add_typing"] *})
+done
+
+lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
+apply (unfold arith_defs)
+apply (tactic {* equal_tac [thm "add_typingL"] *})
+done
+
+(*computation for mult: 0 and successor cases*)
+
+lemma multC0: "b:N ==> 0 #* b = 0 : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+
+(** Difference *)
+
+(*typing of difference*)
+
+lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+
+(*computation for difference: 0 and successor cases*)
+
+lemma diffC0: "a:N ==> a - 0 = a : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+(*Note: rec(a, 0, %z w.z) is pred(a). *)
+
+lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
+apply (unfold arith_defs)
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+
+(*Essential to simplify FIRST!!  (Else we get a critical pair)
+  succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
+lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
+apply (unfold arith_defs)
+apply (tactic "hyp_rew_tac []")
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+
+subsection {* Simplification *}
+
+lemmas arith_typing_rls = add_typing mult_typing diff_typing
+  and arith_congr_rls = add_typingL mult_typingL diff_typingL
+lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
+
+lemmas arithC_rls =
+  addC0 addC_succ
+  multC0 multC_succ
+  diffC0 diff_0_eq_0 diff_succ_succ
+
+ML {*
+
+structure Arith_simp_data: TSIMP_DATA =
+  struct
+  val refl              = thm "refl_elem"
+  val sym               = thm "sym_elem"
+  val trans             = thm "trans_elem"
+  val refl_red          = thm "refl_red"
+  val trans_red         = thm "trans_red"
+  val red_if_equal      = thm "red_if_equal"
+  val default_rls       = thms "arithC_rls" @ thms "comp_rls"
+  val routine_tac       = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
+  end
+
+structure Arith_simp = TSimpFun (Arith_simp_data)
+
+local val congr_rls = thms "congr_rls" in
+
+fun arith_rew_tac prems = make_rew_tac
+    (Arith_simp.norm_tac(congr_rls, prems))
+
+fun hyp_arith_rew_tac prems = make_rew_tac
+    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
 
 end
+*}
+
+
+subsection {* Addition *}
+
+(*Associative law for addition*)
+lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+(*Commutative law for addition.  Can be proved using three inductions.
+  Must simplify after first induction!  Orientation of rewrites is delicate*)
+lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+apply (tactic {* NE_tac "b" 2 *})
+apply (rule sym_elem)
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+subsection {* Multiplication *}
+
+(*right annihilation in product*)
+lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+(*right successor law for multiplication*)
+lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
+done
+
+(*Commutative law for multiplication*)
+lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
+done
+
+(*addition distributes over multiplication*)
+lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+done
+
+(*Associative law for multiplication*)
+lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
+done
+
+
+subsection {* Difference *}
+
+text {*
+Difference on natural numbers, without negative numbers
+  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
+
+lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N"
+  by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
+
+(*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.*)
+lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+apply (tactic {* NE_tac "b" 1 *})
+(*strip one "universal quantifier" but not the "implication"*)
+apply (rule_tac [3] intr_rls)
+(*case analysis on x in
+    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
+apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
+(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
+apply (rule_tac [5] replace_type)
+apply (rule_tac [4] replace_type)
+apply (tactic "arith_rew_tac []")
+(*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
+  Both follow by rewriting, (2) using quantified induction hyp*)
+apply (tactic "intr_tac []") (*strips remaining PRODs*)
+apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+apply assumption
+done
+
+
+(*Version of above with premise   b-a=0   i.e.    a >= b.
+  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. *)
+lemma add_diff_inverse: "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N"
+apply (rule EqE)
+apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
+apply (assumption | rule EqI)+
+done
+
+
+subsection {* Absolute difference *}
+
+(*typing of absolute difference: short and long versions*)
+
+lemma absdiff_typing: "[| a:N;  b:N |] ==> a |-| b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma absdiff_typingL: "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
+apply (unfold absdiff_def)
+apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
+done
+
+lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
+apply (unfold absdiff_def)
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+lemma absdiff_succ_succ: "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
+apply (unfold absdiff_def)
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+(*Note how easy using commutative laws can be?  ...not always... *)
+lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
+apply (unfold absdiff_def)
+apply (rule add_commute)
+apply (tactic {* typechk_tac [thm "diff_typing"] *})
+done
+
+(*If a+b=0 then a=0.   Surprisingly tedious*)
+lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
+apply (tactic {* NE_tac "a" 1 *})
+apply (rule_tac [3] replace_type)
+apply (tactic "arith_rew_tac []")
+apply (tactic "intr_tac []") (*strips remaining PRODs*)
+apply (rule_tac [2] zero_ne_succ [THEN FE])
+apply (erule_tac [3] EqE [THEN sym_elem])
+apply (tactic {* typechk_tac [thm "add_typing"] *})
+done
+
+(*Version of above with the premise  a+b=0.
+  Again, resolution instantiates variables in ProdE *)
+lemma add_eq0: "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N"
+apply (rule EqE)
+apply (rule add_eq0_lemma [THEN ProdE])
+apply (rule_tac [3] EqI)
+apply (tactic "typechk_tac []")
+done
+
+(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
+lemma absdiff_eq0_lem:
+    "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
+     ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
+apply (unfold absdiff_def)
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [2] add_eq0)
+apply (rule add_eq0)
+apply (rule_tac [6] add_commute [THEN trans_elem])
+apply (tactic {* typechk_tac [thm "diff_typing"] *})
+done
+
+(*if  a |-| b = 0  then  a = b
+  proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
+lemma absdiff_eq0: "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N"
+apply (rule EqE)
+apply (rule absdiff_eq0_lem [THEN SumE])
+apply (tactic "TRYALL assume_tac")
+apply (tactic eqintr_tac)
+apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
+apply (rule_tac [3] EqE, tactic "assume_tac 3")
+apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+done
+
+
+subsection {* Remainder and Quotient *}
+
+(*typing of remainder: short and long versions*)
+
+lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
+apply (unfold mod_def)
+apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
+done
+
+lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
+apply (unfold mod_def)
+apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
+done
+
+
+(*computation for  mod : 0 and successor cases*)
+
+lemma modC0: "b:N ==> 0 mod b = 0 : N"
+apply (unfold mod_def)
+apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+done
+
+lemma modC_succ:
+"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
+apply (unfold mod_def)
+apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+done
+
+
+(*typing of quotient: short and long versions*)
+
+lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
+apply (unfold div_def)
+apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
+done
+
+lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
+apply (unfold div_def)
+apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
+done
+
+lemmas div_typing_rls = mod_typing div_typing absdiff_typing
+
+
+(*computation for quotient: 0 and successor cases*)
+
+lemma divC0: "b:N ==> 0 div b = 0 : N"
+apply (unfold div_def)
+apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
+done
+
+lemma divC_succ:
+ "[| a:N;  b:N |] ==> succ(a) div b =
+     rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
+apply (unfold div_def)
+apply (tactic {* rew_tac [thm "mod_typing"] *})
+done
+
+
+(*Version of above with same condition as the  mod  one*)
+lemma divC_succ2: "[| a:N;  b:N |] ==>
+     succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
+apply (rule divC_succ [THEN trans_elem])
+apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
+apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
+apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
+done
+
+(*for case analysis on whether a number is 0 or a successor*)
+lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
+                      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
+apply (tactic {* NE_tac "a" 1 *})
+apply (rule_tac [3] PlusI_inr)
+apply (rule_tac [2] PlusI_inl)
+apply (tactic eqintr_tac)
+apply (tactic "equal_tac []")
+done
+
+(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
+lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
+  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+apply (rule EqE)
+(*case analysis on   succ(u mod b)|-|b  *)
+apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
+apply (erule_tac [3] SumE)
+apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
+  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
+apply (rule add_typingL [THEN trans_elem])
+apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
+apply (rule_tac [3] refl_elem)
+apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
+done
+
+end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/Bool.ML
--- a/src/CTT/Bool.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      CTT/Bool
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-val bool_defs = [Bool_def,true_def,false_def,cond_def];
-
-(*Derivation of rules for the type Bool*)
-
-(*formation rule*)
-Goalw bool_defs "Bool type";
-by (typechk_tac []) ;
-qed "boolF";
-
-
-(*introduction rules for true, false*)
-
-Goalw bool_defs "true : Bool";
-by (typechk_tac []) ;
-qed "boolI_true";
-
-Goalw bool_defs "false : Bool";
-by (typechk_tac []) ;
-qed "boolI_false";
-
-(*elimination rule: typing of cond*)
-Goalw bool_defs
-    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolE";
-
-Goalw bool_defs
-    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
-\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
-by (rtac PlusEL 1);
-by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
-qed "boolEL";
-
-(*computation rules for true, false*)
-
-Goalw bool_defs
-    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
-by (resolve_tac comp_rls 1);
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolC_true";
-
-Goalw bool_defs
-    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
-by (resolve_tac comp_rls 1);
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolC_false";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/Bool.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -8,20 +8,80 @@
 
 theory Bool
 imports CTT
-uses "~~/src/Provers/typedsimp.ML" "rew.ML"
 begin
 
-consts
-  Bool        :: "t"
-  true        :: "i"
-  false       :: "i"
-  cond        :: "[i,i,i]=>i"
-defs
-  Bool_def:   "Bool == T+T"
-  true_def:   "true == inl(tt)"
-  false_def:  "false == inr(tt)"
-  cond_def:   "cond(a,b,c) == when(a, %u. b, %u. c)"
+constdefs
+  Bool :: "t"
+  "Bool == T+T"
+
+  true :: "i"
+  "true == inl(tt)"
+
+  false :: "i"
+  "false == inr(tt)"
+
+  cond :: "[i,i,i]=>i"
+  "cond(a,b,c) == when(a, %u. b, %u. c)"
+
+lemmas bool_defs = Bool_def true_def false_def cond_def
+
+
+subsection {* Derivation of rules for the type Bool *}
+
+(*formation rule*)
+lemma boolF: "Bool type"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+
+(*introduction rules for true, false*)
+
+lemma boolI_true: "true : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolI_false: "false : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
 
-ML {* use_legacy_bindings (the_context ()) *}
+(*elimination rule: typing of cond*)
+lemma boolE: 
+    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolEL: 
+    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
+     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
+apply (unfold bool_defs)
+apply (rule PlusEL)
+apply (erule asm_rl refl_elem [THEN TEL])+
+done
+
+(*computation rules for true, false*)
+
+lemma boolC_true: 
+    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolC_false: 
+    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
 
 end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(*  Title:      CTT/CTT.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Tactics and derived rules for Constructive Type Theory
-*)
-
-(*Formation rules*)
-val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
-and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
-
-
-(*Introduction rules
-  OMITTED: EqI, because its premise is an eqelem, not an elem*)
-val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
-and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
-
-
-(*Elimination rules
-  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
-           TE, because it does not involve a constructor *)
-val elim_rls = [NE, ProdE, SumE, PlusE, FE]
-and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
-
-(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
-val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
-
-(*rules with conclusion a:A, an elem judgement*)
-val element_rls = intr_rls @ elim_rls;
-
-(*Definitions are (meta)equality axioms*)
-val basic_defs = [fst_def,snd_def];
-
-(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-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 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 "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
-\    |] ==> c(p`a): C(p`a)";
-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))
-  | 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 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);
-
-fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;
-
-
-(*For simplification: type formation and checking,
-  but no equalities between terms*)
-val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
-
-fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
-
-
-(*Solve all subgoals "A type" using formation rules. *)
-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. *)
-fun typechk_tac thms =
-  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
-  in  REPEAT_FIRST (ASSUME tac)  end;
-
-
-(*Solve a:A (a flexible, A rigid) by introduction rules.
-  Cannot use stringtrees (filt_resolve_tac) since
-  goals like ?a:SUM(A,B) have a trivial head-string *)
-fun intr_tac thms =
-  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
-  in  REPEAT_FIRST (ASSUME tac)  end;
-
-
-(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
-fun equal_tac thms =
-  let val rls = thms @ form_rls @ element_rls @ intrL_rls @
-                elimL_rls @ [refl_elem]
-  in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;
-
-(*** Simplification ***)
-
-(*To simplify the type in a goal*)
-Goal "[| B = A;  a : A |] ==> a : B";
-by (rtac equal_types 1);
-by (rtac sym_type 2);
-by (ALLGOALS assume_tac) ;
-qed "replace_type";
-
-(*Simplify the parameter of a unary type operator.*)
-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));
-by (assume_tac 1) ;
-qed "subst_eqtyparg";
-
-(*Make a reduction rule for simplification.
-  A goal a=c becomes b=c, by virtue of a=b *)
-fun resolve_trans rl = rl RS trans_elem;
-
-(*Simplification rules for Constructive Type Theory*)
-val reduction_rls = map resolve_trans comp_rls;
-
-(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
-  Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
-
-(** Tactics that instantiate CTT-rules.
-    Vars in the given terms will be incremented!
-    The (rtac EqE i) lets them apply to equality judgements. **)
-
-fun NE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
-
-fun SumE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
-
-fun PlusE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
-
-(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
-
-(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
-fun add_mp_tac i =
-    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
-
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
-
-(*"safe" when regarded as predicate calculus rules*)
-val safe_brls = sort (make_ord lessb)
-    [ (true,FE), (true,asm_rl),
-      (false,ProdI), (true,SumE), (true,PlusE) ];
-
-val unsafe_brls =
-    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
-      (true,subst_prodE) ];
-
-(*0 subgoals vs 1 or more*)
-val (safe0_brls, safep_brls) =
-    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
-
-fun safestep_tac thms i =
-    form_tac  ORELSE
-    resolve_tac thms i  ORELSE
-    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
-    DETERM (biresolve_tac safep_brls i);
-
-fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
-
-fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
-
-(*Fails unless it solves the goal!*)
-fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
-
-(** The elimination rules for fst/snd **)
-
-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 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);
-by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
-by (typechk_tac prems) ;
-qed "SumE_snd";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/CTT.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -8,6 +8,7 @@
 
 theory CTT
 imports Pure
+uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
 begin
 
 typedecl i
@@ -57,36 +58,35 @@
   pair      :: "[i,i]=>i"           ("(1<_,/_>)")
 
 syntax
-  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
-  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
-  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
-  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
-
+  "_PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
+  "_SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
 translations
-  "PROD x:A. B" => "Prod(A, %x. B)"
-  "A --> B"     => "Prod(A, %_. B)"
-  "SUM x:A. B"  => "Sum(A, %x. B)"
-  "A * B"       => "Sum(A, %_. B)"
+  "PROD x:A. B" == "Prod(A, %x. B)"
+  "SUM x:A. B"  == "Sum(A, %x. B)"
+
+abbreviation
+  Arrow     :: "[t,t]=>t"           (infixr "-->" 30)
+  "A --> B == PROD _:A. B"
+  Times     :: "[t,t]=>t"           (infixr "*" 50)
+  "A * B == SUM _:A. B"
 
-print_translation {*
-  [("Prod", dependent_tr' ("@PROD", "@-->")),
-   ("Sum", dependent_tr' ("@SUM", "@*"))]
-*}
+const_syntax (xsymbols)
+  Elem  ("(_ /\<in> _)" [10,10] 5)
+  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
+  Arrow  (infixr "\<longrightarrow>" 30)
+  Times  (infixr "\<times>" 50)
 
+const_syntax (HTML output)
+  Elem  ("(_ /\<in> _)" [10,10] 5)
+  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
+  Times  (infixr "\<times>" 50)
 
 syntax (xsymbols)
-  "@-->"    :: "[t,t]=>t"           ("(_ \<longrightarrow>/ _)" [31,30] 30)
-  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
-  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
-  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
   "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
 
 syntax (HTML output)
-  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
-  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
-  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
   "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
@@ -273,6 +273,233 @@
   TEL: "[| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)"
   TC: "p : T ==> p = tt : T"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection "Tactics and derived rules for Constructive Type Theory"
+
+(*Formation rules*)
+lemmas form_rls = NF ProdF SumF PlusF EqF FF TF
+  and formL_rls = ProdFL SumFL PlusFL EqFL
+
+(*Introduction rules
+  OMITTED: EqI, because its premise is an eqelem, not an elem*)
+lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI
+  and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL
+
+(*Elimination rules
+  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
+           TE, because it does not involve a constructor *)
+lemmas elim_rls = NE ProdE SumE PlusE FE
+  and elimL_rls = NEL ProdEL SumEL PlusEL FEL
+
+(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
+lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr
+
+(*rules with conclusion a:A, an elem judgement*)
+lemmas element_rls = intr_rls elim_rls
+
+(*Definitions are (meta)equality axioms*)
+lemmas basic_defs = fst_def snd_def
+
+(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
+lemma SumIL2: "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
+apply (rule sym_elem)
+apply (rule SumIL)
+apply (rule_tac [!] sym_elem)
+apply assumption+
+done
+
+lemmas 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. *)
+lemma subst_prodE:
+  assumes "p: Prod(A,B)"
+    and "a: A"
+    and "!!z. z: B(a) ==> c(z): C(z)"
+  shows "c(p`a): C(p`a)"
+apply (rule prems ProdE)+
+done
+
+
+subsection {* Tactics for type checking *}
+
+ML {*
+
+local
+
+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
+
+in
+
+(*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)
+
+fun ASSUME tf i = test_assume_tac i  ORELSE  tf i
+
+end;
+
+*}
+
+(*For simplification: type formation and checking,
+  but no equalities between terms*)
+lemmas routine_rls = form_rls formL_rls refl_type element_rls
+
+ML {*
+local
+  val routine_rls = thms "routine_rls";
+  val form_rls = thms "form_rls";
+  val intr_rls = thms "intr_rls";
+  val element_rls = thms "element_rls";
+  val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
+    thms "elimL_rls" @ thms "refl_elem"
+in
+
+fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
+
+(*Solve all subgoals "A type" using formation rules. *)
+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. *)
+fun typechk_tac thms =
+  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
+  in  REPEAT_FIRST (ASSUME tac)  end
+
+(*Solve a:A (a flexible, A rigid) by introduction rules.
+  Cannot use stringtrees (filt_resolve_tac) since
+  goals like ?a:SUM(A,B) have a trivial head-string *)
+fun intr_tac thms =
+  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
+  in  REPEAT_FIRST (ASSUME tac)  end
+
+(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
+fun equal_tac thms =
+  REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
 
 end
+
+*}
+
+
+subsection {* Simplification *}
+
+(*To simplify the type in a goal*)
+lemma replace_type: "[| B = A;  a : A |] ==> a : B"
+apply (rule equal_types)
+apply (rule_tac [2] sym_type)
+apply assumption+
+done
+
+(*Simplify the parameter of a unary type operator.*)
+lemma subst_eqtyparg:
+  assumes "a=c : A"
+    and "!!z. z:A ==> B(z) type"
+  shows "B(a)=B(c)"
+apply (rule subst_typeL)
+apply (rule_tac [2] refl_type)
+apply (rule prems)
+apply assumption
+done
+
+(*Simplification rules for Constructive Type Theory*)
+lemmas reduction_rls = comp_rls [THEN trans_elem]
+
+ML {*
+local
+  val EqI = thm "EqI";
+  val EqE = thm "EqE";
+  val NE = thm "NE";
+  val FE = thm "FE";
+  val ProdI = thm "ProdI";
+  val SumI = thm "SumI";
+  val SumE = thm "SumE";
+  val PlusE = thm "PlusE";
+  val PlusI_inl = thm "PlusI_inl";
+  val PlusI_inr = thm "PlusI_inr";
+  val subst_prodE = thm "subst_prodE";
+  val intr_rls = thms "intr_rls";
+in
+
+(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
+  Uses other intro rules to avoid changing flexible goals.*)
+val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1))
+
+(** Tactics that instantiate CTT-rules.
+    Vars in the given terms will be incremented!
+    The (rtac EqE i) lets them apply to equality judgements. **)
+
+fun NE_tac (sp: string) i =
+  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
+
+fun SumE_tac (sp: string) i =
+  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
+
+fun PlusE_tac (sp: string) i =
+  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
+
+(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
+
+(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
+fun add_mp_tac i =
+    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i
+
+(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+fun mp_tac i = etac subst_prodE i  THEN  assume_tac i
+
+(*"safe" when regarded as predicate calculus rules*)
+val safe_brls = sort (make_ord lessb)
+    [ (true,FE), (true,asm_rl),
+      (false,ProdI), (true,SumE), (true,PlusE) ]
+
+val unsafe_brls =
+    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
+      (true,subst_prodE) ]
+
+(*0 subgoals vs 1 or more*)
+val (safe0_brls, safep_brls) =
+    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
+
+fun safestep_tac thms i =
+    form_tac  ORELSE
+    resolve_tac thms i  ORELSE
+    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
+    DETERM (biresolve_tac safep_brls i)
+
+fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
+
+fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls
+
+(*Fails unless it solves the goal!*)
+fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
+
+end
+*}
+
+use "rew.ML"
+
+
+subsection {* The elimination rules for fst/snd *}
+
+lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A"
+apply (unfold basic_defs)
+apply (erule SumE)
+apply assumption
+done
+
+(*The first premise must be p:Sum(A,B) !!*)
+lemma SumE_snd:
+  assumes major: "p: Sum(A,B)"
+    and "A type"
+    and "!!x. x:A ==> B(x) type"
+  shows "snd(p) : B(fst(p))"
+  apply (unfold basic_defs)
+  apply (rule major [THEN SumE])
+  apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
+  apply (tactic {* typechk_tac (thms "prems") *})
+  done
+
+end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/IsaMakefile	Fri Jun 02 18:15:38 2006 +0200
@@ -26,8 +26,8 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
-  Bool.ML Bool.thy CTT.ML CTT.thy Main.thy ROOT.ML rew.ML
+$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
+  Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
 
 
@@ -35,8 +35,8 @@
 
 CTT-ex: CTT $(LOG)/CTT-ex.gz
 
-$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \
-  ex/synth.ML ex/typechk.ML
+$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
+  ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
 	@$(ISATOOL) usedir $(OUT)/CTT ex
 
 
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/README.html
--- a/src/CTT/README.html	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/README.html	Fri Jun 02 18:15:38 2006 +0200
@@ -13,10 +13,7 @@
 
 <H2>CTT: Constructive Type Theory</H2>
 
-This directory contains the ML sources of the Isabelle system for
-Constructive Type Theory (extensional equality, no universes).<p>
-
-The <tt>ex</tt> subdirectory contains some examples.<p>
+This is a version of Constructive Type Theory (extensional equality, no universes).<p>
 
 Useful references on Constructive Type Theory:
 
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/ROOT.ML	Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,10 @@
-(*  Title:      CTT/ROOT
+(*  Title:      CTT/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
-
-Adds Constructive Type Theory to a database containing pure Isabelle. 
-Should be executed in the subdirectory CTT.
 *)
 
 val banner = "Constructive Type Theory";
 writeln banner;
 
 use_thy "Main";
-
-Goal "tt : T";  (*leave subgoal package empty*)
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/Elimination.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Elimination.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,194 @@
+(*  Title:      CTT/ex/Elimination.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+Some examples taken from P. Martin-L\"of, Intuitionistic type theory
+        (Bibliopolis, 1984).
+*)
+
+header "Examples with elimination rules"
+
+theory Elimination
+imports CTT
+begin
+
+text "This finds the functions fst and snd!"
+
+lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+apply (tactic {* pc_tac [] 1 *})
+done
+
+lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+apply (tactic {* pc_tac [] 1 *})
+back
+done
+
+text "Double negation of the Excluded Middle"
+lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
+apply (tactic "intr_tac []")
+apply (rule ProdE)
+apply assumption
+apply (tactic "pc_tac [] 1")
+done
+
+lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
+apply (tactic "pc_tac [] 1")
+done
+(*The sequent version (ITT) could produce an interesting alternative
+  by backtracking.  No longer.*)
+
+text "Binary sums and products"
+lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*A distributive law*)
+lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general version, same proof*)
+lemma
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!x. x:A ==> C(x) type"
+  shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Construction of the currying functional"
+lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general goal with same proof*)
+lemma
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
+  shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
+                      (PROD x:A . PROD y:B(x) . C(<x,y>))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
+lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general goal with same proof*)
+lemma
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
+  shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
+        --> (PROD z : (SUM x:A . B(x)) . C(z))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Function application"
+lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
+apply (tactic "pc_tac [] 1")
+done
+
+text "Basic test of quantifier reasoning"
+lemma
+  assumes "A type"
+    and "B type"
+    and "!!x y.[| x:A;  y:B |] ==> C(x,y) type"
+  shows
+    "?a :     (SUM y:B . PROD x:A . C(x,y))
+          --> (PROD x:A . SUM y:B . C(x,y))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984) pages 36-7: the combinator S"
+lemma
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
+  shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
+             --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
+lemma
+  assumes "A type"
+    and "B type"
+    and "!!z. z: A+B ==> C(z) type"
+  shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
+          --> (PROD z: A+B. C(z))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+(*towards AXIOM OF CHOICE*)
+lemma [folded basic_defs]:
+  "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
+apply (tactic "pc_tac [] 1")
+done
+
+
+(*Martin-Lof (1984) page 50*)
+text "AXIOM OF CHOICE!  Delicate use of elimination rules"
+lemma
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
+  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
+                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* intr_tac (thms "prems") *})
+apply (tactic "add_mp_tac 2")
+apply (tactic "add_mp_tac 1")
+apply (erule SumE_fst)
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (rule_tac [4] SumE_snd)
+apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
+done
+
+text "Axiom of choice.  Proof without fst, snd.  Harder still!"
+lemma [folded basic_defs]:
+  assumes "A type"
+    and "!!x. x:A ==> B(x) type"
+    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
+  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
+                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* intr_tac (thms "prems") *})
+(*Must not use add_mp_tac as subst_prodE hides the construction.*)
+apply (rule ProdE [THEN SumE], assumption)
+apply (tactic "TRYALL assume_tac")
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (erule_tac [4] ProdE [THEN SumE])
+apply (tactic {* typechk_tac (thms "prems") *})
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (tactic {* typechk_tac (thms "prems") *})
+apply assumption
+done
+
+text "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)     *)
+lemma
+  assumes "A type"
+    and "B type"
+    and "!!z. z:A*B ==> C(z) type"
+  shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
+apply (rule intr_rls)
+apply (tactic {* biresolve_tac safe_brls 2 *})
+(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
+apply (rule_tac [2] a = "y" in ProdE)
+apply (tactic {* typechk_tac (thms "prems") *})
+apply (rule SumE, assumption)
+apply (tactic "intr_tac []")
+apply (tactic "TRYALL assume_tac")
+apply (tactic {* typechk_tac (thms "prems") *})
+done
+
+end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/Equality.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Equality.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,70 @@
+(*  Title:      CTT/ex/Equality.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+header "Equality reasoning by rewriting"
+
+theory Equality
+imports CTT
+begin
+
+lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+lemma when_eq: "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+(*in the "rec" formulation of addition, 0+n=n *)
+lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+(*the harder version, n+0=n: recursive, uses induction hypothesis*)
+lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "hyp_rew_tac []")
+done
+
+(*Associativity of addition*)
+lemma "[| 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"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+(*Martin-Lof (1984) page 62: pairing is surjective*)
+lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
+done
+
+lemma "[| a : A;  b : B |] ==>
+     (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
+apply (tactic "rew_tac []")
+done
+
+(*a contrived, complicated simplication, requires sum-elimination also*)
+lemma "(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)"
+apply (rule reduction_rls)
+apply (rule_tac [3] intrL_rls)
+apply (rule_tac [4] EqE)
+apply (rule_tac [4] SumE, tactic "assume_tac 4")
+(*order of unifiers is essential here*)
+apply (tactic "rew_tac []")
+done
+
+end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/ROOT.ML
--- a/src/CTT/ex/ROOT.ML	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/ex/ROOT.ML	Fri Jun 02 18:15:38 2006 +0200
@@ -3,12 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Executes all examples for Constructive Type Theory. 
+Examples for Constructive Type Theory. 
 *)
 
-print_depth 2;  
-
-time_use "typechk.ML";
-time_use "elim.ML";
-time_use "equal.ML";
-time_use "synth.ML";
+use_thy "Typechecking";
+use_thy "Elimination";
+use_thy "Equality";
+use_thy "Synthesis";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/Synthesis.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Synthesis.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,106 @@
+(*  Title:      CTT/ex/Synthesis.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+header "Synthesis examples, using a crude form of narrowing"
+
+theory Synthesis
+imports Arith
+begin
+
+text "discovery of predecessor function"
+lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)    
+                  *  (PROD n:N. Eq(N, pred ` succ(n), n))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [3] reduction_rls)
+apply (rule_tac [5] comp_rls)
+apply (tactic "rew_tac []")
+done
+
+text "the function fst as an element of a function type"
+lemma [folded basic_defs]:
+  "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [2] reduction_rls)
+apply (rule_tac [4] comp_rls)
+apply (tactic "typechk_tac []")
+txt "now put in A everywhere"
+apply assumption+
+done
+
+text "An interesting use of the eliminator, when"
+(*The early implementation of unification caused non-rigid path in occur check
+  See following example.*)
+lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)   
+                   * Eq(?A, ?b(inr(i)), <succ(0), i>)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule comp_rls)
+apply (tactic "rew_tac []")
+oops
+
+(*Here we allow the type to depend on i.  
+ 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.*)
+lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
+                  *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
+oops
+
+text "A tricky combination of when and split"
+(*Now handled easily, but caused great problems once*)
+lemma [folded basic_defs]:
+  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)    
+                           *  Eq(?A, ?b(inr(<i,j>)), j)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule PlusC_inl [THEN trans_elem])
+apply (rule_tac [4] comp_rls)
+apply (rule_tac [7] reduction_rls)
+apply (rule_tac [10] comp_rls)
+apply (tactic "typechk_tac []")
+oops
+
+(*similar but allows the type to depend on i and j*)
+lemma "?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)"
+oops
+
+(*similar but specifying the type N simplifies the unification problems*)
+lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)   
+                          *   Eq(N, ?b(inr(<i,j>)), j)"
+oops
+
+
+text "Deriving the addition operator"
+lemma [folded arith_defs]:
+  "?c : PROD n:N. Eq(N, ?f(0,n), n)   
+                  *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule comp_rls)
+apply (tactic "rew_tac []")
+oops
+
+text "The addition function -- using explicit lambdas"
+lemma [folded arith_defs]:
+  "?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)))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (tactic "resolve_tac [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (tactic "resolve_tac [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (rule_tac [3] p = "y" in NC_succ)
+  (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
+apply (tactic "rew_tac []")
+done
+
+end
+
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/Typechecking.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Typechecking.thy	Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,88 @@
+(*  Title:      CTT/ex/Typechecking.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+header "Easy examples: type checking and type deduction"
+
+theory Typechecking
+imports CTT
+begin
+
+subsection {* Single-step proofs: verifying that a type is well-formed *}
+
+lemma "?A type"
+apply (rule form_rls)
+done
+
+lemma "?A type"
+apply (rule form_rls)
+back
+apply (rule form_rls)
+apply (rule form_rls)
+done
+
+lemma "PROD z:?A . N + ?B(z) type"
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+done
+
+
+subsection {* Multi-step proofs: Type inference *}
+
+lemma "PROD w:N. N + N type"
+apply (tactic form_tac)
+done
+
+lemma "<0, succ(0)> : ?A"
+apply (tactic "intr_tac []")
+done
+
+lemma "PROD w:N . Eq(?A,w,w) type"
+apply (tactic "typechk_tac []")
+done
+
+lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking an application of fst"
+lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking the predecessor function"
+lemma "lam n. rec(n, 0, %x y. x) : ?A"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking the addition function"
+lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
+apply (tactic "typechk_tac []")
+done
+
+(*Proofs involving arbitrary types.
+  For concreteness, every type variable left over is forced to be N*)
+ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
+
+lemma "lam w. <w,w> : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+lemma "lam x. lam y. x : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+text "typechecking fst (as a function object)"
+lemma "lam i. split(i, %j k. j) : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+end
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(*  Title:      CTT/ex/elim
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Some examples taken from P. Martin-L\"of, Intuitionistic type theory
-        (Bibliopolis, 1984).
-
-by (safe_tac prems 1);
-by (step_tac prems 1);
-by (pc_tac prems 1);
-*)
-
-writeln"Examples with elimination rules";
-
-
-writeln"This finds the functions 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(); 
-back() handle ERROR _ => writeln"And there are indeed no others";  
-
-
-writeln"Double negation of the Excluded Middle";
-Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
-by (intr_tac []);
-by (rtac ProdE 1);
-by (assume_tac 1);
-by (pc_tac [] 1);
-result();
-
-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";
-Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
-by (pc_tac [] 1);
-result();
-
-(*A distributive law*)
-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
-   "[| 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";
-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
-    "[| 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)).    \
-\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
-by (pc_tac prems 1);
-result();
-
-writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
-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 
- "[| 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";
-Goal "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
-by (pc_tac [] 1);
-result();
-
-writeln"Basic test of quantifier reasoning";
-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))";
-by (pc_tac prems 1);
-result();
-
-(*faulty proof attempt, stripping the quantifiers in wrong sequence
-by (intr_tac[]);
-by (pc_tac prems 1);        ...fails!!  *)
-
-writeln"Martin-Lof (1984) pages 36-7: the combinator S";
-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)) \
-\            --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (pc_tac prems 1);
-result();
-
-writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
-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))";
-by (pc_tac prems 1);
-result();
-
-(*towards AXIOM OF CHOICE*)
-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   
-    "[| 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)).        \
-\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (intr_tac prems);
-by (add_mp_tac 2);
-by (add_mp_tac 1);
-by (etac SumE_fst 1);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (rtac SumE_snd 4);
-by (typechk_tac (SumE_fst::prems));
-result();
-
-writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
-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)).        \
-\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (intr_tac prems);
-(*Must not use add_mp_tac as subst_prodE hides the construction.*)
-by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);
-by (TRYALL assume_tac);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (etac (ProdE RS SumE) 4);
-by (typechk_tac prems);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (typechk_tac prems);
-by (assume_tac 1);
-by (fold_tac basic_defs);  (*puts in fst and snd*)
-result();
-
-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   
-    "[| 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);
-by (biresolve_tac safe_brls 2);
-(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
-by (res_inst_tac [ ("a","y") ] ProdE 2);
-by (typechk_tac prems);
-by (rtac SumE 1  THEN  assume_tac 1);
-by (intr_tac[]);
-by (TRYALL assume_tac);
-by (typechk_tac prems);
-result();
-
-writeln"Reached end of file.";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/equal.ML
--- a/src/CTT/ex/equal.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title:      CTT/ex/equal
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Equality reasoning by rewriting.
-*)
-
-Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  assume_tac 1);
-by (rew_tac []);
-qed "split_eq";
-
-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  assume_tac 1);
-by (rew_tac []);
-by (ALLGOALS assume_tac);
-qed "when_eq";
-
-
-(*in the "rec" formulation of addition, 0+n=n *)
-Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  assume_tac 1);
-by (rew_tac []);
-result();
-
-
-(*the harder version, n+0=n: recursive, uses induction hypothesis*)
-Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1  THEN  assume_tac 1);
-by (hyp_rew_tac []);
-result();
-
-
-(*Associativity of addition*)
-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 []);
-result();
-
-
-(*Martin-Lof (1984) page 62: pairing is surjective*)
-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  assume_tac 1);
-by (DEPTH_SOLVE_1 (rew_tac []));   (*!!!!!!!*)
-result();
-
-
-Goal "[| a : A;  b : B |] ==> \
-\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
-by (rew_tac []);
-result();
-
-
-(*a contrived, complicated simplication, requires sum-elimination also*)
-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 []);
-result();
-
-writeln"Reached end of file.";
-(*28 August 1988: loaded this file in 34 seconds*)
-(*2 September 1988: loaded this file in 48 seconds*)
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/synth.ML
--- a/src/CTT/ex/synth.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(*  Title:      CTT/ex/synth
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-writeln"Synthesis examples, using a crude form of narrowing";
-
-context (theory "Arith");
-
-writeln"discovery of predecessor function";
-Goal 
- "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
-\                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
-by (intr_tac[]);
-by eqintr_tac;
-by (resolve_tac reduction_rls 3);
-by (resolve_tac comp_rls 5);
-by (rew_tac[]);
-result();
-
-writeln"the function fst as an element of a function type";
-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 []);
-writeln"now put in A everywhere";
-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 "?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);
-by (rew_tac[]);
-uresult();
-
-(*Here we allow the type to depend on i.  
- 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 "?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 
-    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
-\                          *  Eq(?A, ?b(inr(<i,j>)), j)";
-by (intr_tac[]); 
-by eqintr_tac;
-by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
-by (resolve_tac comp_rls 4); 
-by (resolve_tac reduction_rls 7);
-by (resolve_tac comp_rls 10);
-by (typechk_tac[]); (*2 secs*)
-by (fold_tac basic_defs);
-uresult();
-
-(*similar but allows the type to depend on i and j*)
-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 "?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 "?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);
-by (rew_tac[]);
-by (fold_tac arith_defs);
-result();
-
-writeln"The addition function -- using explicit lambdas";
-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)))";
-by (intr_tac[]);
-by eqintr_tac;
-by (resolve_tac [TSimp.split_eqn] 3);
-by (SELECT_GOAL (rew_tac[]) 4);
-by (resolve_tac [TSimp.split_eqn] 3);
-by (SELECT_GOAL (rew_tac[]) 4);
-by (res_inst_tac [("p","y")] NC_succ 3);
-  (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
-by (rew_tac[]); 
-by (fold_tac arith_defs);
-result();
-
-writeln"Reached end of file.";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/ex/typechk.ML
--- a/src/CTT/ex/typechk.ML	Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(*  Title:      CTT/ex/typechk
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-  
-Easy examples: type checking and type deduction
-*)
-
-writeln"Single-step proofs: verifying that a type is well-formed";
-
-Goal "?A type";
-by (resolve_tac form_rls 1);
-result(); 
-writeln"getting a second solution";
-back();
-by (resolve_tac form_rls 1);
-by (resolve_tac form_rls 1);
-result(); 
-
-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);
-by (resolve_tac form_rls 1);
-by (resolve_tac form_rls 1);
-uresult(); 
-
-
-writeln"Multi-step proofs: Type inference";
-
-Goal "PROD w:N. N + N type";
-by form_tac;
-result(); 
-
-Goal "<0, succ(0)> : ?A";
-by (intr_tac[]);
-result(); 
-
-Goal "PROD w:N . Eq(?A,w,w) type";
-by (typechk_tac[]);
-result(); 
-
-Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
-by (typechk_tac[]);
-result(); 
-
-writeln"typechecking an application of fst";
-Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
-by (typechk_tac[]);
-result(); 
-
-writeln"typechecking the predecessor function";
-Goal "lam n. rec(n, 0, %x y. x) : ?A";
-by (typechk_tac[]);
-result(); 
-
-writeln"typechecking the addition function";
-Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
-by (typechk_tac[]);
-result(); 
-
-(*Proofs involving arbitrary types.
-  For concreteness, every type variable left over is forced to be N*)
-val N_tac = TRYALL (rtac NF);
-
-Goal "lam w. <w,w> : ?A";
-by (typechk_tac[]);
-by N_tac;
-result(); 
-
-Goal "lam x. lam y. x : ?A";
-by (typechk_tac[]);
-by N_tac;
-result(); 
-
-writeln"typechecking fst (as a function object) ";
-Goal "lam i. split(i, %j k. j) : ?A";
-by (typechk_tac[]);
-by N_tac;
-result(); 
-
-writeln"Reached end of file.";
diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/rew.ML
--- a/src/CTT/rew.ML	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/rew.ML	Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,15 @@
-(*  Title:      CTT/rew
+(*  Title:      CTT/rew.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Simplifier for CTT, using Typedsimp
+Simplifier for CTT, using Typedsimp.
 *)
 
 (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
   for using assumptions as rewrite rules*)
 fun peEs 0 = []
-  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
+  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
 
 (*Tactic used for proving conditions for the cond_rls*)
 val prove_cond_tac = eresolve_tac (peEs 5);
@@ -17,19 +17,19 @@
 
 structure TSimp_data: TSIMP_DATA =
   struct
-  val refl              = refl_elem
-  val sym               = sym_elem
-  val trans             = trans_elem
-  val refl_red          = refl_red
-  val trans_red         = trans_red
-  val red_if_equal      = red_if_equal
-  val default_rls       = comp_rls
-  val routine_tac       = routine_tac routine_rls
+  val refl              = thm "refl_elem"
+  val sym               = thm "sym_elem"
+  val trans             = thm "trans_elem"
+  val refl_red          = thm "refl_red"
+  val trans_red         = thm "trans_red"
+  val red_if_equal      = thm "red_if_equal"
+  val default_rls       = thms "comp_rls"
+  val routine_tac       = routine_tac (thms "routine_rls")
   end;
 
 structure TSimp = TSimpFun (TSimp_data);
 
-val standard_congr_rls = intrL2_rls @ elimL_rls;
+val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
 
 (*Make a rewriting tactic from a normalization tactic*)
 fun make_rew_tac ntac =