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