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