# HG changeset patch # User wenzelm # Date 1136567896 -3600 # Node ID 94d658871c98fd5e08f06703d93c0eaa198574f0 # Parent 32c1bf8cf1a41957c86e2fcbc20f38f887315a03 prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned; diff -r 32c1bf8cf1a4 -r 94d658871c98 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Fri Jan 06 18:18:15 2006 +0100 +++ b/src/Provers/eqsubst.ML Fri Jan 06 18:18:16 2006 +0100 @@ -1,131 +1,22 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Title: Provers/eqsubst.ML ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Modified: 18 Feb 2005 - Lucas - - Created: 29 Jan 2005 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - A Tactic to perform a substiution using an equation. - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) + Author: Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk - - -(* Logic specific data stub *) -signature EQRULE_DATA = -sig +A proof method to perform a substiution using an equation. +*) - (* to make a meta equality theorem in the current logic *) - val prep_meta_eq : thm -> thm list - -end; - - -(* the signature of an instance of the SQSUBST tactic *) signature EQSUBST = sig - - exception eqsubst_occL_exp of - string * (int list) * (thm list) * int * thm; - - type match - type searchinfo - - val prep_subst_in_asm : - int (* subgoal to subst in *) - -> thm (* target theorem with subgoals *) - -> int (* premise to subst in *) - -> (cterm list (* certified free var placeholders for vars *) - * int (* premice no. to subst *) - * int (* number of assumptions of premice *) - * thm) (* premice as a new theorem for forward reasoning *) - * searchinfo (* search info: prem id etc *) - - val prep_subst_in_asms : - int (* subgoal to subst in *) - -> thm (* target theorem with subgoals *) - -> ((cterm list (* certified free var placeholders for vars *) - * int (* premice no. to subst *) - * int (* number of assumptions of premice *) - * thm) (* premice as a new theorem for forward reasoning *) - * searchinfo) list - - val apply_subst_in_asm : - int (* subgoal *) - -> thm (* overall theorem *) - -> thm (* rule *) - -> (cterm list (* certified free var placeholders for vars *) - * int (* assump no being subst *) - * int (* num of premises of asm *) - * thm) (* premthm *) - * match - -> thm Seq.seq - - val prep_concl_subst : - int (* subgoal *) - -> thm (* overall goal theorem *) - -> (cterm list * thm) * searchinfo (* (cvfs, conclthm), matchf *) - - val apply_subst_in_concl : - int (* subgoal *) - -> thm (* thm with all goals *) - -> cterm list (* certified free var placeholders for vars *) - * thm (* trivial thm of goal concl *) - (* possible matches/unifiers *) - -> thm (* rule *) - -> match - -> thm Seq.seq (* substituted goal *) - - (* basic notion of search *) - val searchf_tlr_unify_all : - (searchinfo - -> term (* lhs *) - -> match Seq.seq Seq.seq) - val searchf_tlr_unify_valid : - (searchinfo - -> term (* lhs *) - -> match Seq.seq Seq.seq) - - (* specialise search constructor for conclusion skipping occurrences. *) - 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 list -> Proof.method - val eqsubst_asm_tac : - int list -> thm list -> int -> thm -> thm Seq.seq - val eqsubst_asm_tac' : - (* search function with skips *) - (searchinfo -> int -> term -> match IsaPLib.skipseqT) - -> int (* skip to *) - -> thm (* rule *) - -> int (* subgoal number *) - -> thm (* tgt theorem with subgoals *) - -> thm Seq.seq (* new theorems *) - - val eqsubst_meth : int list -> thm list -> Proof.method - val eqsubst_tac : - int list -> thm list -> int -> thm -> thm Seq.seq - val eqsubst_tac' : - (searchinfo -> term -> match Seq.seq) - -> thm -> int -> thm -> thm Seq.seq - - val meth : (bool * int list) * thm list -> Proof.context -> Proof.method val setup : (Theory.theory -> Theory.theory) list end; +structure EqSubst: EQSUBST = +struct -functor EqSubstFun (EqRuleData : EQRULE_DATA): EQSUBST = -struct +fun prep_meta_eq ctxt = + let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) + in mk #> map Drule.zero_var_indexes end; + (* a type abriviation for match information *) type match = @@ -136,7 +27,7 @@ * term (* outer term *) type searchinfo = - Sign.sg (* sign for matching *) + theory * int (* maxidx *) * BasicIsaFTerm.FcTerm (* focusterm to search under *) @@ -157,11 +48,6 @@ exception trace_subst_exp of trace_subst_errT; *) -(* also defined in /HOL/Tools/inductive_codegen.ML, - maybe move this to seq.ML ? *) -infix 5 :->; -fun s :-> f = Seq.flat (Seq.map f s); - (* search from top, left to right, then down *) fun search_tlr_all_f f ft = let @@ -249,17 +135,15 @@ end; (* substitute using an object or meta level equality *) -fun eqsubst_tac' searchf instepthm i th = +fun eqsubst_tac' ctxt searchf instepthm i th = let val (cvfsconclthm, searchinfo) = prep_concl_subst i th; - val stepthms = - Seq.map Drule.zero_var_indexes - (Seq.of_list (EqRuleData.prep_meta_eq instepthm)); + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); fun rewrite_with_thm r = let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); - in (searchf searchinfo lhs) - :-> (apply_subst_in_concl i th cvfsconclthm r) end; - in stepthms :-> rewrite_with_thm end; + in searchf searchinfo lhs + |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end; + in stepthms |> Seq.maps rewrite_with_thm end; (* Tactic.distinct_subgoals_tac -- fails to free type variables *) @@ -290,13 +174,13 @@ IsaPLib.skipmore _ => Seq.empty | IsaPLib.skipseq ss => Seq.flat ss; -fun eqsubst_tac occL thms i th = +fun eqsubst_tac ctxt 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 => eqsubst_tac' (skip_first_occs_search + thmseq |> Seq.maps + (fn r => eqsubst_tac' ctxt (skip_first_occs_search occ searchf_tlr_unify_valid) r (i + ((Thm.nprems_of th) - nprems)) th); @@ -311,10 +195,10 @@ (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) -fun eqsubst_meth occL inthms = +fun eqsubst_meth ctxt occL inthms = Method.METHOD (fn facts => - HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms )); + HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms)); (* apply a substitution inside assumption j, keeps asm in the same place *) fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = @@ -381,12 +265,10 @@ (* substitute in an assumption using an object or meta level equality *) -fun eqsubst_asm_tac' searchf skipocc instepthm i th = +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th = let val asmpreps = prep_subst_in_asms i th; - val stepthms = - Seq.map Drule.zero_var_indexes - (Seq.of_list (EqRuleData.prep_meta_eq instepthm)) + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); fun rewrite_with_thm r = let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) fun occ_search occ [] = Seq.empty @@ -399,23 +281,23 @@ occ_search 1 moreasms)) (* find later substs also *) in - (occ_search skipocc asmpreps) :-> (apply_subst_in_asm i th r) + occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r) end; - in stepthms :-> rewrite_with_thm end; + in stepthms |> Seq.maps rewrite_with_thm 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 = +fun eqsubst_asm_tac ctxt 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 occK th = - thmseq :-> + thmseq |> Seq.maps (fn r => - eqsubst_asm_tac' (skip_first_asm_occs_search + eqsubst_asm_tac' ctxt (skip_first_asm_occs_search searchf_tlr_unify_valid) occK r (i + ((Thm.nprems_of th) - nprems)) th); @@ -430,16 +312,10 @@ (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) -fun eqsubst_asm_meth occL inthms = +fun eqsubst_asm_meth ctxt occL inthms = Method.METHOD (fn facts => - HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms )); - -(* combination method that takes a flag (true indicates that subst -should be done to an assumption, false = apply to the conclusion of -the goal) as well as the theorems to use *) -fun meth ((asmflag, occL), inthms) ctxt = - if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms; + HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms )); (* syntax for options, given "(asm)" will give back true, without gives back false *) @@ -451,15 +327,16 @@ (Args.parens (Scan.repeat Args.nat)) || (Scan.succeed [0]); -(* method syntax, first take options, then theorems *) -fun meth_syntax meth src ctxt = - meth (snd (Method.syntax ((Scan.lift options_syntax) - -- (Scan.lift ith_syntax) - -- Attrib.local_thms) src ctxt)) - ctxt; +(* combination method that takes a flag (true indicates that subst +should be done to an assumption, false = apply to the conclusion of +the goal) as well as the theorems to use *) +fun subst_meth src = + Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src + #> (fn (ctxt, ((asmflag, occL), inthms)) => + (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms); -(* setup function for adding method to theory. *) + val setup = - [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")]; + [Method.add_method ("subst", subst_meth, "substiution with an equation")]; end;