src/Tools/IsaPlanner/rw_inst.ML
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 52245 f76fb8858e0b
child 58318 f95754ca7082
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
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
52245
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    24
(* Given (string,type) pairs capturing the free vars that need to be
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    25
allified in the assumption, and a theorem with assumptions possibly
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    26
containing the free vars, then we give back the assumptions allified
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    27
as hidden hyps.
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    28
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    29
Given: x
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    30
th: A vs ==> B vs
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    31
Results in: "B vs" [!!x. A x]
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    32
*)
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    33
fun allify_conditions Ts th =
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    34
  let
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    35
    val cert = Thm.cterm_of (Thm.theory_of_thm th);
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    36
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    37
    fun allify (x, T) t =
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    38
      Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    39
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    40
    val cTs = map (cert o Free) Ts;
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    41
    val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th);
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    42
    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    43
  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    44
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    45
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    46
(* Given a list of variables that were bound, and a that has been
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    47
instantiated with free variable placeholders for the bound vars, it
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    48
creates an abstracted version of the theorem, with local bound vars as
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    49
lambda-params:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    50
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    51
Ts:
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    52
("x", ty)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    53
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    54
rule::
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    55
C :x ==> P :x = Q :x
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    56
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    57
results in:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    58
("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    59
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    60
note: assumes rule is instantiated
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    61
*)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    62
(* 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
    63
fun mk_abstractedrule ctxt TsFake Ts rule =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    64
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    65
    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    66
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    67
    (* now we change the names of temporary free vars that represent
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    68
       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
    69
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    70
    val ns =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    71
      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
    72
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    73
    val (fromnames, tonames, Ts') =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    74
      fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    75
              (cert (Free(faken,ty)) :: rnf,
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    76
               cert (Free(n2,ty)) :: rnt,
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    77
               (n2,ty) :: Ts''))
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    78
            (TsFake ~~ Ts ~~ ns) ([], [], []);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    79
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    80
    (* rename conflicting free's in the rule to avoid cconflicts
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    81
    with introduced vars from bounds outside in redex *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    82
    val rule' = rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    83
      |> Drule.forall_intr_list fromnames
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    84
      |> Drule.forall_elim_list tonames;
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
    85
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    86
    (* make unconditional rule and prems *)
52245
f76fb8858e0b tuned signature;
wenzelm
parents: 52242
diff changeset
    87
    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    88
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    89
    (* using these names create lambda-abstracted version of the rule *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    90
    val abstractions = rev (Ts' ~~ tonames);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    91
    val abstract_rule =
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
    92
      fold (fn ((n, ty), ct) => Thm.abstract_rule n ct)
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
    93
        abstractions uncond_rule;
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
    94
  in (cprems, abstract_rule) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    95
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    96
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    97
(* given names to avoid, and vars that need to be fixed, it gives
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    98
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
    99
variables *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   100
(* make fixed unique free variable instantiations for non-ground vars *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   101
(* 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
   102
      other uninstantiated vars in the hyps of the rule
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   103
      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
   104
fun mk_renamings ctxt tgt rule_inst =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   105
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   106
    val rule_conds = Thm.prems_of rule_inst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   107
    val (_, cond_vs) =
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   108
      fold (fn t => fn (tyvs, vs) =>
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   109
        (union (op =) (Misc_Legacy.term_tvars t) tyvs,
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   110
         union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []);
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   111
    val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   112
    val vars_to_fix = union (op =) termvars cond_vs;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   113
    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
   114
  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
   115
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   116
(* make a new fresh typefree instantiation for the given tvar *)
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   117
fun new_tfree (tv as (ix,sort)) (pairs, used) =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   118
  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   119
  in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   120
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   121
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   122
(* make instantiations to fix type variables that are not
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   123
   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
   124
fun mk_fixtvar_tyinsts ignore_insts ts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   125
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   126
    val ignore_ixs = map fst ignore_insts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   127
    val (tvars, tfrees) =
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   128
      fold_rev (fn t => fn (varixs, tfrees) =>
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   129
        (Misc_Legacy.add_term_tvars (t,varixs),
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   130
         Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []);
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   131
    val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   132
    val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees)
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   133
  in (fixtyinsts, tfrees) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   134
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   135
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   136
(* cross-instantiate the instantiations - ie for each instantiation
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   137
replace all occurances in other instantiations - no loops are possible
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   138
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
   139
fun cross_inst insts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   140
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   141
    fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) =>
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   142
      (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   143
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   144
    fun cross_instL ([], l) = rev l
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   145
      | cross_instL ((ix, t) :: insts, l) =
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   146
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   147
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   148
  in cross_instL (insts, []) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   149
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   150
(* 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
   151
fun cross_inst_typs insts =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   152
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   153
    fun instL (ix, (srt,ty)) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   154
      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
   155
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   156
    fun cross_instL ([], l) = rev l
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   157
      | cross_instL ((ix, t) :: insts, l) =
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   158
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   159
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   160
  in cross_instL (insts, []) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   161
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   162
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   163
(* assume that rule and target_thm have distinct var names. THINK:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   164
efficient version with tables for vars for: target vars, introduced
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   165
vars, and rule vars, for quicker instantiation?  The outerterm defines
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   166
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
   167
upterm order, ie last abstraction first., and with an outeterm where
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   168
the abstracted subterm has the arguments in the revered order, ie
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   169
first abstraction first.  FakeTs has abstractions using the fake name
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   170
- ie the name distinct from all other abstractions. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   171
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
   172
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   173
  let
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   174
    val thy = Thm.theory_of_thm target_thm;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   175
    val cert = Thm.cterm_of thy;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   176
    val certT = Thm.ctyp_of thy;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   177
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   178
    (* fix all non-instantiated tvars *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   179
    val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   180
      mk_fixtvar_tyinsts nonfixed_typinsts
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   181
        [Thm.prop_of rule, Thm.prop_of target_thm];
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   182
    val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   183
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   184
    (* certified instantiations for types *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   185
    val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   186
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   187
    (* type instantiated versions *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   188
    val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   189
    val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   190
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   191
    val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   192
    (* type instanitated outer term *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   193
    val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   194
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   195
    val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   196
    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
   197
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   198
    (* type-instantiate the var instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   199
    val insts_tyinst =
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   200
      fold_rev (fn (ix, (ty, t)) => fn insts_tyinst =>
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   201
        (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t))
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   202
          :: insts_tyinst) unprepinsts [];
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   203
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   204
    (* cross-instantiate *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   205
    val insts_tyinst_inst = cross_inst insts_tyinst;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   206
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   207
    (* create certms of instantiations *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   208
    val cinsts_tyinst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   209
      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
   210
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   211
    (* The instantiated rule *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   212
    val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   213
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   214
    (* Create a table of vars to be renamed after instantiation - ie
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   215
    other uninstantiated vars in the hyps the *instantiated* rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   216
    ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   217
    val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   218
    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
   219
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   220
    (* Create the specific version of the rule for this target application *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   221
    val outerterm_inst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   222
      outerterm_tyinst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   223
      |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   224
      |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   225
    val couter_inst = Thm.reflexive (cert outerterm_inst);
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   226
    val (cprems, abstract_rule_inst) =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   227
      rule_inst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   228
      |> Thm.instantiate ([], cterm_renamings)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   229
      |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   230
    val specific_tgt_rule =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   231
      Conv.fconv_rule Drule.beta_eta_conversion
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   232
        (Thm.combination couter_inst abstract_rule_inst);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   233
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   234
    (* create an instantiated version of the target thm *)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   235
    val tgt_th_inst =
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   236
      tgt_th_tyinst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   237
      |> Thm.instantiate ([], cinsts_tyinst)
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   238
      |> Thm.instantiate ([], cterm_renamings);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   239
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   240
    val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   241
  in
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   242
    Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   243
    |> Thm.equal_elim specific_tgt_rule
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   244
    |> Drule.implies_intr_list cprems
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   245
    |> Drule.forall_intr_list frees_of_fixed_vars
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   246
    |> Drule.forall_elim_list vars
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   247
    |> Thm.varifyT_global' othertfrees
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   248
    |-> K Drule.zero_var_indexes
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   249
  end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   250
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44121
diff changeset
   251
end;