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