Re: [isabelle] subst_tac?



Hi John,

I think what you're after is something like:

Goal:
"!! a. P (l b, l a)"

and a rule:
"l ?x = r ?x"

but where you can first instantiate "?x" to be the bound "a" in the
goal, presumably to avoid other instantiations, such as "b" in the above
example.

This can be done, but is a little tricky. The underlying tactic is:

EQSubstTac.eqsubst_tac'

this takes a 'search function' as the first argument. A search function
returns information about the position and instantiations with which to
rewrite the goal using the rule's left hand side. By providing a search
function that additionally performs further instantiation, you can get
the desired behaviour.

The following code shows an example...

(* search function copied from: Pure/IsaPlanner/isafterm.ML *)
fun search_tlr_valid_f f ft =
    let
      fun maux ft =
          let
            val hereseq = if IsaFTerm.valid_match_start ft then f ft
else Seq.empty
          in
          (case (IsaFTerm.focus_of_fcterm ft) of
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
                       Seq.cons(hereseq,
                                  maux (IsaFTerm.focus_right ft)))
          | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
          | leaf => Seq.single (hereseq))
          end
    in maux ft end;

(* Calls Higher order unification but handles exceptions *)
(* given theory, max var index, (t1, t2) list of things to unify *)
(* returns Seq of instantiations *)
fun clean_unify thry ix ts =
    let
      (* is it OK to ignore the type instantiation info?
         or should I be using it? *)
      val typs_unify =
          SOME (Library.fold
                  (fn (t1, t2) =>
                      (* type info will be re-derived, maybe this can be
cached
                       for efficiency? *)
                      (Sign.typ_unify thry (Term.type_of t1,
Term.type_of t2)))
                  ts
                  (Term.Vartab.empty, ix))
            handle Type.TUNIFY => NONE;
    in
      case typs_unify of
        SOME (typinsttab, ix2) =>
        let

          fun mk_insts env =
            (Vartab.dest (Envir.type_env env),
             Envir.alist_of env);
          val initenv = Envir.Envir {asol = Vartab.empty,
                                     iTs = typinsttab, maxidx = ix2};
          (* Smashing unifiers can cause problems, better to return them*)
          val useq = (Unify.smash_unifiers (thry,initenv,ts))
	            handle UnequalLengths => Seq.empty
		               | Term.TERM _ => Seq.empty;
          fun clean_unify' useq () =
              (case (Seq.pull useq) of
                 NONE => NONE
               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
	      handle UnequalLengths => NONE
                   | Term.TERM _ => NONE;
        in
          (Seq.make (clean_unify' useq))
        end
      | NONE => Seq.empty
    end;

(* Slight modification from clean_unify in: Pure/IsaPlanner/isafterm.ML *)
fun clean_unify_ft thry ix extrainsts pat ft =
    let val (t, (FakeTs, Ts,absterm)) = IsaFTerm.prepmatch ft in
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
            (clean_unify thry ix ((t, pat)::extrainsts)) end;

(* A search function for the subst tactic, see: Provers/eqsubst.ML *)
fun searchf_and_inst insts (searchinfo as (thry, maxidx, ft)) lhs =
    Seq.flat (IsaFTerm.find_fcterm_matches
                search_tlr_valid_f
                (clean_unify_ft thry maxidx insts lhs)
                ft);

(* a little example *)
context (theory "Main");
Goal "ALL x. P ((0 :: nat) + 0, (0 :: nat) + x)";
val rule = thm "add_0";

(* we get the type of the var "n" in the fule add_0. *)
val [var] = Term.term_vars (Thm.prop_of rule);
val (_, ty) = Term.dest_Var var;
(* we need to correct the name of the var in the rule *)
val v = Var(("y",0), ty);
(* bound variables are renamed internally, and we need to use the
internal name for a free variable that represents it *)
(* see: src/IsaPlanner/rw_tools.ML for tmp var renaming functions *)
val x = Free (RWTools.mk_fake_bound_name "x", ty);
val insts = [(v,x)]; (* this is the custom instantiation *)

(* Now we can compare two applications, one with our custom instantiation *)
Seq.list_of
(EQSubstTac.eqsubst_tac' (searchf_and_inst insts) rule 1 (topthm()));

(* the other without any instantiations - the current default behaviour *)
Seq.list_of
(EQSubstTac.eqsubst_tac' (searchf_and_inst []) rule 1 (topthm()));


(* in more detail to examine the search function's behaviour *)
val [r] = map Drule.zero_var_indexes (EqRuleData.prep_meta_eq rule);
val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
val i = 0;
val matcheseq =
    searchf_and_inst insts
                     (the_context(), 0,
                      IsaFTerm.fcterm_of_term
                        (List.nth (Thm.prems_of (topthm()), i)))
                     lhs;
print_depth 100;
val matches = Seq.list_of matcheseq;

However, as you can see, it's a bit of a pain because variables are
renamed before the rule is applied. I guess this can be fixed by writing
some interface code that manages the renamings.

best,
lucas


John Matthews wrote:
> The subst method is great, I use it a lot (thanks Lucas!). Is there a 
> _tac version of subst that would allow me to instantiate the rewrite 
> rule supplied with expressions that contain meta-bound variables of  the
> subgoal?
> 
> Thanks,
> -john






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.