observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 23:18:26 2012 +0200
@@ -7,7 +7,7 @@
signature CASE_SPLIT =
sig
(* try to recursively split conjectured thm to given list of thms *)
- val splitto : thm list -> thm -> thm
+ val splitto : Proof.context -> thm list -> thm -> thm
end;
structure CaseSplit: CASE_SPLIT =
@@ -121,7 +121,7 @@
(* Note: This should not be a separate tactic but integrated into the
case split done during recdef's case analysis, this would avoid us
having to (re)search for variables to split. *)
-fun splitto splitths genth =
+fun splitto ctxt splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
val thy = Thm.theory_of_thm genth;
@@ -142,7 +142,7 @@
let
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
val split_thm = mk_casesplit_goal_thm thy v gt;
- val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
+ val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
in
expf (map recsplitf subthms)
end)
--- a/src/HOL/Tools/TFL/post.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/HOL/Tools/TFL/post.ML Wed Sep 12 23:18:26 2012 +0200
@@ -166,18 +166,18 @@
fun get_related_thms i =
map_filter ((fn (r,x) => if x = i then SOME r else NONE));
- fun solve_eq (th, [], i) = error "derive_init_eqs: missing rules"
- | solve_eq (th, [a], i) = [(a, i)]
- | solve_eq (th, splitths, i) =
+ fun solve_eq _ (th, [], i) = error "derive_init_eqs: missing rules"
+ | solve_eq _ (th, [a], i) = [(a, i)]
+ | solve_eq ctxt (th, splitths, i) =
(writeln "Proving unsplit equation...";
[((Drule.export_without_context o Object_Logic.rulify_no_asm)
- (CaseSplit.splitto splitths th), i)])
+ (CaseSplit.splitto ctxt splitths th), i)])
handle ERROR s =>
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
in
-fun derive_init_eqs thy rules eqs =
- map (Thm.trivial o Thm.cterm_of thy o HOLogic.mk_Trueprop) eqs
- |> map_index (fn (i, e) => solve_eq (e, (get_related_thms i rules), i))
+fun derive_init_eqs ctxt rules eqs =
+ map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs
+ |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
|> flat;
end;
@@ -192,7 +192,7 @@
val (lhs, _) = Logic.dest_equals (prop_of def)
val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats def
val rules' =
- if strict then derive_init_eqs thy rules eqs
+ if strict then derive_init_eqs ctxt rules eqs
else rules
in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end;
--- a/src/Tools/IsaPlanner/isand.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Wed Sep 12 23:18:26 2012 +0200
@@ -26,13 +26,15 @@
(* 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
+
(* meta level fixed params (i.e. !! vars) *)
- val fix_alls_term : int -> term -> term * term list
+ val fix_alls_term : Proof.context -> int -> term -> term * term list
val unfix_frees : cterm list -> thm -> thm
(* assumptions/subgoals *)
- val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
+ val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
end
structure IsaND : ISA_ND =
@@ -85,6 +87,15 @@
|> Drule.forall_intr_list cfvs
in Drule.compose_single (solth', i, gth) end;
+fun variant_names ctxt ts xs =
+ let
+ val names =
+ Variable.names_of ctxt
+ |> (fold o fold_aterms)
+ (fn Var ((a, _), _) => Name.declare a
+ | Free (a, _) => Name.declare a
+ | _ => I) ts;
+ in fst (fold_map Name.variant xs names) end;
(* fix parameters of a subgoal "i", as free variables, and create an
exporting function that will use the result of this proved goal to
@@ -104,30 +115,26 @@
("As ==> SGi x'" : thm) ->
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
-fun fix_alls_term i t =
+fun fix_alls_term ctxt i t =
let
- val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
- val names = Misc_Legacy.add_term_names (t,varnames);
val gt = Logic.get_goal t i;
val body = Term.strip_all_body gt;
val alls = rev (Term.strip_all_vars gt);
- val fvs = map Free
- (Name.variant_list names (map fst alls)
- ~~ (map snd alls));
+ 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 i th =
+fun fix_alls_cterm ctxt i th =
let
val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
- val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of 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;
-fun fix_alls' i =
- (apfst Thm.trivial) o (fix_alls_cterm i);
+fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
(* hide other goals *)
@@ -154,9 +161,9 @@
("SGi x'" : thm) ->
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
-fun fix_alls i th =
+fun fix_alls ctxt i th =
let
- val (fixed_gth, fixedvars) = fix_alls' i th
+ val (fixed_gth, fixedvars) = fix_alls' ctxt i th
val (sml_gth, othergoals) = hide_other_goals fixed_gth
in
(sml_gth, export {fixes = fixedvars,
@@ -208,7 +215,7 @@
"G" : thm)
*)
(* requires being given solutions! *)
-fun fixed_subgoal_thms th =
+fun fixed_subgoal_thms ctxt th =
let
val (subgoals, expf) = subgoal_thms th;
(* fun export_sg (th, exp) = exp th; *)
@@ -217,7 +224,7 @@
(* expf (map export_sg (ths ~~ expfs)); *)
in
apsnd export_sgs (Library.split_list (map (apsnd export_solution o
- fix_alls 1) subgoals))
+ fix_alls ctxt 1) subgoals))
end;
end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 23:18:26 2012 +0200
@@ -12,7 +12,7 @@
(* Rewrite: give it instantiation infromation, a rule, and the
target thm, and it will return the rewritten target thm *)
- val rw :
+ 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 *)
@@ -37,16 +37,6 @@
in thm3 end;
-(* to get the free names of a theorem (including hyps and flexes) *)
-fun usednames_of_thm th =
- let val rep = Thm.rep_thm th
- val hyps = #hyps rep
- val (tpairl,tpairr) = Library.split_list (#tpairs rep)
- val prop = #prop rep
- in
- List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
- end;
-
(* Given a list of variables that were bound, and a that has been
instantiated with free variable placeholders for the bound vars, it
creates an abstracted version of the theorem, with local bound vars as
@@ -64,22 +54,22 @@
note: assumes rule is instantiated
*)
(* Note, we take abstraction in the order of last abstraction first *)
-fun mk_abstractedrule TsFake Ts rule =
+fun mk_abstractedrule ctxt TsFake Ts rule =
let
val ctermify = 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 *)
- val names = usednames_of_thm rule;
- val (fromnames,tonames,_,Ts') =
- Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
- let val n2 = singleton (Name.variant_list names) n in
+
+ 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 :: names,
- (n2,ty) :: Ts'')
- end)
- (([],[],names, []), TsFake~~Ts);
+ (n2,ty) :: Ts''))
+ (TsFake ~~ Ts ~~ ns) ([], [], []);
(* rename conflicting free's in the rule to avoid cconflicts
with introduced vars from bounds outside in redex *)
@@ -105,10 +95,9 @@
(* Create a table of vars to be renamed after instantiation - ie
other uninstantiated vars in the hyps of the rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
-fun mk_renamings tgt rule_inst =
+fun mk_renamings ctxt tgt rule_inst =
let
- val rule_conds = Thm.prems_of rule_inst
- val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
+ 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,
@@ -116,13 +105,8 @@
(([],[]), rule_conds);
val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
val vars_to_fix = union (op =) termvars cond_vs;
- val (renamings, _) =
- List.foldr (fn (((n,i),ty), (vs, names')) =>
- let val n' = singleton (Name.variant_list names') n in
- ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
- end)
- ([], names) vars_to_fix;
- in renamings end;
+ 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)) =
@@ -184,7 +168,7 @@
first abstraction first. FakeTs has abstractions using the fake name
- ie the name distinct from all other abstractions. *)
-fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
+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);
@@ -192,7 +176,7 @@
val ctypeify = Thm.ctyp_of target_sign;
(* fix all non-instantiated tvars *)
- val (fixtyinsts, othertfrees) =
+ 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);
@@ -236,8 +220,7 @@
(* Create a table of vars to be renamed after instantiation - ie
other uninstantiated vars in the hyps the *instantiated* rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
- val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
- rule_inst;
+ val 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;
@@ -249,7 +232,7 @@
val couter_inst = Thm.reflexive (ctermify outerterm_inst);
val (cprems, abstract_rule_inst) =
rule_inst |> Thm.instantiate ([], cterm_renamings)
- |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
+ |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
val specific_tgt_rule =
beta_eta_contract
(Thm.combination couter_inst abstract_rule_inst);
--- a/src/Tools/eqsubst.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/Tools/eqsubst.ML Wed Sep 12 23:18:26 2012 +0200
@@ -260,15 +260,15 @@
(* conclthm is a theorem of for just the conclusion *)
(* m is instantiation/match information *)
(* rule is the equation for substitution *)
-fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
- (RWInst.rw m rule conclthm)
+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);
(* 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 i gth =
+fun prep_concl_subst ctxt i gth =
let
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
@@ -277,7 +277,7 @@
val ctermify = Thm.cterm_of sgn;
val trivify = Thm.trivial o ctermify;
- val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
+ val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
val cfvs = rev (map ctermify fvs);
val conclterm = Logic.strip_imp_concl fixedbody;
@@ -294,12 +294,12 @@
(* substitute using an object or meta level equality *)
fun eqsubst_tac' ctxt searchf instepthm i th =
let
- val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
+ 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 i th cvfsconclthm r) end;
+ |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end;
in stepthms |> Seq.maps rewrite_with_thm end;
@@ -347,11 +347,11 @@
SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
(* apply a substitution inside assumption j, keeps asm in the same place *)
-fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
+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 m rule pth)
+ (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 *)
@@ -380,7 +380,7 @@
subgoal i of gth. Note the repetition of work done for each
assumption, i.e. this can be made more efficient for search over
multiple assumptions. *)
-fun prep_subst_in_asm i gth j =
+fun prep_subst_in_asm ctxt i gth j =
let
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
@@ -389,7 +389,7 @@
val ctermify = Thm.cterm_of sgn;
val trivify = Thm.trivial o ctermify;
- val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
+ val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
val cfvs = rev (map ctermify fvs);
val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
@@ -404,8 +404,8 @@
in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
(* prepare subst in every possible assumption *)
-fun prep_subst_in_asms i gth =
- map (prep_subst_in_asm i gth)
+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));
@@ -413,7 +413,7 @@
(* 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 i th;
+ 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)
@@ -426,7 +426,7 @@
(occ_search 1 moreasms))
(* find later substs also *)
in
- occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
+ occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
end;
in stepthms |> Seq.maps rewrite_with_thm end;