src/Pure/IsaPlanner/rw_inst.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 16179 fa7e70be26b0
child 18127 9f03d8a9a81b
permissions -rw-r--r--
introduced some new-style AList operations
     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 (* Given a list of variables that were bound, and a that has been
    75 instantiated with free variable placeholders for the bound vars, it
    76 creates an abstracted version of the theorem, with local bound vars as
    77 lambda-params:
    78 
    79 Ts: 
    80 ("x", ty)
    81 
    82 rule::
    83 C :x ==> P :x = Q :x
    84 
    85 results in:
    86 ("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
    87 
    88 note: assumes rule is instantiated
    89 *)
    90 (* Note, we take abstraction in the order of last abstraction first *)
    91 fun mk_abstractedrule TsFake Ts rule = 
    92     let 
    93       val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
    94 
    95       (* now we change the names of temporary free vars that represent 
    96          bound vars with binders outside the redex *)
    97       val prop = Thm.prop_of rule;
    98       val names = TermLib.usednames_of_thm rule;
    99       val (fromnames,tonames,names2,Ts') = 
   100           Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   101                     let val n2 = Term.variant names n in
   102                       (ctermify (Free(faken,ty)) :: rnf,
   103                        ctermify (Free(n2,ty)) :: rnt, 
   104                        n2 :: names,
   105                        (n2,ty) :: Ts'')
   106                     end)
   107                 (([],[],names, []), TsFake~~Ts);
   108 
   109       (* rename conflicting free's in the rule to avoid cconflicts
   110       with introduced vars from bounds outside in redex *)
   111       val rule' = rule |> Drule.forall_intr_list fromnames
   112                        |> Drule.forall_elim_list tonames;
   113       
   114       (* make unconditional rule and prems *)
   115       val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
   116                                                           rule';
   117 
   118       (* using these names create lambda-abstracted version of the rule *)
   119       val abstractions = rev (Ts' ~~ tonames);
   120       val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
   121                                     Thm.abstract_rule n ct th)
   122                                 (uncond_rule, abstractions);
   123     in (cprems, abstract_rule) end;
   124 
   125 
   126 (* given names to avoid, and vars that need to be fixed, it gives
   127 unique new names to the vars so that they can be fixed as free
   128 variables *)
   129 (* make fixed unique free variable instantiations for non-ground vars *)
   130 (* Create a table of vars to be renamed after instantiation - ie
   131       other uninstantiated vars in the hyps of the rule 
   132       ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   133 fun mk_renamings tgt rule_inst = 
   134     let
   135       val rule_conds = Thm.prems_of rule_inst
   136       val names = foldr Term.add_term_names [] (tgt :: rule_conds);
   137       val (conds_tyvs,cond_vs) = 
   138           Library.foldl (fn ((tyvs, vs), t) => 
   139                     (Library.union
   140                        (Term.term_tvars t, tyvs),
   141                      Library.union 
   142                        (map Term.dest_Var (Term.term_vars t), vs))) 
   143                 (([],[]), rule_conds);
   144       val termvars = map Term.dest_Var (Term.term_vars tgt); 
   145       val vars_to_fix = Library.union (termvars, cond_vs);
   146       val (renamings, names2) = 
   147           foldr (fn (((n,i),ty), (vs, names')) => 
   148                     let val n' = Term.variant names' n in
   149                       ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   150                     end)
   151                 ([], names) vars_to_fix;
   152     in renamings end;
   153 
   154 (* make a new fresh typefree instantiation for the given tvar *)
   155 fun new_tfree (tv as (ix,sort), (pairs,used)) =
   156       let val v = variant used (string_of_indexname ix)
   157       in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   158 
   159 
   160 (* make instantiations to fix type variables that are not 
   161    already instantiated (in ignore_ixs) from the list of terms. *)
   162 fun mk_fixtvar_tyinsts ignore_insts ts = 
   163     let 
   164       val ignore_ixs = map fst ignore_insts;
   165       val (tvars, tfrees) = 
   166             foldr (fn (t, (varixs, tfrees)) => 
   167                       (Term.add_term_tvars (t,varixs),
   168                        Term.add_term_tfrees (t,tfrees)))
   169                   ([],[]) ts;
   170         val unfixed_tvars = 
   171             List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
   172         val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
   173     in (fixtyinsts, tfrees) end;
   174 
   175 
   176 (* cross-instantiate the instantiations - ie for each instantiation
   177 replace all occurances in other instantiations - no loops are possible
   178 and thus only one-parsing of the instantiations is necessary. *)
   179 fun cross_inst insts = 
   180     let 
   181       fun instL (ix, (ty,t)) = 
   182           map (fn (ix2,(ty2,t2)) => 
   183                   (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   184 
   185       fun cross_instL ([], l) = rev l
   186         | cross_instL ((ix, t) :: insts, l) = 
   187           cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   188 
   189     in cross_instL (insts, []) end;
   190 
   191 (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   192 fun cross_inst_typs insts = 
   193     let 
   194       fun instL (ix, (srt,ty)) = 
   195           map (fn (ix2,(srt2,ty2)) => 
   196                   (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   197 
   198       fun cross_instL ([], l) = rev l
   199         | cross_instL ((ix, t) :: insts, l) = 
   200           cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   201 
   202     in cross_instL (insts, []) end;
   203 
   204 
   205 (* assume that rule and target_thm have distinct var names. THINK:
   206 efficient version with tables for vars for: target vars, introduced
   207 vars, and rule vars, for quicker instantiation?  The outerterm defines
   208 which part of the target_thm was modified.  Note: we take Ts in the
   209 upterm order, ie last abstraction first., and with an outeterm where
   210 the abstracted subterm has the arguments in the revered order, ie
   211 first abstraction first.  FakeTs has abstractions using the fake name
   212 - ie the name distinct from all other abstractions. *)
   213 
   214 fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
   215     let 
   216       (* general signature info *)
   217       val target_sign = (Thm.sign_of_thm target_thm);
   218       val ctermify = Thm.cterm_of target_sign;
   219       val ctypeify = Thm.ctyp_of target_sign;
   220 
   221       (* fix all non-instantiated tvars *)
   222       val (fixtyinsts, othertfrees) = 
   223           mk_fixtvar_tyinsts nonfixed_typinsts
   224                              [Thm.prop_of rule, Thm.prop_of target_thm];
   225       val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
   226                                fixtyinsts;
   227       val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   228 
   229       (* certified instantiations for types *)
   230       val ctyp_insts = 
   231           map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
   232               typinsts;
   233 
   234       (* type instantiated versions *)
   235       val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   236       val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   237 
   238       val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
   239       (* type instanitated outer term *)
   240       val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   241 
   242       val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   243                               FakeTs;
   244       val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   245                           Ts;
   246 
   247       (* type-instantiate the var instantiations *)
   248       val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   249                             (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   250                                   Term.subst_TVars term_typ_inst t))
   251                             :: insts_tyinst)
   252                         [] unprepinsts;
   253 
   254       (* cross-instantiate *)
   255       val insts_tyinst_inst = cross_inst insts_tyinst;
   256 
   257       (* create certms of instantiations *)
   258       val cinsts_tyinst = 
   259           map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
   260                                   ctermify t)) insts_tyinst_inst;
   261 
   262       (* The instantiated rule *)
   263       val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   264 
   265       (* Create a table of vars to be renamed after instantiation - ie
   266       other uninstantiated vars in the hyps the *instantiated* rule 
   267       ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   268       val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
   269                                    rule_inst;
   270       val cterm_renamings = 
   271           map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   272 
   273       (* Create the specific version of the rule for this target application *)
   274       val outerterm_inst = 
   275           outerterm_tyinst 
   276             |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   277             |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   278       val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   279       val (cprems, abstract_rule_inst) = 
   280           rule_inst |> Thm.instantiate ([], cterm_renamings)
   281                     |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   282       val specific_tgt_rule = 
   283           beta_eta_contract
   284             (Thm.combination couter_inst abstract_rule_inst);
   285 
   286       (* create an instantiated version of the target thm *)
   287       val tgt_th_inst = 
   288           tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   289                         |> Thm.instantiate ([], cterm_renamings);
   290 
   291       val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   292 
   293     in
   294       (beta_eta_contract tgt_th_inst)
   295         |> Thm.equal_elim specific_tgt_rule
   296         |> Drule.implies_intr_list cprems
   297         |> Drule.forall_intr_list frees_of_fixed_vars
   298         |> Drule.forall_elim_list vars
   299         |> fst o Thm.varifyT' othertfrees
   300         |> Drule.zero_var_indexes
   301     end;
   302 
   303 
   304 end; (* struct *)