src/Tools/misc_legacy.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 59165 115965966e15
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@37781
     1
(*  Title:      Tools/misc_legacy.ML
wenzelm@37781
     2
wenzelm@37781
     3
Misc legacy stuff -- to be phased out eventually.
wenzelm@37781
     4
*)
wenzelm@37781
     5
wenzelm@37781
     6
signature MISC_LEGACY =
wenzelm@37781
     7
sig
wenzelm@44121
     8
  val add_term_names: term * string list -> string list
wenzelm@44121
     9
  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
wenzelm@44121
    10
  val add_typ_tfree_names: typ * string list -> string list
wenzelm@44121
    11
  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
wenzelm@44121
    12
  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
wenzelm@44121
    13
  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
wenzelm@44121
    14
  val add_term_tfree_names: term * string list -> string list
wenzelm@44121
    15
  val typ_tfrees: typ -> (string * sort) list
wenzelm@44121
    16
  val typ_tvars: typ -> (indexname * sort) list
wenzelm@44121
    17
  val term_tfrees: term -> (string * sort) list
wenzelm@44121
    18
  val term_tvars: term -> (indexname * sort) list
wenzelm@44121
    19
  val add_term_vars: term * term list -> term list
wenzelm@44121
    20
  val term_vars: term -> term list
wenzelm@44121
    21
  val add_term_frees: term * term list -> term list
wenzelm@44121
    22
  val term_frees: term -> term list
wenzelm@37781
    23
  val mk_defpair: term * term -> string * term
wenzelm@37781
    24
  val get_def: theory -> xstring -> thm
wenzelm@37781
    25
  val METAHYPS: (thm list -> tactic) -> int -> tactic
wenzelm@47022
    26
  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
wenzelm@47022
    27
  val freeze_thaw: thm -> thm * (thm -> thm)
wenzelm@37781
    28
end;
wenzelm@37781
    29
wenzelm@37781
    30
structure Misc_Legacy: MISC_LEGACY =
wenzelm@37781
    31
struct
wenzelm@37781
    32
wenzelm@44121
    33
(*iterate a function over all types in a term*)
wenzelm@44121
    34
fun it_term_types f =
wenzelm@44121
    35
let fun iter(Const(_,T), a) = f(T,a)
wenzelm@44121
    36
      | iter(Free(_,T), a) = f(T,a)
wenzelm@44121
    37
      | iter(Var(_,T), a) = f(T,a)
wenzelm@44121
    38
      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
wenzelm@44121
    39
      | iter(f$u, a) = iter(f, iter(u, a))
wenzelm@44121
    40
      | iter(Bound _, a) = a
wenzelm@44121
    41
in iter end
wenzelm@44121
    42
wenzelm@44121
    43
(*Accumulates the names in the term, suppressing duplicates.
wenzelm@44121
    44
  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
wenzelm@44121
    45
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
wenzelm@44121
    46
  | add_term_names (Free(a,_), bs) = insert (op =) a bs
wenzelm@44121
    47
  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
wenzelm@44121
    48
  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
wenzelm@44121
    49
  | add_term_names (_, bs) = bs;
wenzelm@44121
    50
wenzelm@44121
    51
(*Accumulates the TVars in a type, suppressing duplicates.*)
wenzelm@44121
    52
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
wenzelm@44121
    53
  | add_typ_tvars(TFree(_),vs) = vs
wenzelm@44121
    54
  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
wenzelm@44121
    55
wenzelm@44121
    56
(*Accumulates the TFrees in a type, suppressing duplicates.*)
wenzelm@44121
    57
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
wenzelm@44121
    58
  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
wenzelm@44121
    59
  | add_typ_tfree_names(TVar(_),fs) = fs;
wenzelm@44121
    60
wenzelm@44121
    61
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
wenzelm@44121
    62
  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
wenzelm@44121
    63
  | add_typ_tfrees(TVar(_),fs) = fs;
wenzelm@44121
    64
wenzelm@44121
    65
(*Accumulates the TVars in a term, suppressing duplicates.*)
wenzelm@44121
    66
val add_term_tvars = it_term_types add_typ_tvars;
wenzelm@44121
    67
wenzelm@44121
    68
(*Accumulates the TFrees in a term, suppressing duplicates.*)
wenzelm@44121
    69
val add_term_tfrees = it_term_types add_typ_tfrees;
wenzelm@44121
    70
val add_term_tfree_names = it_term_types add_typ_tfree_names;
wenzelm@44121
    71
wenzelm@44121
    72
(*Non-list versions*)
wenzelm@44121
    73
fun typ_tfrees T = add_typ_tfrees(T,[]);
wenzelm@44121
    74
fun typ_tvars T = add_typ_tvars(T,[]);
wenzelm@44121
    75
fun term_tfrees t = add_term_tfrees(t,[]);
wenzelm@44121
    76
fun term_tvars t = add_term_tvars(t,[]);
wenzelm@44121
    77
wenzelm@44121
    78
wenzelm@44121
    79
(*Accumulates the Vars in the term, suppressing duplicates.*)
wenzelm@44121
    80
fun add_term_vars (t, vars: term list) = case t of
wenzelm@44121
    81
    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
wenzelm@44121
    82
  | Abs (_,_,body) => add_term_vars(body,vars)
wenzelm@44121
    83
  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
wenzelm@44121
    84
  | _ => vars;
wenzelm@44121
    85
wenzelm@44121
    86
fun term_vars t = add_term_vars(t,[]);
wenzelm@44121
    87
wenzelm@44121
    88
(*Accumulates the Frees in the term, suppressing duplicates.*)
wenzelm@44121
    89
fun add_term_frees (t, frees: term list) = case t of
wenzelm@44121
    90
    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
wenzelm@44121
    91
  | Abs (_,_,body) => add_term_frees(body,frees)
wenzelm@44121
    92
  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
wenzelm@44121
    93
  | _ => frees;
wenzelm@44121
    94
wenzelm@44121
    95
fun term_frees t = add_term_frees(t,[]);
wenzelm@44121
    96
wenzelm@44121
    97
wenzelm@37781
    98
fun mk_defpair (lhs, rhs) =
wenzelm@37781
    99
  (case Term.head_of lhs of
wenzelm@37781
   100
    Const (name, _) =>
wenzelm@46909
   101
      (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
wenzelm@37781
   102
  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
wenzelm@37781
   103
wenzelm@37781
   104
wenzelm@37781
   105
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
wenzelm@37781
   106
wenzelm@37781
   107
wenzelm@37781
   108
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
wenzelm@37781
   109
       METAHYPS (fn prems => tac prems) i
wenzelm@37781
   110
wenzelm@37781
   111
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
wenzelm@37781
   112
proof state A==>A, supplying A1,...,An as meta-level assumptions (in
wenzelm@37781
   113
"prems").  The parameters x1,...,xm become free variables.  If the
wenzelm@37781
   114
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
wenzelm@37781
   115
then it is lifted back into the original context, yielding k subgoals.
wenzelm@37781
   116
wenzelm@37781
   117
Replaces unknowns in the context by Frees having the prefix METAHYP_
wenzelm@37781
   118
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
wenzelm@37781
   119
DOES NOT HANDLE TYPE UNKNOWNS.
wenzelm@37781
   120
wenzelm@37781
   121
wenzelm@37781
   122
NOTE: This version does not observe the proof context, and thus cannot
wenzelm@37781
   123
work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
wenzelm@37781
   124
properly localized variants of the same idea.
wenzelm@37781
   125
****)
wenzelm@37781
   126
wenzelm@37781
   127
local
wenzelm@37781
   128
wenzelm@37781
   129
(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
wenzelm@37781
   130
    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
wenzelm@37781
   131
  Main difference from strip_assums concerns parameters:
wenzelm@37781
   132
    it replaces the bound variables by free variables.  *)
wenzelm@56245
   133
fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) =
wenzelm@37781
   134
      strip_context_aux (params, H :: Hs, B)
wenzelm@56245
   135
  | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) =
wenzelm@42284
   136
      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
wenzelm@37781
   137
      in strip_context_aux ((b, T) :: params, Hs, u) end
wenzelm@37781
   138
  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
wenzelm@37781
   139
wenzelm@37781
   140
fun strip_context A = strip_context_aux ([], [], A);
wenzelm@37781
   141
wenzelm@37781
   142
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
wenzelm@37781
   143
  Instantiates distinct free variables by terms of same type.*)
wenzelm@37781
   144
fun free_instantiate ctpairs =
wenzelm@37781
   145
  forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
wenzelm@37781
   146
wenzelm@37781
   147
fun free_of s ((a, i), T) =
wenzelm@37781
   148
  Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
wenzelm@37781
   149
wenzelm@37781
   150
fun mk_inst v = (Var v, free_of "METAHYP1_" v)
wenzelm@37781
   151
wenzelm@37781
   152
fun metahyps_split_prem prem =
wenzelm@37781
   153
  let (*find all vars in the hyps -- should find tvars also!*)
wenzelm@37781
   154
      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
wenzelm@37781
   155
      val insts = map mk_inst hyps_vars
wenzelm@37781
   156
      (*replace the hyps_vars by Frees*)
wenzelm@37781
   157
      val prem' = subst_atomic insts prem
wenzelm@37781
   158
      val (params,hyps,concl) = strip_context prem'
wenzelm@37781
   159
  in (insts,params,hyps,concl)  end;
wenzelm@37781
   160
wenzelm@37781
   161
fun metahyps_aux_tac tacf (prem,gno) state =
wenzelm@37781
   162
  let val (insts,params,hyps,concl) = metahyps_split_prem prem
wenzelm@37781
   163
      val maxidx = Thm.maxidx_of state
wenzelm@37781
   164
      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
wenzelm@37781
   165
      val chyps = map cterm hyps
wenzelm@37781
   166
      val hypths = map Thm.assume chyps
wenzelm@37781
   167
      val subprems = map (Thm.forall_elim_vars 0) hypths
wenzelm@37781
   168
      val fparams = map Free params
wenzelm@37781
   169
      val cparams = map cterm fparams
wenzelm@37781
   170
      fun swap_ctpair (t,u) = (cterm u, cterm t)
wenzelm@37781
   171
      (*Subgoal variables: make Free; lift type over params*)
wenzelm@37781
   172
      fun mk_subgoal_inst concl_vars (v, T) =
wenzelm@37781
   173
          if member (op =) concl_vars (v, T)
wenzelm@37781
   174
          then ((v, T), true, free_of "METAHYP2_" (v, T))
wenzelm@37781
   175
          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
wenzelm@37781
   176
      (*Instantiate subgoal vars by Free applied to params*)
wenzelm@37781
   177
      fun mk_ctpair (v, in_concl, u) =
wenzelm@37781
   178
          if in_concl then (cterm (Var v), cterm u)
wenzelm@37781
   179
          else (cterm (Var v), cterm (list_comb (u, fparams)))
wenzelm@37781
   180
      (*Restore Vars with higher type and index*)
wenzelm@37781
   181
      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
wenzelm@37781
   182
          if in_concl then (cterm u, cterm (Var ((a, i), T)))
wenzelm@37781
   183
          else (cterm u, cterm (Var ((a, i + maxidx), U)))
wenzelm@37781
   184
      (*Embed B in the original context of params and hyps*)
wenzelm@46215
   185
      fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
wenzelm@37781
   186
      (*Strip the context using elimination rules*)
wenzelm@37781
   187
      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
wenzelm@37781
   188
      (*A form of lifting that discharges assumptions.*)
wenzelm@37781
   189
      fun relift st =
wenzelm@37781
   190
        let val prop = Thm.prop_of st
wenzelm@37781
   191
            val subgoal_vars = (*Vars introduced in the subgoals*)
wenzelm@37781
   192
              fold Term.add_vars (Logic.strip_imp_prems prop) []
wenzelm@37781
   193
            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
wenzelm@37781
   194
            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
wenzelm@37781
   195
            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
wenzelm@37781
   196
            val emBs = map (cterm o embed) (prems_of st')
wenzelm@37781
   197
            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
wenzelm@37781
   198
        in  (*restore the unknowns to the hypotheses*)
wenzelm@37781
   199
            free_instantiate (map swap_ctpair insts @
wenzelm@37781
   200
                              map mk_subgoal_swap_ctpair subgoal_insts)
wenzelm@37781
   201
                (*discharge assumptions from state in same order*)
wenzelm@37781
   202
                (implies_intr_list emBs
wenzelm@37781
   203
                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
wenzelm@37781
   204
        end
wenzelm@37781
   205
      (*function to replace the current subgoal*)
wenzelm@52223
   206
      fun next st =
wenzelm@58950
   207
        Thm.bicompose NONE {flatten = true, match = false, incremented = false}
wenzelm@52223
   208
          (false, relift st, nprems_of st) gno state
wenzelm@37781
   209
  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
wenzelm@37781
   210
wenzelm@37781
   211
fun print_vars_terms n thm =
wenzelm@37781
   212
  let
wenzelm@37781
   213
    val thy = theory_of_thm thm
wenzelm@37781
   214
    fun typed s ty =
wenzelm@37781
   215
      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
wenzelm@37781
   216
    fun find_vars (Const (c, ty)) =
wenzelm@37781
   217
          if null (Term.add_tvarsT ty []) then I
wenzelm@37781
   218
          else insert (op =) (typed c ty)
wenzelm@37781
   219
      | find_vars (Var (xi, ty)) =
wenzelm@37781
   220
          insert (op =) (typed (Term.string_of_vname xi) ty)
wenzelm@37781
   221
      | find_vars (Free _) = I
wenzelm@37781
   222
      | find_vars (Bound _) = I
wenzelm@37781
   223
      | find_vars (Abs (_, _, t)) = find_vars t
wenzelm@37781
   224
      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
wenzelm@37781
   225
    val prem = Logic.nth_prem (n, Thm.prop_of thm)
wenzelm@37781
   226
    val tms = find_vars prem []
wenzelm@37781
   227
  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
wenzelm@37781
   228
wenzelm@37781
   229
in
wenzelm@37781
   230
wenzelm@37781
   231
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
wenzelm@37781
   232
  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
wenzelm@37781
   233
wenzelm@37781
   234
end;
wenzelm@37781
   235
wenzelm@47022
   236
wenzelm@47022
   237
(* generating identifiers -- often fresh *)
wenzelm@47022
   238
wenzelm@47022
   239
local
wenzelm@47022
   240
(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
wenzelm@47022
   241
fun gensym_char i =
wenzelm@47022
   242
  if i<26 then chr (ord "A" + i)
wenzelm@47022
   243
  else if i<52 then chr (ord "a" + i - 26)
wenzelm@47022
   244
  else chr (ord "0" + i - 52);
wenzelm@47022
   245
wenzelm@47022
   246
val char_vec = Vector.tabulate (62, gensym_char);
wenzelm@47022
   247
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
wenzelm@47022
   248
wenzelm@56147
   249
val gensym_seed = Synchronized.var "gensym_seed" (0: int);
wenzelm@47022
   250
wenzelm@47022
   251
in
wenzelm@56147
   252
  fun gensym pre =
wenzelm@56147
   253
    Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
wenzelm@37781
   254
end;
wenzelm@37781
   255
wenzelm@47022
   256
wenzelm@47022
   257
(*Convert all Vars in a theorem to Frees.  Also return a function for
wenzelm@47022
   258
  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
wenzelm@47022
   259
wenzelm@47022
   260
fun freeze_thaw_robust th =
wenzelm@47022
   261
 let val fth = Thm.legacy_freezeT th
wenzelm@47022
   262
     val thy = Thm.theory_of_thm fth
wenzelm@47022
   263
 in
wenzelm@47022
   264
   case Thm.fold_terms Term.add_vars fth [] of
haftmann@47576
   265
       [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
wenzelm@47022
   266
     | vars =>
wenzelm@47022
   267
         let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
wenzelm@47022
   268
             val alist = map newName vars
wenzelm@47022
   269
             fun mk_inst (v,T) =
wenzelm@47022
   270
                 (cterm_of thy (Var(v,T)),
wenzelm@47022
   271
                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
wenzelm@47022
   272
             val insts = map mk_inst vars
wenzelm@47022
   273
             fun thaw i th' = (*i is non-negative increment for Var indexes*)
wenzelm@47022
   274
                 th' |> forall_intr_list (map #2 insts)
wenzelm@47022
   275
                     |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
wenzelm@47022
   276
         in  (Thm.instantiate ([],insts) fth, thaw)  end
wenzelm@47022
   277
 end;
wenzelm@47022
   278
wenzelm@47022
   279
(*Basic version of the function above. No option to rename Vars apart in thaw.
wenzelm@47022
   280
  The Frees created from Vars have nice names.*)
wenzelm@47022
   281
fun freeze_thaw th =
wenzelm@47022
   282
 let val fth = Thm.legacy_freezeT th
wenzelm@47022
   283
     val thy = Thm.theory_of_thm fth
wenzelm@47022
   284
 in
wenzelm@47022
   285
   case Thm.fold_terms Term.add_vars fth [] of
wenzelm@47022
   286
       [] => (fth, fn x => x)
wenzelm@47022
   287
     | vars =>
wenzelm@47022
   288
         let fun newName (ix, _) (pairs, used) =
wenzelm@47022
   289
                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
wenzelm@47022
   290
                   in  ((ix,v)::pairs, v::used)  end;
wenzelm@47022
   291
             val (alist, _) =
wenzelm@47022
   292
                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
wenzelm@47022
   293
             fun mk_inst (v, T) =
wenzelm@47022
   294
                 (cterm_of thy (Var(v,T)),
wenzelm@47022
   295
                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
wenzelm@47022
   296
             val insts = map mk_inst vars
wenzelm@47022
   297
             fun thaw th' =
wenzelm@47022
   298
                 th' |> forall_intr_list (map #2 insts)
wenzelm@47022
   299
                     |> forall_elim_list (map #1 insts)
wenzelm@47022
   300
         in  (Thm.instantiate ([],insts) fth, thaw)  end
wenzelm@47022
   301
 end;
wenzelm@47022
   302
wenzelm@47022
   303
end;
wenzelm@47022
   304