paulson@15481: (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) dixon@15538: (* Title: Provers/eqsubst.ML paulson@15481: Author: Lucas Dixon, University of Edinburgh paulson@15481: lucas.dixon@ed.ac.uk dixon@15538: Modified: 18 Feb 2005 - Lucas - paulson@15481: Created: 29 Jan 2005 paulson@15481: *) paulson@15481: (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) paulson@15481: (* DESCRIPTION: paulson@15481: paulson@15481: A Tactic to perform a substiution using an equation. paulson@15481: paulson@15481: *) paulson@15481: (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) paulson@15481: dixon@15538: (* Logic specific data stub *) paulson@15481: signature EQRULE_DATA = paulson@15481: sig dixon@15538: paulson@15481: (* to make a meta equality theorem in the current logic *) paulson@15481: val prep_meta_eq : thm -> thm list dixon@15538: paulson@15481: end; paulson@15481: dixon@15538: paulson@15481: (* the signature of an instance of the SQSUBST tactic *) paulson@15481: signature EQSUBST_TAC = paulson@15481: sig dixon@15538: dixon@15550: type match = dixon@15550: ((Term.indexname * Term.typ) list (* type instantiations *) dixon@15550: * (Term.indexname * Term.term) list) (* term instantiations *) dixon@15550: * (string * Term.typ) list (* type abs env *) dixon@15550: * Term.term (* outer term *) dixon@15550: dixon@15538: val prep_subst_in_asm : dixon@15538: (Sign.sg (* sign for matching *) dixon@15538: -> int (* maxidx *) dixon@15538: -> 'a (* input object kind *) dixon@15538: -> BasicIsaFTerm.FcTerm (* focusterm to search under *) dixon@15538: -> 'b) (* result type *) dixon@15538: -> int (* subgoal to subst in *) dixon@15538: -> Thm.thm (* target theorem with subgoals *) dixon@15538: -> int (* premise to subst in *) dixon@15538: -> (Thm.cterm list (* certified free var placeholders for vars *) dixon@15538: * int (* premice no. to subst *) dixon@15538: * int (* number of assumptions of premice *) dixon@15538: * Thm.thm) (* premice as a new theorem for forward reasoning *) dixon@15538: * ('a -> 'b) (* matchf *) dixon@15538: dixon@15538: val prep_subst_in_asms : dixon@15538: (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) dixon@15538: -> int (* subgoal to subst in *) dixon@15538: -> Thm.thm (* target theorem with subgoals *) dixon@15538: -> ((Thm.cterm list (* certified free var placeholders for vars *) dixon@15538: * int (* premice no. to subst *) dixon@15538: * int (* number of assumptions of premice *) dixon@15538: * Thm.thm) (* premice as a new theorem for forward reasoning *) dixon@15538: * ('a -> 'b)) (* matchf *) dixon@15538: Seq.seq dixon@15538: dixon@15538: val apply_subst_in_asm : dixon@15538: int (* subgoal *) dixon@15538: -> Thm.thm (* overall theorem *) dixon@15538: -> (Thm.cterm list (* certified free var placeholders for vars *) dixon@15538: * int (* assump no being subst *) dixon@15538: * int (* num of premises of asm *) dixon@15538: * Thm.thm) (* premthm *) dixon@15538: -> Thm.thm (* rule *) dixon@15550: -> match dixon@15538: -> Thm.thm Seq.seq dixon@15538: dixon@15538: val prep_concl_subst : dixon@15538: (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *) dixon@15538: -> int (* subgoal *) dixon@15538: -> Thm.thm (* overall goal theorem *) dixon@15538: -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *) dixon@15538: dixon@15538: val apply_subst_in_concl : dixon@15538: int (* subgoal *) dixon@15538: -> Thm.thm (* thm with all goals *) dixon@15538: -> Thm.cterm list (* certified free var placeholders for vars *) dixon@15538: * Thm.thm (* trivial thm of goal concl *) dixon@15538: (* possible matches/unifiers *) dixon@15538: -> Thm.thm (* rule *) dixon@15550: -> match dixon@15538: -> Thm.thm Seq.seq (* substituted goal *) dixon@15538: paulson@15481: val eqsubst_asm_meth : Thm.thm list -> Proof.method paulson@15481: val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq paulson@15481: val eqsubst_asm_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq dixon@15538: paulson@15481: val eqsubst_meth : Thm.thm list -> Proof.method paulson@15481: val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq paulson@15481: val eqsubst_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq dixon@15538: paulson@15481: val meth : bool * Thm.thm list -> Proof.context -> Proof.method paulson@15481: val setup : (Theory.theory -> Theory.theory) list paulson@15481: end; paulson@15481: paulson@15481: functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) dixon@15538: : EQSUBST_TAC paulson@15481: = struct paulson@15481: dixon@15550: (* a type abriviation for match infomration *) dixon@15550: type match = dixon@15550: ((Term.indexname * Term.typ) list (* type instantiations *) dixon@15550: * (Term.indexname * Term.term) list) (* term instantiations *) dixon@15550: * (string * Term.typ) list (* type abs env *) dixon@15550: * Term.term (* outer term *) dixon@15550: dixon@15550: dixon@15538: (* FOR DEBUGGING... dixon@15538: type trace_subst_errT = int (* subgoal *) dixon@15538: * Thm.thm (* thm with all goals *) dixon@15538: * (Thm.cterm list (* certified free var placeholders for vars *) dixon@15538: * Thm.thm) (* trivial thm of goal concl *) dixon@15538: (* possible matches/unifiers *) dixon@15538: * Thm.thm (* rule *) dixon@15538: * (((Term.indexname * Term.typ) list (* type instantiations *) dixon@15538: * (Term.indexname * Term.term) list ) (* term instantiations *) dixon@15538: * (string * Term.typ) list (* Type abs env *) dixon@15538: * Term.term) (* outer term *); dixon@15538: dixon@15538: val trace_subst_err = (ref NONE : trace_subst_errT option ref); dixon@15538: val trace_subst_search = ref false; dixon@15538: exception trace_subst_exp of trace_subst_errT; dixon@15538: *) dixon@15538: dixon@15538: (* also defined in /HOL/Tools/inductive_codegen.ML, dixon@15538: maybe move this to seq.ML ? *) dixon@15538: infix 5 :->; dixon@15538: fun s :-> f = Seq.flat (Seq.map f s); dixon@15538: dixon@15538: (* search from the top to bottom, left to right *) dixon@15538: fun search_lr_f f ft = paulson@15481: let paulson@15481: fun maux ft = paulson@15481: let val t' = (IsaFTerm.focus_of_fcterm ft) dixon@15538: (* val _ = dixon@15538: if !trace_subst_search then dixon@15538: (writeln ("Examining: " ^ (TermLib.string_of_term t')); dixon@15538: TermLib.writeterm t'; ()) dixon@15538: else (); *) paulson@15481: in paulson@15481: (case t' of dixon@15538: (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), dixon@15538: Seq.append(f ft, paulson@15481: maux (IsaFTerm.focus_right ft))) paulson@15481: | (Abs _) => Seq.append (f ft, maux (IsaFTerm.focus_abs ft)) paulson@15481: | leaf => f ft) end paulson@15481: in maux ft end; paulson@15481: dixon@15538: fun search_for_match sgn maxidx lhs = paulson@15481: IsaFTerm.find_fcterm_matches dixon@15538: search_lr_f paulson@15481: (IsaFTerm.clean_unify_ft sgn maxidx lhs); paulson@15481: dixon@15538: (* apply a substitution in the conclusion of the theorem th *) dixon@15538: (* cfvs are certified free var placeholders for goal params *) dixon@15538: (* conclthm is a theorem of for just the conclusion *) dixon@15538: (* m is instantiation/match information *) dixon@15538: (* rule is the equation for substitution *) dixon@15538: fun apply_subst_in_concl i th (cfvs, conclthm) rule m = dixon@15538: (RWInst.rw m rule conclthm) dixon@15538: |> IsaND.schemify_frees_to_vars cfvs dixon@15538: |> RWInst.beta_eta_contract_tac dixon@15538: |> (fn r => Tactic.rtac r i th); paulson@15481: dixon@15538: (* dixon@15538: ? is the following equivalent to rtac ? paulson@15481: dixon@15538: |> Thm.lift_rule (th, i) dixon@15538: |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th) dixon@15538: dixon@15538: *) paulson@15481: paulson@15481: (* substitute within the conclusion of goal i of gth, using a meta dixon@15538: equation rule. Note that we assume rule has var indicies zero'd *) dixon@15538: fun prep_concl_subst searchf i gth = paulson@15481: let paulson@15481: val th = Thm.incr_indexes 1 gth; paulson@15481: val tgt_term = Thm.prop_of th; paulson@15481: paulson@15481: val sgn = Thm.sign_of_thm th; paulson@15481: val ctermify = Thm.cterm_of sgn; paulson@15481: val trivify = Thm.trivial o ctermify; paulson@15481: paulson@15481: val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; paulson@15481: val cfvs = rev (map ctermify fvs); paulson@15481: dixon@15538: val conclterm = Logic.strip_imp_concl fixedbody; dixon@15538: val conclthm = trivify conclterm; dixon@15538: val maxidx = Term.maxidx_of_term conclterm; paulson@15481: in dixon@15538: ((cfvs, conclthm), dixon@15538: (fn lhs => searchf sgn maxidx lhs dixon@15538: ((IsaFTerm.focus_right dixon@15538: o IsaFTerm.focus_left dixon@15538: o IsaFTerm.fcterm_of_term dixon@15538: o Thm.prop_of) conclthm))) paulson@15481: end; paulson@15481: dixon@15538: paulson@15481: (* substitute using an object or meta level equality *) paulson@15481: fun eqsubst_tac' instepthm i th = dixon@15538: let dixon@15538: val (cvfsconclthm, findmatchf) = dixon@15538: prep_concl_subst search_for_match i th; dixon@15538: dixon@15538: val stepthms = dixon@15538: Seq.map Drule.zero_var_indexes dixon@15538: (Seq.of_list (EqRuleData.prep_meta_eq instepthm)); dixon@15538: dixon@15538: fun rewrite_with_thm r = dixon@15538: let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); dixon@15538: in (findmatchf lhs) dixon@15538: :-> (apply_subst_in_concl i th cvfsconclthm r) end; dixon@15538: dixon@15538: in (stepthms :-> rewrite_with_thm) end; dixon@15538: dixon@15538: paulson@15481: (* substitute using one of the given theorems *) paulson@15481: fun eqsubst_tac instepthms i th = dixon@15538: if Thm.nprems_of th < i then Seq.empty else dixon@15538: (Seq.of_list instepthms) :-> (fn r => eqsubst_tac' r i th); paulson@15481: paulson@15481: (* inthms are the given arguments in Isar, and treated as eqstep with paulson@15481: the first one, then the second etc *) paulson@15481: fun eqsubst_meth inthms = paulson@15481: Method.METHOD dixon@15538: (fn facts => dixon@15538: HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac inthms )); paulson@15481: paulson@15481: dixon@15538: fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = dixon@15538: (RWInst.rw m rule pth) dixon@15538: |> Thm.permute_prems 0 ~1 dixon@15538: |> IsaND.schemify_frees_to_vars cfvs dixon@15538: |> RWInst.beta_eta_contract_tac dixon@15538: |> (fn r => Tactic.dtac r i th); dixon@15538: dixon@15538: (* dixon@15538: ? should I be using bicompose what if we match more than one dixon@15538: assumption, even after instantiation ? (back will work, but it would dixon@15538: be nice to avoid the redudent search) dixon@15538: dixon@15538: something like... dixon@15538: |> Thm.lift_rule (th, i) dixon@15538: |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th) dixon@15538: dixon@15538: *) paulson@15481: paulson@15481: dixon@15538: (* prepare to substitute within the j'th premise of subgoal i of gth, dixon@15538: using a meta-level equation. Note that we assume rule has var indicies dixon@15538: zero'd. Note that we also assume that premt is the j'th premice of dixon@15538: subgoal i of gth. Note the repetition of work done for each dixon@15538: assumption, i.e. this can be made more efficient for search over dixon@15538: multiple assumptions. *) dixon@15538: fun prep_subst_in_asm searchf i gth j = paulson@15481: let paulson@15481: val th = Thm.incr_indexes 1 gth; paulson@15481: val tgt_term = Thm.prop_of th; paulson@15481: paulson@15481: val sgn = Thm.sign_of_thm th; paulson@15481: val ctermify = Thm.cterm_of sgn; paulson@15481: val trivify = Thm.trivial o ctermify; paulson@15481: paulson@15481: val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; paulson@15481: val cfvs = rev (map ctermify fvs); paulson@15481: dixon@15538: val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody)); dixon@15538: val asm_nprems = length (Logic.strip_imp_prems asmt); dixon@15538: dixon@15538: val pth = trivify asmt; dixon@15538: val maxidx = Term.maxidx_of_term asmt; dixon@15538: paulson@15481: in dixon@15538: ((cfvs, j, asm_nprems, pth), dixon@15538: (fn lhs => (searchf sgn maxidx lhs dixon@15538: ((IsaFTerm.focus_right dixon@15538: o IsaFTerm.fcterm_of_term dixon@15538: o Thm.prop_of) pth)))) paulson@15481: end; paulson@15481: dixon@15538: (* prepare subst in every possible assumption *) dixon@15538: fun prep_subst_in_asms searchf i gth = dixon@15538: Seq.map dixon@15538: (prep_subst_in_asm searchf i gth) dixon@15538: (Seq.of_list (IsaPLib.mk_num_list dixon@15538: (length (Logic.prems_of_goal (Thm.prop_of gth) i)))); dixon@15538: dixon@15538: dixon@15538: (* substitute in an assumption using an object or meta level equality *) paulson@15481: fun eqsubst_asm_tac' instepthm i th = dixon@15538: let dixon@15538: val asmpreps = prep_subst_in_asms search_for_match i th; dixon@15538: val stepthms = dixon@15538: Seq.map Drule.zero_var_indexes dixon@15538: (Seq.of_list (EqRuleData.prep_meta_eq instepthm)) dixon@15538: dixon@15538: fun rewrite_with_thm (asminfo, findmatchf) r = dixon@15538: let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); dixon@15538: in (findmatchf lhs) dixon@15538: :-> (apply_subst_in_asm i th asminfo r) end; dixon@15538: in dixon@15538: (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a)) paulson@15481: end; paulson@15481: paulson@15481: (* substitute using one of the given theorems *) paulson@15481: fun eqsubst_asm_tac instepthms i th = dixon@15538: if Thm.nprems_of th < i then Seq.empty else dixon@15538: (Seq.of_list instepthms) :-> (fn r => eqsubst_asm_tac' r i th); paulson@15481: paulson@15481: (* inthms are the given arguments in Isar, and treated as eqstep with paulson@15481: the first one, then the second etc *) paulson@15481: fun eqsubst_asm_meth inthms = paulson@15481: Method.METHOD dixon@15538: (fn facts => dixon@15538: HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms )); paulson@15481: paulson@15481: (* combination method that takes a flag (true indicates that subst paulson@15481: should be done to an assumption, false = apply to the conclusion of paulson@15481: the goal) as well as the theorems to use *) paulson@15481: fun meth (asmflag, inthms) ctxt = paulson@15481: if asmflag then eqsubst_asm_meth inthms else eqsubst_meth inthms; paulson@15481: paulson@15481: (* syntax for options, given "(asm)" will give back true, without paulson@15481: gives back false *) paulson@15481: val options_syntax = paulson@15481: (Args.parens (Args.$$$ "asm") >> (K true)) || paulson@15481: (Scan.succeed false); paulson@15481: paulson@15481: (* method syntax, first take options, then theorems *) paulson@15481: fun meth_syntax meth src ctxt = paulson@15481: meth (snd (Method.syntax ((Scan.lift options_syntax) paulson@15481: -- Attrib.local_thms) src ctxt)) paulson@15481: ctxt; paulson@15481: paulson@15481: (* setup function for adding method to theory. *) paulson@15481: val setup = paulson@15481: [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")]; paulson@15481: paulson@15481: end;