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