*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] subst_tac?*From*: Lucas Dixon <lucas.dixon at ed.ac.uk>*Date*: Mon, 23 Jan 2006 10:28:43 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <91D0E45A-8AF9-4B74-B141-6B7759F8F136@galois.com>*References*: <91D0E45A-8AF9-4B74-B141-6B7759F8F136@galois.com>*User-agent*: Mozilla Thunderbird 1.0.2-1.3.2.ed.1 (X11/20050420)

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

**Follow-Ups**:**Re: [isabelle] subst_tac?***From:*John Matthews

**References**:**[isabelle] subst_tac?***From:*John Matthews

- Previous by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Date: Re: [isabelle] primrec on nested mutually-recursive datatype
- Previous by Thread: [isabelle] subst_tac?
- Next by Thread: Re: [isabelle] subst_tac?
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list