src/Provers/IsaPlanner/rw_tools.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 20548 8ef25fe585a8
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Pure/IsaPlanner/rw_tools.ML
     3     ID:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucas.dixon@ed.ac.uk
     6     Created:    28 May 2004
     7 *)
     8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     9 (*  DESCRIPTION:
    10 
    11     term related tools used for rewriting
    12 
    13 *)   
    14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    15 
    16 signature RWTOOLS =
    17 sig
    18 end;
    19 
    20 structure RWTools 
    21 = struct
    22 
    23 (* fake free variable names for locally bound variables - these work
    24 as placeholders. *)
    25 
    26 (* don't use dest_fake.. - we should instead be working with numbers
    27 and a list... else we rely on naming conventions which can break, or
    28 be violated - in contrast list locations are correct by
    29 construction/definition. *)
    30 (*
    31 fun dest_fake_bound_name n = 
    32     case (explode n) of 
    33       (":" :: realchars) => implode realchars
    34     | _ => n; *)
    35 fun is_fake_bound_name n = (hd (explode n) = ":");
    36 fun mk_fake_bound_name n = ":b_" ^ n;
    37 
    38 
    39 
    40 (* fake free variable names for local meta variables - these work
    41 as placeholders. *)
    42 fun dest_fake_fix_name n = 
    43     case (explode n) of 
    44       ("@" :: realchars) => implode realchars
    45     | _ => n;
    46 fun is_fake_fix_name n = (hd (explode n) = "@");
    47 fun mk_fake_fix_name n = "@" ^ n;
    48 
    49 
    50 
    51 (* fake free variable names for meta level bound variables *)
    52 fun dest_fake_all_name n = 
    53     case (explode n) of 
    54       ("+" :: realchars) => implode realchars
    55     | _ => n;
    56 fun is_fake_all_name n = (hd (explode n) = "+");
    57 fun mk_fake_all_name n = "+" ^ n;
    58 
    59 
    60 
    61 
    62 (* Ys and Ts not used, Ns are real names of faked local bounds, the
    63 idea is that this will be mapped to free variables thus if a free
    64 variable is a faked local bound then we change it to being a meta
    65 variable so that it can later be instantiated *)
    66 (* FIXME: rename this - avoid the word fix! *)
    67 (* note we are not really "fix"'ing the free, more like making it variable! *)
    68 (* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
    69     if n mem Ns then Var((n,0),ty) else Free (n,ty);
    70 *)
    71 
    72 (* make a var into a fixed free (ie prefixed with "@") *)
    73 fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
    74 
    75 
    76 (* mk_frees_bound: string list -> Term.term -> Term.term *)
    77 (* This function changes free variables to being represented as bound
    78 variables if the free's variable name is in the given list. The debruijn 
    79 index is simply the position in the list *)
    80 (* THINKABOUT: danger of an existing free variable with the same name: fix
    81 this so that name conflict are avoided automatically! In the meantime,
    82 don't have free variables named starting with a ":" *)
    83 fun bounds_of_fakefrees Ys (a $ b) = 
    84     (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
    85   | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
    86     Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
    87   | bounds_of_fakefrees Ys (Free (n,ty)) = 
    88     let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
    89           | try_mk_bound_of_free (i,(y::ys)) = 
    90             if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
    91     in try_mk_bound_of_free (0,Ys) end
    92   | bounds_of_fakefrees Ys t = t;
    93 
    94 
    95 (* map a function f onto each free variables *)
    96 fun map_to_frees f Ys (a $ b) = 
    97     (map_to_frees f Ys a) $ (map_to_frees f Ys b)
    98   | map_to_frees f Ys (Abs(n,ty,t)) = 
    99     Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
   100   | map_to_frees f Ys (Free a) = 
   101     f Ys a
   102   | map_to_frees f Ys t = t;
   103 
   104 
   105 (* map a function f onto each meta variable  *)
   106 fun map_to_vars f Ys (a $ b) = 
   107     (map_to_vars f Ys a) $ (map_to_vars f Ys b)
   108   | map_to_vars f Ys (Abs(n,ty,t)) = 
   109     Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
   110   | map_to_vars f Ys (Var a) = 
   111     f Ys a
   112   | map_to_vars f Ys t = t;
   113 
   114 (* map a function f onto each free variables *)
   115 fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
   116     let val (n2,ty2) = f (n,ty) 
   117     in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
   118   | map_to_alls f x = x;
   119 
   120 (* map a function f to each type variable in a term *)
   121 (* implicit arg: term *)
   122 fun map_to_term_tvars f =
   123     Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
   124 
   125 
   126 
   127 (* what if a param desn't occur in the concl? think about! Note: This
   128 simply fixes meta level univ bound vars as Frees.  At the end, we will
   129 change them back to schematic vars that will then unify
   130 appropriactely, ie with unfake_vars *)
   131 fun fake_concl_of_goal gt i = 
   132     let 
   133       val prems = Logic.strip_imp_prems gt
   134       val sgt = List.nth (prems, i - 1)
   135 
   136       val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   137       val tparams = Term.strip_all_vars sgt
   138 
   139       val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   140                           tparams
   141     in
   142       Term.subst_bounds (rev fakefrees,tbody)
   143     end;
   144 
   145 (* what if a param desn't occur in the concl? think about! Note: This
   146 simply fixes meta level univ bound vars as Frees.  At the end, we will
   147 change them back to schematic vars that will then unify
   148 appropriactely, ie with unfake_vars *)
   149 fun fake_goal gt i = 
   150     let 
   151       val prems = Logic.strip_imp_prems gt
   152       val sgt = List.nth (prems, i - 1)
   153 
   154       val tbody = Term.strip_all_body sgt
   155       val tparams = Term.strip_all_vars sgt
   156 
   157       val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   158                           tparams
   159     in
   160       Term.subst_bounds (rev fakefrees,tbody)
   161     end;
   162 
   163 
   164 (* hand written - for some reason the Isabelle version in drule is broken!
   165 Example? something to do with Bin Yangs examples? 
   166  *)
   167 fun rename_term_bvars ns (Abs(s,ty,t)) = 
   168     let val s2opt = Library.find_first (fn (x,y) => s = x) ns
   169     in case s2opt of 
   170          NONE => (Abs(s,ty,rename_term_bvars  ns t))
   171        | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
   172   | rename_term_bvars ns (a$b) = 
   173     (rename_term_bvars ns a) $ (rename_term_bvars ns b)
   174   | rename_term_bvars _ x = x;
   175 
   176 fun rename_thm_bvars ns th = 
   177     let val t = Thm.prop_of th 
   178     in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
   179 
   180 (* Finish this to show how it breaks! (raises the exception): 
   181 
   182 exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
   183 
   184     Drule.rename_bvars ns th 
   185     handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
   186 *)
   187 
   188 end;