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