23175

1 
(* Title: Tools/IsaPlanner/rw_tools.ML

23171

2 
Author: Lucas Dixon, University of Edinburgh


3 

23175

4 
Term related tools used for rewriting.

23171

5 
*)


6 


7 
signature RWTOOLS =


8 
sig


9 
end;


10 


11 
structure RWTools


12 
= struct


13 


14 
(* fake free variable names for locally bound variables  these work


15 
as placeholders. *)


16 


17 
(* don't use dest_fake..  we should instead be working with numbers


18 
and a list... else we rely on naming conventions which can break, or


19 
be violated  in contrast list locations are correct by


20 
construction/definition. *)


21 
(*


22 
fun dest_fake_bound_name n =


23 
case (explode n) of


24 
(":" :: realchars) => implode realchars


25 
 _ => n; *)


26 
fun is_fake_bound_name n = (hd (explode n) = ":");


27 
fun mk_fake_bound_name n = ":b_" ^ n;


28 


29 


30 


31 
(* fake free variable names for local meta variables  these work


32 
as placeholders. *)


33 
fun dest_fake_fix_name n =


34 
case (explode n) of


35 
("@" :: realchars) => implode realchars


36 
 _ => n;


37 
fun is_fake_fix_name n = (hd (explode n) = "@");


38 
fun mk_fake_fix_name n = "@" ^ n;


39 


40 


41 


42 
(* fake free variable names for meta level bound variables *)


43 
fun dest_fake_all_name n =


44 
case (explode n) of


45 
("+" :: realchars) => implode realchars


46 
 _ => n;


47 
fun is_fake_all_name n = (hd (explode n) = "+");


48 
fun mk_fake_all_name n = "+" ^ n;


49 


50 


51 


52 


53 
(* Ys and Ts not used, Ns are real names of faked local bounds, the


54 
idea is that this will be mapped to free variables thus if a free


55 
variable is a faked local bound then we change it to being a meta


56 
variable so that it can later be instantiated *)


57 
(* FIXME: rename this  avoid the word fix! *)


58 
(* note we are not really "fix"'ing the free, more like making it variable! *)


59 
(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) =


60 
if n mem Ns then Var((n,0),ty) else Free (n,ty);


61 
*)


62 


63 
(* make a var into a fixed free (ie prefixed with "@") *)


64 
fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);


65 


66 


67 
(* mk_frees_bound: string list > Term.term > Term.term *)


68 
(* This function changes free variables to being represented as bound


69 
variables if the free's variable name is in the given list. The debruijn


70 
index is simply the position in the list *)


71 
(* THINKABOUT: danger of an existing free variable with the same name: fix


72 
this so that name conflict are avoided automatically! In the meantime,


73 
don't have free variables named starting with a ":" *)


74 
fun bounds_of_fakefrees Ys (a $ b) =


75 
(bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)


76 
 bounds_of_fakefrees Ys (Abs(n,ty,t)) =


77 
Abs(n,ty, bounds_of_fakefrees (n::Ys) t)


78 
 bounds_of_fakefrees Ys (Free (n,ty)) =


79 
let fun try_mk_bound_of_free (i,[]) = Free (n,ty)


80 
 try_mk_bound_of_free (i,(y::ys)) =


81 
if n = y then Bound i else try_mk_bound_of_free (i+1,ys)


82 
in try_mk_bound_of_free (0,Ys) end


83 
 bounds_of_fakefrees Ys t = t;


84 


85 


86 
(* map a function f onto each free variables *)


87 
fun map_to_frees f Ys (a $ b) =


88 
(map_to_frees f Ys a) $ (map_to_frees f Ys b)


89 
 map_to_frees f Ys (Abs(n,ty,t)) =


90 
Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)


91 
 map_to_frees f Ys (Free a) =


92 
f Ys a


93 
 map_to_frees f Ys t = t;


94 


95 


96 
(* map a function f onto each meta variable *)


97 
fun map_to_vars f Ys (a $ b) =


98 
(map_to_vars f Ys a) $ (map_to_vars f Ys b)


99 
 map_to_vars f Ys (Abs(n,ty,t)) =


100 
Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)


101 
 map_to_vars f Ys (Var a) =


102 
f Ys a


103 
 map_to_vars f Ys t = t;


104 


105 
(* map a function f onto each free variables *)


106 
fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) =


107 
let val (n2,ty2) = f (n,ty)


108 
in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end


109 
 map_to_alls f x = x;


110 


111 
(* map a function f to each type variable in a term *)


112 
(* implicit arg: term *)


113 
fun map_to_term_tvars f =


114 
Term.map_types (fn TVar(ix,ty) => f (ix,ty)  x => x); (* FIXME map_atyps !? *)


115 


116 


117 


118 
(* what if a param desn't occur in the concl? think about! Note: This


119 
simply fixes meta level univ bound vars as Frees. At the end, we will


120 
change them back to schematic vars that will then unify


121 
appropriactely, ie with unfake_vars *)


122 
fun fake_concl_of_goal gt i =


123 
let


124 
val prems = Logic.strip_imp_prems gt


125 
val sgt = List.nth (prems, i  1)


126 


127 
val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)


128 
val tparams = Term.strip_all_vars sgt


129 


130 
val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))


131 
tparams


132 
in


133 
Term.subst_bounds (rev fakefrees,tbody)


134 
end;


135 


136 
(* what if a param desn't occur in the concl? think about! Note: This


137 
simply fixes meta level univ bound vars as Frees. At the end, we will


138 
change them back to schematic vars that will then unify


139 
appropriactely, ie with unfake_vars *)


140 
fun fake_goal gt i =


141 
let


142 
val prems = Logic.strip_imp_prems gt


143 
val sgt = List.nth (prems, i  1)


144 


145 
val tbody = Term.strip_all_body sgt


146 
val tparams = Term.strip_all_vars sgt


147 


148 
val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))


149 
tparams


150 
in


151 
Term.subst_bounds (rev fakefrees,tbody)


152 
end;


153 


154 


155 
(* hand written  for some reason the Isabelle version in drule is broken!


156 
Example? something to do with Bin Yangs examples?


157 
*)


158 
fun rename_term_bvars ns (Abs(s,ty,t)) =


159 
let val s2opt = Library.find_first (fn (x,y) => s = x) ns


160 
in case s2opt of


161 
NONE => (Abs(s,ty,rename_term_bvars ns t))


162 
 SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end


163 
 rename_term_bvars ns (a$b) =


164 
(rename_term_bvars ns a) $ (rename_term_bvars ns b)


165 
 rename_term_bvars _ x = x;


166 


167 
fun rename_thm_bvars ns th =


168 
let val t = Thm.prop_of th


169 
in Thm.rename_boundvars t (rename_term_bvars ns t) th end;


170 


171 
(* Finish this to show how it breaks! (raises the exception):


172 


173 
exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)


174 


175 
Drule.rename_bvars ns th


176 
handle TERM _ => raise rename_thm_bvars_exp (ns, th);


177 
*)


178 


179 
end;
