src/Provers/IsaPlanner/rw_tools.ML
changeset 23171 861f63a35d31
parent 23170 94e9413bd7fc
child 23172 f1ae6a8648ef
     1.1 --- a/src/Provers/IsaPlanner/rw_tools.ML	Thu May 31 19:11:19 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,188 +0,0 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/rw_tools.ML
     1.6 -    ID:		$Id$
     1.7 -    Author:     Lucas Dixon, University of Edinburgh
     1.8 -                lucas.dixon@ed.ac.uk
     1.9 -    Created:    28 May 2004
    1.10 -*)
    1.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.12 -(*  DESCRIPTION:
    1.13 -
    1.14 -    term related tools used for rewriting
    1.15 -
    1.16 -*)   
    1.17 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    1.18 -
    1.19 -signature RWTOOLS =
    1.20 -sig
    1.21 -end;
    1.22 -
    1.23 -structure RWTools 
    1.24 -= struct
    1.25 -
    1.26 -(* fake free variable names for locally bound variables - these work
    1.27 -as placeholders. *)
    1.28 -
    1.29 -(* don't use dest_fake.. - we should instead be working with numbers
    1.30 -and a list... else we rely on naming conventions which can break, or
    1.31 -be violated - in contrast list locations are correct by
    1.32 -construction/definition. *)
    1.33 -(*
    1.34 -fun dest_fake_bound_name n = 
    1.35 -    case (explode n) of 
    1.36 -      (":" :: realchars) => implode realchars
    1.37 -    | _ => n; *)
    1.38 -fun is_fake_bound_name n = (hd (explode n) = ":");
    1.39 -fun mk_fake_bound_name n = ":b_" ^ n;
    1.40 -
    1.41 -
    1.42 -
    1.43 -(* fake free variable names for local meta variables - these work
    1.44 -as placeholders. *)
    1.45 -fun dest_fake_fix_name n = 
    1.46 -    case (explode n) of 
    1.47 -      ("@" :: realchars) => implode realchars
    1.48 -    | _ => n;
    1.49 -fun is_fake_fix_name n = (hd (explode n) = "@");
    1.50 -fun mk_fake_fix_name n = "@" ^ n;
    1.51 -
    1.52 -
    1.53 -
    1.54 -(* fake free variable names for meta level bound variables *)
    1.55 -fun dest_fake_all_name n = 
    1.56 -    case (explode n) of 
    1.57 -      ("+" :: realchars) => implode realchars
    1.58 -    | _ => n;
    1.59 -fun is_fake_all_name n = (hd (explode n) = "+");
    1.60 -fun mk_fake_all_name n = "+" ^ n;
    1.61 -
    1.62 -
    1.63 -
    1.64 -
    1.65 -(* Ys and Ts not used, Ns are real names of faked local bounds, the
    1.66 -idea is that this will be mapped to free variables thus if a free
    1.67 -variable is a faked local bound then we change it to being a meta
    1.68 -variable so that it can later be instantiated *)
    1.69 -(* FIXME: rename this - avoid the word fix! *)
    1.70 -(* note we are not really "fix"'ing the free, more like making it variable! *)
    1.71 -(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
    1.72 -    if n mem Ns then Var((n,0),ty) else Free (n,ty);
    1.73 -*)
    1.74 -
    1.75 -(* make a var into a fixed free (ie prefixed with "@") *)
    1.76 -fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
    1.77 -
    1.78 -
    1.79 -(* mk_frees_bound: string list -> Term.term -> Term.term *)
    1.80 -(* This function changes free variables to being represented as bound
    1.81 -variables if the free's variable name is in the given list. The debruijn 
    1.82 -index is simply the position in the list *)
    1.83 -(* THINKABOUT: danger of an existing free variable with the same name: fix
    1.84 -this so that name conflict are avoided automatically! In the meantime,
    1.85 -don't have free variables named starting with a ":" *)
    1.86 -fun bounds_of_fakefrees Ys (a $ b) = 
    1.87 -    (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
    1.88 -  | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
    1.89 -    Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
    1.90 -  | bounds_of_fakefrees Ys (Free (n,ty)) = 
    1.91 -    let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
    1.92 -          | try_mk_bound_of_free (i,(y::ys)) = 
    1.93 -            if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
    1.94 -    in try_mk_bound_of_free (0,Ys) end
    1.95 -  | bounds_of_fakefrees Ys t = t;
    1.96 -
    1.97 -
    1.98 -(* map a function f onto each free variables *)
    1.99 -fun map_to_frees f Ys (a $ b) = 
   1.100 -    (map_to_frees f Ys a) $ (map_to_frees f Ys b)
   1.101 -  | map_to_frees f Ys (Abs(n,ty,t)) = 
   1.102 -    Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
   1.103 -  | map_to_frees f Ys (Free a) = 
   1.104 -    f Ys a
   1.105 -  | map_to_frees f Ys t = t;
   1.106 -
   1.107 -
   1.108 -(* map a function f onto each meta variable  *)
   1.109 -fun map_to_vars f Ys (a $ b) = 
   1.110 -    (map_to_vars f Ys a) $ (map_to_vars f Ys b)
   1.111 -  | map_to_vars f Ys (Abs(n,ty,t)) = 
   1.112 -    Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
   1.113 -  | map_to_vars f Ys (Var a) = 
   1.114 -    f Ys a
   1.115 -  | map_to_vars f Ys t = t;
   1.116 -
   1.117 -(* map a function f onto each free variables *)
   1.118 -fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
   1.119 -    let val (n2,ty2) = f (n,ty) 
   1.120 -    in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
   1.121 -  | map_to_alls f x = x;
   1.122 -
   1.123 -(* map a function f to each type variable in a term *)
   1.124 -(* implicit arg: term *)
   1.125 -fun map_to_term_tvars f =
   1.126 -    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
   1.127 -
   1.128 -
   1.129 -
   1.130 -(* what if a param desn't occur in the concl? think about! Note: This
   1.131 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   1.132 -change them back to schematic vars that will then unify
   1.133 -appropriactely, ie with unfake_vars *)
   1.134 -fun fake_concl_of_goal gt i = 
   1.135 -    let 
   1.136 -      val prems = Logic.strip_imp_prems gt
   1.137 -      val sgt = List.nth (prems, i - 1)
   1.138 -
   1.139 -      val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   1.140 -      val tparams = Term.strip_all_vars sgt
   1.141 -
   1.142 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   1.143 -                          tparams
   1.144 -    in
   1.145 -      Term.subst_bounds (rev fakefrees,tbody)
   1.146 -    end;
   1.147 -
   1.148 -(* what if a param desn't occur in the concl? think about! Note: This
   1.149 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   1.150 -change them back to schematic vars that will then unify
   1.151 -appropriactely, ie with unfake_vars *)
   1.152 -fun fake_goal gt i = 
   1.153 -    let 
   1.154 -      val prems = Logic.strip_imp_prems gt
   1.155 -      val sgt = List.nth (prems, i - 1)
   1.156 -
   1.157 -      val tbody = Term.strip_all_body sgt
   1.158 -      val tparams = Term.strip_all_vars sgt
   1.159 -
   1.160 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   1.161 -                          tparams
   1.162 -    in
   1.163 -      Term.subst_bounds (rev fakefrees,tbody)
   1.164 -    end;
   1.165 -
   1.166 -
   1.167 -(* hand written - for some reason the Isabelle version in drule is broken!
   1.168 -Example? something to do with Bin Yangs examples? 
   1.169 - *)
   1.170 -fun rename_term_bvars ns (Abs(s,ty,t)) = 
   1.171 -    let val s2opt = Library.find_first (fn (x,y) => s = x) ns
   1.172 -    in case s2opt of 
   1.173 -         NONE => (Abs(s,ty,rename_term_bvars  ns t))
   1.174 -       | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
   1.175 -  | rename_term_bvars ns (a$b) = 
   1.176 -    (rename_term_bvars ns a) $ (rename_term_bvars ns b)
   1.177 -  | rename_term_bvars _ x = x;
   1.178 -
   1.179 -fun rename_thm_bvars ns th = 
   1.180 -    let val t = Thm.prop_of th 
   1.181 -    in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
   1.182 -
   1.183 -(* Finish this to show how it breaks! (raises the exception): 
   1.184 -
   1.185 -exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
   1.186 -
   1.187 -    Drule.rename_bvars ns th 
   1.188 -    handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
   1.189 -*)
   1.190 -
   1.191 -end;