# HG changeset patch
# User wenzelm
# Date 968172822 -7200
# Node ID bf8300fa42382a9de82b6580bfd979f333d6bd3c
# Parent  90cbf68b92273a630a9f987c55e164182f8fe14b
tuned;

diff -r 90cbf68b9227 -r bf8300fa4238 Admin/makedist
--- a/Admin/makedist	Tue Sep 05 18:53:21 2000 +0200
+++ b/Admin/makedist	Tue Sep 05 18:53:42 2000 +0200
@@ -13,7 +13,6 @@
 DISTPREFIX=~/tmp/isadist
 
 umask 022
-newgrp isabelle
 
 
 ## diagnostics
@@ -80,7 +79,7 @@
 DISTDATE=$(date "+%B %Y")
 
 if [ "$VERSION" = "--" ]; then
-  DISTNAME="Isabelle_$DATE_test"
+  DISTNAME="Isabelle_${DATE}_test"
   DISTVERSION="$DISTNAME"
   EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"
   UNOFFICIAL=""
@@ -218,6 +217,8 @@
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
 
+chgrp -R isabelle "$DISTNAME"
+
 rm -rf "${DISTNAME}-old"
 
 
diff -r 90cbf68b9227 -r bf8300fa4238 TFL/rules.sml
--- a/TFL/rules.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/rules.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      TFL/rules
+(*  Title:      TFL/rules.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
@@ -6,6 +6,62 @@
 Emulation of HOL inference rules for TFL
 *)
 
+signature Rules_sig =
+sig
+(*  structure USyntax : USyntax_sig *)
+  val dest_thm : thm -> term list * term
+
+  (* Inference rules *)
+  val REFL      :cterm -> thm
+  val ASSUME    :cterm -> thm
+  val MP        :thm -> thm -> thm
+  val MATCH_MP  :thm -> thm -> thm
+  val CONJUNCT1 :thm -> thm
+  val CONJUNCT2 :thm -> thm
+  val CONJUNCTS :thm -> thm list
+  val DISCH     :cterm -> thm -> thm
+  val UNDISCH   :thm  -> thm
+  val INST_TYPE :(typ*typ)list -> thm -> thm
+  val SPEC      :cterm -> thm -> thm
+  val ISPEC     :cterm -> thm -> thm
+  val ISPECL    :cterm list -> thm -> thm
+  val GEN       :cterm -> thm -> thm
+  val GENL      :cterm list -> thm -> thm
+  val LIST_CONJ :thm list -> thm
+
+  val SYM : thm -> thm
+  val DISCH_ALL : thm -> thm
+  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
+  val SPEC_ALL  : thm -> thm
+  val GEN_ALL   : thm -> thm
+  val IMP_TRANS : thm -> thm -> thm
+  val PROVE_HYP : thm -> thm -> thm
+
+  val CHOOSE : cterm * thm -> thm -> thm
+  val EXISTS : cterm * cterm -> thm -> thm
+  val EXISTL : cterm list -> thm -> thm
+  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
+
+  val EVEN_ORS : thm list -> thm list
+  val DISJ_CASESL : thm -> thm list -> thm
+
+  val list_beta_conv : cterm -> cterm list -> thm
+  val SUBS : thm list -> thm -> thm
+  val simpl_conv : simpset -> thm list -> cterm -> thm
+
+  val rbeta : thm -> thm
+(* For debugging my isabelle solver in the conditional rewriter *)
+  val term_ref : term list ref
+  val thm_ref : thm list ref
+  val mss_ref : meta_simpset list ref
+  val tracing : bool ref
+  val CONTEXT_REWRITE_RULE : term * term list * thm * thm list 
+                             -> thm -> thm * term list
+  val RIGHT_ASSOC : thm -> thm 
+
+  val prove : cterm * tactic -> thm
+end;
+
 
 structure Rules : Rules_sig = 
 struct
diff -r 90cbf68b9227 -r bf8300fa4238 TFL/thms.sml
--- a/TFL/thms.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/thms.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,37 +1,32 @@
-(*  Title:      TFL/thms
+(*  Title:      TFL/thms.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
 
-structure Thms : Thms_sig =
-struct
-   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
-   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
-   val CUT_DEF = cut_def
+signature Thms_sig =
+sig
+   val WF_INDUCTION_THM: thm
+   val WFREC_COROLLARY: thm
+   val CUT_DEF: thm
+   val SELECT_AX: thm
+   val eqT: thm
+   val rev_eq_mp: thm
+   val simp_thm: thm
+end;
 
-   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
-         val _ = by (strip_tac 1)
-         val _ = by (rtac selectI 1)
-         val _ = by (assume_tac 1)
-   in val SELECT_AX = result()
-   end;
+structure Thms: Thms_sig =
+struct
+   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
+   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
+   val CUT_DEF = get_thm WF.thy "cut_def";
 
-  (*-------------------------------------------------------------------------
-   *  Congruence rule needed for TFL, but not for general simplification
-   *-------------------------------------------------------------------------*)
-   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
-                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
-                          \ (Let M f = Let N g)";
-         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
-         val _ = by (rtac p2 1);
-         val _ = by (rtac refl 1);
-   in val LET_CONG = result() end;
+   val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
+     (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
 
    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
 
-   val eqT       = prove"(x = True) --> x"
-   val rev_eq_mp = prove"(x = y) --> y --> x"
-   val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
-
+   val eqT = prove"(x = True) --> x";
+   val rev_eq_mp = prove"(x = y) --> y --> x";
+   val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
 end;
diff -r 90cbf68b9227 -r bf8300fa4238 TFL/thry.sml
--- a/TFL/thry.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/thry.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,9 +1,30 @@
-(*  Title:      TFL/thry
+(*  Title:      TFL/thry.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
 
+signature Thry_sig =
+sig
+  val match_term : theory -> term -> term 
+                    -> (term*term)list * (typ*typ)list
+
+  val match_type : theory -> typ -> typ -> (typ*typ)list
+
+  val typecheck : theory -> term -> cterm
+
+  (* Datatype facts of various flavours *)
+  val match_info: theory -> string -> {constructors:term list,
+                                     case_const:term} option
+
+  val induct_info: theory -> string -> {constructors:term list,
+                                      nchotomy:thm} option
+
+  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
+
+end;
+
+
 structure Thry : Thry_sig (* LThry_sig *) = 
 struct
 
diff -r 90cbf68b9227 -r bf8300fa4238 TFL/usyntax.sml
--- a/TFL/usyntax.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/usyntax.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,11 +1,100 @@
-(*  Title:      TFL/usyntax
+(*  Title:      TFL/usyntax.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
-Emulation of HOL's abstract syntax functions
+Emulation of HOL's abstract syntax functions.
 *)
 
+signature USyntax_sig =
+sig
+  structure Utils : Utils_sig
+
+  datatype lambda = VAR   of {Name : string, Ty : typ}
+                  | CONST of {Name : string, Ty : typ}
+                  | COMB  of {Rator: term, Rand : term}
+                  | LAMB  of {Bvar : term, Body : term}
+
+  val alpha : typ
+
+  (* Types *)
+  val type_vars  : typ -> typ list
+  val type_varsl : typ list -> typ list
+  val mk_vartype : string -> typ
+  val is_vartype : typ -> bool
+  val strip_prod_type : typ -> typ list
+
+  (* Terms *)
+  val free_vars_lr : term -> term list
+  val type_vars_in_term : term -> typ list
+  val dest_term  : term -> lambda
+  
+  (* Prelogic *)
+  val inst      : (typ*typ) list -> term -> term
+
+  (* Construction routines *)
+  val mk_abs    :{Bvar  : term, Body : term} -> term
+
+  val mk_imp    :{ant : term, conseq :  term} -> term
+  val mk_select :{Bvar : term, Body : term} -> term
+  val mk_forall :{Bvar : term, Body : term} -> term
+  val mk_exists :{Bvar : term, Body : term} -> term
+  val mk_conj   :{conj1 : term, conj2 : term} -> term
+  val mk_disj   :{disj1 : term, disj2 : term} -> term
+  val mk_pabs   :{varstruct : term, body : term} -> term
+
+  (* Destruction routines *)
+  val dest_const: term -> {Name : string, Ty : typ}
+  val dest_comb : term -> {Rator : term, Rand : term}
+  val dest_abs  : term -> {Bvar : term, Body : term}
+  val dest_eq     : term -> {lhs : term, rhs : term}
+  val dest_imp    : term -> {ant : term, conseq : term}
+  val dest_forall : term -> {Bvar : term, Body : term}
+  val dest_exists : term -> {Bvar : term, Body : term}
+  val dest_neg    : term -> term
+  val dest_conj   : term -> {conj1 : term, conj2 : term}
+  val dest_disj   : term -> {disj1 : term, disj2 : term}
+  val dest_pair   : term -> {fst : term, snd : term}
+  val dest_pabs   : term -> {varstruct : term, body : term}
+
+  val lhs   : term -> term
+  val rhs   : term -> term
+  val rand  : term -> term
+
+  (* Query routines *)
+  val is_imp    : term -> bool
+  val is_forall : term -> bool 
+  val is_exists : term -> bool 
+  val is_neg    : term -> bool
+  val is_conj   : term -> bool
+  val is_disj   : term -> bool
+  val is_pair   : term -> bool
+  val is_pabs   : term -> bool
+
+  (* Construction of a term from a list of Preterms *)
+  val list_mk_abs    : (term list * term) -> term
+  val list_mk_imp    : (term list * term) -> term
+  val list_mk_forall : (term list * term) -> term
+  val list_mk_conj   : term list -> term
+
+  (* Destructing a term to a list of Preterms *)
+  val strip_comb     : term -> (term * term list)
+  val strip_abs      : term -> (term list * term)
+  val strip_imp      : term -> (term list * term)
+  val strip_forall   : term -> (term list * term)
+  val strip_exists   : term -> (term list * term)
+  val strip_disj     : term -> term list
+
+  (* Miscellaneous *)
+  val mk_vstruct : typ -> term list -> term
+  val gen_all    : term -> term
+  val find_term  : (term -> bool) -> term -> term option
+  val dest_relation : term -> term * term * term
+  val is_WFR : term -> bool
+  val ARB : typ -> term
+end;
+
+
 structure USyntax : USyntax_sig =
 struct
 
diff -r 90cbf68b9227 -r bf8300fa4238 TFL/utils.sml
--- a/TFL/utils.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/utils.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,11 +1,31 @@
-(*  Title:      TFL/utils
+(*  Title:      TFL/utils.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
-Basic utilities
+Basic utilities.
 *)
 
+signature Utils_sig =
+sig
+  exception ERR of {module:string,func:string, mesg:string}
+
+  val can   : ('a -> 'b) -> 'a -> bool
+  val holds : ('a -> bool) -> 'a -> bool
+  val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
+
+  val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
+  val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
+  val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
+  val take  : ('a -> 'b) -> int * 'a list -> 'b list
+  val sort  : ('a -> 'a -> bool) -> 'a list -> 'a list
+
+end;
+
+
 structure Utils = 
 struct