src/Provers/eqsubst.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18598 94d658871c98
child 18833 bead1a4e966b
permissions -rw-r--r--
setup: theory -> theory;
     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: EQSUBST =
    14 struct
    15 
    16 fun prep_meta_eq ctxt =
    17   let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
    18   in mk #> map Drule.zero_var_indexes end;
    19 
    20 
    21   (* a type abriviation for match information *)
    22   type match =
    23        ((indexname * (sort * typ)) list (* type instantiations *)
    24         * (indexname * (typ * term)) list) (* term instantiations *)
    25        * (string * typ) list (* fake named type abs env *)
    26        * (string * typ) list (* type abs env *)
    27        * term (* outer term *)
    28 
    29   type searchinfo =
    30        theory
    31        * int (* maxidx *)
    32        * BasicIsaFTerm.FcTerm (* focusterm to search under *)
    33 
    34 (* FOR DEBUGGING...
    35 type trace_subst_errT = int (* subgoal *)
    36         * thm (* thm with all goals *)
    37         * (Thm.cterm list (* certified free var placeholders for vars *)
    38            * thm)  (* trivial thm of goal concl *)
    39             (* possible matches/unifiers *)
    40         * thm (* rule *)
    41         * (((indexname * typ) list (* type instantiations *)
    42               * (indexname * term) list ) (* term instantiations *)
    43              * (string * typ) list (* Type abs env *)
    44              * term) (* outer term *);
    45 
    46 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
    47 val trace_subst_search = ref false;
    48 exception trace_subst_exp of trace_subst_errT;
    49  *)
    50 
    51 (* search from top, left to right, then down *)
    52 fun search_tlr_all_f f ft =
    53     let
    54       fun maux ft =
    55           let val t' = (IsaFTerm.focus_of_fcterm ft)
    56             (* val _ =
    57                 if !trace_subst_search then
    58                   (writeln ("Examining: " ^ (TermLib.string_of_term t'));
    59                    TermLib.writeterm t'; ())
    60                 else (); *)
    61           in
    62           (case t' of
    63             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
    64                        Seq.cons(f ft,
    65                                   maux (IsaFTerm.focus_right ft)))
    66           | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
    67           | leaf => Seq.single (f ft)) end
    68     in maux ft end;
    69 
    70 (* search from top, left to right, then down *)
    71 fun search_tlr_valid_f f ft =
    72     let
    73       fun maux ft =
    74           let
    75             val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
    76           in
    77           (case (IsaFTerm.focus_of_fcterm ft) of
    78             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
    79                        Seq.cons(hereseq,
    80                                   maux (IsaFTerm.focus_right ft)))
    81           | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
    82           | leaf => Seq.single (hereseq))
    83           end
    84     in maux ft end;
    85 
    86 (* search all unifications *)
    87 fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
    88     IsaFTerm.find_fcterm_matches
    89       search_tlr_all_f
    90       (IsaFTerm.clean_unify_ft sgn maxidx lhs)
    91       ft;
    92 
    93 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
    94 fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs  =
    95     IsaFTerm.find_fcterm_matches
    96       search_tlr_valid_f
    97       (IsaFTerm.clean_unify_ft sgn maxidx lhs)
    98       ft;
    99 
   100 
   101 (* apply a substitution in the conclusion of the theorem th *)
   102 (* cfvs are certified free var placeholders for goal params *)
   103 (* conclthm is a theorem of for just the conclusion *)
   104 (* m is instantiation/match information *)
   105 (* rule is the equation for substitution *)
   106 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   107     (RWInst.rw m rule conclthm)
   108       |> IsaND.unfix_frees cfvs
   109       |> RWInst.beta_eta_contract
   110       |> (fn r => Tactic.rtac r i th);
   111 
   112 (* substitute within the conclusion of goal i of gth, using a meta
   113 equation rule. Note that we assume rule has var indicies zero'd *)
   114 fun prep_concl_subst i gth =
   115     let
   116       val th = Thm.incr_indexes 1 gth;
   117       val tgt_term = Thm.prop_of th;
   118 
   119       val sgn = Thm.sign_of_thm th;
   120       val ctermify = Thm.cterm_of sgn;
   121       val trivify = Thm.trivial o ctermify;
   122 
   123       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   124       val cfvs = rev (map ctermify fvs);
   125 
   126       val conclterm = Logic.strip_imp_concl fixedbody;
   127       val conclthm = trivify conclterm;
   128       val maxidx = Term.maxidx_of_term conclterm;
   129       val ft = ((IsaFTerm.focus_right
   130                  o IsaFTerm.focus_left
   131                  o IsaFTerm.fcterm_of_term
   132                  o Thm.prop_of) conclthm)
   133     in
   134       ((cfvs, conclthm), (sgn, maxidx, ft))
   135     end;
   136 
   137 (* substitute using an object or meta level equality *)
   138 fun eqsubst_tac' ctxt searchf instepthm i th =
   139     let
   140       val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   141       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   142       fun rewrite_with_thm r =
   143           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   144           in searchf searchinfo lhs
   145              |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   146     in stepthms |> Seq.maps rewrite_with_thm end;
   147 
   148 
   149 (* Tactic.distinct_subgoals_tac -- fails to free type variables *)
   150 
   151 (* custom version of distinct subgoals that works with term and
   152    type variables. Asssumes th is in beta-eta normal form.
   153    Also, does nothing if flexflex contraints are present. *)
   154 fun distinct_subgoals th =
   155     if List.null (Thm.tpairs_of th) then
   156       let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
   157         val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
   158       in
   159         IsaND.unfix_frees_and_tfrees
   160           fixes
   161           (Drule.implies_intr_list
   162              (Library.gen_distinct
   163                 (fn (x, y) => Thm.term_of x = Thm.term_of y)
   164                 cprems) fixedthconcl)
   165       end
   166     else th;
   167 
   168 (* General substiuttion of multiple occurances using one of
   169    the given theorems*)
   170 exception eqsubst_occL_exp of
   171           string * (int list) * (thm list) * int * thm;
   172 fun skip_first_occs_search occ srchf sinfo lhs =
   173     case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
   174       IsaPLib.skipmore _ => Seq.empty
   175     | IsaPLib.skipseq ss => Seq.flat ss;
   176 
   177 fun eqsubst_tac ctxt occL thms i th =
   178     let val nprems = Thm.nprems_of th in
   179       if nprems < i then Seq.empty else
   180       let val thmseq = (Seq.of_list thms)
   181         fun apply_occ occ th =
   182             thmseq |> Seq.maps
   183                     (fn r => eqsubst_tac' ctxt (skip_first_occs_search
   184                                     occ searchf_tlr_unify_valid) r
   185                                  (i + ((Thm.nprems_of th) - nprems))
   186                                  th);
   187         val sortedoccL =
   188             Library.sort (Library.rev_order o Library.int_ord) occL;
   189       in
   190         Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   191       end
   192     end
   193     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   194 
   195 
   196 (* inthms are the given arguments in Isar, and treated as eqstep with
   197    the first one, then the second etc *)
   198 fun eqsubst_meth ctxt occL inthms =
   199     Method.METHOD
   200       (fn facts =>
   201           HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
   202 
   203 (* apply a substitution inside assumption j, keeps asm in the same place *)
   204 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   205     let
   206       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   207       val preelimrule =
   208           (RWInst.rw m rule pth)
   209             |> (Seq.hd o Tactic.prune_params_tac)
   210             |> Thm.permute_prems 0 ~1 (* put old asm first *)
   211             |> IsaND.unfix_frees cfvs (* unfix any global params *)
   212             |> RWInst.beta_eta_contract; (* normal form *)
   213   (*    val elimrule =
   214           preelimrule
   215             |> Tactic.make_elim (* make into elim rule *)
   216             |> Thm.lift_rule (th2, i); (* lift into context *)
   217    *)
   218     in
   219       (* ~j because new asm starts at back, thus we subtract 1 *)
   220       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   221       (Tactic.dtac preelimrule i th2)
   222 
   223       (* (Thm.bicompose
   224                  false (* use unification *)
   225                  (true, (* elim resolution *)
   226                   elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   227                  i th2) *)
   228     end;
   229 
   230 
   231 (* prepare to substitute within the j'th premise of subgoal i of gth,
   232 using a meta-level equation. Note that we assume rule has var indicies
   233 zero'd. Note that we also assume that premt is the j'th premice of
   234 subgoal i of gth. Note the repetition of work done for each
   235 assumption, i.e. this can be made more efficient for search over
   236 multiple assumptions.  *)
   237 fun prep_subst_in_asm i gth j =
   238     let
   239       val th = Thm.incr_indexes 1 gth;
   240       val tgt_term = Thm.prop_of th;
   241 
   242       val sgn = Thm.sign_of_thm th;
   243       val ctermify = Thm.cterm_of sgn;
   244       val trivify = Thm.trivial o ctermify;
   245 
   246       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   247       val cfvs = rev (map ctermify fvs);
   248 
   249       val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   250       val asm_nprems = length (Logic.strip_imp_prems asmt);
   251 
   252       val pth = trivify asmt;
   253       val maxidx = Term.maxidx_of_term asmt;
   254 
   255       val ft = ((IsaFTerm.focus_right
   256                  o IsaFTerm.fcterm_of_term
   257                  o Thm.prop_of) pth)
   258     in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   259 
   260 (* prepare subst in every possible assumption *)
   261 fun prep_subst_in_asms i gth =
   262     map (prep_subst_in_asm i gth)
   263         ((rev o IsaPLib.mk_num_list o length)
   264            (Logic.prems_of_goal (Thm.prop_of gth) i));
   265 
   266 
   267 (* substitute in an assumption using an object or meta level equality *)
   268 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   269     let
   270       val asmpreps = prep_subst_in_asms i th;
   271       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   272       fun rewrite_with_thm r =
   273           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   274             fun occ_search occ [] = Seq.empty
   275               | occ_search occ ((asminfo, searchinfo)::moreasms) =
   276                 (case searchf searchinfo occ lhs of
   277                    IsaPLib.skipmore i => occ_search i moreasms
   278                  | IsaPLib.skipseq ss =>
   279                    Seq.append (Seq.map (Library.pair asminfo)
   280                                        (Seq.flat ss),
   281                                occ_search 1 moreasms))
   282                               (* find later substs also *)
   283           in
   284             occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   285           end;
   286     in stepthms |> Seq.maps rewrite_with_thm end;
   287 
   288 
   289 fun skip_first_asm_occs_search searchf sinfo occ lhs =
   290     IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
   291 
   292 fun eqsubst_asm_tac ctxt occL thms i th =
   293     let val nprems = Thm.nprems_of th
   294     in
   295       if nprems < i then Seq.empty else
   296       let val thmseq = (Seq.of_list thms)
   297         fun apply_occ occK th =
   298             thmseq |> Seq.maps
   299                     (fn r =>
   300                         eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   301                                             searchf_tlr_unify_valid) occK r
   302                                          (i + ((Thm.nprems_of th) - nprems))
   303                                          th);
   304         val sortedoccs =
   305             Library.sort (Library.rev_order o Library.int_ord) occL
   306       in
   307         Seq.map distinct_subgoals
   308                 (Seq.EVERY (map apply_occ sortedoccs) th)
   309       end
   310     end
   311     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   312 
   313 (* inthms are the given arguments in Isar, and treated as eqstep with
   314    the first one, then the second etc *)
   315 fun eqsubst_asm_meth ctxt occL inthms =
   316     Method.METHOD
   317       (fn facts =>
   318           HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
   319 
   320 (* syntax for options, given "(asm)" will give back true, without
   321    gives back false *)
   322 val options_syntax =
   323     (Args.parens (Args.$$$ "asm") >> (K true)) ||
   324      (Scan.succeed false);
   325 
   326 val ith_syntax =
   327     (Args.parens (Scan.repeat Args.nat))
   328       || (Scan.succeed [0]);
   329 
   330 (* combination method that takes a flag (true indicates that subst
   331 should be done to an assumption, false = apply to the conclusion of
   332 the goal) as well as the theorems to use *)
   333 fun subst_meth src =
   334   Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src
   335   #> (fn (ctxt, ((asmflag, occL), inthms)) =>
   336     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   337 
   338 
   339 val setup =
   340   Method.add_method ("subst", subst_meth, "substiution with an equation");
   341 
   342 end;