# HG changeset patch
# User paulson
# Date 864732150 -7200
# Node ID 9112a2efb9a3eeee2a63e4c2f9a1b713c77d0c32
# Parent  04502e5431fb44768c0fda654030afd426f1d0bf
Removal of module Mask and datatype binding with its constructor |->

diff -r 04502e5431fb -r 9112a2efb9a3 TFL/mask.sig
--- 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
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/mask.sml
--- 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;
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/rules.new.sml
--- 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
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/rules.sig
--- 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
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/sys.sml
--- 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";
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/tfl.sml
--- 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
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/thry.sig
--- 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
 
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/thry.sml
--- 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))
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/usyntax.sig
--- 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 *)
diff -r 04502e5431fb -r 9112a2efb9a3 TFL/usyntax.sml
--- 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;