src/Tools/IsaPlanner/rw_inst.ML
author wenzelm
Thu, 30 May 2013 16:31:53 +0200
changeset 52240 066c2ff17f7c
parent 52239 6a6033fa507c
child 52242 2d634bfa1bbf
permissions -rw-r--r--
misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     1
(*  Title:      Tools/IsaPlanner/rw_inst.ML
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     2
    Author:     Lucas Dixon, University of Edinburgh
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     3
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     4
Rewriting using a conditional meta-equality theorem which supports
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     5
schematic variable instantiation.
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
     6
*)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     7
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     8
signature RW_INST =
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     9
sig
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    10
  val rw: Proof.context ->
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    11
    ((indexname * (sort * typ)) list * (* type var instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    12
     (indexname * (typ * term)) list) (* schematic var instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    13
    * (string * typ) list (* Fake named bounds + types *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    14
    * (string * typ) list (* names of bound + types *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    15
    * term -> (* outer term for instantiation *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    16
    thm -> (* rule with indexes lifted *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    17
    thm -> (* target thm *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    18
    thm  (* rewritten theorem possibly with additional premises for rule conditions *)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    19
end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    20
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    21
structure RW_Inst: RW_INST =
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    22
struct
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    23
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    24
(* Given a list of variables that were bound, and a that has been
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    25
instantiated with free variable placeholders for the bound vars, it
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    26
creates an abstracted version of the theorem, with local bound vars as
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    27
lambda-params:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    28
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    29
Ts:
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    30
("x", ty)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    31
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    32
rule::
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    33
C :x ==> P :x = Q :x
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    34
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    35
results in:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    36
("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    37
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    38
note: assumes rule is instantiated
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    39
*)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    40
(* Note, we take abstraction in the order of last abstraction first *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    41
fun mk_abstractedrule ctxt TsFake Ts rule =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    42
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    43
    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    44
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    45
    (* now we change the names of temporary free vars that represent
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    46
       bound vars with binders outside the redex *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    47
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    48
    val ns =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    49
      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    50
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    51
    val (fromnames, tonames, Ts') =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    52
      fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    53
              (cert (Free(faken,ty)) :: rnf,
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    54
               cert (Free(n2,ty)) :: rnt,
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    55
               (n2,ty) :: Ts''))
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    56
            (TsFake ~~ Ts ~~ ns) ([], [], []);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    57
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    58
    (* rename conflicting free's in the rule to avoid cconflicts
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    59
    with introduced vars from bounds outside in redex *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    60
    val rule' = rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    61
      |> Drule.forall_intr_list fromnames
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    62
      |> Drule.forall_elim_list tonames;
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    63
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    64
    (* make unconditional rule and prems *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    65
    val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule';
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    66
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    67
    (* using these names create lambda-abstracted version of the rule *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    68
    val abstractions = rev (Ts' ~~ tonames);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    69
    val abstract_rule =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    70
      Library.foldl (fn (th,((n,ty),ct)) => Thm.abstract_rule n ct th)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    71
        (uncond_rule, abstractions);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    72
  in (cprems, abstract_rule) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    73
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    74
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    75
(* given names to avoid, and vars that need to be fixed, it gives
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    76
unique new names to the vars so that they can be fixed as free
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    77
variables *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    78
(* make fixed unique free variable instantiations for non-ground vars *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    79
(* Create a table of vars to be renamed after instantiation - ie
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    80
      other uninstantiated vars in the hyps of the rule
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    81
      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    82
fun mk_renamings ctxt tgt rule_inst =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    83
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    84
    val rule_conds = Thm.prems_of rule_inst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    85
    val (_, cond_vs) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    86
      Library.foldl (fn ((tyvs, vs), t) =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    87
                (union (op =) (Misc_Legacy.term_tvars t) tyvs,
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    88
                 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    89
            (([], []), rule_conds);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    90
    val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    91
    val vars_to_fix = union (op =) termvars cond_vs;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    92
    val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix);
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    93
  in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    94
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    95
(* make a new fresh typefree instantiation for the given tvar *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    96
fun new_tfree (tv as (ix,sort), (pairs,used)) =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    97
  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    98
  in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    99
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   100
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   101
(* make instantiations to fix type variables that are not
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   102
   already instantiated (in ignore_ixs) from the list of terms. *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   103
fun mk_fixtvar_tyinsts ignore_insts ts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   104
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   105
    val ignore_ixs = map fst ignore_insts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   106
    val (tvars, tfrees) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   107
      List.foldr (fn (t, (varixs, tfrees)) =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   108
        (Misc_Legacy.add_term_tvars (t,varixs),
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   109
         Misc_Legacy.add_term_tfrees (t,tfrees))) ([],[]) ts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   110
    val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   111
    val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   112
  in (fixtyinsts, tfrees) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   113
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   114
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   115
(* cross-instantiate the instantiations - ie for each instantiation
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   116
replace all occurances in other instantiations - no loops are possible
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   117
and thus only one-parsing of the instantiations is necessary. *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   118
fun cross_inst insts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   119
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   120
    fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   121
      (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   122
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   123
    fun cross_instL ([], l) = rev l
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   124
      | cross_instL ((ix, t) :: insts, l) =
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   125
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   126
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   127
  in cross_instL (insts, []) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   128
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   129
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   130
fun cross_inst_typs insts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   131
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   132
    fun instL (ix, (srt,ty)) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   133
      map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   134
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   135
    fun cross_instL ([], l) = rev l
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   136
      | cross_instL ((ix, t) :: insts, l) =
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   137
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   138
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   139
  in cross_instL (insts, []) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   140
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   141
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   142
(* assume that rule and target_thm have distinct var names. THINK:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   143
efficient version with tables for vars for: target vars, introduced
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   144
vars, and rule vars, for quicker instantiation?  The outerterm defines
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   145
which part of the target_thm was modified.  Note: we take Ts in the
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   146
upterm order, ie last abstraction first., and with an outeterm where
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   147
the abstracted subterm has the arguments in the revered order, ie
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   148
first abstraction first.  FakeTs has abstractions using the fake name
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   149
- ie the name distinct from all other abstractions. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   150
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   151
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   152
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   153
    val thy = Thm.theory_of_thm target_thm;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   154
    val cert = Thm.cterm_of thy;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   155
    val certT = Thm.ctyp_of thy;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   156
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   157
    (* fix all non-instantiated tvars *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   158
    val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   159
      mk_fixtvar_tyinsts nonfixed_typinsts
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   160
        [Thm.prop_of rule, Thm.prop_of target_thm];
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   161
    val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   162
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   163
    (* certified instantiations for types *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   164
    val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   165
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   166
    (* type instantiated versions *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   167
    val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   168
    val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   169
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   170
    val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   171
    (* type instanitated outer term *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   172
    val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   173
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   174
    val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   175
    val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   176
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   177
    (* type-instantiate the var instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   178
    val insts_tyinst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   179
      List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   180
        (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t))
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   181
          :: insts_tyinst)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   182
        [] unprepinsts;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   183
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   184
    (* cross-instantiate *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   185
    val insts_tyinst_inst = cross_inst insts_tyinst;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   186
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   187
    (* create certms of instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   188
    val cinsts_tyinst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   189
      map (fn (ix, (ty, t)) => (cert (Var (ix, ty)), cert t)) insts_tyinst_inst;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   190
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   191
    (* The instantiated rule *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   192
    val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   193
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   194
    (* Create a table of vars to be renamed after instantiation - ie
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   195
    other uninstantiated vars in the hyps the *instantiated* rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   196
    ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   197
    val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   198
    val cterm_renamings = map (fn (x, y) => (cert (Var x), cert y)) renamings;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   199
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   200
    (* Create the specific version of the rule for this target application *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   201
    val outerterm_inst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   202
      outerterm_tyinst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   203
      |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   204
      |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   205
    val couter_inst = Thm.reflexive (cert outerterm_inst);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   206
    val (cprems, abstract_rule_inst) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   207
      rule_inst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   208
      |> Thm.instantiate ([], cterm_renamings)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   209
      |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   210
    val specific_tgt_rule =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   211
      Conv.fconv_rule Drule.beta_eta_conversion
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   212
        (Thm.combination couter_inst abstract_rule_inst);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   213
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   214
    (* create an instantiated version of the target thm *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   215
    val tgt_th_inst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   216
      tgt_th_tyinst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   217
      |> Thm.instantiate ([], cinsts_tyinst)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   218
      |> Thm.instantiate ([], cterm_renamings);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   219
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   220
    val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   221
  in
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   222
    Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   223
    |> Thm.equal_elim specific_tgt_rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   224
    |> Drule.implies_intr_list cprems
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   225
    |> Drule.forall_intr_list frees_of_fixed_vars
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   226
    |> Drule.forall_elim_list vars
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   227
    |> Thm.varifyT_global' othertfrees
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   228
    |-> K Drule.zero_var_indexes
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   229
  end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   230
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   231
end;