*To*: Lucas Dixon <lucas.dixon at ed.ac.uk>*Subject*: Re: [isabelle] subst_tac?*From*: John Matthews <matthews at galois.com>*Date*: Mon, 23 Jan 2006 10:01:35 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43D4AFDB.70604@ed.ac.uk>*References*: <91D0E45A-8AF9-4B74-B141-6B7759F8F136@galois.com> <43D4AFDB.70604@ed.ac.uk>

-john On Jan 23, 2006, at 2:28 AM, Lucas Dixon wrote:

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 thegoal, presumably to avoid other instantiations, such as "b" in theaboveexample. 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 searchfunctionreturns information about the position and instantiations withwhich torewrite the goal using the rule's left hand side. By providing asearchfunction 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 thiscan becached 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 returnthem*)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 custominstantiation *)Seq.list_of (EQSubstTac.eqsubst_tac' (searchf_and_inst insts) rule 1 (topthm()));(* the other without any instantiations - the current defaultbehaviour *)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 arerenamed before the rule is applied. I guess this can be fixed bywritingsome 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 rewriterule supplied with expressions that contain meta-bound variablesof thesubgoal? Thanks, -john

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

**Re: [isabelle] subst_tac?***From:*Lucas Dixon

- Previous by Date: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Date: Re: [isabelle] primrec on nested mutually-recursive datatype
- Previous by Thread: Re: [isabelle] subst_tac?
- Next by Thread: [isabelle] proving that a value is outside of an inductively defined set
- 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