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