src/Pure/IsaPlanner/term_lib.ML

the new subst tactic, by Lucas Dixon

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  Title:      libs/term_lib.ML
    Author:     Lucas Dixon, University of Edinburgh
                [e-mail]
    Created:    17 Aug 2002
*)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  DESCRIPTION:

    Additional code to work with terms.

*)   
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
signature TERM_LIB =
sig
    val fo_term_height : Term.term -> int
    val ho_term_height : Term.term -> int

    val current_sign : unit -> Sign.sg

    structure fvartabS : TABLE

    (* Matching/unification with exceptions handled *)
    val clean_match : Type.tsig -> Term.term * Term.term 
                      -> ((Term.indexname * Term.typ) list 
                         * (Term.indexname * Term.term) list) Library.option
    val clean_unify : Sign.sg -> int -> Term.term * Term.term 
                      -> ((Term.indexname * Term.typ) list 
                         * (Term.indexname * Term.term) list) Seq.seq

    (* managing variables in terms, can doing conversions *)
    val bounds_to_frees : Term.term -> Term.term
    val bounds_to_frees_with_vars :
       (string * Term.typ) list -> Term.term -> Term.term

    val change_bounds_to_frees : Term.term -> Term.term
    val change_frees_to_vars : Term.term -> Term.term
    val change_vars_to_frees : Term.term -> Term.term
    val loose_bnds_to_frees :
       (string * Term.typ) list -> Term.term -> Term.term

    (* make all variables named uniquely *)
    val unique_namify : Term.term -> Term.term

		(* breasking up a term and putting it into a normal form 
       independent of internal term context *)
    val cleaned_term_conc : Term.term -> Term.term
    val cleaned_term_parts : Term.term -> Term.term list * Term.term
    val cterm_of_term : Term.term -> Thm.cterm

    (* terms of theorems and subgoals *)
    val term_of_thm : Thm.thm -> Term.term
    val get_prems_of_sg_term : Term.term -> Term.term list
    val triv_thm_from_string : string -> Thm.thm
(*    val make_term_into_simp_thm :
       (string * Term.typ) list -> Sign.sg -> Term.term -> Thm.thm
    val thms_of_prems_in_goal : int -> Thm.thm -> Thm.thm list
*)


    (* some common term manipulations *)
    val try_dest_Goal : Term.term -> Term.term
    val try_dest_Trueprop : Term.term -> Term.term

    val bot_left_leaf_of : Term.term -> Term.term

    (* term containing another term - an embedding check *)
    val term_contains : Term.term -> Term.term -> bool

    (* name-convertable checking - like ae-convertable, but allows for
       var's and free's to be mixed - and doesn't used buggy code. :-) *)
		val get_name_eq_member : Term.term -> Term.term list -> Term.term option
    val name_eq_member : Term.term -> Term.term list -> bool
    val term_name_eq :
       Term.term ->
       Term.term ->
       (Term.term * Term.term) list ->
       (Term.term * Term.term) list Library.option

     (* is the typ a function or is it atomic *)
     val is_fun_typ : Term.typ -> bool
     val is_atomic_typ : Term.typ -> bool

    (* variable analysis *)
    val is_some_kind_of_var : Term.term -> bool
    val same_var_check :
       ''a -> ''b -> (''a * ''b) list -> (''a * ''b) list Library.option
		val has_new_vars : Term.term * Term.term -> bool
    val has_new_typ_vars : Term.term * Term.term -> bool
   (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
    val is_not_valid_rwrule : Type.tsig -> (Term.term * Term.term) -> bool

    (* get the frees in a term that are of atomic type, ie non-functions *)
    val atomic_frees_of_term : Term.term -> (string * Term.typ) list

    (* Isar term skolemisationm and unsolemisation *)
    (* I think this is written also in IsarRTechn and also in somewhere else *)
    (* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term
     val unskolemise_term : (string,Term.typ) list -> Term.term -> Term.term *)
    val unskolemise_all_term : 
        Term.term -> 
        (((string * Term.typ) * string) list * Term.term)

    (* given a string describing term then a string for its type, returns 
       read term *)
    val readwty : string -> string -> Term.term

    (* pretty stuff *)
    val pp_term : Term.term -> unit
    val pretty_print_sort : string list -> string
    val pretty_print_term : Term.term -> string
    val pretty_print_type : Term.typ -> string
    val pretty_print_typelist :
       Term.typ list -> (Term.typ -> string) -> string
 
    val string_of_term : Term.term -> string

    (* these are perhaps redundent, check the standard basis 
       lib for generic versions for any datatype? *)
    val writesort : string list -> unit
    val writeterm : Term.term -> unit
    val writetype : Term.typ -> unit
  end


structure TermLib : TERM_LIB = 
struct

(* Two kinds of depth measure for HOAS terms, a first order (flat) and a 
   higher order one. 
   Note: not stable of eta-contraction: embedding eta-expands term, 
   thus we assume eta-expanded *)
fun fo_term_height (a $ b) = 
    IsaPLib.max (1 + fo_term_height b, (fo_term_height a))
  | fo_term_height (Abs(_,_,t)) = fo_term_height t
  | fo_term_height _ = 0;
    
fun ho_term_height  (a $ b) = 
    1 + (IsaPLib.max (ho_term_height b, ho_term_height a))
  | ho_term_height (Abs(_,_,t)) = ho_term_height t
  | ho_term_height _ = 0;

(* Higher order matching with exception handled *)
(* returns optional instantiation *)
fun clean_match tsig (a as (pat, t)) = 
    Some (Pattern.match tsig a) handle Pattern.MATCH => None;
(* Higher order unification with exception handled, return the instantiations *)
(* given Signature, max var index, pat, tgt *)
(* returns Seq of instantiations *)
fun clean_unify sgn ix (a as (pat, tgt)) = 
    let 
      (* type info will be re-derived, maybe this can be cached 
         for efficiency? *)
      val pat_ty = Term.type_of pat;
      val tgt_ty = Term.type_of tgt;
      (* is it OK to ignore the type instantiation info? 
         or should I be using it? *)
      val typs_unify = 
          (Some (Type.unify (Sign.tsig_of sgn) (Term.Vartab.empty, ix) 
                            (pat_ty, tgt_ty)))
          handle Type.TUNIFY => None;
    in
      case typs_unify of
        Some (typinsttab, ix2) =>
        let 
      (* is it right to throw away teh flexes? 
         or should I be using them somehow? *)
          fun mk_insts (env,flexflexes) = 
              (Vartab.dest (Envir.type_env env),  Envir.alist_of env);
          val initenv = Envir.Envir {asol = Vartab.empty, 
                                     iTs = typinsttab, maxidx = ix2};
          val useq = (Unify.unifiers (sgn,initenv,[a]))
              handle Library.LIST _ => Seq.empty
                   | Term.TERM _ => Seq.empty;
          fun clean_unify' useq () = 
              (case (Seq.pull useq) of 
                 None => None
               | Some (h,t) => Some (mk_insts h, Seq.make (clean_unify' t)))
              handle Library.LIST _ => None
                   | Term.TERM _ => None;
        in
          (Seq.make (clean_unify' useq))
        end
      | None => Seq.empty
    end;

fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t));
fun asm_read s = 
    (Thm.assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT)));


(* more pretty printing code for Isabelle terms etc *)


(* pretty_print_typelist l f = print a typelist. 
   l = list of types to print : typ list
   f = function used to print a single type : typ -> string
*)
fun pretty_print_typelist [] f = ""
  | pretty_print_typelist [(h: typ)] (f : typ -> string) = (f h)
  | pretty_print_typelist ((h: typ) :: t) (f : typ -> string) = 
      (f h) ^ ", " ^ (pretty_print_typelist t f);



(* pretty_print_sort s = print a sort 
   s = sort to print : string list
*)
fun pretty_print_sort [] = ""
  | pretty_print_sort ([h])  = "\"" ^ h ^ "\""
  | pretty_print_sort (h :: t)  = "\"" ^ h ^ "\"," ^ (pretty_print_sort t);


(* pretty_print_type t = print a type
   t = type to print : type
*)
fun pretty_print_type (Type (n, l)) = 
      "Type(\"" ^ n ^ "\", [" ^ (pretty_print_typelist l pretty_print_type) ^ "])"
  | pretty_print_type (TFree (n, s)) = 
      "TFree(\"" ^ n ^ "\", [" ^ (pretty_print_sort s) ^ "])"
  | pretty_print_type (TVar ((n, i), s)) = 
      "TVar( (\"" ^ n ^ "\", " ^ (string_of_int i) ^ "), [" ^ (pretty_print_sort s) ^ "])";


(* pretty_print_term t = print a term prints types and sorts too.
   t = term to print : term
*)
fun pretty_print_term (Const (s, t)) = 
      "Const(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
  | pretty_print_term (Free (s, t)) = 
      "Free(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
  | pretty_print_term (Var ((n, i), t)) = 
      "Var( (\"" ^ n ^ "\"," ^ (string_of_int i) ^ "), " ^ (pretty_print_type t) ^ ")"
  | pretty_print_term (Bound i) = 
      "Bound(" ^ (string_of_int i) ^ ")"
  | pretty_print_term (Abs (s, t, r)) = 
      "Abs(\"" ^ s ^ "\"," ^ (pretty_print_type t) ^ ", \n  " ^ (pretty_print_term r) ^ ")"
  | pretty_print_term (op $ (t1, t2)) = 
      "(" ^ (pretty_print_term t1) ^ ") $\n (" ^ (pretty_print_term t2) ^ ")";

(* Write the term out nicly instead of just creating a string for it *)
fun writeterm t = writeln (pretty_print_term t);
fun writetype t = writeln (pretty_print_type t);
fun writesort s = writeln (pretty_print_sort s);


(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
(*  Turn on show types *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)

(* if (!show_types) then true else set show_types; *)

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
(*  functions *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)

fun current_sign () = sign_of (the_context());
fun cterm_of_term (t : term) = cterm_of (current_sign()) t;
fun term_of_thm t = (Thm.prop_of t);

(* little function to make a trueprop of anything by putting a P 
   function in front of it... 
fun HOL_mk_term_prop t = 
  ((Const("Trueprop", Type("fun", 
    [Type("bool", []), Type("prop", [])]))) $
      ((Free("P", Type("fun", [type_of t, 
        Type("bool", [])]))) $ t));

*)

fun string_of_term t =
  (Sign.string_of_term (current_sign()) t);

(*
(allt as (Const("Trueprop", ty) $ m)) = 
    (string_of_cterm (cterm_of_term allt))
  | string_of_term (t : term) = 
    string_of_cterm (cterm_of_term (HOL_mk_term_prop t));
*)

(* creates a simple cterm of the term if it's not already a prop by 
   prefixing it with a polymorphic function P, then create the cterm
   and print that. Handy tool for printing terms that are not
   already propositions, or not cterms. 
*)
fun pp_term t = writeln (string_of_term t);

(* create a trivial HOL thm from anything... *)
fun triv_thm_from_string s = 
  Thm.trivial (cterm_of (current_sign()) (read s));

  (* Checks if vars could be the same - alpha convertable
  w.r.t. previous vars, a and b are assumed to be vars,
  free vars, but not bound vars,
  Note frees and vars must all have unique names. *)
  fun same_var_check a b L =
  let 
    fun bterm_from t [] = None
      | bterm_from t ((a,b)::m) = 
          if t = a then Some b else bterm_from t m

    val bl_opt = bterm_from a L
  in
		case bterm_from a L of
			None => Some ((a,b)::L)
		| Some b2 => if b2 = b then Some L else None
  end;

  (* FIXME: make more efficient, only require a single new var! *)
  (* check if the new term has any meta variables not in the old term *)
  fun has_new_vars (old, new) = 
			(case IsaPLib.lrem (op =) (Term.term_vars old) (Term.term_vars new) of 
				 [] => false
			 | (_::_) => true);
  (* check if the new term has any meta variables not in the old term *)
  fun has_new_typ_vars (old, new) = 
			(case IsaPLib.lrem (op =) (Term.term_tvars old) (Term.term_tvars new) of 
				 [] => false
			 | (_::_) => true);

  (* working with Isar terms and their skolemisation(s) *)
(*    val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term
    val unskolemise_term : (string,Term.typ) list -> Term.term -> Term.term
*)

(* cunning version *)

(* This version avoids name conflicts that might be intorduced by
unskolemisation, and returns a list of (string * Term.typ) * string,
where the outer string is the original name, and the inner string is
the new name, and the type is the type of the free variable that was
renamed. *)
local
  fun myadd (n,ty) (L as (renames, names)) = 
      let val n' = Syntax.dest_skolem n in 
        case (Library.find_first (fn (_,n2) => (n2 = n)) renames) of 
          None => 
          let val renamedn = Term.variant names n' in 
            (renamedn, (((renamedn, ty), n) :: renames, 
                        renamedn :: names)) end
        | (Some ((renamedn, _), _)) => (renamedn, L)
      end
      handle LIST _ => (n, L);

  fun unsk (L,f) (t1 $ t2) = 
      let val (L', t1') = unsk (L, I) t1 
      in unsk (L', (fn x => f (t1' $ x))) t2 end
    | unsk (L,f) (Abs(n,ty,t)) = 
      unsk (L, (fn x => Abs(n,ty,x))) t
    | unsk (L, f) (Free (n,ty)) = 
      let val (renamed_n, L') = myadd (n ,ty) L
       in (L', f (Free (renamed_n, ty))) end
    | unsk (L, f) l = (L, f l);
in
fun unskolemise_all_term t = 
    let 
      val names = Term.add_term_names (t,[]) 
      val ((renames,names'),t') = unsk (([], names),I) t
    in (renames,t') end;
end

(*    fun unskolemise_all_term t = 
        let 
          fun fmap fv = 
              let (n,ty) = (Term.dest_Free fv) in 
                Some (fv, Free (Syntax.dest_skolem n, ty)) handle LIST _ => None
              end
          val substfrees = mapfilter fmap (Term.term_frees t)
        in
          Term.subst_free substfrees t
        end; *)

(* true if the type t is a function *)
fun is_fun_typ (Type(s, l)) = 
    if s = "fun" then true else false
  | is_fun_typ _ = false;

val is_atomic_typ = not o is_fun_typ;

(* get the frees in a term that are of atomic type, ie non-functions *)
val atomic_frees_of_term =
     filter (is_atomic_typ o snd) 
     o map Term.dest_Free 
     o Term.term_frees;


(* read in a string and a top-level type and this will give back a term *) 
fun readwty tstr tystr = 
    let 
      val sgn = Theory.sign_of (the_context())
    in
      Sign.simple_read_term sgn (Sign.read_typ (sgn, K None) tystr) tstr
    end;


  (* first term is equal to the second in some name convertable
  way... Note: This differs from the aeconv in the Term.ML file of
  Isabelle in that it allows a var to be alpha-equiv to a free var. 
  
  Also, the isabelle term.ML version of aeconv uses a
  function that it claims doesn't work! *)

  fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l = 
    if ty1 = ty2 then term_name_eq t1 t2 l
    else None

  | term_name_eq (ah $ at) (bh $ bt) l =
    let 
      val lopt = (term_name_eq ah bh l)
    in
      if is_some lopt then 
	term_name_eq at bt (the lopt)
      else
        None
    end

  | term_name_eq (Const(a,T)) (Const(b,U)) l = 
    if a=b andalso T=U then Some l
    else None

  | term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l = 
    same_var_check a b l

  | term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l = 
    same_var_check a b l

  | term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l = 
    same_var_check a b l

  | term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l = 
    same_var_check a b l

  | term_name_eq (Bound i) (Bound j) l = 
    if i = j then Some l else None

  | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) None);

 (* checks to see if the term in a name-equivalent member of the list of terms. *)
  fun get_name_eq_member a [] = None
    | get_name_eq_member a (h :: t) = 
        if is_some (term_name_eq a h []) then Some h 
				else get_name_eq_member a t;

  fun name_eq_member a [] = false
    | name_eq_member a (h :: t) = 
        if is_some (term_name_eq a h []) then true 
				else name_eq_member a t;

  (* true if term is a variable *)
  fun is_some_kind_of_var (Free(s, ty)) = true
    | is_some_kind_of_var (Var(i, ty)) = true
    | is_some_kind_of_var (Bound(i)) = true
    | is_some_kind_of_var _ = false;

    (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
(* FIXME: we should really check that there is a subterm on the lhs
which embeds into the rhs, this would be much closer to the normal
notion of valid wave rule - ie there exists at least one case where it
is a valid wave rule... *)                                        
	fun is_not_valid_rwrule tysig (lhs, rhs) = 
			(Pattern.matches_subterm tysig (lhs, rhs)) orelse
			has_new_vars (lhs,rhs) orelse
      has_new_typ_vars (lhs,rhs);


  (* first term contains the second in some name convertable way... *)
  (* note: this is equivalent to an alpha-convertable emedding *)
  (* takes as args: term containing a, term contained b,
     (bound vars of a, bound vars of b), 
     current alpha-conversion-pairs, 
     returns: bool:can convert, new alpha-conversion table *)
  (* in bellow: we *don't* use: a loose notion that only requires
  variables to match variables, and doesn't worry about the actual
  pattern in the variables. *)
  fun term_contains1 (Bs, FVs) (Abs(s,ty,t)) (Abs(s2,ty2,t2)) = 
			if ty = ty2 then 
				term_contains1 ((Some(s,s2,ty)::Bs), FVs) t t2
			else []

  | term_contains1 T t1 (Abs(s2,ty2,t2)) = []

  | term_contains1 (Bs, FVs) (Abs(s,ty,t)) t2 = 
    term_contains1 (None::Bs, FVs) t t2

  | term_contains1 T (ah $ at) (bh $ bt) =
    (term_contains1 T ah (bh $ bt)) @ 
    (term_contains1 T at (bh $ bt)) @
    (flat (map (fn inT => (term_contains1 inT at bt)) 
               (term_contains1 T ah bh)))

  | term_contains1 T a (bh $ bt) = []

  | term_contains1 T (ah $ at) b =
		(term_contains1 T ah b) @ (term_contains1 T at b)

  | term_contains1 T a b = 
  (* simple list table lookup to check if a named variable has been
  mapped to a variable, if not adds the mapping and return some new
  list mapping, if it is then it checks that the pair are mapped to
  each other, if so returns the current mapping list, else none. *)
		let 
			fun bterm_from t [] = None
				| bterm_from t ((a,b)::m) = 
					if t = a then Some b else bterm_from t m

  (* check to see if, w.r.t. the variable mapping, two terms are leaf
  terms and are mapped to each other. Note constants are only mapped
  to the same constant. *) 
			fun same_leaf_check (T as (Bs,FVs)) (Bound i) (Bound j) =
					let 
						fun aux_chk (i1,i2) [] = false
							| aux_chk (0,0) ((Some _) :: bnds) = true
							| aux_chk (i1,0) (None :: bnds) = false
							| aux_chk (i1,i2) ((Some _) :: bnds) =
								aux_chk (i1 - 1,i2 - 1) bnds
							| aux_chk (i1,i2) (None :: bnds) =
								aux_chk (i1,i2 - 1) bnds 
					in
						if (aux_chk (i,j) Bs) then [T]
						else []
					end
				| same_leaf_check (T as (Bs,(Fs,Vs))) 
                          (a as (Free (an,aty))) 
                          (b as (Free (bn,bty))) =
					(case bterm_from an Fs of 
						 Some b2n => if bn = b2n then [T]
												 else [] (* conflict of var name *)
					 | None => [(Bs,((an,bn)::Fs,Vs))])
				| same_leaf_check (T as (Bs,(Fs,Vs))) 
                          (a as (Var (an,aty))) 
                          (b as (Var (bn,bty))) =
					(case bterm_from an Vs of 
						 Some b2n => if bn = b2n then [T]
												 else [] (* conflict of var name *)
					 | None => [(Bs,(Fs,(an,bn)::Vs))])
				| same_leaf_check T (a as (Const _)) (b as (Const _)) =
					if a = b then [T] else []
				| same_leaf_check T _ _ = []

		in
			same_leaf_check T a b
		end;

  (* wrapper for term_contains1: checks if the term "a" contains in
  some embedded way, (w.r.t. name -convertable) the term "b" *)
  fun term_contains a b = 
			case term_contains1 ([],([],[])) a b of
			  (_ :: _) => true
			| [] => false;


      (* pp_term a; pp_term b; writeln "EQTerm matches are: "; map (fn (a,b) => writeln ("(" ^ (string_of_term a) ^ ", " ^ (string_of_term b) ^ ")")) L;*) 


  (* change all bound variables to see ones with appropriate name and
  type *)

  (* naming convention is OK as we use 'variant' from term.ML *)

  (* Note "bounds_to_frees" defined below, its better and quicker, but
  keeps the quantifiers handing about, and changes all bounds, not
  just universally quantified ones. *)
  fun change_bounds_to_frees t =  
    let 
      val vars = strip_all_vars t
      val frees_names = map (fn Free(s,n) => s | _ => "") (term_frees t)
      val body = strip_all_body t

      fun bnds_to_frees [] _ acc = acc
        | bnds_to_frees ((name,ty)::more) names acc = 
            let 
	      val new_name = variant names name
	    in
	      bnds_to_frees more (new_name::names) (Free(new_name,ty)::acc)
	    end
    in
      (subst_bounds ((bnds_to_frees vars frees_names []), body))
    end; 



structure fvartabS = TableFun(type key = string val ord = string_ord);

(* a runtime-quick function which makes sure that every variable has a
unique name *)
fun unique_namify_aux (ntab,(Abs(s,ty,t))) = 
    (case (fvartabS.lookup (ntab,s)) of
       None => 
       let 
				 val (ntab2,t2) = unique_namify_aux ((fvartabS.update ((s,s),ntab)), t)
       in
				 (ntab2,Abs(s,ty,t2))
       end
     | Some s2 => 
       let 
				 val s_new = (Term.variant (fvartabS.keys ntab) s)
				 val (ntab2,t2) = 
						 unique_namify_aux ((fvartabS.update ((s_new,s_new),ntab)), t)
       in
				 (ntab2,Abs(s_new,ty,t2))
       end)
  | unique_namify_aux (ntab,(a $ b)) = 
    let 
      val (ntab1,t1) = unique_namify_aux (ntab,a)
      val (ntab2,t2) = unique_namify_aux (ntab1,b)		       
    in
      (ntab2, t1$t2)
    end
  | unique_namify_aux (nt as (ntab,Const x)) = nt
  | unique_namify_aux (nt as (ntab,f as Free (s,ty))) = 
    (case (fvartabS.lookup (ntab,s)) of
       None => ((fvartabS.update ((s,s),ntab)), f)
     | Some _ => nt)
  | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = 
    (case (fvartabS.lookup (ntab,s)) of
       None => ((fvartabS.update ((s,s),ntab)), v)
     | Some _ => nt)
  | unique_namify_aux (nt as (ntab, Bound i)) = nt;
		
fun unique_namify t = 
    #2 (unique_namify_aux (fvartabS.empty, t));

(* a runtime-quick function which makes sure that every variable has a
unique name and also changes bound variables to free variables, used
for embedding checks, Note that this is a pretty naughty term
manipulation, which doesn't have necessary relation to the original
sematics of the term. This is really a trick for our embedding code. *)

fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = 
    (case (fvartabS.lookup (ntab,s)) of
      None => 
      let 
	val (ntab2,t2) = bounds_to_frees_aux ((s,ty)::T)
				       ((fvartabS.update ((s,s),ntab)), t)
      in
	(ntab2,Abs(s,ty,t2))
      end
    | Some s2 => 
      let 
	val s_new = (Term.variant (fvartabS.keys ntab) s)
	val (ntab2,t2) = 
	    bounds_to_frees_aux ((s_new,ty)::T) 
			  (fvartabS.update (((s_new,s_new),ntab)), t)
      in
	(ntab2,Abs(s_new,ty,t2))
      end)
  | bounds_to_frees_aux T (ntab,(a $ b)) = 
    let 
      val (ntab1,t1) = bounds_to_frees_aux T (ntab,a)
      val (ntab2,t2) = bounds_to_frees_aux T (ntab1,b)		       
    in
      (ntab2, t1$t2)
    end
  | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt
  | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = 
    (case (fvartabS.lookup (ntab,s)) of
      None => ((fvartabS.update ((s,s),ntab)), f)
    | Some _ => nt)
  | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = 
     (case (fvartabS.lookup (ntab,s)) of
      None => ((fvartabS.update ((s,s),ntab)), v)
    | Some _ => nt)
  | bounds_to_frees_aux T (nt as (ntab, Bound i)) = 
    let 
      val (s,ty) = Library.nth_elem (i,T) 
    in
      (ntab, Free (s,ty))
    end;


fun bounds_to_frees t = 
    #2 (bounds_to_frees_aux [] (fvartabS.empty,t));

fun bounds_to_frees_with_vars vars t = 
    #2 (bounds_to_frees_aux vars (fvartabS.empty,t));



(* loose bounds to frees *)
fun loose_bnds_to_frees_aux (bnds,vars) (Abs(s,ty,t)) = 
    Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t)
  | loose_bnds_to_frees_aux (bnds,vars) (a $ b) = 
    (loose_bnds_to_frees_aux (bnds,vars) a) 
      $ (loose_bnds_to_frees_aux (bnds,vars) b)
  | loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) = 
    if (bnds <= i) then Free (Library.nth_elem (i - bnds,vars))
    else t
  | loose_bnds_to_frees_aux (bnds,vars) t = t;


fun loose_bnds_to_frees vars t = 
    loose_bnds_to_frees_aux (0,vars) t;

(* puts prems of a theorem into a useful form, (rulify) 
  Note that any loose bound variables are treated as free vars 
*)
(* fun make_term_into_simp_thm vars sgn t = 
    let 
      val triv = 
					Thm.trivial (Thm.cterm_of 
			 sgn (loose_bnds_to_frees vars t))
    in
      SplitterData.mk_eq (Drule.standard (ObjectLogic.rulify_no_asm triv))
    end;

fun thms_of_prems_in_goal i tm= 
    let 
      val goal = (nth_elem (i-1,Thm.prems_of tm))
      val vars = rev (strip_all_vars goal)
      val prems = Logic.strip_assums_hyp (strip_all_body goal)
      val simp_prem_thms = 
					map (make_term_into_simp_thm vars (Thm.sign_of_thm tm)) prems
    in
      simp_prem_thms
    end;
*)

  (* replace all universally quantifief variables (at HOL object level) 
     with free vars 
  fun HOL_Alls_to_frees TL (Const("All", _) $ Abs(v, ty, t)) = 
      HOL_Alls_to_frees ((Free (v, ty)) :: TL) t
    | HOL_Alls_to_frees TL t = 
      (TL,(subst_bounds (TL, t)));
*)

  (* this is just a hack for mixing with interactive mode, and using topthm() *)

  fun try_dest_Goal (Const("Goal", _) $ T) = T
    | try_dest_Goal T = T;

  fun try_dest_Trueprop (Const("Trueprop", _) $ T) = T
    | try_dest_Trueprop T = T; 

  fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
    | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
    | bot_left_leaf_of x = x;


(* cleaned up normal form version of the subgoal terms conclusion *)
fun cleaned_term_conc t = 
    let
      val concl = Logic.strip_imp_concl (change_bounds_to_frees t)
    in 
      (try_dest_Trueprop (try_dest_Goal concl))
    end;

(*   fun get_prems_of_sg_term t = 
			map opt_dest_Trueprop (Logic.strip_imp_prems t); *)

fun get_prems_of_sg_term t = 
		map try_dest_Trueprop (Logic.strip_assums_hyp t);


(* drop premices, clean bound var stuff, and make a trueprop... *)
  fun cleaned_term_parts t = 
      let 
				val t2 = (change_bounds_to_frees t)
        val concl = Logic.strip_imp_concl t2
				val prems = map try_dest_Trueprop (Logic.strip_imp_prems t2)
      in 
				(prems, (try_dest_Trueprop (try_dest_Goal concl)))
      end;

(* old version
      fun cleaned_term t =  
        let 
            val concl = (HOLogic.dest_Trueprop (Logic.strip_imp_concl 
                          (change_bounds_to_frees t) ))
	in 
	  concl
	end;
*)

  (* change free variables to vars and visa versa *)
  (* *** check naming is OK, can we just use the vasr old name? *)
  (* *** Check: Logic.varify and Logic.unvarify *)
  fun change_vars_to_frees (a$b) = 
        (change_vars_to_frees a) $ (change_vars_to_frees b)
    | change_vars_to_frees (Abs(s,ty,t)) = 
        (Abs(s,Type.varifyT ty,change_vars_to_frees t))
    | change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty))
    | change_vars_to_frees l = l;

  fun change_frees_to_vars (a$b) = 
        (change_frees_to_vars a) $ (change_frees_to_vars b)
    | change_frees_to_vars (Abs(s,ty,t)) = 
        (Abs(s,Type.varifyT ty,change_frees_to_vars t))
    | change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty))
    | change_frees_to_vars l = l;


end;



  (* ignores lambda abstractions, ie (\x y = y) 
     same as embedding check code, ie. (f a b) = can "a" be embedded in "b"
  *)
  (* fun term_is_same_or_simpler_than (Abs(s,ty,t)) b = 
    term_is_same_or_simpler_than t b

  | term_is_same_or_simpler_than a (Abs(s,ty,t)) = 
    term_is_same_or_simpler_than a t

  | term_is_same_or_simpler_than (ah $ at) (bh $ bt) =
    (term_is_same_or_simpler_than (ah $ at) bh) orelse
    (term_is_same_or_simpler_than (ah $ at) bt) orelse
    ((term_is_same_or_simpler_than ah bh) andalso 
     (term_is_same_or_simpler_than at bt))

  | term_is_same_or_simpler_than (ah $ at) b = false

  | term_is_same_or_simpler_than a (bh $ bt) =
      (term_is_same_or_simpler_than a bh) orelse 
      (term_is_same_or_simpler_than a bt)

  | term_is_same_or_simpler_than a b =
      if a = b then true else false;
  *)

(*  fun term_is_simpler_than t1 t2 = 
    (are_different_terms t1 t2) andalso 
    (term_is_same_or_simpler_than t1 t2);
*)