# HG changeset patch # User wenzelm # Date 1347485892 -7200 # Node ID bcce6988f6fa39a4caf5f6ae975d7c7c69adde9b # Parent 8ea4bad49ed568927e60dfeb894d0e14aa77b392# Parent 25fc6e0da45997c7ed3f4ad2dcda35e7f20f8f89 merged diff -r 8ea4bad49ed5 -r bcce6988f6fa src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 23:06:39 2012 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 23:38:12 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) diff -r 8ea4bad49ed5 -r bcce6988f6fa src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Wed Sep 12 23:06:39 2012 +0200 +++ b/src/HOL/Tools/TFL/post.ML Wed Sep 12 23:38:12 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; diff -r 8ea4bad49ed5 -r bcce6988f6fa src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Wed Sep 12 23:06:39 2012 +0200 +++ b/src/Tools/IsaPlanner/isand.ML Wed Sep 12 23:38:12 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; diff -r 8ea4bad49ed5 -r bcce6988f6fa src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 23:06:39 2012 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 23:38:12 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); diff -r 8ea4bad49ed5 -r bcce6988f6fa src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Wed Sep 12 23:06:39 2012 +0200 +++ b/src/Tools/eqsubst.ML Wed Sep 12 23:38:12 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;