src/Provers/eqsubst.ML
author wenzelm
Fri Jun 17 18:33:19 2005 +0200 (2005-06-17)
changeset 16434 d17817dd61e9
parent 16007 4dcccaa11a13
child 16978 e35b518bffc9
permissions -rw-r--r--
added Id;
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Provers/eqsubst.ML
     3     ID:         $Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucas.dixon@ed.ac.uk
     6     Modified:   18 Feb 2005 - Lucas - 
     7     Created:    29 Jan 2005
     8 *)
     9 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    10 (*  DESCRIPTION:
    11 
    12     A Tactic to perform a substiution using an equation.
    13 
    14 *)
    15 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    16 
    17 
    18 
    19 (* Logic specific data stub *)
    20 signature EQRULE_DATA =
    21 sig
    22 
    23   (* to make a meta equality theorem in the current logic *)
    24   val prep_meta_eq : thm -> thm list
    25 
    26 end;
    27 
    28 
    29 (* the signature of an instance of the SQSUBST tactic *)
    30 signature EQSUBST_TAC = 
    31 sig
    32 
    33   exception eqsubst_occL_exp of 
    34             string * (int list) * (Thm.thm list) * int * Thm.thm;
    35 
    36 
    37   type match = 
    38        ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
    39         * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
    40        * (string * Term.typ) list (* fake named type abs env *)
    41        * (string * Term.typ) list (* type abs env *)
    42        * Term.term (* outer term *)
    43 
    44   type searchinfo = 
    45        Sign.sg (* sign for matching *)
    46        * int (* maxidx *)
    47        * BasicIsaFTerm.FcTerm (* focusterm to search under *)
    48 
    49   val prep_subst_in_asm :
    50          int (* subgoal to subst in *)
    51       -> Thm.thm (* target theorem with subgoals *)
    52       -> int (* premise to subst in *)
    53       -> (Thm.cterm list (* certified free var placeholders for vars *) 
    54           * int (* premice no. to subst *)
    55           * int (* number of assumptions of premice *)
    56           * Thm.thm) (* premice as a new theorem for forward reasoning *)
    57          * searchinfo (* search info: prem id etc *)
    58 
    59   val prep_subst_in_asms :
    60          int (* subgoal to subst in *)
    61       -> Thm.thm (* target theorem with subgoals *)
    62       -> ((Thm.cterm list (* certified free var placeholders for vars *) 
    63           * int (* premice no. to subst *)
    64           * int (* number of assumptions of premice *)
    65           * Thm.thm) (* premice as a new theorem for forward reasoning *)
    66          * searchinfo) list
    67 
    68   val apply_subst_in_asm :
    69       int (* subgoal *)
    70       -> Thm.thm (* overall theorem *)
    71       -> Thm.thm (* rule *)
    72       -> (Thm.cterm list (* certified free var placeholders for vars *) 
    73           * int (* assump no being subst *)
    74           * int (* num of premises of asm *) 
    75           * Thm.thm) (* premthm *)
    76       * match
    77       -> Thm.thm Seq.seq
    78 
    79   val prep_concl_subst :
    80          int (* subgoal *)
    81       -> Thm.thm (* overall goal theorem *)
    82       -> (Thm.cterm list * Thm.thm) * searchinfo (* (cvfs, conclthm), matchf *)
    83 
    84   val apply_subst_in_concl :
    85         int (* subgoal *)
    86         -> Thm.thm (* thm with all goals *)
    87         -> Thm.cterm list (* certified free var placeholders for vars *)
    88            * Thm.thm  (* trivial thm of goal concl *)
    89             (* possible matches/unifiers *)
    90         -> Thm.thm (* rule *)
    91         -> match
    92         -> Thm.thm Seq.seq (* substituted goal *)
    93 
    94   (* basic notion of search *)
    95   val searchf_tlr_unify_all : 
    96       (searchinfo 
    97        -> Term.term (* lhs *)
    98        -> match Seq.seq Seq.seq)
    99   val searchf_tlr_unify_valid : 
   100       (searchinfo 
   101        -> Term.term (* lhs *)
   102        -> match Seq.seq Seq.seq)
   103 
   104   (* specialise search constructor for conclusion skipping occurnaces. *)
   105      val skip_first_occs_search :
   106         int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
   107   (* specialised search constructor for assumptions using skips *)
   108      val skip_first_asm_occs_search :
   109         ('a -> 'b -> 'c Seq.seq Seq.seq) ->
   110         'a -> int -> 'b -> 'c IsaPLib.skipseqT
   111 
   112   (* tactics and methods *)
   113   val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method
   114   val eqsubst_asm_tac : 
   115       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
   116   val eqsubst_asm_tac' : 
   117       (* search function with skips *)
   118       (searchinfo -> int -> Term.term -> match IsaPLib.skipseqT) 
   119       -> int (* skip to *)
   120       -> Thm.thm (* rule *)
   121       -> int (* subgoal number *)
   122       -> Thm.thm (* tgt theorem with subgoals *)
   123       -> Thm.thm Seq.seq (* new theorems *)
   124 
   125   val eqsubst_meth : int list -> Thm.thm list -> Proof.method
   126   val eqsubst_tac : 
   127       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
   128   val eqsubst_tac' : 
   129       (searchinfo -> Term.term -> match Seq.seq) 
   130       -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
   131 
   132   val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method
   133   val setup : (Theory.theory -> Theory.theory) list
   134 end;
   135 
   136 
   137 functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) 
   138   : EQSUBST_TAC
   139 = struct
   140 
   141   (* a type abriviation for match information *)
   142   type match = 
   143        ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
   144         * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
   145        * (string * Term.typ) list (* fake named type abs env *)
   146        * (string * Term.typ) list (* type abs env *)
   147        * Term.term (* outer term *)
   148 
   149   type searchinfo = 
   150        Sign.sg (* sign for matching *)
   151        * int (* maxidx *)
   152        * BasicIsaFTerm.FcTerm (* focusterm to search under *)
   153 
   154 (* FOR DEBUGGING...
   155 type trace_subst_errT = int (* subgoal *)
   156         * Thm.thm (* thm with all goals *)
   157         * (Thm.cterm list (* certified free var placeholders for vars *)
   158            * Thm.thm)  (* trivial thm of goal concl *)
   159             (* possible matches/unifiers *)
   160         * Thm.thm (* rule *)
   161         * (((Term.indexname * Term.typ) list (* type instantiations *)
   162               * (Term.indexname * Term.term) list ) (* term instantiations *)
   163              * (string * Term.typ) list (* Type abs env *)
   164              * Term.term) (* outer term *);
   165 
   166 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
   167 val trace_subst_search = ref false;
   168 exception trace_subst_exp of trace_subst_errT;
   169  *)
   170 
   171 (* also defined in /HOL/Tools/inductive_codegen.ML, 
   172    maybe move this to seq.ML ? *)
   173 infix 5 :->;
   174 fun s :-> f = Seq.flat (Seq.map f s);
   175 
   176 (* search from top, left to right, then down *)
   177 fun search_tlr_all_f f ft = 
   178     let
   179       fun maux ft = 
   180           let val t' = (IsaFTerm.focus_of_fcterm ft) 
   181             (* val _ = 
   182                 if !trace_subst_search then 
   183                   (writeln ("Examining: " ^ (TermLib.string_of_term t'));
   184                    TermLib.writeterm t'; ())
   185                 else (); *)
   186           in 
   187           (case t' of 
   188             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), 
   189                        Seq.cons(f ft, 
   190                                   maux (IsaFTerm.focus_right ft)))
   191           | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
   192           | leaf => Seq.single (f ft)) end
   193     in maux ft end;
   194 
   195 (* search from top, left to right, then down *)
   196 fun search_tlr_valid_f f ft = 
   197     let
   198       fun maux ft = 
   199           let 
   200             val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
   201           in 
   202           (case (IsaFTerm.focus_of_fcterm ft) of 
   203             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), 
   204                        Seq.cons(hereseq, 
   205                                   maux (IsaFTerm.focus_right ft)))
   206           | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
   207           | leaf => Seq.single (hereseq))
   208           end
   209     in maux ft end;
   210 
   211 (* search all unifications *)
   212 fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs = 
   213     IsaFTerm.find_fcterm_matches 
   214       search_tlr_all_f 
   215       (IsaFTerm.clean_unify_ft sgn maxidx lhs)
   216       ft;
   217 
   218 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
   219 fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs  = 
   220     IsaFTerm.find_fcterm_matches 
   221       search_tlr_valid_f 
   222       (IsaFTerm.clean_unify_ft sgn maxidx lhs)
   223       ft;
   224 
   225 
   226 (* apply a substitution in the conclusion of the theorem th *)
   227 (* cfvs are certified free var placeholders for goal params *)
   228 (* conclthm is a theorem of for just the conclusion *)
   229 (* m is instantiation/match information *)
   230 (* rule is the equation for substitution *)
   231 fun apply_subst_in_concl i th (cfvs, conclthm) rule m = 
   232     (RWInst.rw m rule conclthm)
   233       |> IsaND.unfix_frees cfvs
   234       |> RWInst.beta_eta_contract
   235       |> (fn r => Tactic.rtac r i th);
   236 
   237 (* substitute within the conclusion of goal i of gth, using a meta
   238 equation rule. Note that we assume rule has var indicies zero'd *)
   239 fun prep_concl_subst i gth = 
   240     let 
   241       val th = Thm.incr_indexes 1 gth;
   242       val tgt_term = Thm.prop_of th;
   243 
   244       val sgn = Thm.sign_of_thm th;
   245       val ctermify = Thm.cterm_of sgn;
   246       val trivify = Thm.trivial o ctermify;
   247 
   248       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   249       val cfvs = rev (map ctermify fvs);
   250 
   251       val conclterm = Logic.strip_imp_concl fixedbody;
   252       val conclthm = trivify conclterm;
   253       val maxidx = Term.maxidx_of_term conclterm;
   254       val ft = ((IsaFTerm.focus_right  
   255                  o IsaFTerm.focus_left
   256                  o IsaFTerm.fcterm_of_term 
   257                  o Thm.prop_of) conclthm)
   258     in
   259       ((cfvs, conclthm), (sgn, maxidx, ft))
   260     end;
   261 
   262 (* substitute using an object or meta level equality *)
   263 fun eqsubst_tac' searchf instepthm i th = 
   264     let 
   265       val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   266       val stepthms = 
   267           Seq.map Drule.zero_var_indexes 
   268                   (Seq.of_list (EqRuleData.prep_meta_eq instepthm));
   269       fun rewrite_with_thm r =
   270           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   271           in (searchf searchinfo lhs)
   272              :-> (apply_subst_in_concl i th cvfsconclthm r) end;
   273     in stepthms :-> rewrite_with_thm end;
   274 
   275 
   276 (* Tactic.distinct_subgoals_tac -- fails to free type variables *)
   277 
   278 (* custom version of distinct subgoals that works with term and 
   279    type variables. Asssumes th is in beta-eta normal form. 
   280    Also, does nothing if flexflex contraints are present. *)
   281 fun distinct_subgoals th =
   282     if List.null (Thm.tpairs_of th) then
   283       let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
   284         val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
   285       in
   286         IsaND.unfix_frees_and_tfrees 
   287           fixes
   288           (Drule.implies_intr_list 
   289              (Library.gen_distinct 
   290                 (fn (x, y) => Thm.term_of x = Thm.term_of y)
   291                 cprems) fixedthconcl)
   292       end
   293     else th;
   294 
   295 (* General substiuttion of multiple occurances using one of 
   296    the given theorems*)
   297 exception eqsubst_occL_exp of 
   298           string * (int list) * (Thm.thm list) * int * Thm.thm;
   299 fun skip_first_occs_search occ srchf sinfo lhs = 
   300     case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of 
   301       IsaPLib.skipmore _ => Seq.empty
   302     | IsaPLib.skipseq ss => Seq.flat ss;
   303 
   304 fun eqsubst_tac occL thms i th = 
   305     let val nprems = Thm.nprems_of th in
   306       if nprems < i then Seq.empty else
   307       let val thmseq = (Seq.of_list thms) 
   308         fun apply_occ occ th = 
   309             thmseq :-> 
   310                     (fn r => eqsubst_tac' (skip_first_occs_search 
   311                                     occ searchf_tlr_unify_valid) r
   312                                  (i + ((Thm.nprems_of th) - nprems))
   313                                  th);
   314         val sortedoccL = 
   315             Library.sort (Library.rev_order o Library.int_ord) occL;
   316       in
   317         Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   318       end
   319     end
   320     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   321 
   322 
   323 (* inthms are the given arguments in Isar, and treated as eqstep with
   324    the first one, then the second etc *)
   325 fun eqsubst_meth occL inthms =
   326     Method.METHOD 
   327       (fn facts =>
   328           HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms ));
   329 
   330 (* apply a substitution inside assumption j, keeps asm in the same place *)
   331 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = 
   332     let 
   333       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   334       val preelimrule = 
   335           (RWInst.rw m rule pth)
   336             |> (Seq.hd o Tactic.prune_params_tac)
   337             |> Thm.permute_prems 0 ~1 (* put old asm first *)
   338             |> IsaND.unfix_frees cfvs (* unfix any global params *)
   339             |> RWInst.beta_eta_contract; (* normal form *)
   340   (*    val elimrule = 
   341           preelimrule
   342             |> Tactic.make_elim (* make into elim rule *)
   343             |> Thm.lift_rule (th2, i); (* lift into context *)
   344    *)
   345     in
   346       (* ~j because new asm starts at back, thus we subtract 1 *)
   347       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   348       (Tactic.dtac preelimrule i th2)
   349 
   350       (* (Thm.bicompose 
   351                  false (* use unification *)
   352                  (true, (* elim resolution *)
   353                   elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   354                  i th2) *)
   355     end;
   356 
   357 
   358 (* prepare to substitute within the j'th premise of subgoal i of gth,
   359 using a meta-level equation. Note that we assume rule has var indicies
   360 zero'd. Note that we also assume that premt is the j'th premice of
   361 subgoal i of gth. Note the repetition of work done for each
   362 assumption, i.e. this can be made more efficient for search over
   363 multiple assumptions.  *)
   364 fun prep_subst_in_asm i gth j = 
   365     let 
   366       val th = Thm.incr_indexes 1 gth;
   367       val tgt_term = Thm.prop_of th;
   368 
   369       val sgn = Thm.sign_of_thm th;
   370       val ctermify = Thm.cterm_of sgn;
   371       val trivify = Thm.trivial o ctermify;
   372 
   373       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   374       val cfvs = rev (map ctermify fvs);
   375 
   376       val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
   377       val asm_nprems = length (Logic.strip_imp_prems asmt);
   378 
   379       val pth = trivify asmt;
   380       val maxidx = Term.maxidx_of_term asmt;
   381 
   382       val ft = ((IsaFTerm.focus_right 
   383                  o IsaFTerm.fcterm_of_term 
   384                  o Thm.prop_of) pth)
   385     in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   386 
   387 (* prepare subst in every possible assumption *)
   388 fun prep_subst_in_asms i gth = 
   389     map (prep_subst_in_asm i gth)
   390         ((rev o IsaPLib.mk_num_list o length) 
   391            (Logic.prems_of_goal (Thm.prop_of gth) i));
   392 
   393 
   394 (* substitute in an assumption using an object or meta level equality *)
   395 fun eqsubst_asm_tac' searchf skipocc instepthm i th = 
   396     let 
   397       val asmpreps = prep_subst_in_asms i th;
   398       val stepthms = 
   399           Seq.map Drule.zero_var_indexes 
   400               (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
   401       fun rewrite_with_thm r =
   402           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   403             fun occ_search occ [] = Seq.empty
   404               | occ_search occ ((asminfo, searchinfo)::moreasms) =
   405                 (case searchf searchinfo occ lhs of 
   406                    IsaPLib.skipmore i => occ_search i moreasms
   407                  | IsaPLib.skipseq ss => 
   408                    Seq.append (Seq.map (Library.pair asminfo)
   409                                        (Seq.flat ss), 
   410                                occ_search 1 moreasms))
   411                               (* find later substs also *)
   412           in 
   413             (occ_search skipocc asmpreps) :-> (apply_subst_in_asm i th r)
   414           end;
   415     in stepthms :-> rewrite_with_thm end;
   416 
   417 
   418 fun skip_first_asm_occs_search searchf sinfo occ lhs = 
   419     IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
   420 
   421 fun eqsubst_asm_tac occL thms i th = 
   422     let val nprems = Thm.nprems_of th 
   423     in
   424       if nprems < i then Seq.empty else
   425       let val thmseq = (Seq.of_list thms) 
   426         fun apply_occ occK th = 
   427             thmseq :-> 
   428                     (fn r => 
   429                         eqsubst_asm_tac' (skip_first_asm_occs_search 
   430                                             searchf_tlr_unify_valid) occK r
   431                                          (i + ((Thm.nprems_of th) - nprems))
   432                                          th);
   433         val sortedoccs = 
   434             Library.sort (Library.rev_order o Library.int_ord) occL
   435       in
   436         Seq.map distinct_subgoals
   437                 (Seq.EVERY (map apply_occ sortedoccs) th)
   438       end
   439     end
   440     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   441 
   442 (* inthms are the given arguments in Isar, and treated as eqstep with
   443    the first one, then the second etc *)
   444 fun eqsubst_asm_meth occL inthms =
   445     Method.METHOD 
   446       (fn facts =>
   447           HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms ));
   448 
   449 (* combination method that takes a flag (true indicates that subst
   450 should be done to an assumption, false = apply to the conclusion of
   451 the goal) as well as the theorems to use *)
   452 fun meth ((asmflag, occL), inthms) ctxt = 
   453     if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms;
   454 
   455 (* syntax for options, given "(asm)" will give back true, without
   456    gives back false *)
   457 val options_syntax =
   458     (Args.parens (Args.$$$ "asm") >> (K true)) ||
   459      (Scan.succeed false);
   460 
   461 val ith_syntax =
   462     (Args.parens (Scan.repeat Args.nat))
   463       || (Scan.succeed [0]);
   464 
   465 (* method syntax, first take options, then theorems *)
   466 fun meth_syntax meth src ctxt =
   467     meth (snd (Method.syntax ((Scan.lift options_syntax) 
   468                                 -- (Scan.lift ith_syntax) 
   469                                 -- Attrib.local_thms) src ctxt)) 
   470          ctxt;
   471 
   472 (* setup function for adding method to theory. *)
   473 val setup = 
   474     [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")];
   475 
   476 end;