src/Tools/IsaPlanner/rw_inst.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 23175 267ba70e7a9d
child 29265 5b4247055bd7
permissions -rw-r--r--
simplified interfaces for outer syntax;
     1 (*  Title:      Tools/IsaPlanner/rw_inst.ML
     2     ID:         $Id$
     3     Author:     Lucas Dixon, University of Edinburgh
     4 
     5 Rewriting using a conditional meta-equality theorem which supports
     6 schematic variable instantiation.
     7 *)   
     8 
     9 signature RW_INST =
    10 sig
    11 
    12   (* Rewrite: give it instantiation infromation, a rule, and the
    13   target thm, and it will return the rewritten target thm *)
    14   val rw :
    15       ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
    16        (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
    17       * (string * Term.typ) list           (* Fake named bounds + types *)
    18       * (string * Term.typ) list           (* names of bound + types *)
    19       * Term.term ->                       (* outer term for instantiation *)
    20       Thm.thm ->                           (* rule with indexies lifted *)
    21       Thm.thm ->                           (* target thm *)
    22       Thm.thm                              (* rewritten theorem possibly 
    23                                               with additional premises for 
    24                                               rule conditions *)
    25 
    26   (* used tools *)
    27   val mk_abstractedrule :
    28       (string * Term.typ) list (* faked outer bound *)
    29       -> (string * Term.typ) list (* hopeful name of outer bounds *)
    30       -> Thm.thm -> Thm.cterm list * Thm.thm
    31   val mk_fixtvar_tyinsts :
    32       (Term.indexname * (Term.sort * Term.typ)) list ->
    33       Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
    34                         * (string * Term.sort) list
    35   val mk_renamings :
    36       Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
    37   val new_tfree :
    38       ((string * int) * Term.sort) *
    39       (((string * int) * (Term.sort * Term.typ)) list * string list) ->
    40       ((string * int) * (Term.sort * Term.typ)) list * string list
    41   val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
    42                    -> (Term.indexname *(Term.typ * Term.term)) list
    43   val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
    44                    -> (Term.indexname * (Term.sort * Term.typ)) list
    45 
    46   val beta_contract : Thm.thm -> Thm.thm
    47   val beta_eta_contract : Thm.thm -> Thm.thm
    48 
    49 end;
    50 
    51 structure RWInst 
    52 : RW_INST
    53 = struct
    54 
    55 
    56 (* beta contract the theorem *)
    57 fun beta_contract thm = 
    58     equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    59 
    60 (* beta-eta contract the theorem *)
    61 fun beta_eta_contract thm = 
    62     let
    63       val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    64       val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    65     in thm3 end;
    66 
    67 
    68 (* to get the free names of a theorem (including hyps and flexes) *)
    69 fun usednames_of_thm th =
    70     let val rep = Thm.rep_thm th
    71       val hyps = #hyps rep
    72       val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    73       val prop = #prop rep
    74     in
    75       List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    76     end;
    77 
    78 (* Given a list of variables that were bound, and a that has been
    79 instantiated with free variable placeholders for the bound vars, it
    80 creates an abstracted version of the theorem, with local bound vars as
    81 lambda-params:
    82 
    83 Ts: 
    84 ("x", ty)
    85 
    86 rule::
    87 C :x ==> P :x = Q :x
    88 
    89 results in:
    90 ("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
    91 
    92 note: assumes rule is instantiated
    93 *)
    94 (* Note, we take abstraction in the order of last abstraction first *)
    95 fun mk_abstractedrule TsFake Ts rule = 
    96     let 
    97       val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
    98 
    99       (* now we change the names of temporary free vars that represent 
   100          bound vars with binders outside the redex *)
   101       val prop = Thm.prop_of rule;
   102       val names = usednames_of_thm rule;
   103       val (fromnames,tonames,names2,Ts') = 
   104           Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   105                     let val n2 = Name.variant names n in
   106                       (ctermify (Free(faken,ty)) :: rnf,
   107                        ctermify (Free(n2,ty)) :: rnt, 
   108                        n2 :: names,
   109                        (n2,ty) :: Ts'')
   110                     end)
   111                 (([],[],names, []), TsFake~~Ts);
   112 
   113       (* rename conflicting free's in the rule to avoid cconflicts
   114       with introduced vars from bounds outside in redex *)
   115       val rule' = rule |> Drule.forall_intr_list fromnames
   116                        |> Drule.forall_elim_list tonames;
   117       
   118       (* make unconditional rule and prems *)
   119       val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
   120                                                           rule';
   121 
   122       (* using these names create lambda-abstracted version of the rule *)
   123       val abstractions = rev (Ts' ~~ tonames);
   124       val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
   125                                     Thm.abstract_rule n ct th)
   126                                 (uncond_rule, abstractions);
   127     in (cprems, abstract_rule) end;
   128 
   129 
   130 (* given names to avoid, and vars that need to be fixed, it gives
   131 unique new names to the vars so that they can be fixed as free
   132 variables *)
   133 (* make fixed unique free variable instantiations for non-ground vars *)
   134 (* Create a table of vars to be renamed after instantiation - ie
   135       other uninstantiated vars in the hyps of the rule 
   136       ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   137 fun mk_renamings tgt rule_inst = 
   138     let
   139       val rule_conds = Thm.prems_of rule_inst
   140       val names = foldr Term.add_term_names [] (tgt :: rule_conds);
   141       val (conds_tyvs,cond_vs) = 
   142           Library.foldl (fn ((tyvs, vs), t) => 
   143                     (Library.union
   144                        (Term.term_tvars t, tyvs),
   145                      Library.union 
   146                        (map Term.dest_Var (Term.term_vars t), vs))) 
   147                 (([],[]), rule_conds);
   148       val termvars = map Term.dest_Var (Term.term_vars tgt); 
   149       val vars_to_fix = Library.union (termvars, cond_vs);
   150       val (renamings, names2) = 
   151           foldr (fn (((n,i),ty), (vs, names')) => 
   152                     let val n' = Name.variant names' n in
   153                       ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   154                     end)
   155                 ([], names) vars_to_fix;
   156     in renamings end;
   157 
   158 (* make a new fresh typefree instantiation for the given tvar *)
   159 fun new_tfree (tv as (ix,sort), (pairs,used)) =
   160       let val v = Name.variant used (string_of_indexname ix)
   161       in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   162 
   163 
   164 (* make instantiations to fix type variables that are not 
   165    already instantiated (in ignore_ixs) from the list of terms. *)
   166 fun mk_fixtvar_tyinsts ignore_insts ts = 
   167     let 
   168       val ignore_ixs = map fst ignore_insts;
   169       val (tvars, tfrees) = 
   170             foldr (fn (t, (varixs, tfrees)) => 
   171                       (Term.add_term_tvars (t,varixs),
   172                        Term.add_term_tfrees (t,tfrees)))
   173                   ([],[]) ts;
   174         val unfixed_tvars = 
   175             List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   176         val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
   177     in (fixtyinsts, tfrees) end;
   178 
   179 
   180 (* cross-instantiate the instantiations - ie for each instantiation
   181 replace all occurances in other instantiations - no loops are possible
   182 and thus only one-parsing of the instantiations is necessary. *)
   183 fun cross_inst insts = 
   184     let 
   185       fun instL (ix, (ty,t)) = 
   186           map (fn (ix2,(ty2,t2)) => 
   187                   (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   188 
   189       fun cross_instL ([], l) = rev l
   190         | cross_instL ((ix, t) :: insts, l) = 
   191           cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   192 
   193     in cross_instL (insts, []) end;
   194 
   195 (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   196 fun cross_inst_typs insts = 
   197     let 
   198       fun instL (ix, (srt,ty)) = 
   199           map (fn (ix2,(srt2,ty2)) => 
   200                   (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   201 
   202       fun cross_instL ([], l) = rev l
   203         | cross_instL ((ix, t) :: insts, l) = 
   204           cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   205 
   206     in cross_instL (insts, []) end;
   207 
   208 
   209 (* assume that rule and target_thm have distinct var names. THINK:
   210 efficient version with tables for vars for: target vars, introduced
   211 vars, and rule vars, for quicker instantiation?  The outerterm defines
   212 which part of the target_thm was modified.  Note: we take Ts in the
   213 upterm order, ie last abstraction first., and with an outeterm where
   214 the abstracted subterm has the arguments in the revered order, ie
   215 first abstraction first.  FakeTs has abstractions using the fake name
   216 - ie the name distinct from all other abstractions. *)
   217 
   218 fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
   219     let 
   220       (* general signature info *)
   221       val target_sign = (Thm.theory_of_thm target_thm);
   222       val ctermify = Thm.cterm_of target_sign;
   223       val ctypeify = Thm.ctyp_of target_sign;
   224 
   225       (* fix all non-instantiated tvars *)
   226       val (fixtyinsts, othertfrees) = 
   227           mk_fixtvar_tyinsts nonfixed_typinsts
   228                              [Thm.prop_of rule, Thm.prop_of target_thm];
   229       val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
   230                                fixtyinsts;
   231       val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   232 
   233       (* certified instantiations for types *)
   234       val ctyp_insts = 
   235           map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
   236               typinsts;
   237 
   238       (* type instantiated versions *)
   239       val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   240       val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   241 
   242       val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
   243       (* type instanitated outer term *)
   244       val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   245 
   246       val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   247                               FakeTs;
   248       val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   249                           Ts;
   250 
   251       (* type-instantiate the var instantiations *)
   252       val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   253                             (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   254                                   Term.subst_TVars term_typ_inst t))
   255                             :: insts_tyinst)
   256                         [] unprepinsts;
   257 
   258       (* cross-instantiate *)
   259       val insts_tyinst_inst = cross_inst insts_tyinst;
   260 
   261       (* create certms of instantiations *)
   262       val cinsts_tyinst = 
   263           map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
   264                                   ctermify t)) insts_tyinst_inst;
   265 
   266       (* The instantiated rule *)
   267       val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   268 
   269       (* Create a table of vars to be renamed after instantiation - ie
   270       other uninstantiated vars in the hyps the *instantiated* rule 
   271       ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   272       val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
   273                                    rule_inst;
   274       val cterm_renamings = 
   275           map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   276 
   277       (* Create the specific version of the rule for this target application *)
   278       val outerterm_inst = 
   279           outerterm_tyinst 
   280             |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   281             |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   282       val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   283       val (cprems, abstract_rule_inst) = 
   284           rule_inst |> Thm.instantiate ([], cterm_renamings)
   285                     |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   286       val specific_tgt_rule = 
   287           beta_eta_contract
   288             (Thm.combination couter_inst abstract_rule_inst);
   289 
   290       (* create an instantiated version of the target thm *)
   291       val tgt_th_inst = 
   292           tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   293                         |> Thm.instantiate ([], cterm_renamings);
   294 
   295       val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   296 
   297     in
   298       (beta_eta_contract tgt_th_inst)
   299         |> Thm.equal_elim specific_tgt_rule
   300         |> Drule.implies_intr_list cprems
   301         |> Drule.forall_intr_list frees_of_fixed_vars
   302         |> Drule.forall_elim_list vars
   303         |> Thm.varifyT' othertfrees
   304         |-> K Drule.zero_var_indexes
   305     end;
   306 
   307 
   308 end; (* struct *)