diff --git a/src/Provers/eqsubst.ML b/src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML +++ b/src/Provers/eqsubst.ML @@ -1,421 +1,449 @@ (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Title: Provers/eqsubst.ML 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. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Logic specific data stub *) signature EQRULE_DATA = sig (* 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_TAC = sig + 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 *) * (string * Term.typ) list (* fake named type abs env *) * (string * Term.typ) list (* type abs env *) * Term.term (* outer term *) 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 *) -> 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 *) val prep_subst_in_asms : (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) -> 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 val apply_subst_in_asm : int (* subgoal *) -> Thm.thm (* overall theorem *) -> (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 -> Thm.thm Seq.seq val prep_concl_subst : (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *) -> int (* subgoal *) -> Thm.thm (* overall goal theorem *) -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *) val apply_subst_in_concl : int (* subgoal *) -> Thm.thm (* thm with all goals *) -> Thm.cterm list (* certified free var placeholders for vars *) * Thm.thm (* trivial thm of goal concl *) (* possible matches/unifiers *) -> Thm.thm (* rule *) -> match -> Thm.thm Seq.seq (* substituted goal *) val searchf_tlr_unify_all : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> match Seq.seq Seq.seq) val searchf_tlr_unify_valid : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> match Seq.seq Seq.seq) 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' : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq 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' : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> 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 (* a type abriviation for match information *) type match = ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *) * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *) * (string * Term.typ) list (* fake named type abs env *) * (string * Term.typ) list (* type abs env *) * Term.term (* outer term *) (* FOR DEBUGGING... type trace_subst_errT = int (* subgoal *) * Thm.thm (* thm with all goals *) * (Thm.cterm list (* certified free var placeholders for vars *) * Thm.thm) (* trivial thm of goal concl *) (* possible matches/unifiers *) * Thm.thm (* rule *) * (((Term.indexname * Term.typ) list (* type instantiations *) * (Term.indexname * Term.term) list ) (* term instantiations *) * (string * Term.typ) list (* Type abs env *) * Term.term) (* outer term *); val trace_subst_err = (ref NONE : trace_subst_errT option ref); val trace_subst_search = ref false; 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 fun maux ft = let val t' = (IsaFTerm.focus_of_fcterm ft) (* val _ = if !trace_subst_search then (writeln ("Examining: " ^ (TermLib.string_of_term t')); TermLib.writeterm t'; ()) else (); *) in (case t' of (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), Seq.cons(f ft, maux (IsaFTerm.focus_right ft))) | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft)) | leaf => Seq.single (f ft)) end in maux ft end; (* search from top, left to right, then down *) 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; (* search all unifications *) fun searchf_tlr_unify_all sgn maxidx lhs = IsaFTerm.find_fcterm_matches search_tlr_all_f (IsaFTerm.clean_unify_ft sgn maxidx lhs); (* search only for 'valid' unifiers (non abs subterms and non vars) *) fun searchf_tlr_unify_valid sgn maxidx 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; (* apply a substitution in the conclusion of the theorem th *) (* cfvs are certified free var placeholders for goal params *) (* conclthm is a theorem of for just the conclusion *) (* m is instantiation/match information *) (* rule is the equation for substitution *) fun apply_subst_in_concl i th (cfvs, conclthm) rule m = (RWInst.rw m rule conclthm) |> 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 = let val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn; val trivify = Thm.trivial o ctermify; val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; val cfvs = rev (map ctermify fvs); val conclterm = Logic.strip_imp_concl fixedbody; val conclthm = trivify conclterm; val maxidx = Term.maxidx_of_term conclterm; 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))) 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 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) :-> (apply_subst_in_concl i th cvfsconclthm r) end; in (stepthms :-> rewrite_with_thm) end; +(* Tactic.distinct_subgoals_tac *) + +(* custom version of distinct subgoals that works with term and + type variables. Asssumes th is in beta-eta normal form. + Also, does nothing if flexflex contraints are present. *) +fun distinct_subgoals th = + if List.null (Thm.tpairs_of th) then + let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th + val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm + in + IsaND.unfix_frees_and_tfrees + fixes + (Drule.implies_intr_list + (Library.gen_distinct + (fn (x, y) => Thm.term_of x = Thm.term_of y) + cprems) fixedthconcl) + end + else th; (* General substiuttion of multiple occurances using one of 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 = 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 occ searchf_tlr_unify_valid) r (i + ((Thm.nprems_of th) - nprems)) th); in - 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 + (Library.sort (Library.rev_order + o Library.int_ord) occL)) th) end - 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 *) fun eqsubst_meth occL inthms = Method.METHOD (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) *) (* prepare to substitute within the j'th premise of subgoal i of gth, using a meta-level equation. Note that we assume rule has var indicies zero'd. Note that we also assume that premt is the j'th premice of 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 = let val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn; val trivify = Thm.trivial o ctermify; val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; val cfvs = rev (map ctermify fvs); val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody)); val asm_nprems = length (Logic.strip_imp_prems asmt); 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; (* 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)))); (* substitute in an assumption using an object or meta level equality *) fun eqsubst_asm_tac' searchf instepthm i th = let val asmpreps = prep_subst_in_asms searchf i th; val stepthms = Seq.map Drule.zero_var_indexes (Seq.of_list (EqRuleData.prep_meta_eq instepthm)) 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; 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'; (* 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 = 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; (* syntax for options, given "(asm)" will give back true, without gives back false *) val options_syntax = (Args.parens (Args.$$$ "asm") >> (K true)) || (Scan.succeed false); val ith_syntax = (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; (* 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.")]; end; \ No newline at end of file diff --git a/src/Pure/IsaPlanner/isand.ML b/src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML +++ b/src/Pure/IsaPlanner/isand.ML @@ -1,635 +1,644 @@ (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Title: isand.ML Author: Lucas Dixon, University of Edinburgh lucas.dixon@ed.ac.uk Updated: 26 Apr 2005 Date: 6 Aug 2004 *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* DESCRIPTION: Natural Deduction tools For working with Isabelle theorems in a natural detuction style. ie, not having to deal with meta level quantified varaibles, instead, we work with newly introduced frees, and hide the "all"'s, exporting results from theorems proved with the frees, to solve the all cases of the previous goal. This allows resolution to do proof search normally. Note: A nice idea: allow exporting to solve any subgoal, thus allowing the interleaving of proof, or provide a structure for the ordering of proof, thus allowing proof attempts in parrell, but recording the order to apply things in. debugging tools: fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); fun asm_read s = (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); THINK: are we really ok with our varify name w.r.t the prop - do we also need to avoid names in the hidden hyps? What about unification contraints in flex-flex pairs - might they also have extra free vars? *) signature ISA_ND = sig (* export data *) datatype export = export of {gth: Thm.thm, (* initial goal theorem *) sgid: int, (* subgoal id which has been fixed etc *) fixes: Thm.cterm list, (* frees *) assumes: Thm.cterm list} (* assumptions *) val fixes_of_exp : export -> Thm.cterm list val export_back : export -> Thm.thm -> Thm.thm Seq.seq val export_solution : export -> Thm.thm -> Thm.thm val export_solutions : export list * Thm.thm -> Thm.thm (* inserting meta level params for frees in the conditions *) val allify_conditions : (Term.term -> Thm.cterm) -> (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list val allify_conditions' : (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list val assume_allified : Sign.sg -> (string * Term.sort) list * (string * Term.typ) list -> Term.term -> (Thm.cterm * Thm.thm) (* meta level fixed params (i.e. !! vars) *) val fix_alls_in_term : Term.term -> Term.term * Term.term list val fix_alls_term : int -> Term.term -> Term.term * Term.term list val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list val fix_alls : int -> Thm.thm -> Thm.thm * export (* meta variables in types and terms *) val fix_tvars_to_tfrees_in_terms : string list (* avoid these names *) -> Term.term list -> (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *) val fix_vars_to_frees_in_terms : string list (* avoid these names *) -> Term.term list -> (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *) val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm val fix_vars_and_tvars : Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm val unfix_frees_and_tfrees : (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm (* assumptions/subgoals *) val assume_prems : int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list (* abstracts cterms (vars) to locally meta-all bounds *) val prepare_goal_export : string list * Thm.cterm list -> Thm.thm -> int * Thm.thm val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) end structure IsaND : ISA_ND = struct (* Solve *some* subgoal of "th" directly by "sol" *) (* Note: this is probably what Markus ment to do upon export of a "show" but maybe he used RS/rtac instead, which would wrongly lead to failing if there are premices to the shown goal. given: sol : Thm.thm = [| Ai... |] ==> Ci th : Thm.thm = [| ... [| Ai... |] ==> Ci ... |] ==> G results in: [| ... [| Ai-1... |] ==> Ci-1 [| Ai+1... |] ==> Ci+1 ... |] ==> G i.e. solves some subgoal of th that is identical to sol. *) fun solve_with sol th = let fun solvei 0 = Seq.empty | solvei i = Seq.append (bicompose false (false,sol,0) i th, solvei (i - 1)) in solvei (Thm.nprems_of th) end; (* Given ctertmify function, (string,type) pairs capturing the free vars that need to be allified in the assumption, and a theorem with assumptions possibly containing the free vars, then we give back the assumptions allified as hidden hyps. Given: x th: A vs ==> B vs Results in: "B vs" [!!x. A x] *) fun allify_conditions ctermify Ts th = let val premts = Thm.prems_of th; fun allify_prem_var (vt as (n,ty),t) = (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) fun allify_prem Ts p = foldr allify_prem_var p Ts val cTs = map (ctermify o Free) Ts val cterm_asms = map (ctermify o allify_prem Ts) premts val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms in (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms) end; fun allify_conditions' Ts th = allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th; (* allify types *) fun allify_typ ts ty = let fun trec (x as (TFree (s,srt))) = (case Library.find_first (fn (s2,srt2) => s = s2) ts of NONE => x | SOME (s2,_) => TVar ((s,0),srt)) (* Maybe add in check here for bad sorts? if srt = srt2 then TVar ((s,0),srt) else raise ("thaw_typ", ts, ty) *) | trec (Type (s,typs)) = Type (s, map trec typs) | trec (v as TVar _) = v; in trec ty end; (* implicit types and term *) fun allify_term_typs ty = Term.map_term_types (allify_typ ty); (* allified version of term, given frees to allify over. Note that we only allify over the types on the given allified cterm, we can't do this for the theorem as we are not allowed type-vars in the hyp. *) fun assume_allified sgn (tyvs,vs) t = let fun allify_var (vt as (n,ty),t) = (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) fun allify Ts p = List.foldr allify_var p Ts val ctermify = Thm.cterm_of sgn; val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs val allified_term = t |> allify vs; val ct = ctermify allified_term; val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term); in (typ_allified_ct, Drule.forall_elim_vars 0 (Thm.assume ct)) end; (* change type-vars to fresh type frees *) fun fix_tvars_to_tfrees_in_terms names ts = let val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts); val tvars = List.foldr Term.add_term_tvars [] ts; val (names',renamings) = List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => let val n2 = Term.variant Ns n in (n2::Ns, (tv, (n2,s))::Rs) end) (tfree_names @ names,[]) tvars; in renamings end; fun fix_tvars_to_tfrees th = let val sign = Thm.sign_of_thm th; val ctypify = Thm.ctyp_of sign; - val renamings = fix_tvars_to_tfrees_in_terms [] [Thm.prop_of th]; + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); + val renamings = fix_tvars_to_tfrees_in_terms + [] ((Thm.prop_of th) :: tpairs); val crenamings = map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) renamings; val fixedfrees = map snd crenamings; in (fixedfrees, Thm.instantiate (crenamings, []) th) end; (* change type-free's to type-vars *) fun unfix_tfrees ns th = let val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) ns) val skiptfrees = Term.add_term_tfrees (Thm.prop_of th,[]) \\ varfiytfrees; in fst (Thm.varifyT' skiptfrees th) end; (* change schematic/meta vars to fresh free vars *) fun fix_vars_to_frees_in_terms names ts = let val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts); val Ns = List.foldr Term.add_term_names names ts; val (_,renamings) = Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => let val n2 = Term.variant Ns n in (n2 :: Ns, (v, (n2,ty)) :: Rs) end) ((Ns,[]), vars); in renamings end; fun fix_vars_to_frees th = let val ctermify = Thm.cterm_of (Thm.sign_of_thm th) - val renamings = fix_vars_to_frees_in_terms [] [Thm.prop_of th]; + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); + val renamings = fix_vars_to_frees_in_terms + [] ([Thm.prop_of th] @ tpairs); val crenamings = map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) renamings; val fixedfrees = map snd crenamings; in (fixedfrees, Thm.instantiate ([], crenamings) th) end; fun fix_tvars_upto_idx ix th = let val sgn = Thm.sign_of_thm th; val ctypify = Thm.ctyp_of sgn + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); val prop = (Thm.prop_of th); - val tvars = Term.term_tvars prop; + val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); val ctyfixes = Library.mapfilter (fn (v as ((s,i),ty)) => if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) else NONE) tvars; in Thm.instantiate (ctyfixes, []) th end; fun fix_vars_upto_idx ix th = let val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); val prop = (Thm.prop_of th); - val vars = map Term.dest_Var (Term.term_vars prop); + val vars = map Term.dest_Var (List.foldr Term.add_term_vars + [] (prop :: tpairs)); val cfixes = Library.mapfilter (fn (v as ((s,i),ty)) => if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) else NONE) vars; in Thm.instantiate ([], cfixes) th end; (* make free vars into schematic vars with index zero *) fun unfix_frees frees = apply (map (K (Drule.forall_elim_var 0)) frees) o Drule.forall_intr_list frees; (* fix term and type variables *) fun fix_vars_and_tvars th = let val (tvars, th') = fix_tvars_to_tfrees th val (vars, th'') = fix_vars_to_frees th' in ((vars, tvars), th'') end; (* implicit Thm.thm argument *) +(* assumes: vars may contain fixed versions of the frees *) +(* THINK: what if vs already has types varified? *) fun unfix_frees_and_tfrees (vs,tvs) = - (unfix_frees vs o unfix_tfrees tvs); + (unfix_tfrees tvs o unfix_frees vs); (* datatype to capture an exported result, ie a fix or assume. *) datatype export = export of {fixes : Thm.cterm list, (* fixed vars *) assumes : Thm.cterm list, (* hidden hyps/assumed prems *) sgid : int, gth : Thm.thm}; (* subgoal/goalthm *) fun fixes_of_exp (export rep) = #fixes rep; (* export the result of the new goal thm, ie if we reduced teh subgoal, then we get a new reduced subtgoal with the old all-quantified variables *) local (* allify puts in a meta level univ quantifier for a free variavble *) fun allify_term (v, t) = let val vt = #t (Thm.rep_cterm v) val (n,ty) = Term.dest_Free vt in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; fun allify_for_sg_term ctermify vs t = let val t_alls = foldr allify_term t vs; val ct_alls = ctermify t_alls; in (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) end; (* lookup type of a free var name from a list *) fun lookupfree vs vn = case Library.find_first (fn (n,ty) => n = vn) vs of NONE => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term") | SOME x => x; in fun export_back (export {fixes = vs, assumes = hprems, sgid = i, gth = gth}) newth = let val sgn = Thm.sign_of_thm newth; val ctermify = Thm.cterm_of sgn; val sgs = prems_of newth; val (sgallcts, sgthms) = Library.split_list (map (allify_for_sg_term ctermify vs) sgs); val minimal_newth = (Library.foldl (fn ( newth', sgthm) => Drule.compose_single (sgthm, 1, newth')) (newth, sgthms)); val allified_newth = minimal_newth |> Drule.implies_intr_list hprems |> Drule.forall_intr_list vs val newth' = Drule.implies_intr_list sgallcts allified_newth in bicompose false (false, newth', (length sgallcts)) i gth end; (* Given "vs" : names of free variables to abstract over, Given cterms : premices to abstract over (P1... Pn) in terms of vs, Given a thm of the form: P1 vs; ...; Pn vs ==> Goal(C vs) Gives back: (n, length of given cterms which have been allified [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm *) (* note: C may contain further premices etc Note that cterms is the assumed facts, ie prems of "P1" that are reintroduced in allified form. *) fun prepare_goal_export (vs, cterms) th = let val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn; val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th)) val cfrees = map (ctermify o Free o lookupfree allfrees) vs val sgs = prems_of th; val (sgallcts, sgthms) = Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); val minimal_th = (Library.foldl (fn ( th', sgthm) => Drule.compose_single (sgthm, 1, th')) (th, sgthms)) RS Drule.rev_triv_goal; val allified_th = minimal_th |> Drule.implies_intr_list cterms |> Drule.forall_intr_list cfrees val th' = Drule.implies_intr_list sgallcts allified_th in ((length sgallcts), th') end; end; (* exporting function that takes a solution to the fixed/assumed goal, and uses this to solve the subgoal in the main theorem *) fun export_solution (export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth = let val solth' = solth |> Drule.implies_intr_list hcprems |> Drule.forall_intr_list cfvs in Drule.compose_single (solth', i, gth) end; fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs; (* fix parameters of a subgoal "i", as free variables, and create an exporting function that will use the result of this proved goal to show the goal in the original theorem. Note, an advantage of this over Isar is that it supports instantiation of unkowns in the earlier theorem, ie we can do instantiation of meta vars! avoids constant, free and vars names. loosely corresponds to: Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm Result: ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, expf : ("As ==> SGi x'" : thm) -> ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) *) fun fix_alls_in_term alledt = let val t = Term.strip_all_body alledt; val alls = rev (Term.strip_all_vars alledt); val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) val names = Term.add_term_names (t,varnames); val fvs = map Free ((Term.variantlist (map fst alls, names)) ~~ (map snd alls)); in ((subst_bounds (fvs,t)), fvs) end; fun fix_alls_term i t = let val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) val names = Term.add_term_names (t,varnames); val gt = Logic.get_goal t i; val body = Term.strip_all_body gt; val alls = rev (Term.strip_all_vars gt); val fvs = map Free ((Term.variantlist (map fst alls, names)) ~~ (map snd alls)); in ((subst_bounds (fvs,body)), fvs) end; fun fix_alls_cterm i th = let val ctermify = Thm.cterm_of (Thm.sign_of_thm th); val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th); val cfvs = rev (map ctermify fvs); val ct_body = ctermify fixedbody in (ct_body, cfvs) end; fun fix_alls' i = (apfst Thm.trivial) o (fix_alls_cterm i); (* hide other goals *) (* note the export goal is rotated by (i - 1) and will have to be unrotated to get backto the originial position(s) *) fun hide_other_goals th = let (* tl beacuse fst sg is the goal we are interested in *) val cprems = tl (Drule.cprems_of th) val aprems = map Thm.assume cprems in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end; (* a nicer version of the above that leaves only a single subgoal (the other subgoals are hidden hyps, that the exporter suffles about) namely the subgoal that we were trying to solve. *) (* loosely corresponds to: Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm Result: ("(As ==> SGi x') ==> SGi x'" : thm, expf : ("SGi x'" : thm) -> ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) *) fun fix_alls i th = let val (fixed_gth, fixedvars) = fix_alls' i th val (sml_gth, othergoals) = hide_other_goals fixed_gth in (sml_gth, export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end; (* assume the premises of subgoal "i", this gives back a list of assumed theorems that are the premices of subgoal i, it also gives back a new goal thm and an exporter, the new goalthm is as the old one, but without the premices, and the exporter will use a proof of the new goalthm, possibly using the assumed premices, to shoe the orginial goal. Note: Dealing with meta vars, need to meta-level-all them in the shyps, which we can later instantiate with a specific value.... ? think about this... maybe need to introduce some new fixed vars and then remove them again at the end... like I do with rw_inst. loosely corresponds to: Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm Result: (["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions "SGi ==> SGi" : thm, -- new goal "SGi" ["A0" ... "An"] : thm -> -- export function ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) *) fun assume_prems i th = let val t = (prop_of th); val gt = Logic.get_goal t i; val _ = case Term.strip_all_vars gt of [] => () | _ => raise ERROR_MESSAGE "assume_prems: goal has params" val body = gt; val prems = Logic.strip_imp_prems body; val concl = Logic.strip_imp_concl body; val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn; val cprems = map ctermify prems; val aprems = map Thm.assume cprems; val gthi = Thm.trivial (ctermify concl); (* fun explortf thi = Drule.compose (Drule.implies_intr_list cprems thi, i, th) *) in (aprems, gthi, cprems) end; (* first fix the variables, then assume the assumptions *) (* loosely corresponds to: Given "[| SG0; ... !! xs. [| A0 xs; ... An xs |] ==> SGi xs; ... SGm |] ==> G" : thm Result: (["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions "SGi xs' ==> SGi xs'" : thm, -- new goal "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) *) (* Note: the fix_alls actually pulls through all the assumptions which means that the second export is not needed. *) fun fixes_and_assumes i th = let val (fixgth, exp1) = fix_alls i th val (assumps, goalth, _) = assume_prems 1 fixgth in (assumps, goalth, exp1) end; (* Fixme: allow different order of subgoals given to expf *) (* make each subgoal into a separate thm that needs to be proved *) (* loosely corresponds to: Given "[| SG0; ... SGm |] ==> G" : thm Result: (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ["SG0", ..., "SGm"] : thm list -> -- export function "G" : thm) *) fun subgoal_thms th = let val t = (prop_of th); val prems = Logic.strip_imp_prems t; val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn; val aprems = map (Thm.trivial o ctermify) prems; fun explortf premths = Drule.implies_elim_list th premths in (aprems, explortf) end; (* make all the premices of a theorem hidden, and provide an unhide function, that will bring them back out at a later point. This is useful if you want to get back these premices, after having used the theorem with the premices hidden *) (* loosely corresponds to: Given "As ==> G" : thm Result: ("G [As]" : thm, "G [As]" : thm -> "As ==> G" : thm *) fun hide_prems th = let val cprems = Drule.cprems_of th; val aprems = map Thm.assume cprems; (* val unhidef = Drule.implies_intr_list cprems; *) in (Drule.implies_elim_list th aprems, cprems) end; (* Fixme: allow different order of subgoals in exportf *) (* as above, but also fix all parameters in all subgoals, and uses fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent subgoals. *) (* loosely corresponds to: Given "[| !! x0s. A0s x0s ==> SG0 x0s; ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm Result: (["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function "G" : thm) *) (* requires being given solutions! *) fun fixed_subgoal_thms th = let val (subgoals, expf) = subgoal_thms th; (* fun export_sg (th, exp) = exp th; *) fun export_sgs expfs solthms = expf (map2 (op |>) (solthms, expfs)); (* expf (map export_sg (ths ~~ expfs)); *) in apsnd export_sgs (Library.split_list (map (apsnd export_solution o fix_alls 1) subgoals)) end; end; diff --git a/src/Pure/IsaPlanner/rw_inst.ML b/src/Pure/IsaPlanner/rw_inst.ML --- a/src/Pure/IsaPlanner/rw_inst.ML +++ b/src/Pure/IsaPlanner/rw_inst.ML @@ -1,294 +1,303 @@ (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Title: sys/rw_inst.ML Author: Lucas Dixon, University of Edinburgh lucas.dixon@ed.ac.uk Created: 25 Aug 2004 *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* DESCRIPTION: rewriting using a conditional meta-equality theorem which supports schematic variable instantiation. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) signature RW_INST = sig (* Rewrite: give it instantiation infromation, a rule, and the target thm, and it will return the rewritten target thm *) val rw : ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *) (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *) * (string * Term.typ) list (* Fake named bounds + types *) * (string * Term.typ) list (* names of bound + types *) * Term.term -> (* outer term for instantiation *) Thm.thm -> (* rule with indexies lifted *) Thm.thm -> (* target thm *) Thm.thm (* rewritten theorem possibly with additional premises for rule conditions *) (* used tools *) val mk_abstractedrule : (string * Term.typ) list (* faked outer bound *) -> (string * Term.typ) list (* hopeful name of outer bounds *) -> Thm.thm -> Thm.cterm list * Thm.thm val mk_fixtvar_tyinsts : (Term.indexname * (Term.sort * Term.typ)) list -> Term.term list -> ((string * int) * (Term.sort * Term.typ)) list * (string * Term.sort) list val mk_renamings : Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list val new_tfree : ((string * int) * Term.sort) * (((string * int) * (Term.sort * Term.typ)) list * string list) -> ((string * int) * (Term.sort * Term.typ)) list * string list val cross_inst : (Term.indexname * (Term.typ * Term.term)) list -> (Term.indexname *(Term.typ * Term.term)) list val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list -> (Term.indexname * (Term.sort * Term.typ)) list val beta_contract : Thm.thm -> Thm.thm val beta_eta_contract : Thm.thm -> Thm.thm end; structure RWInst (* : RW_INST *) = struct (* beta contract the theorem *) fun beta_contract thm = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; (* beta-eta contract the theorem *) fun beta_eta_contract thm = let val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 in thm3 end; (* Given a list of variables that were bound, and a that has been instantiated with free variable placeholders for the bound vars, it creates an abstracted version of the theorem, with local bound vars as lambda-params: Ts: ("x", ty) rule:: C :x ==> P :x = Q :x results in: ("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) note: assumes rule is instantiated *) (* Note, we take abstraction in the order of last abstraction first *) fun mk_abstractedrule TsFake Ts rule = let val ctermify = Thm.cterm_of (Thm.sign_of_thm rule); (* now we change the names of temporary free vars that represent bound vars with binders outside the redex *) val prop = Thm.prop_of rule; val names = TermLib.usednames_of_thm rule; val (fromnames,tonames,names2,Ts') = Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => let val n2 = Term.variant names n in (ctermify (Free(faken,ty)) :: rnf, ctermify (Free(n2,ty)) :: rnt, n2 :: names, (n2,ty) :: Ts'') end) (([],[],names, []), TsFake~~Ts); (* rename conflicting free's in the rule to avoid cconflicts with introduced vars from bounds outside in redex *) val rule' = rule |> Drule.forall_intr_list fromnames |> Drule.forall_elim_list tonames; (* make unconditional rule and prems *) val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') rule'; (* using these names create lambda-abstracted version of the rule *) val abstractions = rev (Ts' ~~ tonames); val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => Thm.abstract_rule n ct th) (uncond_rule, abstractions); in (cprems, abstract_rule) end; (* given names to avoid, and vars that need to be fixed, it gives unique new names to the vars so that they can be fixed as free variables *) (* make fixed unique free variable instantiations for non-ground vars *) (* Create a table of vars to be renamed after instantiation - ie other uninstantiated vars in the hyps of the rule ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) fun mk_renamings tgt rule_inst = let val rule_conds = Thm.prems_of rule_inst val names = foldr Term.add_term_names [] (tgt :: rule_conds); val (conds_tyvs,cond_vs) = Library.foldl (fn ((tyvs, vs), t) => (Library.union (Term.term_tvars t, tyvs), Library.union (map Term.dest_Var (Term.term_vars t), vs))) (([],[]), rule_conds); val termvars = map Term.dest_Var (Term.term_vars tgt); val vars_to_fix = Library.union (termvars, cond_vs); val (renamings, names2) = foldr (fn (((n,i),ty), (vs, names')) => let val n' = Term.variant names' n in ((((n,i),ty), Free (n', ty)) :: vs, n'::names') end) ([], names) vars_to_fix; in renamings end; (* make a new fresh typefree instantiation for the given tvar *) fun new_tfree (tv as (ix,sort), (pairs,used)) = let val v = variant used (string_of_indexname ix) in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; (* make instantiations to fix type variables that are not already instantiated (in ignore_ixs) from the list of terms. *) fun mk_fixtvar_tyinsts ignore_insts ts = let val ignore_ixs = map fst ignore_insts; val (tvars, tfrees) = foldr (fn (t, (varixs, tfrees)) => (Term.add_term_tvars (t,varixs), Term.add_term_tfrees (t,tfrees))) ([],[]) ts; val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars in (fixtyinsts, tfrees) end; (* cross-instantiate the instantiations - ie for each instantiation replace all occurances in other instantiations - no loops are possible and thus only one-parsing of the instantiations is necessary. *) fun cross_inst insts = let fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); in cross_instL (insts, []) end; (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) fun cross_inst_typs insts = let fun instL (ix, (srt,ty)) = map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); in cross_instL (insts, []) end; -(* assume that rule and target_thm have distinct var names *) -(* THINK: efficient version with tables for vars for: target vars, -introduced vars, and rule vars, for quicker instantiation? *) -(* The outerterm defines which part of the target_thm was modified *) -(* Note: we take Ts in the upterm order, ie last abstraction first., -and with an outeterm where the abstracted subterm has the arguments in -the revered order, ie first abstraction first. *) +(* assume that rule and target_thm have distinct var names. THINK: +efficient version with tables for vars for: target vars, introduced +vars, and rule vars, for quicker instantiation? The outerterm defines +which part of the target_thm was modified. Note: we take Ts in the +upterm order, ie last abstraction first., and with an outeterm where +the abstracted subterm has the arguments in the revered order, ie +first abstraction first. FakeTs has abstractions using the fake name +- ie the name distinct from all other abstractions. *) + fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = let (* general signature info *) val target_sign = (Thm.sign_of_thm target_thm); val ctermify = Thm.cterm_of target_sign; val ctypeify = Thm.ctyp_of target_sign; (* fix all non-instantiated tvars *) val (fixtyinsts, othertfrees) = mk_fixtvar_tyinsts nonfixed_typinsts [Thm.prop_of rule, Thm.prop_of target_thm]; - + val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty)) + fixtyinsts; val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) val ctyp_insts = - map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) typinsts; + map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) + typinsts; (* type instantiated versions *) val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts; (* type instanitated outer term *) val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; + val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) + FakeTs; + val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) + Ts; + (* type-instantiate the var instantiations *) val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) :: insts_tyinst) [] unprepinsts; (* cross-instantiate *) val insts_tyinst_inst = cross_inst insts_tyinst; (* create certms of instantiations *) val cinsts_tyinst = map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), ctermify t)) insts_tyinst_inst; (* The instantiated rule *) val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); (* Create a table of vars to be renamed after instantiation - ie other uninstantiated vars in the hyps the *instantiated* rule ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) rule_inst; val cterm_renamings = map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; (* Create the specific version of the rule for this target application *) val outerterm_inst = outerterm_tyinst |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); val couter_inst = Thm.reflexive (ctermify outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst |> Thm.instantiate ([], cterm_renamings) - |> mk_abstractedrule FakeTs Ts; + |> mk_abstractedrule FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = beta_eta_contract (Thm.combination couter_inst abstract_rule_inst); (* create an instantiated version of the target thm *) val tgt_th_inst = tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) |> Thm.instantiate ([], cterm_renamings); val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in (beta_eta_contract tgt_th_inst) |> Thm.equal_elim specific_tgt_rule |> Drule.implies_intr_list cprems |> Drule.forall_intr_list frees_of_fixed_vars |> Drule.forall_elim_list vars |> fst o Thm.varifyT' othertfrees |> Drule.zero_var_indexes end; end; (* struct *)