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