# HG changeset patch # User wenzelm # Date 1369929158 -7200 # Node ID 3244ccb7e9db5e35601d9437c288b313ea770a74 # Parent 13171b27eacaa7ba4a6e30c26b8d6b6d695b3167# Parent 54c0d4128b30fa5e0d00fc3b6717bbd6995a7692 merged diff -r 13171b27eaca -r 3244ccb7e9db src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu May 30 14:37:35 2013 +0200 +++ b/src/FOL/FOL.thy Thu May 30 17:52:38 2013 +0200 @@ -349,6 +349,8 @@ setup "Simplifier.method_setup Splitter.split_modifiers" setup Splitter.setup setup clasimp_setup + +ML_file "~~/src/Tools/eqsubst.ML" setup EqSubst.setup diff -r 13171b27eaca -r 3244ccb7e9db src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu May 30 14:37:35 2013 +0200 +++ b/src/FOL/IFOL.thy Thu May 30 17:52:38 2013 +0200 @@ -14,7 +14,6 @@ ML_file "~~/src/Tools/IsaPlanner/zipper.ML" ML_file "~~/src/Tools/IsaPlanner/isand.ML" ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" -ML_file "~~/src/Tools/eqsubst.ML" ML_file "~~/src/Provers/quantifier1.ML" ML_file "~~/src/Tools/intuitionistic.ML" ML_file "~~/src/Tools/project_rule.ML" @@ -224,7 +223,6 @@ done -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) lemma iffE: assumes major: "P <-> Q" and r: "P-->Q ==> Q-->P ==> R" diff -r 13171b27eaca -r 3244ccb7e9db src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Thu May 30 14:37:35 2013 +0200 +++ b/src/FOLP/IFOLP.thy Thu May 30 17:52:38 2013 +0200 @@ -292,8 +292,6 @@ done -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) - schematic_lemma iffE: assumes "p:P <-> Q" and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu May 30 17:52:38 2013 +0200 @@ -141,7 +141,7 @@ REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN EVERY [REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), - if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, + if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, atac 1, mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] end; diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/HOL.thy Thu May 30 17:52:38 2013 +0200 @@ -1499,8 +1499,7 @@ in if is_conj P then SOME @{thm induct_conj_curry} else NONE end | _ => NONE))] |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #> - map (Simplifier.rewrite_rule (map Thm.symmetric - @{thms induct_rulify_fallback}))))) + map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback}))))) *} text {* Pre-simplification of induction and cases rules *} diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Prolog/prolog.ML Thu May 30 17:52:38 2013 +0200 @@ -59,8 +59,7 @@ in map zero_var_indexes (at thm) end; val atomize_ss = - (Simplifier.global_context @{theory} empty_ss - |> Simplifier.set_mksimps (mksimps mksimps_pairs)) + (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs)) addsimps [ @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 30 17:52:38 2013 +0200 @@ -51,7 +51,7 @@ in thms |> Conjunction.intr_balanced - |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)] + |> rewrite_rule [Thm.symmetric (Thm.assume asm)] |> Thm.implies_intr asm |> Thm.generalize ([], params) 0 |> Axclass.unoverload thy diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Thu May 30 17:52:38 2013 +0200 @@ -554,7 +554,7 @@ fun presimplify ctxt = rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify (put_simpset nnf_ss ctxt) - #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]} + #> rewrite_rule @{thms Let_def [abs_def]} fun make_nnf ctxt th = case prems_of th of [] => th |> presimplify ctxt |> make_nnf1 ctxt diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Thu May 30 17:52:38 2013 +0200 @@ -218,9 +218,9 @@ fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of) val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) - val case_th = Raw_Simplifier.simplify true - (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) - val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems + val case_th = + rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) + val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th OF (replicate nargs @{thm refl}) diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu May 30 17:52:38 2013 +0200 @@ -1025,7 +1025,7 @@ fun peephole_optimisation thy intro = let val process = - Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy)) + rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy)) fun process_False intro_t = if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t fun process_True intro_t = diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu May 30 17:52:38 2013 +0200 @@ -213,8 +213,7 @@ error ("unexpected specification for constant " ^ quote constname ^ ":\n" ^ commas (map (quote o Display.string_of_thm_global thy) specs)) val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} - val intros = map (Raw_Simplifier.rewrite_rule - [if_beta RS @{thm eq_reflection}]) intros + val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros val _ = print_specs options thy "normalized intros" intros (*val intros = maps (split_cases thy) intros*) val (intros', (local_defs, thy')) = flatten_intros constname intros thy diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu May 30 17:52:38 2013 +0200 @@ -127,7 +127,7 @@ fun param_rewrite prem = param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem))) val SOME rew_eq = find_first param_rewrite prems' - val param_prem' = Raw_Simplifier.rewrite_rule + val param_prem' = rewrite_rule (map (fn th => th RS @{thm eq_reflection}) [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) param_prem diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu May 30 17:52:38 2013 +0200 @@ -480,7 +480,7 @@ val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1) - val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 + val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 val (insp, inst) = if ty_c = ty_d then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu May 30 17:52:38 2013 +0200 @@ -38,8 +38,7 @@ val merge = Net.merge eq ) - val prep = - `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true] + val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true] fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Thu May 30 17:52:38 2013 +0200 @@ -13,13 +13,6 @@ structure CaseSplit: CASE_SPLIT = struct -(* beta-eta contract the theorem *) -fun beta_eta_contract thm = - let - val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm - val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 - in thm3 end; - (* make a casethm from an induction thm *) val cases_thm_of_induct_thm = Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); @@ -62,10 +55,10 @@ val cPv = ctermify (Envir.subst_term_types type_insts Pv); val cDv = ctermify (Envir.subst_term_types type_insts Dv); in - (beta_eta_contract + Conv.fconv_rule Drule.beta_eta_conversion (case_thm |> Thm.instantiate (type_cinsts, []) - |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))) + |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])) end; diff -r 13171b27eaca -r 3244ccb7e9db src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/HOL/Tools/record.ML Thu May 30 17:52:38 2013 +0200 @@ -1748,8 +1748,7 @@ THEN rewrite_goals_tac [Simpdata.mk_eq eq_def] THEN ALLGOALS (rtac @{thm refl}); fun mk_eq thy eq_def = - Simplifier.rewrite_rule - [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject; + rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject; fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/Isar/element.ML Thu May 30 17:52:38 2013 +0200 @@ -466,7 +466,7 @@ {binding = [], typ = [], term = [Raw_Simplifier.rewrite_term thy thms []], - fact = [map (Raw_Simplifier.rewrite_rule thms)]}); + fact = [map (rewrite_rule thms)]}); (* transfer to theory using closure *) diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/Isar/expression.ML Thu May 30 17:52:38 2013 +0200 @@ -671,8 +671,7 @@ Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); val conjuncts = - (Drule.equal_elim_rule2 OF [body_eq, - Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) + (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))]) |> Conjunction.elim_balanced (length ts); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness defs_ctxt t diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/Isar/generic_target.ML Thu May 30 17:52:38 2013 +0200 @@ -125,7 +125,7 @@ (*export assumes/defines*) val th = Goal.norm_result raw_th; val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; - val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms; + val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/Isar/object_logic.ML Thu May 30 17:52:38 2013 +0200 @@ -201,7 +201,7 @@ fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st; fun gen_rulify full thm = - Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm + Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes; val rulify = gen_rulify true; diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/axclass.ML Thu May 30 17:52:38 2013 +0200 @@ -292,8 +292,8 @@ fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); -fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy); -fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy)); +fun unoverload thy = rewrite_rule (inst_thms thy); +fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy)); fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy); fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy)); diff -r 13171b27eaca -r 3244ccb7e9db src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Pure/raw_simplifier.ML Thu May 30 17:52:38 2013 +0200 @@ -129,7 +129,6 @@ val generic_rewrite_goal_tac: bool * bool * bool -> (Proof.context -> tactic) -> Proof.context -> int -> tactic val rewrite: bool -> thm list -> conv - val simplify: bool -> thm list -> thm -> thm end; structure Raw_Simplifier: RAW_SIMPLIFIER = @@ -1329,8 +1328,7 @@ rewrite_cterm (full, false, false) simple_prover (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct; -fun simplify full thms = Conv.fconv_rule (rewrite full thms); -val rewrite_rule = simplify true; +val rewrite_rule = Conv.fconv_rule o rewrite true; (*simple term rewriting -- no proof*) fun rewrite_term thy rules procs = diff -r 13171b27eaca -r 3244ccb7e9db src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Tools/IsaPlanner/isand.ML Thu May 30 17:52:38 2013 +0200 @@ -1,7 +1,7 @@ (* Title: Tools/IsaPlanner/isand.ML Author: Lucas Dixon, University of Edinburgh -Natural Deduction tools. +Natural Deduction tools (obsolete). For working with Isabelle theorems in a natural detuction style. ie, not having to deal with meta level quantified varaibles, @@ -23,69 +23,34 @@ signature ISA_ND = sig - (* inserting meta level params for frees in the conditions *) - val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list - - val variant_names : Proof.context -> term list -> string list -> string list + val variant_names: Proof.context -> term list -> string list -> string list (* meta level fixed params (i.e. !! vars) *) - val fix_alls_term : Proof.context -> int -> term -> term * term list - - val unfix_frees : cterm list -> thm -> thm + val fix_alls_term: Proof.context -> int -> term -> term * term list (* assumptions/subgoals *) - val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm) + val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm) end structure IsaND : ISA_ND = struct -(* 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) = - (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) - - fun allify_prem Ts p = List.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; - -(* make free vars into schematic vars with index zero *) -fun unfix_frees frees = - fold (K (Thm.forall_elim_var 0)) frees - o Drule.forall_intr_list frees; - (* 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 *) + Export of + {fixes : Thm.cterm list, (* fixed vars *) + assumes : Thm.cterm list, (* hidden hyps/assumed prems *) + sgid : int, + gth : Thm.thm}; (* subgoal/goalthm *) (* 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_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 variant_names ctxt ts xs = let @@ -116,23 +81,21 @@ ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) *) fun fix_alls_term ctxt i t = - let - val gt = Logic.get_goal t i; - val body = Term.strip_all_body gt; - val alls = rev (Term.strip_all_vars gt); - val xs = variant_names ctxt [t] (map fst alls); - val fvs = map Free (xs ~~ map snd alls); - in ((subst_bounds (fvs,body)), fvs) end; + let + val gt = Logic.get_goal t i; + val body = Term.strip_all_body gt; + val alls = rev (Term.strip_all_vars gt); + val xs = variant_names ctxt [t] (map fst alls); + val fvs = map Free (xs ~~ map snd alls); + in ((subst_bounds (fvs,body)), fvs) end; fun fix_alls_cterm ctxt i th = - let - val ctermify = Thm.cterm_of (Thm.theory_of_thm th); - val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); - val cfvs = rev (map ctermify fvs); - val ct_body = ctermify fixedbody - in - (ct_body, cfvs) - end; + let + val cert = Thm.cterm_of (Thm.theory_of_thm th); + val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); + val cfvs = rev (map cert fvs); + val ct_body = cert fixedbody; + in (ct_body, cfvs) end; fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i; @@ -141,14 +104,11 @@ (* 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; + 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) @@ -162,14 +122,10 @@ ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) *) fun fix_alls ctxt i th = - let - val (fixed_gth, fixedvars) = fix_alls' ctxt i th - val (sml_gth, othergoals) = hide_other_goals fixed_gth - in - (sml_gth, export {fixes = fixedvars, - assumes = othergoals, - sgid = i, gth = th}) - end; + let + val (fixed_gth, fixedvars) = fix_alls' ctxt i th + val (sml_gth, othergoals) = hide_other_goals fixed_gth + in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end; (* Fixme: allow different order of subgoals given to expf *) @@ -183,21 +139,16 @@ "G" : thm) *) fun subgoal_thms th = - let - val t = (prop_of th); + let + val cert = Thm.cterm_of (Thm.theory_of_thm th); - val prems = Logic.strip_imp_prems t; - - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; + val t = prop_of th; - val aprems = map (Thm.trivial o ctermify) prems; + val prems = Logic.strip_imp_prems t; + val aprems = map (Thm.trivial o cert) prems; - fun explortf premths = - Drule.implies_elim_list th premths - in - (aprems, explortf) - end; + fun explortf premths = Drule.implies_elim_list th premths; + in (aprems, explortf) end; (* Fixme: allow different order of subgoals in exportf *) @@ -216,15 +167,15 @@ *) (* requires being given solutions! *) fun fixed_subgoal_thms ctxt th = - let - val (subgoals, expf) = subgoal_thms th; -(* fun export_sg (th, exp) = exp th; *) - fun export_sgs expfs solthms = - expf (map2 (curry (op |>)) solthms expfs); -(* expf (map export_sg (ths ~~ expfs)); *) - in - apsnd export_sgs (Library.split_list (map (apsnd export_solution o - fix_alls ctxt 1) subgoals)) - end; + let + val (subgoals, expf) = subgoal_thms th; +(* fun export_sg (th, exp) = exp th; *) + fun export_sgs expfs solthms = + expf (map2 (curry (op |>)) solthms expfs); +(* expf (map export_sg (ths ~~ expfs)); *) + in + apsnd export_sgs + (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals)) + end; end; diff -r 13171b27eaca -r 3244ccb7e9db src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 17:52:38 2013 +0200 @@ -7,34 +7,40 @@ signature RW_INST = sig - - val beta_eta_contract : thm -> thm - - (* Rewrite: give it instantiation infromation, a rule, and the - target thm, and it will return the rewritten target thm *) - val rw : Proof.context -> - ((indexname * (sort * typ)) list * (* type var instantiations *) - (indexname * (typ * term)) list) (* schematic var instantiations *) - * (string * typ) list (* Fake named bounds + types *) - * (string * typ) list (* names of bound + types *) - * term -> (* outer term for instantiation *) - thm -> (* rule with indexies lifted *) - thm -> (* target thm *) - thm (* rewritten theorem possibly - with additional premises for - rule conditions *) + val rw: Proof.context -> + ((indexname * (sort * typ)) list * (* type var instantiations *) + (indexname * (typ * term)) list) (* schematic var instantiations *) + * (string * typ) list (* Fake named bounds + types *) + * (string * typ) list (* names of bound + types *) + * term -> (* outer term for instantiation *) + thm -> (* rule with indexes lifted *) + thm -> (* target thm *) + thm (* rewritten theorem possibly with additional premises for rule conditions *) end; -structure RWInst : RW_INST = +structure RW_Inst: RW_INST = struct +(* Given (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. -(* beta-eta contract the theorem *) -fun beta_eta_contract thm = - let - val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm - val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 - in thm3 end; +Given: x +th: A vs ==> B vs +Results in: "B vs" [!!x. A x] +*) +fun allify_conditions Ts th = + let + val cert = Thm.cterm_of (Thm.theory_of_thm th); + + fun allify (x, T) t = + Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); + + val cTs = map (cert o Free) Ts; + val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th); + val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; + in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; (* Given a list of variables that were bound, and a that has been @@ -55,37 +61,37 @@ *) (* Note, we take abstraction in the order of last abstraction first *) fun mk_abstractedrule ctxt TsFake Ts rule = - let - val ctermify = Thm.cterm_of (Thm.theory_of_thm rule); + let + val cert = Thm.cterm_of (Thm.theory_of_thm rule); - (* now we change the names of temporary free vars that represent - bound vars with binders outside the redex *) + (* now we change the names of temporary free vars that represent + bound vars with binders outside the redex *) - val ns = - IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); + val ns = + IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); - val (fromnames, tonames, Ts') = - fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => - (ctermify (Free(faken,ty)) :: rnf, - ctermify (Free(n2,ty)) :: rnt, - (n2,ty) :: Ts'')) - (TsFake ~~ Ts ~~ ns) ([], [], []); + val (fromnames, tonames, Ts') = + fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => + (cert (Free(faken,ty)) :: rnf, + cert (Free(n2,ty)) :: rnt, + (n2,ty) :: Ts'')) + (TsFake ~~ Ts ~~ ns) ([], [], []); - (* 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; + (* 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'; + (* make unconditional rule and prems *) + val (uncond_rule, cprems) = allify_conditions (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; + (* using these names create lambda-abstracted version of the rule *) + val abstractions = rev (Ts' ~~ tonames); + val abstract_rule = + fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) + abstractions uncond_rule; + in (cprems, abstract_rule) end; (* given names to avoid, and vars that need to be fixed, it gives @@ -96,67 +102,62 @@ other uninstantiated vars in the hyps of the rule ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) fun mk_renamings ctxt tgt rule_inst = - let - val rule_conds = Thm.prems_of rule_inst; - val (_, cond_vs) = - Library.foldl (fn ((tyvs, vs), t) => - (union (op =) (Misc_Legacy.term_tvars t) tyvs, - union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) - (([],[]), rule_conds); - val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); - val vars_to_fix = union (op =) termvars cond_vs; - val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); + let + val rule_conds = Thm.prems_of rule_inst; + val (_, cond_vs) = + fold (fn t => fn (tyvs, vs) => + (union (op =) (Misc_Legacy.term_tvars t) tyvs, + union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); + val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); + val vars_to_fix = union (op =) termvars cond_vs; + val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; (* make a new fresh typefree instantiation for the given tvar *) -fun new_tfree (tv as (ix,sort), (pairs,used)) = - let val v = singleton (Name.variant_list used) (string_of_indexname ix) - in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; +fun new_tfree (tv as (ix,sort)) (pairs, used) = + let val v = singleton (Name.variant_list 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) = - List.foldr (fn (t, (varixs, tfrees)) => - (Misc_Legacy.add_term_tvars (t,varixs), - Misc_Legacy.add_term_tfrees (t,tfrees))) - ([],[]) ts; - val unfixed_tvars = - filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; - val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars - in (fixtyinsts, tfrees) end; + let + val ignore_ixs = map fst ignore_insts; + val (tvars, tfrees) = + fold_rev (fn t => fn (varixs, tfrees) => + (Misc_Legacy.add_term_tvars (t,varixs), + Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); + val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; + val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) + 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))); + 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) = + 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; + 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))); + 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) = + 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; + in cross_instL (insts, []) end; (* assume that rule and target_thm have distinct var names. THINK: @@ -169,90 +170,82 @@ - ie the name distinct from all other abstractions. *) fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = - let - (* general signature info *) - val target_sign = (Thm.theory_of_thm target_thm); - val ctermify = Thm.cterm_of target_sign; - val ctypeify = Thm.ctyp_of target_sign; + let + val thy = Thm.theory_of_thm target_thm; + val cert = Thm.cterm_of thy; + val certT = Thm.ctyp_of thy; - (* fix all non-instantiated tvars *) - val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) - mk_fixtvar_tyinsts nonfixed_typinsts - [Thm.prop_of rule, Thm.prop_of target_thm]; - val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); + (* fix all non-instantiated tvars *) + val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) + mk_fixtvar_tyinsts nonfixed_typinsts + [Thm.prop_of rule, Thm.prop_of target_thm]; + 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; + (* certified instantiations for types *) + val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts; + + (* type instantiated versions *) + val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; + val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; - (* 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,(_,ty)) => (ix,ty)) typinsts; + (* type instanitated outer term *) + val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; - val term_typ_inst = map (fn (ix,(_,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; - 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 = + fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => + (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) + :: insts_tyinst) unprepinsts []; - (* type-instantiate the var instantiations *) - val insts_tyinst = List.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; - (* cross-instantiate *) - val insts_tyinst_inst = cross_inst insts_tyinst; + (* create certms of instantiations *) + val cinsts_tyinst = + map (fn (ix, (ty, t)) => (cert (Var (ix, ty)), cert t)) insts_tyinst_inst; - (* 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); - (* 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 ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; - val cterm_renamings = - map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; + (* 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 ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; + val cterm_renamings = map (fn (x, y) => (cert (Var x), cert 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 ctxt FakeTs_tyinst Ts_tyinst; - val specific_tgt_rule = - beta_eta_contract - (Thm.combination couter_inst abstract_rule_inst); + (* 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 (cert outerterm_inst); + val (cprems, abstract_rule_inst) = + rule_inst + |> Thm.instantiate ([], cterm_renamings) + |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; + val specific_tgt_rule = + Conv.fconv_rule Drule.beta_eta_conversion + (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; + (* create an instantiated version of the target thm *) + val tgt_th_inst = + tgt_th_tyinst + |> Thm.instantiate ([], cinsts_tyinst) + |> Thm.instantiate ([], 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 - |> Thm.varifyT_global' othertfrees - |-> K Drule.zero_var_indexes - end; - + val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; + in + Conv.fconv_rule Drule.beta_eta_conversion 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 + |> Thm.varifyT_global' othertfrees + |-> K Drule.zero_var_indexes + end; end; diff -r 13171b27eaca -r 3244ccb7e9db src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Thu May 30 14:37:35 2013 +0200 +++ b/src/Tools/eqsubst.ML Thu May 30 17:52:38 2013 +0200 @@ -1,66 +1,52 @@ (* Title: Tools/eqsubst.ML Author: Lucas Dixon, University of Edinburgh -A proof method to perform a substiution using an equation. +Perform a substitution using an equation. *) signature EQSUBST = sig - (* a type abbreviation for match information *) type match = - ((indexname * (sort * typ)) list (* type instantiations *) - * (indexname * (typ * term)) list) (* term instantiations *) - * (string * typ) list (* fake named type abs env *) - * (string * typ) list (* type abs env *) - * term (* outer term *) + ((indexname * (sort * typ)) list (* type instantiations *) + * (indexname * (typ * term)) list) (* term instantiations *) + * (string * typ) list (* fake named type abs env *) + * (string * typ) list (* type abs env *) + * term (* outer term *) type searchinfo = - theory - * int (* maxidx *) - * Zipper.T (* focusterm to search under *) + theory + * int (* maxidx *) + * Zipper.T (* focusterm to search under *) datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq - val skip_first_asm_occs_search : - ('a -> 'b -> 'c Seq.seq Seq.seq) -> - 'a -> int -> 'b -> 'c skipseq - val skip_first_occs_search : - int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq - val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq + val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq + val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq + val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq (* tactics *) - val eqsubst_asm_tac : - Proof.context -> - int list -> thm list -> int -> tactic - val eqsubst_asm_tac' : - Proof.context -> - (searchinfo -> int -> term -> match skipseq) -> - int -> thm -> int -> tactic - val eqsubst_tac : - Proof.context -> - int list -> (* list of occurences to rewrite, use [0] for any *) - thm list -> int -> tactic - val eqsubst_tac' : - Proof.context -> (* proof context *) - (searchinfo -> term -> match Seq.seq) (* search function *) - -> thm (* equation theorem to rewrite with *) - -> int (* subgoal number in goal theorem *) - -> thm (* goal theorem *) - -> thm Seq.seq (* rewritten goal theorem *) + val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic + val eqsubst_asm_tac': Proof.context -> + (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic + val eqsubst_tac: Proof.context -> + int list -> (* list of occurences to rewrite, use [0] for any *) + thm list -> int -> tactic + val eqsubst_tac': Proof.context -> + (searchinfo -> term -> match Seq.seq) (* search function *) + -> thm (* equation theorem to rewrite with *) + -> int (* subgoal number in goal theorem *) + -> thm (* goal theorem *) + -> thm Seq.seq (* rewritten goal theorem *) (* search for substitutions *) - val valid_match_start : Zipper.T -> bool - val search_lr_all : Zipper.T -> Zipper.T Seq.seq - val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq - val searchf_lr_unify_all : - searchinfo -> term -> match Seq.seq Seq.seq - val searchf_lr_unify_valid : - searchinfo -> term -> match Seq.seq Seq.seq - val searchf_bt_unify_valid : - searchinfo -> term -> match Seq.seq Seq.seq + val valid_match_start: Zipper.T -> bool + val search_lr_all: Zipper.T -> Zipper.T Seq.seq + val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq + val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq + val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq + val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq val setup : theory -> theory - end; structure EqSubst: EQSUBST = @@ -70,302 +56,287 @@ fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes; +(* make free vars into schematic vars with index zero *) +fun unfix_frees frees = + fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees; - (* a type abriviation for match information *) - type match = - ((indexname * (sort * typ)) list (* type instantiations *) - * (indexname * (typ * term)) list) (* term instantiations *) - * (string * typ) list (* fake named type abs env *) - * (string * typ) list (* type abs env *) - * term (* outer term *) - type searchinfo = - theory - * int (* maxidx *) - * Zipper.T (* focusterm to search under *) +type match = + ((indexname * (sort * typ)) list (* type instantiations *) + * (indexname * (typ * term)) list) (* term instantiations *) + * (string * typ) list (* fake named type abs env *) + * (string * typ) list (* type abs env *) + * term; (* outer term *) + +type searchinfo = + theory + * int (* maxidx *) + * Zipper.T; (* focusterm to search under *) (* skipping non-empty sub-sequences but when we reach the end of the seq, remembering how much we have left to skip. *) -datatype 'a skipseq = SkipMore of int - | SkipSeq of 'a Seq.seq Seq.seq; +datatype 'a skipseq = + SkipMore of int | + SkipSeq of 'a Seq.seq Seq.seq; + (* given a seqseq, skip the first m non-empty seq's, note deficit *) fun skipto_skipseq 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; + 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; (* note: outerterm is the taget with the match replaced by a bound - variable : ie: "P lhs" beocmes "%x. P x" - insts is the types of instantiations of vars in lhs - and typinsts is the type instantiations of types in the lhs - Note: Final rule is the rule lifted into the ontext of the - taget thm. *) + variable : ie: "P lhs" beocmes "%x. P x" + insts is the types of instantiations of vars in lhs + and typinsts is the type instantiations of types in the lhs + Note: Final rule is the rule lifted into the ontext of the + taget thm. *) fun mk_foo_match mkuptermfunc Ts t = - let - val ty = Term.type_of t - val bigtype = (rev (map snd Ts)) ---> ty - fun mk_foo 0 t = t - | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) - val num_of_bnds = (length Ts) - (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) - val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) - in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; + let + val ty = Term.type_of t + val bigtype = rev (map snd Ts) ---> ty + fun mk_foo 0 t = t + | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) + val num_of_bnds = length Ts + (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) + val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) + in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end; (* T is outer bound vars, n is number of locally bound vars *) (* THINK: is order of Ts correct...? or reversed? *) fun mk_fake_bound_name n = ":b_" ^ n; fun fakefree_badbounds Ts t = - let val (FakeTs,Ts,newnames) = - List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => - let val newname = singleton (Name.variant_list usednames) n - in ((mk_fake_bound_name newname,ty)::FakeTs, - (newname,ty)::Ts, - newname::usednames) end) - ([],[],[]) - Ts - in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; + let val (FakeTs, Ts, newnames) = + fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) => + let + val newname = singleton (Name.variant_list usednames) n + in + ((mk_fake_bound_name newname, ty) :: FakeTs, + (newname, ty) :: Ts, + newname :: usednames) + end) Ts ([], [], []) + in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; (* before matching we need to fake the bound vars that are missing an -abstraction. In this function we additionally construct the -abstraction environment, and an outer context term (with the focus -abstracted out) for use in rewriting with RWInst.rw *) + abstraction. In this function we additionally construct the + abstraction environment, and an outer context term (with the focus + abstracted out) for use in rewriting with RW_Inst.rw *) fun prep_zipper_match z = - let - val t = Zipper.trm z - val c = Zipper.ctxt z - val Ts = Zipper.C.nty_ctxt c - val (FakeTs', Ts', t') = fakefree_badbounds Ts t - val absterm = mk_foo_match (Zipper.C.apply c) Ts' t' - in - (t', (FakeTs', Ts', absterm)) - end; + let + val t = Zipper.trm z + val c = Zipper.ctxt z + val Ts = Zipper.C.nty_ctxt c + val (FakeTs', Ts', t') = fakefree_badbounds Ts t + val absterm = mk_foo_match (Zipper.C.apply c) Ts' t' + in + (t', (FakeTs', Ts', absterm)) + end; (* Unification with exception handled *) (* given theory, max var index, pat, tgt; returns Seq of instantiations *) -fun clean_unify thry ix (a as (pat, tgt)) = - let - (* type info will be re-derived, maybe this can be cached - for efficiency? *) - val pat_ty = Term.type_of pat; - val tgt_ty = Term.type_of tgt; - (* is it OK to ignore the type instantiation info? - or should I be using it? *) - val typs_unify = - SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix)) - handle Type.TUNIFY => NONE; - in - case typs_unify of - SOME (typinsttab, ix2) => +fun clean_unify thy ix (a as (pat, tgt)) = + let + (* type info will be re-derived, maybe this can be cached + for efficiency? *) + val pat_ty = Term.type_of pat; + val tgt_ty = Term.type_of tgt; + (* FIXME is it OK to ignore the type instantiation info? + or should I be using it? *) + val typs_unify = + SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix)) + handle Type.TUNIFY => NONE; + in + (case typs_unify of + SOME (typinsttab, ix2) => let - (* is it right to throw away the flexes? - or should I be using them somehow? *) + (* FIXME is it right to throw away the flexes? + or should I be using them somehow? *) fun mk_insts env = (Vartab.dest (Envir.type_env env), Vartab.dest (Envir.term_env env)); val initenv = Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; - val useq = Unify.smash_unifiers thry [a] initenv - handle ListPair.UnequalLengths => Seq.empty - | Term.TERM _ => Seq.empty; + val useq = Unify.smash_unifiers thy [a] initenv + handle ListPair.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 ListPair.UnequalLengths => NONE - | Term.TERM _ => NONE + (case (Seq.pull useq) of + NONE => NONE + | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t))) + handle ListPair.UnequalLengths => NONE + | Term.TERM _ => NONE; in (Seq.make (clean_unify' useq)) end - | NONE => Seq.empty - end; + | NONE => Seq.empty) + end; (* Unification for zippers *) (* Note: Ts is a modified version of the original names of the outer -bound variables. New names have been introduced to make sure they are -unique w.r.t all names in the term and each other. usednames' is -oldnames + new names. *) -(* ix = max var index *) -fun clean_unify_z sgn ix pat z = - let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in + bound variables. New names have been introduced to make sure they are + unique w.r.t all names in the term and each other. usednames' is + oldnames + new names. *) +fun clean_unify_z thy maxidx pat z = + let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) - (clean_unify sgn ix (t, pat)) end; + (clean_unify thy maxidx (t, pat)) + end; -fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l - | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t +fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l + | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t | bot_left_leaf_of x = x; (* Avoid considering replacing terms which have a var at the head as they always succeed trivially, and uninterestingly. *) fun valid_match_start z = - (case bot_left_leaf_of (Zipper.trm z) of - Var _ => false - | _ => true); + (case bot_left_leaf_of (Zipper.trm z) of + Var _ => false + | _ => true); (* search from top, left to right, then down *) val search_lr_all = ZipperSearch.all_bl_ur; (* search from top, left to right, then down *) fun search_lr_valid validf = - let - fun sf_valid_td_lr z = - let val here = if validf z then [Zipper.Here z] else [] in - case Zipper.trm z - of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] - @ here - @ [Zipper.LookIn (Zipper.move_down_right z)] - | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)] - | _ => here - end; - in Zipper.lzy_search sf_valid_td_lr end; + let + fun sf_valid_td_lr z = + let val here = if validf z then [Zipper.Here z] else [] in + (case Zipper.trm z of + _ $ _ => + [Zipper.LookIn (Zipper.move_down_left z)] @ here @ + [Zipper.LookIn (Zipper.move_down_right z)] + | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)] + | _ => here) + end; + in Zipper.lzy_search sf_valid_td_lr end; (* search from bottom to top, left to right *) +fun search_bt_valid validf = + let + fun sf_valid_td_lr z = + let val here = if validf z then [Zipper.Here z] else [] in + (case Zipper.trm z of + _ $ _ => + [Zipper.LookIn (Zipper.move_down_left z), + Zipper.LookIn (Zipper.move_down_right z)] @ here + | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here + | _ => here) + end; + in Zipper.lzy_search sf_valid_td_lr end; -fun search_bt_valid validf = - let - fun sf_valid_td_lr z = - let val here = if validf z then [Zipper.Here z] else [] in - case Zipper.trm z - of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), - Zipper.LookIn (Zipper.move_down_right z)] @ here - | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here - | _ => here - end; - in Zipper.lzy_search sf_valid_td_lr end; - -fun searchf_unify_gen f (sgn, maxidx, z) lhs = - Seq.map (clean_unify_z sgn maxidx lhs) - (Zipper.limit_apply f z); +fun searchf_unify_gen f (thy, maxidx, z) lhs = + Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z); (* search all unifications *) -val searchf_lr_unify_all = - searchf_unify_gen search_lr_all; +val searchf_lr_unify_all = searchf_unify_gen search_lr_all; (* search only for 'valid' unifiers (non abs subterms and non vars) *) -val searchf_lr_unify_valid = - searchf_unify_gen (search_lr_valid valid_match_start); +val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start); -val searchf_bt_unify_valid = - searchf_unify_gen (search_bt_valid valid_match_start); +val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start); -(* apply a substitution in the conclusion of the theorem th *) +(* apply a substitution in the conclusion of the theorem *) (* 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 ctxt i th (cfvs, conclthm) rule m = - (RWInst.rw ctxt m rule conclthm) - |> IsaND.unfix_frees cfvs - |> RWInst.beta_eta_contract - |> (fn r => Tactic.rtac r i th); +fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m = + RW_Inst.rw ctxt m rule conclthm + |> unfix_frees cfvs + |> Conv.fconv_rule Drule.beta_eta_conversion + |> (fn r => Tactic.rtac r i st); (* 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 ctxt i gth = - let - val th = Thm.incr_indexes 1 gth; - val tgt_term = Thm.prop_of th; + let + val th = Thm.incr_indexes 1 gth; + val tgt_term = Thm.prop_of th; - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; + val thy = Thm.theory_of_thm th; + val cert = Thm.cterm_of thy; - val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; - val cfvs = rev (map ctermify fvs); + val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; + val cfvs = rev (map cert fvs); - val conclterm = Logic.strip_imp_concl fixedbody; - val conclthm = trivify conclterm; - val maxidx = Thm.maxidx_of th; - val ft = ((Zipper.move_down_right (* ==> *) - o Zipper.move_down_left (* Trueprop *) - o Zipper.mktop - o Thm.prop_of) conclthm) - in - ((cfvs, conclthm), (sgn, maxidx, ft)) - end; + val conclterm = Logic.strip_imp_concl fixedbody; + val conclthm = Thm.trivial (cert conclterm); + val maxidx = Thm.maxidx_of th; + val ft = + (Zipper.move_down_right (* ==> *) + o Zipper.move_down_left (* Trueprop *) + o Zipper.mktop + o Thm.prop_of) conclthm + in + ((cfvs, conclthm), (thy, maxidx, ft)) + end; (* substitute using an object or meta level equality *) -fun eqsubst_tac' ctxt searchf instepthm i th = - let - val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th; - 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 - |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end; - in stepthms |> Seq.maps rewrite_with_thm end; +fun eqsubst_tac' ctxt searchf instepthm i st = + let + val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st; + 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 + |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r) + end; + in stepthms |> Seq.maps rewrite_with_thm end; -(* distinct subgoals *) -fun distinct_subgoals th = - the_default th (SINGLE distinct_subgoals_tac th); - (* General substitution of multiple occurances using one of - the given theorems*) - + the given theorems *) fun skip_first_occs_search occ srchf sinfo lhs = - case (skipto_skipseq occ (srchf sinfo lhs)) of - SkipMore _ => Seq.empty - | SkipSeq ss => Seq.flat ss; + (case skipto_skipseq occ (srchf sinfo lhs) of + SkipMore _ => Seq.empty + | SkipSeq ss => Seq.flat ss); -(* The occL is a list of integers indicating which occurence +(* The "occs" argument is a list of integers indicating which occurence w.r.t. the search order, to rewrite. Backtracking will also find later occurences, but all earlier ones are skipped. Thus you can use [0] to just find all rewrites. *) -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 |> Seq.maps - (fn r => eqsubst_tac' - ctxt - (skip_first_occs_search - occ searchf_lr_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 sortedoccL) th) - end - end; +fun eqsubst_tac ctxt occs thms i st = + let val nprems = Thm.nprems_of st in + if nprems < i then Seq.empty else + let + val thmseq = Seq.of_list thms; + fun apply_occ occ st = + thmseq |> Seq.maps (fn r => + eqsubst_tac' ctxt + (skip_first_occs_search occ searchf_lr_unify_valid) r + (i + (Thm.nprems_of st - nprems)) st); + val sorted_occs = Library.sort (rev_order o int_ord) occs; + in + Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) + end + end; -(* inthms are the given arguments in Isar, and treated as eqstep with - the first one, then the second etc *) -fun eqsubst_meth ctxt occL inthms = - SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms); - (* apply a substitution inside assumption j, keeps asm in the same place *) -fun apply_subst_in_asm ctxt i th rule ((cfvs, j, ngoalprems, pth),m) = - let - val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *) - val preelimrule = - (RWInst.rw ctxt m rule pth) - |> (Seq.hd o 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) ((Thm.nprems_of rule) + i)) - (Tactic.dtac preelimrule i th2) - end; +fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) = + let + val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *) + val preelimrule = + RW_Inst.rw ctxt m rule pth + |> (Seq.hd o prune_params_tac) + |> Thm.permute_prems 0 ~1 (* put old asm first *) + |> unfix_frees cfvs (* unfix any global params *) + |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *) + in + (* ~j because new asm starts at back, thus we subtract 1 *) + Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) + (Tactic.dtac preelimrule i st2) + end; (* prepare to substitute within the j'th premise of subgoal i of gth, @@ -375,83 +346,75 @@ assumption, i.e. this can be made more efficient for search over multiple assumptions. *) fun prep_subst_in_asm ctxt i gth j = - let - val th = Thm.incr_indexes 1 gth; - val tgt_term = Thm.prop_of th; + let + val th = Thm.incr_indexes 1 gth; + val tgt_term = Thm.prop_of th; - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; + val thy = Thm.theory_of_thm th; + val cert = Thm.cterm_of thy; - val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; - val cfvs = rev (map ctermify fvs); + val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; + val cfvs = rev (map cert fvs); - val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); - val asm_nprems = length (Logic.strip_imp_prems asmt); + val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); + val asm_nprems = length (Logic.strip_imp_prems asmt); + + val pth = Thm.trivial (cert asmt); + val maxidx = Thm.maxidx_of th; - val pth = trivify asmt; - val maxidx = Thm.maxidx_of th; - - val ft = ((Zipper.move_down_right (* trueprop *) - o Zipper.mktop - o Thm.prop_of) pth) - in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; + val ft = + (Zipper.move_down_right (* trueprop *) + o Zipper.mktop + o Thm.prop_of) pth + in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end; (* prepare subst in every possible assumption *) fun prep_subst_in_asms ctxt i gth = - map (prep_subst_in_asm ctxt i gth) - ((fn l => Library.upto (1, length l)) - (Logic.prems_of_goal (Thm.prop_of gth) i)); + map (prep_subst_in_asm ctxt i gth) + ((fn l => Library.upto (1, length l)) + (Logic.prems_of_goal (Thm.prop_of gth) i)); (* substitute in an assumption using an object or meta level equality *) -fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th = - let - val asmpreps = prep_subst_in_asms ctxt i th; - 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 - | occ_search occ ((asminfo, searchinfo)::moreasms) = - (case searchf searchinfo occ lhs of - SkipMore i => occ_search i moreasms - | 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 |> Seq.maps (apply_subst_in_asm ctxt i th r) - end; - in stepthms |> Seq.maps rewrite_with_thm end; +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st = + let + val asmpreps = prep_subst_in_asms ctxt i st; + 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 + | occ_search occ ((asminfo, searchinfo)::moreasms) = + (case searchf searchinfo occ lhs of + SkipMore i => occ_search i moreasms + | 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 |> Seq.maps (apply_subst_in_asm ctxt i st r) + end; + in stepthms |> Seq.maps rewrite_with_thm end; fun skip_first_asm_occs_search searchf sinfo occ lhs = - skipto_skipseq occ (searchf sinfo lhs); + skipto_skipseq occ (searchf sinfo lhs); -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 |> Seq.maps - (fn r => - eqsubst_asm_tac' ctxt (skip_first_asm_occs_search - searchf_lr_unify_valid) occK r - (i + ((Thm.nprems_of th) - nprems)) - th); - val sortedoccs = - Library.sort (Library.rev_order o Library.int_ord) occL +fun eqsubst_asm_tac ctxt occs thms i st = + let val nprems = Thm.nprems_of st in + if nprems < i then Seq.empty + else + let + val thmseq = Seq.of_list thms; + fun apply_occ occ st = + thmseq |> Seq.maps (fn r => + eqsubst_asm_tac' ctxt + (skip_first_asm_occs_search searchf_lr_unify_valid) occ r + (i + (Thm.nprems_of st - nprems)) st); + val sorted_occs = Library.sort (rev_order o int_ord) occs; in - Seq.map distinct_subgoals - (Seq.EVERY (map apply_occ sortedoccs) th) + Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) end - end; - -(* inthms are the given arguments in Isar, and treated as eqstep with - the first one, then the second etc *) -fun eqsubst_asm_meth ctxt occL inthms = - SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms); + end; (* combination method that takes a flag (true indicates that subst should be done to an assumption, false = apply to the conclusion of @@ -460,8 +423,8 @@ Method.setup @{binding subst} (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- Attrib.thms >> - (fn ((asm, occL), inthms) => fn ctxt => - (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms)) + (fn ((asm, occs), inthms) => fn ctxt => + SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) "single-step substitution"; end;