# HG changeset patch # User wenzelm # Date 1153935462 -7200 # Node ID 3bff4719f3d65e52039699a93f56d8803c5f6f0a # Parent be3bfb0699ba247abcbbfa8e73375bd0e8d2538b focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition; diff -r be3bfb0699ba -r 3bff4719f3d6 src/Pure/subgoal.ML --- a/src/Pure/subgoal.ML Wed Jul 26 19:37:41 2006 +0200 +++ b/src/Pure/subgoal.ML Wed Jul 26 19:37:42 2006 +0200 @@ -8,16 +8,17 @@ signature BASIC_SUBGOAL = sig val SUBPROOF: Proof.context -> - ({context: Proof.context, asms: cterm list, concl: cterm, - params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic + ({context: Proof.context, schematics: ctyp list * cterm list, + params: cterm list, asms: cterm list, concl: cterm, + prems: thm list} -> tactic) -> int -> tactic end signature SUBGOAL = sig include BASIC_SUBGOAL val focus: Proof.context -> int -> thm -> - {context: Proof.context, asms: cterm list, concl: cterm, - params: (string * typ) list, prems: thm list} * thm + {context: Proof.context, schematics: ctyp list * cterm list, + params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm end; @@ -28,23 +29,28 @@ fun focus ctxt i st = let - val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt; + val ((schematics, [st']), ctxt') = Variable.import true [Goal.norm_hhf st] ctxt; val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt'; val asms = Drule.strip_imp_prems goal; val concl = Drule.strip_imp_concl goal; val (prems, context) = ProofContext.add_assumes asms ctxt''; in - ({context = context, asms = asms, concl = concl, params = params, prems = prems}, - Goal.init concl) + ({context = context, schematics = schematics, params = params, + asms = asms, concl = concl, prems = prems}, Goal.init concl) end; fun SUBPROOF ctxt tac i st = if Thm.nprems_of st < i then Seq.empty else let - val (args as {context, ...}, st') = focus ctxt i st - val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt); - in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end + val (args as {context, params, ...}, st') = focus ctxt i st; + fun export_closed th = + let + val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params); + val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params'; + in Drule.forall_intr_list vs th' end; + fun retrofit th = Thm.compose_no_flatten false (th, 0) i; + in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end end;