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