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