src/Provers/eqsubst.ML
author wenzelm
Mon Jun 12 21:19:00 2006 +0200 (2006-06-12)
changeset 19861 620d90091788
parent 19835 81d6dc597559
child 19871 88e8f6173bab
permissions -rw-r--r--
tuned Seq/Envir/Unify interfaces;
     1 (*  Title:      Provers/eqsubst.ML
     2     ID:         $Id$
     3     Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
     4 
     5 A proof method to perform a substiution using an equation.
     6 *)
     7 
     8 signature EQSUBST =
     9 sig
    10   val setup : theory -> theory
    11 end;
    12 
    13 structure EqSubst
    14 (* : EQSUBST *)
    15 = struct
    16 
    17 structure Z = Zipper;
    18 
    19 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
    20 fun prep_meta_eq ctxt =
    21   let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
    22   in mk #> map Drule.zero_var_indexes end;
    23 
    24 
    25   (* a type abriviation for match information *)
    26   type match =
    27        ((indexname * (sort * typ)) list (* type instantiations *)
    28         * (indexname * (typ * term)) list) (* term instantiations *)
    29        * (string * typ) list (* fake named type abs env *)
    30        * (string * typ) list (* type abs env *)
    31        * term (* outer term *)
    32 
    33   type searchinfo =
    34        theory
    35        * int (* maxidx *)
    36        * Zipper.T (* focusterm to search under *)
    37 
    38 
    39 (* skipping non-empty sub-sequences but when we reach the end
    40    of the seq, remembering how much we have left to skip. *)
    41 datatype 'a skipseq = SkipMore of int
    42   | SkipSeq of 'a Seq.seq Seq.seq;
    43 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
    44 fun skipto_skipseq m s = 
    45     let 
    46       fun skip_occs n sq = 
    47           case Seq.pull sq of 
    48             NONE => SkipMore n
    49           | SOME (h,t) => 
    50             (case Seq.pull h of NONE => skip_occs n t
    51              | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
    52                          else skip_occs (n - 1) t)
    53     in (skip_occs m s) end;
    54 
    55 (* note: outerterm is the taget with the match replaced by a bound 
    56          variable : ie: "P lhs" beocmes "%x. P x" 
    57          insts is the types of instantiations of vars in lhs
    58          and typinsts is the type instantiations of types in the lhs
    59          Note: Final rule is the rule lifted into the ontext of the 
    60          taget thm. *)
    61 fun mk_foo_match mkuptermfunc Ts t = 
    62     let 
    63       val ty = Term.type_of t
    64       val bigtype = (rev (map snd Ts)) ---> ty
    65       fun mk_foo 0 t = t
    66         | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
    67       val num_of_bnds = (length Ts)
    68       (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
    69       val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
    70     in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
    71 
    72 (* T is outer bound vars, n is number of locally bound vars *)
    73 (* THINK: is order of Ts correct...? or reversed? *)
    74 fun fakefree_badbounds Ts t = 
    75     let val (FakeTs,Ts,newnames) = 
    76             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
    77                            let val newname = Term.variant usednames n
    78                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
    79                                (newname,ty)::Ts, 
    80                                newname::usednames) end)
    81                        ([],[],[])
    82                        Ts
    83     in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
    84 
    85 (* before matching we need to fake the bound vars that are missing an
    86 abstraction. In this function we additionally construct the
    87 abstraction environment, and an outer context term (with the focus
    88 abstracted out) for use in rewriting with RWInst.rw *)
    89 fun prep_zipper_match z = 
    90     let 
    91       val t = Z.trm z  
    92       val c = Z.ctxt z
    93       val Ts = Z.C.nty_ctxt c
    94       val (FakeTs', Ts', t') = fakefree_badbounds Ts t
    95       val absterm = mk_foo_match (Z.C.apply c) Ts' t'
    96     in
    97       (t', (FakeTs', Ts', absterm))
    98     end;
    99 
   100 (* Matching and Unification with exception handled *)
   101 fun clean_match thy (a as (pat, t)) =
   102   let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   103   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   104   end handle Pattern.MATCH => NONE;
   105 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   106 fun clean_unify sgn ix (a as (pat, tgt)) =
   107     let
   108       (* type info will be re-derived, maybe this can be cached
   109          for efficiency? *)
   110       val pat_ty = Term.type_of pat;
   111       val tgt_ty = Term.type_of tgt;
   112       (* is it OK to ignore the type instantiation info?
   113          or should I be using it? *)
   114       val typs_unify =
   115           SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
   116             handle Type.TUNIFY => NONE;
   117     in
   118       case typs_unify of
   119         SOME (typinsttab, ix2) =>
   120         let
   121       (* is it right to throw away the flexes?
   122          or should I be using them somehow? *)
   123           fun mk_insts env =
   124             (Vartab.dest (Envir.type_env env),
   125              Envir.alist_of env);
   126           val initenv = Envir.Envir {asol = Vartab.empty,
   127                                      iTs = typinsttab, maxidx = ix2};
   128           val useq = Unify.smash_unifiers sgn [a] initenv
   129 	            handle UnequalLengths => Seq.empty
   130 		               | Term.TERM _ => Seq.empty;
   131           fun clean_unify' useq () =
   132               (case (Seq.pull useq) of
   133                  NONE => NONE
   134                | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   135 	      handle UnequalLengths => NONE
   136                    | Term.TERM _ => NONE;
   137         in
   138           (Seq.make (clean_unify' useq))
   139         end
   140       | NONE => Seq.empty
   141     end;
   142 
   143 (* Matching and Unification for zippers *)
   144 (* Note: Ts is a modified version of the original names of the outer
   145 bound variables. New names have been introduced to make sure they are
   146 unique w.r.t all names in the term and each other. usednames' is
   147 oldnames + new names. *)
   148 fun clean_match_z thy pat z = 
   149     let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   150       case clean_match thy (pat, t) of 
   151         NONE => NONE 
   152       | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   153 (* ix = max var index *)
   154 fun clean_unify_z sgn ix pat z = 
   155     let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   156     Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   157             (clean_unify sgn ix (t, pat)) end;
   158 
   159 
   160 (* FOR DEBUGGING...
   161 type trace_subst_errT = int (* subgoal *)
   162         * thm (* thm with all goals *)
   163         * (Thm.cterm list (* certified free var placeholders for vars *)
   164            * thm)  (* trivial thm of goal concl *)
   165             (* possible matches/unifiers *)
   166         * thm (* rule *)
   167         * (((indexname * typ) list (* type instantiations *)
   168               * (indexname * term) list ) (* term instantiations *)
   169              * (string * typ) list (* Type abs env *)
   170              * term) (* outer term *);
   171 
   172 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
   173 val trace_subst_search = ref false;
   174 exception trace_subst_exp of trace_subst_errT;
   175 *)
   176 
   177 
   178 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   179   | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   180   | bot_left_leaf_of x = x;
   181 
   182 fun valid_match_start z =
   183     (case bot_left_leaf_of (Z.trm z) of 
   184        Const _ => true
   185      | Free _ => true
   186      | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
   187      | _ => false); (* avoid vars - always suceeds uninterestingly. *)
   188                       
   189 (* search from top, left to right, then down *)
   190 val search_tlr_all = ZipperSearch.all_td_lr;
   191 
   192 (* search from top, left to right, then down *)
   193 fun search_tlr_valid validf =
   194     let 
   195       fun sf_valid_td_lr z = 
   196           let val here = if validf z then [Z.Here z] else [] in
   197             case Z.trm z 
   198              of _ $ _ => here @ [Z.LookIn (Z.move_down_left z),
   199                                  Z.LookIn (Z.move_down_right z)]
   200               | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
   201               | _ => here
   202           end;
   203     in Z.lzy_search sf_valid_td_lr end;
   204 
   205 (* search all unifications *)
   206 fun searchf_tlr_unify_all (sgn, maxidx, z) lhs =
   207     Seq.map (clean_unify_z sgn maxidx lhs) 
   208             (Z.limit_apply search_tlr_all z);
   209 
   210 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
   211 fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs  =
   212     Seq.map (clean_unify_z sgn maxidx lhs) 
   213             (Z.limit_apply (search_tlr_valid valid_match_start) z);
   214 
   215 
   216 (* apply a substitution in the conclusion of the theorem th *)
   217 (* cfvs are certified free var placeholders for goal params *)
   218 (* conclthm is a theorem of for just the conclusion *)
   219 (* m is instantiation/match information *)
   220 (* rule is the equation for substitution *)
   221 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   222     (RWInst.rw m rule conclthm)
   223       |> IsaND.unfix_frees cfvs
   224       |> RWInst.beta_eta_contract
   225       |> (fn r => Tactic.rtac r i th);
   226 
   227 (* substitute within the conclusion of goal i of gth, using a meta
   228 equation rule. Note that we assume rule has var indicies zero'd *)
   229 fun prep_concl_subst i gth =
   230     let
   231       val th = Thm.incr_indexes 1 gth;
   232       val tgt_term = Thm.prop_of th;
   233 
   234       val sgn = Thm.sign_of_thm th;
   235       val ctermify = Thm.cterm_of sgn;
   236       val trivify = Thm.trivial o ctermify;
   237 
   238       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   239       val cfvs = rev (map ctermify fvs);
   240 
   241       val conclterm = Logic.strip_imp_concl fixedbody;
   242       val conclthm = trivify conclterm;
   243       val maxidx = Term.maxidx_of_term conclterm;
   244       val ft = ((Z.move_down_right (* ==> *)
   245                  o Z.move_down_left (* Trueprop *)
   246                  o Z.mktop
   247                  o Thm.prop_of) conclthm)
   248     in
   249       ((cfvs, conclthm), (sgn, maxidx, ft))
   250     end;
   251 
   252 (* substitute using an object or meta level equality *)
   253 fun eqsubst_tac' ctxt searchf instepthm i th =
   254     let
   255       val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   256       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   257       fun rewrite_with_thm r =
   258           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   259           in searchf searchinfo lhs
   260              |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   261     in stepthms |> Seq.maps rewrite_with_thm end;
   262 
   263 
   264 (* distinct subgoals *)
   265 fun distinct_subgoals th =
   266   the_default th (SINGLE distinct_subgoals_tac th);
   267 
   268 (* General substitution of multiple occurances using one of
   269    the given theorems*)
   270 
   271 
   272 exception eqsubst_occL_exp of
   273           string * (int list) * (thm list) * int * thm;
   274 fun skip_first_occs_search occ srchf sinfo lhs =
   275     case (skipto_skipseq occ (srchf sinfo lhs)) of
   276       SkipMore _ => Seq.empty
   277     | SkipSeq ss => Seq.flat ss;
   278 
   279 fun eqsubst_tac ctxt occL thms i th =
   280     let val nprems = Thm.nprems_of th in
   281       if nprems < i then Seq.empty else
   282       let val thmseq = (Seq.of_list thms)
   283         fun apply_occ occ th =
   284             thmseq |> Seq.maps
   285                     (fn r => eqsubst_tac' 
   286                                ctxt 
   287                                (skip_first_occs_search
   288                                   occ searchf_tlr_unify_valid) r
   289                                  (i + ((Thm.nprems_of th) - nprems))
   290                                  th);
   291         val sortedoccL =
   292             Library.sort (Library.rev_order o Library.int_ord) occL;
   293       in
   294         Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   295       end
   296     end
   297     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   298 
   299 
   300 (* inthms are the given arguments in Isar, and treated as eqstep with
   301    the first one, then the second etc *)
   302 fun eqsubst_meth ctxt occL inthms =
   303     Method.METHOD
   304       (fn facts =>
   305           HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
   306 
   307 (* apply a substitution inside assumption j, keeps asm in the same place *)
   308 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   309     let
   310       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   311       val preelimrule =
   312           (RWInst.rw m rule pth)
   313             |> (Seq.hd o Tactic.prune_params_tac)
   314             |> Thm.permute_prems 0 ~1 (* put old asm first *)
   315             |> IsaND.unfix_frees cfvs (* unfix any global params *)
   316             |> RWInst.beta_eta_contract; (* normal form *)
   317   (*    val elimrule =
   318           preelimrule
   319             |> Tactic.make_elim (* make into elim rule *)
   320             |> Thm.lift_rule (th2, i); (* lift into context *)
   321    *)
   322     in
   323       (* ~j because new asm starts at back, thus we subtract 1 *)
   324       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   325       (Tactic.dtac preelimrule i th2)
   326 
   327       (* (Thm.bicompose
   328                  false (* use unification *)
   329                  (true, (* elim resolution *)
   330                   elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   331                  i th2) *)
   332     end;
   333 
   334 
   335 (* prepare to substitute within the j'th premise of subgoal i of gth,
   336 using a meta-level equation. Note that we assume rule has var indicies
   337 zero'd. Note that we also assume that premt is the j'th premice of
   338 subgoal i of gth. Note the repetition of work done for each
   339 assumption, i.e. this can be made more efficient for search over
   340 multiple assumptions.  *)
   341 fun prep_subst_in_asm i gth j =
   342     let
   343       val th = Thm.incr_indexes 1 gth;
   344       val tgt_term = Thm.prop_of th;
   345 
   346       val sgn = Thm.sign_of_thm th;
   347       val ctermify = Thm.cterm_of sgn;
   348       val trivify = Thm.trivial o ctermify;
   349 
   350       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   351       val cfvs = rev (map ctermify fvs);
   352 
   353       val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   354       val asm_nprems = length (Logic.strip_imp_prems asmt);
   355 
   356       val pth = trivify asmt;
   357       val maxidx = Term.maxidx_of_term asmt;
   358 
   359       val ft = ((Z.move_down_right (* trueprop *)
   360                  o Z.mktop
   361                  o Thm.prop_of) pth)
   362     in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   363 
   364 (* prepare subst in every possible assumption *)
   365 fun prep_subst_in_asms i gth =
   366     map (prep_subst_in_asm i gth)
   367         ((fn l => Library.upto (1, length l))
   368            (Logic.prems_of_goal (Thm.prop_of gth) i));
   369 
   370 
   371 (* substitute in an assumption using an object or meta level equality *)
   372 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   373     let
   374       val asmpreps = prep_subst_in_asms i th;
   375       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   376       fun rewrite_with_thm r =
   377           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   378             fun occ_search occ [] = Seq.empty
   379               | occ_search occ ((asminfo, searchinfo)::moreasms) =
   380                 (case searchf searchinfo occ lhs of
   381                    SkipMore i => occ_search i moreasms
   382                  | SkipSeq ss =>
   383                    Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   384                                (occ_search 1 moreasms))
   385                               (* find later substs also *)
   386           in
   387             occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   388           end;
   389     in stepthms |> Seq.maps rewrite_with_thm end;
   390 
   391 
   392 fun skip_first_asm_occs_search searchf sinfo occ lhs =
   393     skipto_skipseq occ (searchf sinfo lhs);
   394 
   395 fun eqsubst_asm_tac ctxt occL thms i th =
   396     let val nprems = Thm.nprems_of th
   397     in
   398       if nprems < i then Seq.empty else
   399       let val thmseq = (Seq.of_list thms)
   400         fun apply_occ occK th =
   401             thmseq |> Seq.maps
   402                     (fn r =>
   403                         eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   404                                             searchf_tlr_unify_valid) occK r
   405                                          (i + ((Thm.nprems_of th) - nprems))
   406                                          th);
   407         val sortedoccs =
   408             Library.sort (Library.rev_order o Library.int_ord) occL
   409       in
   410         Seq.map distinct_subgoals
   411                 (Seq.EVERY (map apply_occ sortedoccs) th)
   412       end
   413     end
   414     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   415 
   416 (* inthms are the given arguments in Isar, and treated as eqstep with
   417    the first one, then the second etc *)
   418 fun eqsubst_asm_meth ctxt occL inthms =
   419     Method.METHOD
   420       (fn facts =>
   421           HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
   422 
   423 (* syntax for options, given "(asm)" will give back true, without
   424    gives back false *)
   425 val options_syntax =
   426     (Args.parens (Args.$$$ "asm") >> (K true)) ||
   427      (Scan.succeed false);
   428 
   429 val ith_syntax =
   430     (Args.parens (Scan.repeat Args.nat))
   431       || (Scan.succeed [0]);
   432 
   433 (* combination method that takes a flag (true indicates that subst
   434 should be done to an assumption, false = apply to the conclusion of
   435 the goal) as well as the theorems to use *)
   436 fun subst_meth src =
   437   Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   438   #> (fn (ctxt, ((asmflag, occL), inthms)) =>
   439     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   440 
   441 
   442 val setup =
   443   Method.add_method ("subst", subst_meth, "single-step substitution");
   444 
   445 end;