# HG changeset patch # User dixon # Date 1116450253 -7200 # Node ID 031f560124834e3988fd32a5501848bf446d6f4b # Parent 48ae07a95c70bf18b5e6e696d961913e96af5734 lucas - fixed subst in assumptions to count redexes from left to right. diff -r 48ae07a95c70 -r 031f56012483 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Wed May 18 11:31:00 2005 +0200 +++ b/src/Provers/eqsubst.ML Wed May 18 23:04:13 2005 +0200 @@ -13,6 +13,8 @@ *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) + + (* Logic specific data stub *) signature EQRULE_DATA = sig @@ -30,6 +32,7 @@ exception eqsubst_occL_exp of string * (int list) * (Thm.thm list) * int * Thm.thm; + type match = ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *) * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *) @@ -37,48 +40,45 @@ * (string * Term.typ) list (* type abs env *) * Term.term (* outer term *) + type searchinfo = + Sign.sg (* sign for matching *) + * int (* maxidx *) + * BasicIsaFTerm.FcTerm (* focusterm to search under *) + val prep_subst_in_asm : - (Sign.sg (* sign for matching *) - -> int (* maxidx *) - -> 'a (* input object kind *) - -> BasicIsaFTerm.FcTerm (* focusterm to search under *) - -> 'b) (* result type *) - -> int (* subgoal to subst in *) + int (* subgoal to subst in *) -> Thm.thm (* target theorem with subgoals *) -> int (* premise to subst in *) -> (Thm.cterm list (* certified free var placeholders for vars *) * int (* premice no. to subst *) * int (* number of assumptions of premice *) * Thm.thm) (* premice as a new theorem for forward reasoning *) - * ('a -> 'b) (* matchf *) + * searchinfo (* search info: prem id etc *) val prep_subst_in_asms : - (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) - -> int (* subgoal to subst in *) + int (* subgoal to subst in *) -> Thm.thm (* target theorem with subgoals *) -> ((Thm.cterm list (* certified free var placeholders for vars *) * int (* premice no. to subst *) * int (* number of assumptions of premice *) * Thm.thm) (* premice as a new theorem for forward reasoning *) - * ('a -> 'b)) (* matchf *) - Seq.seq + * searchinfo) list val apply_subst_in_asm : int (* subgoal *) -> Thm.thm (* overall theorem *) + -> Thm.thm (* rule *) -> (Thm.cterm list (* certified free var placeholders for vars *) * int (* assump no being subst *) * int (* num of premises of asm *) * Thm.thm) (* premthm *) - -> Thm.thm (* rule *) - -> match + * match -> Thm.thm Seq.seq val prep_concl_subst : - (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *) - -> int (* subgoal *) + int (* subgoal *) -> Thm.thm (* overall goal theorem *) - -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *) + -> (Thm.cterm list * Thm.thm) * searchinfo (* (cvfs, conclthm), matchf *) val apply_subst_in_concl : int (* subgoal *) @@ -90,37 +90,49 @@ -> match -> Thm.thm Seq.seq (* substituted goal *) + (* basic notion of search *) val searchf_tlr_unify_all : - (Sign.sg -> int -> - Term.term -> - BasicIsaFTerm.FcTerm -> - match Seq.seq Seq.seq) + (searchinfo + -> Term.term (* lhs *) + -> match Seq.seq Seq.seq) val searchf_tlr_unify_valid : - (Sign.sg -> int -> - Term.term -> - BasicIsaFTerm.FcTerm -> - match Seq.seq Seq.seq) + (searchinfo + -> Term.term (* lhs *) + -> match Seq.seq Seq.seq) + (* specialise search constructor for conclusion skipping occurnaces. *) + val skip_first_occs_search : + int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq + (* specialised search constructor for assumptions using skips *) + val skip_first_asm_occs_search : + ('a -> 'b -> 'c Seq.seq Seq.seq) -> + 'a -> int -> 'b -> 'c IsaPLib.skipseqT + + (* tactics and methods *) val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method - val eqsubst_asm_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_asm_tac : + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq val eqsubst_asm_tac' : - (Sign.sg -> int -> - Term.term -> - BasicIsaFTerm.FcTerm -> - match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq + (* search function with skips *) + (searchinfo -> int -> Term.term -> match IsaPLib.skipseqT) + -> int (* skip to *) + -> Thm.thm (* rule *) + -> int (* subgoal number *) + -> Thm.thm (* tgt theorem with subgoals *) + -> Thm.thm Seq.seq (* new theorems *) val eqsubst_meth : int list -> Thm.thm list -> Proof.method - val eqsubst_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_tac : + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq val eqsubst_tac' : - (Sign.sg -> int -> - Term.term -> - BasicIsaFTerm.FcTerm -> - match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq + (searchinfo -> Term.term -> match Seq.seq) + -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method val setup : (Theory.theory -> Theory.theory) list end; + functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) : EQSUBST_TAC = struct @@ -133,6 +145,10 @@ * (string * Term.typ) list (* type abs env *) * Term.term (* outer term *) + type searchinfo = + Sign.sg (* sign for matching *) + * int (* maxidx *) + * BasicIsaFTerm.FcTerm (* focusterm to search under *) (* FOR DEBUGGING... type trace_subst_errT = int (* subgoal *) @@ -192,28 +208,18 @@ in maux ft end; (* search all unifications *) -fun searchf_tlr_unify_all sgn maxidx lhs = +fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs = IsaFTerm.find_fcterm_matches search_tlr_all_f - (IsaFTerm.clean_unify_ft sgn maxidx lhs); + (IsaFTerm.clean_unify_ft sgn maxidx lhs) + ft; (* search only for 'valid' unifiers (non abs subterms and non vars) *) -fun searchf_tlr_unify_valid sgn maxidx lhs = +fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs = IsaFTerm.find_fcterm_matches search_tlr_valid_f - (IsaFTerm.clean_unify_ft sgn maxidx lhs); - -(* special tactic to skip the first "occ" occurances - ie start at the nth match *) -fun skip_first_occs_search occ searchf sgn i t ft = - let - fun skip_occs n sq = - if n <= 1 then sq - else - (case (Seq.pull sq) of NONE => Seq.empty - | SOME (h,t) => - (case Seq.pull h of NONE => skip_occs n t - | SOME _ => skip_occs (n - 1) t)) - in Seq.flat (skip_occs occ (searchf sgn i t ft)) end; + (IsaFTerm.clean_unify_ft sgn maxidx lhs) + ft; (* apply a substitution in the conclusion of the theorem th *) @@ -226,16 +232,13 @@ |> IsaND.unfix_frees cfvs |> RWInst.beta_eta_contract |> (fn r => Tactic.rtac r i th); - (* - |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th) - *) (* substitute within the conclusion of goal i of gth, using a meta equation rule. Note that we assume rule has var indicies zero'd *) -fun prep_concl_subst searchf i gth = +fun prep_concl_subst i gth = let val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; @@ -250,33 +253,29 @@ val conclterm = Logic.strip_imp_concl fixedbody; val conclthm = trivify conclterm; val maxidx = Term.maxidx_of_term conclterm; + val ft = ((IsaFTerm.focus_right + o IsaFTerm.focus_left + o IsaFTerm.fcterm_of_term + o Thm.prop_of) conclthm) in - ((cfvs, conclthm), - (fn lhs => searchf sgn maxidx lhs - ((IsaFTerm.focus_right - o IsaFTerm.focus_left - o IsaFTerm.fcterm_of_term - o Thm.prop_of) conclthm))) + ((cfvs, conclthm), (sgn, maxidx, ft)) end; (* substitute using an object or meta level equality *) fun eqsubst_tac' searchf instepthm i th = let - val (cvfsconclthm, findmatchf) = - prep_concl_subst searchf i th; - + val (cvfsconclthm, searchinfo) = prep_concl_subst i th; val stepthms = Seq.map Drule.zero_var_indexes (Seq.of_list (EqRuleData.prep_meta_eq instepthm)); - fun rewrite_with_thm r = let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); - in (findmatchf lhs) + in (searchf searchinfo lhs) :-> (apply_subst_in_concl i th cvfsconclthm r) end; + in stepthms :-> rewrite_with_thm end; - in (stepthms :-> rewrite_with_thm) end; -(* Tactic.distinct_subgoals_tac *) +(* Tactic.distinct_subgoals_tac -- fails to free type variables *) (* custom version of distinct subgoals that works with term and type variables. Asssumes th is in beta-eta normal form. @@ -299,30 +298,29 @@ the given theorems*) exception eqsubst_occL_exp of string * (int list) * (Thm.thm list) * int * Thm.thm; -fun eqsubst_occL tac occL thms i th = +fun skip_first_occs_search occ srchf sinfo lhs = + case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of + IsaPLib.skipmore _ => Seq.empty + | IsaPLib.skipseq ss => Seq.flat ss; + +fun eqsubst_tac occL thms i th = let val nprems = Thm.nprems_of th in if nprems < i then Seq.empty else let val thmseq = (Seq.of_list thms) fun apply_occ occ th = thmseq :-> - (fn r => tac (skip_first_occs_search + (fn r => eqsubst_tac' (skip_first_occs_search occ searchf_tlr_unify_valid) r (i + ((Thm.nprems_of th) - nprems)) th); + val sortedoccL = + Library.sort (Library.rev_order o Library.int_ord) occL; in - Seq.map distinct_subgoals - (Seq.EVERY (map apply_occ - (Library.sort (Library.rev_order - o Library.int_ord) occL)) th) + Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th) end end handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); - - -(* implicit argus: occL thms i th *) -val eqsubst_tac = eqsubst_occL eqsubst_tac'; - (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) @@ -331,24 +329,29 @@ (fn facts => HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms )); - -fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = - (RWInst.rw m rule pth) - |> Thm.permute_prems 0 ~1 - |> IsaND.unfix_frees cfvs - |> RWInst.beta_eta_contract - |> (fn r => Tactic.dtac r i th); - -(* -? should I be using bicompose what if we match more than one -assumption, even after instantiation ? (back will work, but it would -be nice to avoid the redudent search) - -something like... - |> Thm.lift_rule (th, i) - |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th) - -*) +(* apply a substitution inside assumption j, keeps asm in the same place *) +fun apply_subst_in_asm i th rule ((cfvs, j, nprems, pth),m) = + let + val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *) + val preelimrule = + (RWInst.rw m rule pth) + |> (Seq.hd o Tactic.prune_params_tac) + |> Thm.permute_prems 0 ~1 (* put old asm first *) + |> IsaND.unfix_frees cfvs (* unfix any global params *) + |> RWInst.beta_eta_contract; (* normal form *) + val elimrule = + preelimrule + |> Tactic.make_elim (* make into elim rule *) + |> Thm.lift_rule (th2, i); (* lift into context *) + in + (* ~j because new asm starts at back, thus we subtract 1 *) + Seq.map (Thm.rotate_rule (~j) (nprems + i)) + (Thm.bicompose + false (* use unification *) + (true, (* elim resolution *) + elimrule, 2 + nprems) + i th2) + end; (* prepare to substitute within the j'th premise of subgoal i of gth, @@ -357,7 +360,7 @@ subgoal i of gth. Note the repetition of work done for each assumption, i.e. this can be made more efficient for search over multiple assumptions. *) -fun prep_subst_in_asm searchf i gth j = +fun prep_subst_in_asm i gth j = let val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; @@ -375,42 +378,65 @@ val pth = trivify asmt; val maxidx = Term.maxidx_of_term asmt; - in - ((cfvs, j, asm_nprems, pth), - (fn lhs => (searchf sgn maxidx lhs - ((IsaFTerm.focus_right - o IsaFTerm.fcterm_of_term - o Thm.prop_of) pth)))) - end; + val ft = ((IsaFTerm.focus_right + o IsaFTerm.fcterm_of_term + o Thm.prop_of) pth) + in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; (* prepare subst in every possible assumption *) -fun prep_subst_in_asms searchf i gth = - Seq.map - (prep_subst_in_asm searchf i gth) - (Seq.of_list (IsaPLib.mk_num_list - (length (Logic.prems_of_goal (Thm.prop_of gth) i)))); +fun prep_subst_in_asms i gth = + map (prep_subst_in_asm i gth) + ((rev o IsaPLib.mk_num_list o length) + (Logic.prems_of_goal (Thm.prop_of gth) i)); (* substitute in an assumption using an object or meta level equality *) -fun eqsubst_asm_tac' searchf instepthm i th = +fun eqsubst_asm_tac' searchf skipocc instepthm i th = let - val asmpreps = prep_subst_in_asms searchf i th; + val asmpreps = prep_subst_in_asms i th; val stepthms = Seq.map Drule.zero_var_indexes - (Seq.of_list (EqRuleData.prep_meta_eq instepthm)) + (Seq.of_list (EqRuleData.prep_meta_eq instepthm)) + fun rewrite_with_thm r = + let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) + fun occ_search occ [] = Seq.empty + | occ_search occ ((asminfo, searchinfo)::moreasms) = + (case searchf searchinfo occ lhs of + IsaPLib.skipmore i => occ_search i moreasms + | IsaPLib.skipseq ss => + Seq.append (Seq.map (Library.pair asminfo) + (Seq.flat ss), + occ_search 1 moreasms)) + (* find later substs also *) + in + (occ_search skipocc asmpreps) :-> (apply_subst_in_asm i th r) + end; + in stepthms :-> rewrite_with_thm end; - fun rewrite_with_thm (asminfo, findmatchf) r = - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); - in (findmatchf lhs) - :-> (apply_subst_in_asm i th asminfo r) end; + +fun skip_first_asm_occs_search searchf sinfo occ lhs = + IsaPLib.skipto_seqseq occ (searchf sinfo lhs); + +fun eqsubst_asm_tac occL thms i th = + let val nprems = Thm.nprems_of th in - (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a)) - end; - -(* substitute using one of the given theorems in an assumption. -Implicit args: occL thms i th *) -val eqsubst_asm_tac = eqsubst_occL eqsubst_asm_tac'; - + if nprems < i then Seq.empty else + let val thmseq = (Seq.of_list thms) + fun apply_occ occK th = + thmseq :-> + (fn r => + eqsubst_asm_tac' (skip_first_asm_occs_search + searchf_tlr_unify_valid) occK r + (i + ((Thm.nprems_of th) - nprems)) + th); + val sortedoccs = + Library.sort (Library.rev_order o Library.int_ord) occL + in + Seq.map distinct_subgoals + (Seq.EVERY (map apply_occ sortedoccs) th) + end + end + handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) diff -r 48ae07a95c70 -r 031f56012483 src/Pure/IsaPlanner/isaplib.ML --- a/src/Pure/IsaPlanner/isaplib.ML Wed May 18 11:31:00 2005 +0200 +++ b/src/Pure/IsaPlanner/isaplib.ML Wed May 18 23:04:13 2005 +0200 @@ -25,6 +25,12 @@ val seq_is_empty : 'a Seq.seq -> bool val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq + datatype 'a skipseqT = + skipmore of int + | skipseq of 'a Seq.seq Seq.seq; + val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT + val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq + (* lists *) val mk_num_list : int -> int list val number_list : int -> 'a list -> (int * 'a) list @@ -164,10 +170,52 @@ (* First result of a tactic... uses NTH, so if there is no elements, - then no_tac is returned. *) fun FST f = NTH 1 f; +datatype 'a skipseqT = skipmore of int + | skipseq of 'a Seq.seq Seq.seq; +(* given a seqseq, skip the first m non-empty seq's *) +fun skipto_seqseq m s = + let + fun skip_occs n sq = + case Seq.pull sq of + NONE => skipmore n + | SOME (h,t) => + (case Seq.pull h of NONE => skip_occs n t + | SOME _ => if n <= 1 then skipseq (Seq.cons (h, t)) + else skip_occs (n - 1) t) + in (skip_occs m s) end; + +(* handy function for re-arranging Sequence operations *) +(* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *) +fun seqflat_seq ss = + let + fun pulltl LL () = + (case Seq.pull LL of + NONE => NONE + | SOME (hL,tLL) => + (case Seq.pull hL of + NONE => pulltl tLL () + | SOME (h,tL) => + SOME (h, Seq.make (recf (tLL, (Seq.single tL)))))) + and recf (fstLL,sndLL) () = + (case Seq.pull fstLL of + NONE => pulltl sndLL () + | SOME (hL, tLL) => + (case Seq.pull hL of + NONE => recf (tLL, sndLL) () + | SOME (h,tL) => + SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL)))))) + in Seq.make (pulltl ss) end; +(* tested with: +val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]]; +Seq.list_of (seqflat_seq ss); +val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list +*) + + + (* create a list opf the form (n, n-1, n-2, ... ) *) fun mk_num_list n = if n < 1 then [] else (n :: (mk_num_list (n-1)));