--- 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
--- 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"
--- 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"
--- 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;
--- 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 *}
--- 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)" *)
--- 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
--- 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
--- 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})
--- 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 =
--- 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
--- 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
--- 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)
--- 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
--- 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;
--- 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
--- 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 *)
--- 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
--- 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' []);
--- 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;
--- 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));
--- 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 =
--- 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;
--- 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;
--- 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;