--- a/TFL/mask.sig Tue May 27 13:03:41 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: TFL/mask
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-signature Mask_sig =
-sig
- datatype 'a binding = |-> of ('a * 'a) (* infix 7 |->; *)
-
- type mask
- val ERR : mask
-
-end
--- a/TFL/mask.sml Tue May 27 13:03:41 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: TFL/mask
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-(*---------------------------------------------------------------------------
- * This structure is intended to shield TFL from any constructors already
- * declared in the environment. In the Isabelle port, for example, there
- * was already a datatype with "|->" being a constructor. In TFL we were
- * trying to define a function "|->", but it failed in PolyML (which conforms
- * better to the Standard) while the definition was accepted in NJ/SML
- * (which doesn't always conform so well to the standard).
- *---------------------------------------------------------------------------*)
-
-structure Mask : Mask_sig =
-struct
-
- datatype 'a binding = |-> of ('a * 'a) (* infix 7 |->; *)
-
- datatype mask = ERR
-end;
--- a/TFL/rules.new.sml Tue May 27 13:03:41 1997 +0200
+++ b/TFL/rules.new.sml Tue May 27 13:22:30 1997 +0200
@@ -10,8 +10,6 @@
struct
open Utils;
-open Mask;
-infix 7 |->;
structure USyntax = USyntax;
structure S = USyntax;
@@ -53,7 +51,7 @@
*---------------------------------------------------------------------------*)
fun INST_TYPE blist thm =
let val {sign,...} = rep_thm thm
- val blist' = map (fn (TVar(idx,_) |-> B) => (idx, ctyp_of sign B)) blist
+ val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist
in Thm.instantiate (blist',[]) thm
end
handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};
@@ -368,18 +366,19 @@
* A |- ?y_1...y_n. M
*
*---------------------------------------------------------------------------*)
-(* Could be improved, but needs "subst" for certified terms *)
+(* Could be improved, but needs "subst_free" for certified terms *)
fun IT_EXISTS blist th =
let val {sign,...} = rep_thm th
val tych = cterm_of sign
val detype = #t o rep_cterm
- val blist' = map (fn (x|->y) => (detype x |-> detype y)) blist
+ val blist' = map (fn (x,y) => (detype x, detype y)) blist
fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
in
- U.itlist (fn (b as (r1 |-> r2)) => fn thm =>
- EXISTS(?r2(S.subst[b] (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
+ U.itlist (fn (b as (r1,r2)) => fn thm =>
+ EXISTS(?r2(subst_free[b]
+ (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
thm)
blist' th
end;
@@ -389,10 +388,10 @@
* fun IT_EXISTS blist th =
* let val {sign,...} = rep_thm th
* val tych = cterm_of sign
- * fun detype (x |-> y) = ((#t o rep_cterm) x |-> (#t o rep_cterm) y)
+ * fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
* in
- * fold (fn (b as (r1|->r2), thm) =>
- * EXISTS(D.mk_exists(r2, tych(S.subst[detype b](#t(rep_cterm(cconcl thm))))),
+ * fold (fn (b as (r1,r2), thm) =>
+ * EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
* r1) thm) blist th
* end;
*---------------------------------------------------------------------------*)
@@ -692,9 +691,8 @@
(ListPair.zip (vlist, args)))
"assertion failed in CONTEXT_REWRITE_RULE"
(* val fbvs1 = variants (S.free_vars imp) fbvs *)
- val imp_body1 = S.subst (map (op|->)
- (ListPair.zip (args, vstrl)))
- imp_body
+ val imp_body1 = subst_free (ListPair.zip (args, vstrl))
+ imp_body
val tych = cterm_of sign
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
--- a/TFL/rules.sig Tue May 27 13:03:41 1997 +0200
+++ b/TFL/rules.sig Tue May 27 13:22:30 1997 +0200
@@ -9,8 +9,6 @@
signature Rules_sig =
sig
(* structure USyntax : USyntax_sig *)
- type 'a binding
-
val dest_thm : thm -> term list * term
(* Inference rules *)
@@ -23,7 +21,7 @@
val CONJUNCTS :thm -> thm list
val DISCH :cterm -> thm -> thm
val UNDISCH :thm -> thm
- val INST_TYPE :typ binding list -> 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
@@ -42,7 +40,7 @@
val CHOOSE : cterm * thm -> thm -> thm
val EXISTS : cterm * cterm -> thm -> thm
val EXISTL : cterm list -> thm -> thm
- val IT_EXISTS : cterm binding 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
--- a/TFL/sys.sml Tue May 27 13:03:41 1997 +0200
+++ b/TFL/sys.sml Tue May 27 13:22:30 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: TFL/mask
+(* Title: TFL/sys
ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
@@ -8,8 +8,6 @@
(* Portability stuff *)
nonfix prefix;
-use"mask.sig";
-use"mask.sml";
(* Establish a base of common and/or helpful functions. *)
use "utils.sig";
--- a/TFL/tfl.sml Tue May 27 13:03:41 1997 +0200
+++ b/TFL/tfl.sml Tue May 27 13:22:30 1997 +0200
@@ -8,9 +8,7 @@
functor TFL(structure Rules : Rules_sig
structure Thry : Thry_sig
- structure Thms : Thms_sig
- sharing type Rules.binding = Thry.binding =
- Thry.USyntax.binding = Mask.binding) : TFL_sig =
+ structure Thms : Thms_sig) : TFL_sig =
struct
(* Declarations *)
@@ -25,14 +23,10 @@
structure S = USyntax;
structure U = S.Utils;
-(* Declares 'a binding datatype *)
-open Mask;
-
-nonfix mem --> |->;
+nonfix mem -->;
val --> = S.-->;
infixr 3 -->;
-infixr 7 |->;
val concl = #2 o R.dest_thm;
val hyp = #1 o R.dest_thm;
@@ -118,8 +112,8 @@
datatype pattern = GIVEN of term * int
| OMITTED of term * int
-fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
- | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
+fun psubst theta (GIVEN (tm,i)) = GIVEN(subst_free theta tm, i)
+ | psubst theta (OMITTED (tm,i)) = OMITTED(subst_free theta tm, i);
fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
| dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
@@ -217,7 +211,7 @@
then let val fresh = fresh_constr ty_match ty fresh_var
fun expnd (c,gvs) =
let val capp = list_comb(c,gvs)
- in ((prefix, capp::rst), psubst[p |-> capp] rhs)
+ in ((prefix, capp::rst), psubst[(p,capp)] rhs)
end
in map expnd (map fresh constructors) end
else [row]
@@ -235,7 +229,7 @@
val col0 = map(hd o #2) pat_rectangle
in
if (forall is_Free col0)
- then let val rights' = map (fn(v,e) => psubst[v|->u] e)
+ then let val rights' = map (fn(v,e) => psubst[(v,u)] e)
(ListPair.zip (col0, rights))
val pat_rectangle' = map v_to_prefix pat_rectangle
val (pref_patl,tm) = mk{path = rstp,
@@ -330,7 +324,7 @@
of [] => ()
| L => mk_functional_err("The following rows (counting from zero)\
\ are inaccessible: "^stringize L)
- val case_tm' = S.subst [f |-> fvar] case_tm
+ val case_tm' = subst_free [(f,fvar)] case_tm
in {functional = S.list_mk_abs ([fvar,a], case_tm'),
pats = patts2}
end end;
@@ -497,7 +491,7 @@
val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
val R'abs = S.rand R'
val (def,theory) = Thry.make_definition thy (Name ^ "_def")
- (S.subst[R1 |-> R'] proto_def)
+ (subst_free[(R1,R')] proto_def)
val fconst = #lhs(S.dest_eq(concl def))
val tych = Thry.typecheck theory
val baz = R.DISCH (tych proto_def)
@@ -571,7 +565,7 @@
let
val divide = ipartition (gvvariant FV)
val tych = Thry.typecheck thy
- fun tych_binding(x|->y) = (tych x |-> tych y)
+ fun tych_binding(x,y) = (tych x, tych y)
fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
fun mk{rows=[],...} = fail"no rows"
| mk{path=[], rows = [([], (thm, bindings))]} =
@@ -582,7 +576,7 @@
val pat_rectangle' = map tl pat_rectangle
in
if (forall is_Free col0) (* column 0 is all variables *)
- then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
+ then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
(ListPair.zip (rights, col0))
in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
end
--- a/TFL/thry.sig Tue May 27 13:03:41 1997 +0200
+++ b/TFL/thry.sig Tue May 27 13:22:30 1997 +0200
@@ -6,13 +6,11 @@
signature Thry_sig =
sig
- type 'a binding
-
structure USyntax : USyntax_sig
val match_term : theory -> term -> term
- -> term binding list * typ binding list
+ -> (term*term)list * (typ*typ)list
- val match_type : theory -> typ -> typ -> typ binding list
+ val match_type : theory -> typ -> typ -> (typ*typ)list
val typecheck : theory -> term -> cterm
--- a/TFL/thry.sml Tue May 27 13:03:41 1997 +0200
+++ b/TFL/thry.sml Tue May 27 13:22:30 1997 +0200
@@ -8,21 +8,16 @@
struct
structure USyntax = USyntax;
-
-open Mask;
structure S = USyntax;
-
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
(*---------------------------------------------------------------------------
* Matching
*---------------------------------------------------------------------------*)
-local open Utils
- infix 3 |->
- fun tybind (x,y) = TVar (x,["term"]) |-> y
- fun tmbind (x,y) = Var (x,type_of y) |-> y
+local fun tybind (x,y) = (TVar (x,["term"]) , y)
+ fun tmbind (x,y) = (Var (x,type_of y), y)
in
fun match_term thry pat ob =
let val tsig = #tsig(Sign.rep_sg(sign_of thry))
--- a/TFL/usyntax.sig Tue May 27 13:03:41 1997 +0200
+++ b/TFL/usyntax.sig Tue May 27 13:22:30 1997 +0200
@@ -10,8 +10,6 @@
sig
structure Utils : Utils_sig
- type 'a binding
-
datatype lambda = VAR of {Name : string, Ty : typ}
| CONST of {Name : string, Ty : typ}
| COMB of {Rator: term, Rand : term}
@@ -28,7 +26,6 @@
val --> : typ * typ -> typ
val strip_type : typ -> typ list * typ
val strip_prod_type : typ -> typ list
- val match_type: typ -> typ -> typ binding list
(* Terms *)
val free_vars : term -> term list
@@ -42,8 +39,7 @@
(* Prelogic *)
val aconv : term -> term -> bool
- val subst : term binding list -> term -> term
- val inst : typ binding list -> term -> term
+ val inst : (typ*typ) list -> term -> term
val beta_conv : term -> term
(* Construction routines *)
--- a/TFL/usyntax.sml Tue May 27 13:03:41 1997 +0200
+++ b/TFL/usyntax.sml Tue May 27 13:22:30 1997 +0200
@@ -11,12 +11,10 @@
structure Utils = Utils;
open Utils;
-open Mask;
-infix 7 |->;
infix 4 ##;
-fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
+fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
(*---------------------------------------------------------------------------
@@ -29,7 +27,7 @@
(* But internally, it's useful *)
fun dest_vtype (TVar x) = x
- | dest_vtype _ = raise ERR{func = "dest_vtype",
+ | dest_vtype _ = raise USYN_ERR{func = "dest_vtype",
mesg = "not a flexible type variable"};
val is_vartype = Utils.can dest_vtype;
@@ -41,7 +39,6 @@
val alpha = mk_vartype "'a"
val beta = mk_vartype "'b"
-fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
(* What nonsense *)
@@ -102,13 +99,11 @@
(* Prelogic *)
-val subst = subst_free o map (fn (a |-> b) => (a,b));
-
-fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty)
+fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
fun inst theta = subst_vars (map dest_tybinding theta,[])
fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
- | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"};
+ | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"};
(* Construction routines *)
@@ -119,7 +114,7 @@
local fun var_name(Var((Name,_),_)) = Name
| var_name(Free(s,_)) = s
- | var_name _ = raise ERR{func = "variant",
+ | var_name _ = raise USYN_ERR{func = "variant",
mesg = "list elem. is not a variable"}
in
fun variant [] v = v
@@ -127,7 +122,7 @@
Var((string_variant (map var_name vlist) Name,i),ty)
| variant vlist (Free(Name,ty)) =
Free(string_variant (map var_name vlist) Name,ty)
- | variant _ _ = raise ERR{func = "variant",
+ | variant _ _ = raise USYN_ERR{func = "variant",
mesg = "2nd arg. should be a variable"}
end;
@@ -136,7 +131,7 @@
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
| mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
- | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
+ | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
fun mk_imp{ant,conseq} =
@@ -179,7 +174,7 @@
fun mk_uncurry(xt,yt,zt) =
mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt}
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
- | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}
+ | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}
fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
in
fun mk_pabs{varstruct,body} =
@@ -192,7 +187,7 @@
end
in mpa(varstruct,body)
end
- handle _ => raise ERR{func = "mk_pabs", mesg = ""};
+ handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""};
end;
(* Destruction routines *)
@@ -210,43 +205,43 @@
| dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty}
in LAMB{Bvar = v, Body = betapply (M,v)}
end
- | dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"};
+ | dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"};
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
- | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
+ | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"};
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
- | dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"};
+ | dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
fun dest_abs(a as Abs(s,ty,M)) =
let val v = mk_var{Name = s, Ty = ty}
in {Bvar = v, Body = betapply (a,v)}
end
- | dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"};
+ | dest_abs _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
- | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};
+ | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
- | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};
+ | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a
- | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};
+ | dest_select _ = raise USYN_ERR{func = "dest_select", mesg = "not a select"};
fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
- | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};
+ | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
- | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};
+ | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
fun dest_neg(Const("not",_) $ M) = M
- | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};
+ | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"};
fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
- | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};
+ | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"};
fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
- | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};
+ | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"};
fun mk_pair{fst,snd} =
let val ty1 = type_of fst
@@ -256,7 +251,7 @@
end;
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
- | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
+ | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"};
local fun ucheck t = (if #Name(dest_const t) = "split" then t
@@ -404,7 +399,7 @@
then find (#Body(dest_abs tm))
else let val {Rator,Rand} = dest_comb tm
in find Rator handle _ => find Rand
- end handle _ => raise ERR{func = "find_term",mesg = ""}
+ end handle _ => raise USYN_ERR{func = "find_term",mesg = ""}
in find
end;
@@ -431,9 +426,9 @@
if (type_of tm = HOLogic.boolT)
then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
in (R,y,x)
- end handle _ => raise ERR{func="dest_relation",
+ end handle _ => raise USYN_ERR{func="dest_relation",
mesg="unexpected term structure"}
- else raise ERR{func="dest_relation",mesg="not a boolean term"};
+ else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;