--- a/TFL/rules.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(* Title: TFL/rules
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-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;
--- a/TFL/tfl.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(* Title: TFL/tfl
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Main module
-*)
-
-signature TFL_sig =
-sig
-
- val trace : bool ref
-
- val default_simps : thm list (*simprules used for deriving rules...*)
-
- val Add_recdef_congs: thm list -> unit
- val Del_recdef_congs: thm list -> unit
- val init: theory -> theory
- val print_recdef_congs: theory -> unit
- val congs : theory -> thm list -> thm list (*fn to make congruence rules*)
-
- type pattern
-
- val mk_functional : theory -> term list
- -> {functional:term,
- pats: pattern list}
-
- val wfrec_definition0 : theory -> string -> term -> term -> theory * thm
-
- val post_definition : thm list -> theory * (thm * pattern list)
- -> {theory : theory,
- rules : thm,
- rows : int list,
- TCs : term list list,
- full_pats_TCs : (term * term list) list}
-
- val wfrec_eqns : theory -> xstring
- -> thm list (* congruence rules *)
- -> term list
- -> {WFR : term, SV : term list,
- proto_def : term,
- extracta :(thm * term list) list,
- pats : pattern list}
-
- val lazyR_def : theory -> xstring
- -> thm list (* congruence rules *)
- -> term list
- -> {theory : theory,
- rules : thm,
- R : term,
- SV : term list,
- full_pats_TCs : (term * term list) list,
- patterns : pattern list}
-
- val mk_induction : theory
- -> {fconst:term,
- R : term,
- SV : term list,
- pat_TCs_list : (term * term list) list}
- -> thm
-
- val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
- -> theory
- -> {rules:thm, induction:thm, TCs:term list list}
- -> {rules:thm, induction:thm, nested_tcs:thm list}
-end;
--- a/TFL/thms.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: TFL/thms
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-signature Thms_sig =
-sig
- val WF_INDUCTION_THM:thm
- val WFREC_COROLLARY :thm
- val CUT_DEF :thm
- val SELECT_AX :thm
-
- val LET_CONG :thm
-
- val eqT :thm
- val rev_eq_mp :thm
- val simp_thm :thm
-end;
--- a/TFL/thry.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: TFL/thry
- 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;
-
-
--- a/TFL/usyntax.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(* Title: TFL/usyntax
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-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;
--- a/TFL/utils.sig Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: TFL/utils
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-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;
-