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