src/Pure/IsaPlanner/term_lib.ML
author wenzelm
Thu Jul 28 15:19:49 2005 +0200 (2005-07-28)
changeset 16934 9ef19e3c7fdd
parent 16857 6389511d4609
child 17203 29b2563f5c11
permissions -rw-r--r--
Sign.typ_unify;
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Pure/IsaPlanner/term_lib.ML
     3     ID:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucasd@dai.ed.ac.uk
     6     Created:    17 Aug 2002
     7 *)
     8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     9 (*  DESCRIPTION:
    10 
    11     Additional code to work with terms.
    12 
    13 *)   
    14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    15 signature TERM_LIB =
    16 sig
    17     val fo_term_height : Term.term -> int
    18     val ho_term_height : Term.term -> int
    19 
    20     val current_sign : unit -> Sign.sg
    21 
    22     (* Matching/unification with exceptions handled *)
    23     val clean_match : Type.tsig -> Term.term * Term.term 
    24                       -> ((Term.indexname * (Term.sort * Term.typ)) list 
    25                          * (Term.indexname * (Term.typ * Term.term)) list) option
    26     val clean_unify : Sign.sg -> int -> Term.term * Term.term 
    27                       -> ((Term.indexname * (Term.sort * Term.typ)) list 
    28                          * (Term.indexname * (Term.typ * Term.term)) list) Seq.seq
    29 
    30     (* managing variables in terms, can doing conversions *)
    31     val bounds_to_frees : Term.term -> Term.term
    32     val bounds_to_frees_with_vars :
    33        (string * Term.typ) list -> Term.term -> Term.term
    34 
    35     val change_bounds_to_frees : Term.term -> Term.term
    36     val change_frees_to_vars : Term.term -> Term.term
    37     val change_vars_to_frees : Term.term -> Term.term
    38     val loose_bnds_to_frees :
    39        (string * Term.typ) list -> Term.term -> Term.term
    40 
    41     (* make all variables named uniquely *)
    42     val unique_namify : Term.term -> Term.term
    43 
    44 		(* breasking up a term and putting it into a normal form 
    45        independent of internal term context *)
    46     val cleaned_term_conc : Term.term -> Term.term
    47     val cleaned_term_parts : Term.term -> Term.term list * Term.term
    48     val cterm_of_term : Term.term -> Thm.cterm
    49 
    50     (* terms of theorems and subgoals *)
    51     val term_of_thm : Thm.thm -> Term.term
    52     val get_prems_of_sg_term : Term.term -> Term.term list
    53     val triv_thm_from_string : string -> Thm.thm
    54 
    55     (* some common term manipulations *)
    56     val try_dest_Goal : Term.term -> Term.term
    57     val try_dest_Trueprop : Term.term -> Term.term
    58 
    59     val bot_left_leaf_of : Term.term -> Term.term
    60     val bot_left_leaf_noabs_of : Term.term -> Term.term
    61 
    62     (* term containing another term - an embedding check *)
    63     val term_contains : Term.term -> Term.term -> bool
    64 
    65     (* name-convertable checking - like ae-convertable, but allows for
    66        var's and free's to be mixed - and doesn't used buggy code. :-) *)
    67 		val get_name_eq_member : Term.term -> Term.term list -> Term.term option
    68     val name_eq_member : Term.term -> Term.term list -> bool
    69     val term_name_eq :
    70        Term.term ->
    71        Term.term ->
    72        (Term.term * Term.term) list ->
    73        (Term.term * Term.term) list option
    74 
    75      (* is the typ a function or is it atomic *)
    76      val is_fun_typ : Term.typ -> bool
    77      val is_atomic_typ : Term.typ -> bool
    78 
    79     (* variable analysis *)
    80     val is_some_kind_of_var : Term.term -> bool
    81     val same_var_check :
    82        ''a -> ''b -> (''a * ''b) list -> (''a * ''b) list option
    83 		val has_new_vars : Term.term * Term.term -> bool
    84     val has_new_typ_vars : Term.term * Term.term -> bool
    85    (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
    86     val is_not_valid_rwrule : Type.tsig -> (Term.term * Term.term) -> bool
    87 
    88     (* get the frees in a term that are of atomic type, ie non-functions *)
    89     val atomic_frees_of_term : Term.term -> (string * Term.typ) list
    90 
    91     (* get used names in a theorem to avoid upon instantiation. *)
    92     val usednames_of_term : Term.term -> string list
    93     val usednames_of_thm : Thm.thm -> string list
    94 
    95     (* Isar term skolemisationm and unsolemisation *)
    96     (* I think this is written also in IsarRTechn and also in somewhere else *)
    97     (* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term *)
    98     val unskolemise_all_term : 
    99         Term.term -> 
   100         (((string * Term.typ) * string) list * Term.term)
   101 
   102     (* given a string describing term then a string for its type, returns 
   103        read term *)
   104     val readwty : string -> string -> Term.term
   105 
   106     (* pretty stuff *)
   107     val print_term : Term.term -> unit
   108     val pretty_print_sort : string list -> string
   109     val pretty_print_term : Term.term -> string
   110     val pretty_print_type : Term.typ -> string
   111     val pretty_print_typelist :
   112        Term.typ list -> (Term.typ -> string) -> string
   113  
   114     (* for debugging: quickly get a string of a term w.r.t the_context() *)
   115     val string_of_term : Term.term -> string
   116 
   117     (* Pretty printing in a way that allows them to be parsed by ML.
   118        these are perhaps redundent, check the standard basis 
   119        lib for generic versions for any datatype? *)
   120     val writesort : string list -> unit
   121     val writeterm : Term.term -> unit
   122     val writetype : Term.typ -> unit
   123   end
   124 
   125 
   126 structure TermLib : TERM_LIB = 
   127 struct
   128 
   129 (* Two kinds of depth measure for HOAS terms, a first order (flat) and a 
   130    higher order one. 
   131    Note: not stable of eta-contraction: embedding eta-expands term, 
   132    thus we assume eta-expanded *)
   133 fun fo_term_height (a $ b) = 
   134     IsaPLib.max (1 + fo_term_height b, (fo_term_height a))
   135   | fo_term_height (Abs(_,_,t)) = fo_term_height t
   136   | fo_term_height _ = 0;
   137     
   138 fun ho_term_height  (a $ b) = 
   139     1 + (IsaPLib.max (ho_term_height b, ho_term_height a))
   140   | ho_term_height (Abs(_,_,t)) = ho_term_height t
   141   | ho_term_height _ = 0;
   142 
   143 
   144 (* Higher order matching with exception handled *)
   145 (* returns optional instantiation *)
   146 fun clean_match tsig (a as (pat, t)) = 
   147   let val (tyenv, tenv) = Pattern.match tsig a
   148   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   149   end handle Pattern.MATCH => NONE;
   150 (* Higher order unification with exception handled, return the instantiations *)
   151 (* given Signature, max var index, pat, tgt *)
   152 (* returns Seq of instantiations *)
   153 fun clean_unify sgn ix (a as (pat, tgt)) = 
   154     let 
   155       (* type info will be re-derived, maybe this can be cached 
   156          for efficiency? *)
   157       val pat_ty = Term.type_of pat;
   158       val tgt_ty = Term.type_of tgt;
   159       (* is it OK to ignore the type instantiation info? 
   160          or should I be using it? *)
   161       val typs_unify = 
   162           SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
   163             handle Type.TUNIFY => NONE;
   164     in
   165       case typs_unify of
   166         SOME (typinsttab, ix2) =>
   167         let 
   168       (* is it right to throw away the flexes? 
   169          or should I be using them somehow? *)
   170           fun mk_insts env = 
   171             (Vartab.dest (Envir.type_env env),
   172              Envir.alist_of env);
   173           val initenv = Envir.Envir {asol = Vartab.empty, 
   174                                      iTs = typinsttab, maxidx = ix2};
   175           val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
   176 	            handle UnequalLengths => Seq.empty
   177 		               | Term.TERM _ => Seq.empty;
   178           fun clean_unify' useq () = 
   179               (case (Seq.pull useq) of 
   180                  NONE => NONE
   181                | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   182 	      handle UnequalLengths => NONE
   183                    | Term.TERM _ => NONE;
   184         in
   185           (Seq.make (clean_unify' useq))
   186         end
   187       | NONE => Seq.empty
   188     end;
   189 
   190 fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t));
   191 fun asm_read s = 
   192     (Thm.assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT)));
   193 
   194 
   195 (* more pretty printing code for Isabelle terms etc *)
   196 
   197 
   198 (* pretty_print_typelist l f = print a typelist. 
   199    l = list of types to print : typ list
   200    f = function used to print a single type : typ -> string
   201 *)
   202 fun pretty_print_typelist [] f = ""
   203   | pretty_print_typelist [(h: typ)] (f : typ -> string) = (f h)
   204   | pretty_print_typelist ((h: typ) :: t) (f : typ -> string) = 
   205       (f h) ^ ", " ^ (pretty_print_typelist t f);
   206 
   207 
   208 
   209 (* pretty_print_sort s = print a sort 
   210    s = sort to print : string list
   211 *)
   212 fun pretty_print_sort [] = ""
   213   | pretty_print_sort ([h])  = "\"" ^ h ^ "\""
   214   | pretty_print_sort (h :: t)  = "\"" ^ h ^ "\"," ^ (pretty_print_sort t);
   215 
   216 
   217 (* pretty_print_type t = print a type
   218    t = type to print : type
   219 *)
   220 fun pretty_print_type (Type (n, l)) = 
   221       "Type(\"" ^ n ^ "\", [" ^ (pretty_print_typelist l pretty_print_type) ^ "])"
   222   | pretty_print_type (TFree (n, s)) = 
   223       "TFree(\"" ^ n ^ "\", [" ^ (pretty_print_sort s) ^ "])"
   224   | pretty_print_type (TVar ((n, i), s)) = 
   225       "TVar( (\"" ^ n ^ "\", " ^ (string_of_int i) ^ "), [" ^ (pretty_print_sort s) ^ "])";
   226 
   227 
   228 (* pretty_print_term t = print a term prints types and sorts too.
   229    t = term to print : term
   230 *)
   231 fun pretty_print_term (Const (s, t)) = 
   232       "Const(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
   233   | pretty_print_term (Free (s, t)) = 
   234       "Free(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
   235   | pretty_print_term (Var ((n, i), t)) = 
   236       "Var( (\"" ^ n ^ "\"," ^ (string_of_int i) ^ "), " ^ (pretty_print_type t) ^ ")"
   237   | pretty_print_term (Bound i) = 
   238       "Bound(" ^ (string_of_int i) ^ ")"
   239   | pretty_print_term (Abs (s, t, r)) = 
   240       "Abs(\"" ^ s ^ "\"," ^ (pretty_print_type t) ^ ", \n  " ^ (pretty_print_term r) ^ ")"
   241   | pretty_print_term (op $ (t1, t2)) = 
   242       "(" ^ (pretty_print_term t1) ^ ") $\n (" ^ (pretty_print_term t2) ^ ")";
   243 
   244 (* Write the term out nicly instead of just creating a string for it *)
   245 fun writeterm t = writeln (pretty_print_term t);
   246 fun writetype t = writeln (pretty_print_type t);
   247 fun writesort s = writeln (pretty_print_sort s);
   248 
   249 fun current_sign () = Theory.sign_of (the_context());
   250 fun cterm_of_term (t : term) = Thm.cterm_of (current_sign()) t;
   251 fun term_of_thm t = (Thm.prop_of t);
   252 
   253 fun string_of_term t =
   254   (Sign.string_of_term (current_sign()) t);
   255 fun print_term t = writeln (string_of_term t);
   256 
   257 (* create a trivial HOL thm from anything... *)
   258 fun triv_thm_from_string s = 
   259   Thm.trivial (cterm_of (current_sign()) (read s));
   260 
   261   (* Checks if vars could be the same - alpha convertable
   262   w.r.t. previous vars, a and b are assumed to be vars,
   263   free vars, but not bound vars,
   264   Note frees and vars must all have unique names. *)
   265   fun same_var_check a b L =
   266   let 
   267     fun bterm_from t [] = NONE
   268       | bterm_from t ((a,b)::m) = 
   269           if t = a then SOME b else bterm_from t m
   270 
   271     val bl_opt = bterm_from a L
   272   in
   273 		case bterm_from a L of
   274 			NONE => SOME ((a,b)::L)
   275 		| SOME b2 => if b2 = b then SOME L else NONE
   276   end;
   277 
   278   (* FIXME: make more efficient, only require a single new var! *)
   279   (* check if the new term has any meta variables not in the old term *)
   280   fun has_new_vars (old, new) = 
   281 			(case IsaPLib.lrem (op =) (Term.term_vars old) (Term.term_vars new) of 
   282 				 [] => false
   283 			 | (_::_) => true);
   284   (* check if the new term has any meta variables not in the old term *)
   285   fun has_new_typ_vars (old, new) = 
   286 			(case IsaPLib.lrem (op =) (Term.term_tvars old) (Term.term_tvars new) of 
   287 				 [] => false
   288 			 | (_::_) => true);
   289 
   290 (* This version avoids name conflicts that might be introduced by
   291 unskolemisation, and returns a list of (string * Term.typ) * string,
   292 where the outer string is the original name, and the inner string is
   293 the new name, and the type is the type of the free variable that was
   294 renamed. *)
   295 local
   296   fun myadd (n,ty) (L as (renames, names)) = 
   297       let val n' = Syntax.dest_skolem n in 
   298         case (Library.find_first (fn (_,n2) => (n2 = n)) renames) of 
   299           NONE => 
   300           let val renamedn = Term.variant names n' in 
   301             (renamedn, (((renamedn, ty), n) :: renames, 
   302                         renamedn :: names)) end
   303         | (SOME ((renamedn, _), _)) => (renamedn, L)
   304       end
   305       handle Fail _ => (n, L);
   306 
   307   fun unsk (L,f) (t1 $ t2) = 
   308       let val (L', t1') = unsk (L, I) t1 
   309       in unsk (L', (fn x => f (t1' $ x))) t2 end
   310     | unsk (L,f) (Abs(n,ty,t)) = 
   311       unsk (L, (fn x => Abs(n,ty,x))) t
   312     | unsk (L, f) (Free (n,ty)) = 
   313       let val (renamed_n, L') = myadd (n ,ty) L
   314        in (L', f (Free (renamed_n, ty))) end
   315     | unsk (L, f) l = (L, f l);
   316 in
   317 fun unskolemise_all_term t = 
   318     let 
   319       val names = Term.add_term_names (t,[]) 
   320       val ((renames,names'),t') = unsk (([], names),I) t
   321     in (renames,t') end;
   322 end
   323 
   324 (* true if the type t is a function *)
   325 fun is_fun_typ (Type(s, l)) = 
   326     if s = "fun" then true else false
   327   | is_fun_typ _ = false;
   328 
   329 val is_atomic_typ = not o is_fun_typ;
   330 
   331 (* get the frees in a term that are of atomic type, ie non-functions *)
   332 val atomic_frees_of_term =
   333      List.filter (is_atomic_typ o snd) 
   334      o map Term.dest_Free 
   335      o Term.term_frees;
   336 
   337 fun usednames_of_term t = Term.add_term_names (t,[]);
   338 fun usednames_of_thm th = 
   339     let val rep = Thm.rep_thm th
   340       val hyps = #hyps rep
   341       val (tpairl,tpairr) = Library.split_list (#tpairs rep)
   342       val prop = #prop rep 
   343     in
   344       List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
   345     end;
   346 
   347 (* read in a string and a top-level type and this will give back a term *) 
   348 fun readwty tstr tystr = 
   349     let 
   350       val sgn = Theory.sign_of (the_context())
   351     in
   352       Sign.simple_read_term sgn (Sign.read_typ (sgn, K NONE) tystr) tstr
   353     end;
   354 
   355 
   356   (* first term is equal to the second in some name convertable
   357   way... Note: This differs from the aeconv in the Term.ML file of
   358   Isabelle in that it allows a var to be alpha-equiv to a free var. 
   359   
   360   Also, the isabelle term.ML version of aeconv uses a
   361   function that it claims doesn't work! *)
   362   fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l = 
   363     if ty1 = ty2 then term_name_eq t1 t2 l
   364     else NONE
   365   | term_name_eq (ah $ at) (bh $ bt) l =
   366     let 
   367       val lopt = (term_name_eq ah bh l)
   368     in
   369       if isSome lopt then 
   370 	      term_name_eq at bt (valOf lopt)
   371       else
   372         NONE
   373     end
   374   | term_name_eq (Const(a,T)) (Const(b,U)) l = 
   375     if a=b andalso T=U then SOME l
   376     else NONE
   377   | term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l = 
   378     same_var_check a b l
   379   | term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l = 
   380     same_var_check a b l
   381   | term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l = 
   382     same_var_check a b l
   383   | term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l = 
   384     same_var_check a b l
   385   | term_name_eq (Bound i) (Bound j) l = 
   386     if i = j then SOME l else NONE
   387   | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE);
   388 
   389  (* checks to see if the term in a name-equivalent member of the list of terms. *)
   390   fun get_name_eq_member a [] = NONE
   391     | get_name_eq_member a (h :: t) = 
   392         if isSome (term_name_eq a h []) then SOME h 
   393 				else get_name_eq_member a t;
   394 
   395   fun name_eq_member a [] = false
   396     | name_eq_member a (h :: t) = 
   397         if isSome (term_name_eq a h []) then true 
   398 				else name_eq_member a t;
   399 
   400   (* true if term is a variable *)
   401   fun is_some_kind_of_var (Free(s, ty)) = true
   402     | is_some_kind_of_var (Var(i, ty)) = true
   403     | is_some_kind_of_var (Bound(i)) = true
   404     | is_some_kind_of_var _ = false;
   405 
   406     (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
   407 (* FIXME: we should really check that there is a subterm on the lhs
   408 which embeds into the rhs, this would be much closer to the normal
   409 notion of valid wave rule - ie there exists at least one case where it
   410 is a valid wave rule... *)
   411 	fun is_not_valid_rwrule tysig (lhs, rhs) = 
   412       Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *)
   413       orelse has_new_vars (lhs,rhs) 
   414       orelse has_new_typ_vars (lhs,rhs) 
   415       orelse Pattern.matches_subterm tysig (lhs, rhs);
   416 
   417 
   418   (* first term contains the second in some name convertable way... *)
   419   (* note: this is equivalent to an alpha-convertable emedding *)
   420   (* takes as args: term containing a, term contained b,
   421      (bound vars of a, bound vars of b), 
   422      current alpha-conversion-pairs, 
   423      returns: bool:can convert, new alpha-conversion table *)
   424   (* in bellow: we *don't* use: a loose notion that only requires
   425   variables to match variables, and doesn't worry about the actual
   426   pattern in the variables. *)
   427   fun term_contains1 (Bs, FVs) (Abs(s,ty,t)) (Abs(s2,ty2,t2)) = 
   428 			if ty = ty2 then 
   429 				term_contains1 ((SOME(s,s2,ty)::Bs), FVs) t t2
   430 			else []
   431 
   432   | term_contains1 T t1 (Abs(s2,ty2,t2)) = []
   433 
   434   | term_contains1 (Bs, FVs) (Abs(s,ty,t)) t2 = 
   435     term_contains1 (NONE::Bs, FVs) t t2
   436 
   437   | term_contains1 T (ah $ at) (bh $ bt) =
   438     (term_contains1 T ah (bh $ bt)) @ 
   439     (term_contains1 T at (bh $ bt)) @
   440     (List.concat (map (fn inT => (term_contains1 inT at bt)) 
   441                (term_contains1 T ah bh)))
   442 
   443   | term_contains1 T a (bh $ bt) = []
   444 
   445   | term_contains1 T (ah $ at) b =
   446 		(term_contains1 T ah b) @ (term_contains1 T at b)
   447 
   448   | term_contains1 T a b = 
   449   (* simple list table lookup to check if a named variable has been
   450   mapped to a variable, if not adds the mapping and return some new
   451   list mapping, if it is then it checks that the pair are mapped to
   452   each other, if so returns the current mapping list, else none. *)
   453 		let 
   454 			fun bterm_from t [] = NONE
   455 				| bterm_from t ((a,b)::m) = 
   456 					if t = a then SOME b else bterm_from t m
   457 
   458   (* check to see if, w.r.t. the variable mapping, two terms are leaf
   459   terms and are mapped to each other. Note constants are only mapped
   460   to the same constant. *) 
   461 			fun same_leaf_check (T as (Bs,FVs)) (Bound i) (Bound j) =
   462 					let 
   463 						fun aux_chk (i1,i2) [] = false
   464 							| aux_chk (0,0) ((SOME _) :: bnds) = true
   465 							| aux_chk (i1,0) (NONE :: bnds) = false
   466 							| aux_chk (i1,i2) ((SOME _) :: bnds) =
   467 								aux_chk (i1 - 1,i2 - 1) bnds
   468 							| aux_chk (i1,i2) (NONE :: bnds) =
   469 								aux_chk (i1,i2 - 1) bnds 
   470 					in
   471 						if (aux_chk (i,j) Bs) then [T]
   472 						else []
   473 					end
   474 				| same_leaf_check (T as (Bs,(Fs,Vs))) 
   475                           (a as (Free (an,aty))) 
   476                           (b as (Free (bn,bty))) =
   477 					(case bterm_from an Fs of 
   478 						 SOME b2n => if bn = b2n then [T]
   479 												 else [] (* conflict of var name *)
   480 					 | NONE => [(Bs,((an,bn)::Fs,Vs))])
   481 				| same_leaf_check (T as (Bs,(Fs,Vs))) 
   482                           (a as (Var (an,aty))) 
   483                           (b as (Var (bn,bty))) =
   484 					(case bterm_from an Vs of 
   485 						 SOME b2n => if bn = b2n then [T]
   486 												 else [] (* conflict of var name *)
   487 					 | NONE => [(Bs,(Fs,(an,bn)::Vs))])
   488 				| same_leaf_check T (a as (Const _)) (b as (Const _)) =
   489 					if a = b then [T] else []
   490 				| same_leaf_check T _ _ = []
   491 
   492 		in
   493 			same_leaf_check T a b
   494 		end;
   495 
   496   (* wrapper for term_contains1: checks if the term "a" contains in
   497   some embedded way, (w.r.t. name -convertable) the term "b" *)
   498   fun term_contains a b = 
   499 			case term_contains1 ([],([],[])) a b of
   500 			  (_ :: _) => true
   501 			| [] => false;
   502 
   503   (* change all bound variables to see ones with appropriate name and
   504   type *)
   505   (* naming convention is OK as we use 'variant' from term.ML *)
   506   (* Note "bounds_to_frees" defined below, its better and quicker, but
   507   keeps the quantifiers handing about, and changes all bounds, not
   508   just universally quantified ones. *)
   509   fun change_bounds_to_frees t =  
   510     let 
   511       val vars = strip_all_vars t
   512       val frees_names = map (fn Free(s,n) => s | _ => "") (term_frees t)
   513       val body = strip_all_body t
   514 
   515       fun bnds_to_frees [] _ acc = acc
   516         | bnds_to_frees ((name,ty)::more) names acc = 
   517             let 
   518 	      val new_name = variant names name
   519 	    in
   520 	      bnds_to_frees more (new_name::names) (Free(new_name,ty)::acc)
   521 	    end
   522     in
   523       (subst_bounds ((bnds_to_frees vars frees_names []), body))
   524     end; 
   525 
   526 (* a runtime-quick function which makes sure that every variable has a
   527 unique name *)
   528 fun unique_namify_aux (ntab,(Abs(s,ty,t))) = 
   529     (case (Symtab.lookup (ntab,s)) of
   530        NONE => 
   531        let 
   532 				 val (ntab2,t2) = unique_namify_aux ((Symtab.update ((s,s),ntab)), t)
   533        in
   534 				 (ntab2,Abs(s,ty,t2))
   535        end
   536      | SOME s2 => 
   537        let 
   538 				 val s_new = (Term.variant (Symtab.keys ntab) s)
   539 				 val (ntab2,t2) = 
   540 						 unique_namify_aux ((Symtab.update ((s_new,s_new),ntab)), t)
   541        in
   542 				 (ntab2,Abs(s_new,ty,t2))
   543        end)
   544   | unique_namify_aux (ntab,(a $ b)) = 
   545     let 
   546       val (ntab1,t1) = unique_namify_aux (ntab,a)
   547       val (ntab2,t2) = unique_namify_aux (ntab1,b)		       
   548     in
   549       (ntab2, t1$t2)
   550     end
   551   | unique_namify_aux (nt as (ntab,Const x)) = nt
   552   | unique_namify_aux (nt as (ntab,f as Free (s,ty))) = 
   553     (case (Symtab.lookup (ntab,s)) of
   554        NONE => ((Symtab.update ((s,s),ntab)), f)
   555      | SOME _ => nt)
   556   | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = 
   557     (case (Symtab.lookup (ntab,s)) of
   558        NONE => ((Symtab.update ((s,s),ntab)), v)
   559      | SOME _ => nt)
   560   | unique_namify_aux (nt as (ntab, Bound i)) = nt;
   561 		
   562 fun unique_namify t = 
   563     #2 (unique_namify_aux (Symtab.empty, t));
   564 
   565 (* a runtime-quick function which makes sure that every variable has a
   566 unique name and also changes bound variables to free variables, used
   567 for embedding checks, Note that this is a pretty naughty term
   568 manipulation, which doesn't have necessary relation to the original
   569 sematics of the term. This is really a trick for our embedding code. *)
   570 
   571 fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = 
   572     (case (Symtab.lookup (ntab,s)) of
   573       NONE => 
   574       let 
   575 	val (ntab2,t2) = bounds_to_frees_aux ((s,ty)::T)
   576 				       ((Symtab.update ((s,s),ntab)), t)
   577       in
   578 	(ntab2,Abs(s,ty,t2))
   579       end
   580     | SOME s2 => 
   581       let 
   582 	val s_new = (Term.variant (Symtab.keys ntab) s)
   583 	val (ntab2,t2) = 
   584 	    bounds_to_frees_aux ((s_new,ty)::T) 
   585 			  (Symtab.update (((s_new,s_new),ntab)), t)
   586       in
   587 	(ntab2,Abs(s_new,ty,t2))
   588       end)
   589   | bounds_to_frees_aux T (ntab,(a $ b)) = 
   590     let 
   591       val (ntab1,t1) = bounds_to_frees_aux T (ntab,a)
   592       val (ntab2,t2) = bounds_to_frees_aux T (ntab1,b)		       
   593     in
   594       (ntab2, t1$t2)
   595     end
   596   | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt
   597   | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = 
   598     (case (Symtab.lookup (ntab,s)) of
   599       NONE => ((Symtab.update ((s,s),ntab)), f)
   600     | SOME _ => nt)
   601   | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = 
   602      (case (Symtab.lookup (ntab,s)) of
   603       NONE => ((Symtab.update ((s,s),ntab)), v)
   604     | SOME _ => nt)
   605   | bounds_to_frees_aux T (nt as (ntab, Bound i)) = 
   606     let 
   607       val (s,ty) = List.nth (T,i) 
   608     in
   609       (ntab, Free (s,ty))
   610     end;
   611 
   612 
   613 fun bounds_to_frees t = 
   614     #2 (bounds_to_frees_aux [] (Symtab.empty,t));
   615 
   616 fun bounds_to_frees_with_vars vars t = 
   617     #2 (bounds_to_frees_aux vars (Symtab.empty,t));
   618 
   619 
   620 
   621 (* loose bounds to frees *)
   622 fun loose_bnds_to_frees_aux (bnds,vars) (Abs(s,ty,t)) = 
   623     Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t)
   624   | loose_bnds_to_frees_aux (bnds,vars) (a $ b) = 
   625     (loose_bnds_to_frees_aux (bnds,vars) a) 
   626       $ (loose_bnds_to_frees_aux (bnds,vars) b)
   627   | loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) = 
   628     if (bnds <= i) then Free (List.nth (vars,i - bnds))
   629     else t
   630   | loose_bnds_to_frees_aux (bnds,vars) t = t;
   631 
   632 
   633 fun loose_bnds_to_frees vars t = 
   634     loose_bnds_to_frees_aux (0,vars) t;
   635 
   636 
   637   fun try_dest_Goal (Const("Goal", _) $ T) = T
   638     | try_dest_Goal T = T;
   639 
   640   fun try_dest_Trueprop (Const("Trueprop", _) $ T) = T
   641     | try_dest_Trueprop T = T; 
   642 
   643   fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   644     | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   645     | bot_left_leaf_of x = x;
   646 
   647   fun bot_left_leaf_noabs_of (l $ r) = bot_left_leaf_noabs_of l
   648     | bot_left_leaf_noabs_of x = x;
   649 
   650 (* cleaned up normal form version of the subgoal terms conclusion *)
   651 fun cleaned_term_conc t = 
   652     let
   653       val concl = Logic.strip_imp_concl (change_bounds_to_frees t)
   654     in 
   655       (try_dest_Trueprop (try_dest_Goal concl))
   656     end;
   657 
   658 (*   fun get_prems_of_sg_term t = 
   659 			map opt_dest_Trueprop (Logic.strip_imp_prems t); *)
   660 
   661 fun get_prems_of_sg_term t = 
   662 		map try_dest_Trueprop (Logic.strip_assums_hyp t);
   663 
   664 
   665 (* drop premices, clean bound var stuff, and make a trueprop... *)
   666   fun cleaned_term_parts t = 
   667       let 
   668 				val t2 = (change_bounds_to_frees t)
   669         val concl = Logic.strip_imp_concl t2
   670 				val prems = map try_dest_Trueprop (Logic.strip_imp_prems t2)
   671       in 
   672 				(prems, (try_dest_Trueprop (try_dest_Goal concl)))
   673       end;
   674 
   675   (* change free variables to vars and visa versa *)
   676   (* *** check naming is OK, can we just use the vasr old name? *)
   677   (* *** Check: Logic.varify and Logic.unvarify *)
   678   fun change_vars_to_frees (a$b) = 
   679         (change_vars_to_frees a) $ (change_vars_to_frees b)
   680     | change_vars_to_frees (Abs(s,ty,t)) = 
   681         (Abs(s,Type.varifyT ty,change_vars_to_frees t))
   682     | change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty))
   683     | change_vars_to_frees l = l;
   684 
   685   fun change_frees_to_vars (a$b) = 
   686         (change_frees_to_vars a) $ (change_frees_to_vars b)
   687     | change_frees_to_vars (Abs(s,ty,t)) = 
   688         (Abs(s,Type.varifyT ty,change_frees_to_vars t))
   689     | change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty))
   690     | change_frees_to_vars l = l;
   691 
   692 
   693 end;