--- 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"
--- 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
--- 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;
--- 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
--- 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
--- 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