src/Pure/subgoal.ML
changeset 20219 3bff4719f3d6
parent 20210 8fe4ae4360eb
child 20231 dcdd565a7fbe
     1.1 --- a/src/Pure/subgoal.ML	Wed Jul 26 19:37:41 2006 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Wed Jul 26 19:37:42 2006 +0200
     1.3 @@ -8,16 +8,17 @@
     1.4  signature BASIC_SUBGOAL =
     1.5  sig
     1.6    val SUBPROOF: Proof.context ->
     1.7 -    ({context: Proof.context, asms: cterm list, concl: cterm,
     1.8 -      params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
     1.9 +    ({context: Proof.context, schematics: ctyp list * cterm list,
    1.10 +      params: cterm list, asms: cterm list, concl: cterm,
    1.11 +      prems: thm list} -> tactic) -> int -> tactic
    1.12  end
    1.13  
    1.14  signature SUBGOAL =
    1.15  sig
    1.16    include BASIC_SUBGOAL
    1.17    val focus: Proof.context -> int -> thm ->
    1.18 -   {context: Proof.context, asms: cterm list, concl: cterm,
    1.19 -    params: (string * typ) list, prems: thm list} * thm
    1.20 +   {context: Proof.context, schematics: ctyp list * cterm list,
    1.21 +    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
    1.22  
    1.23  end;
    1.24  
    1.25 @@ -28,23 +29,28 @@
    1.26  
    1.27  fun focus ctxt i st =
    1.28    let
    1.29 -    val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
    1.30 +    val ((schematics, [st']), ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
    1.31      val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
    1.32      val asms = Drule.strip_imp_prems goal;
    1.33      val concl = Drule.strip_imp_concl goal;
    1.34      val (prems, context) = ProofContext.add_assumes asms ctxt'';
    1.35    in
    1.36 -    ({context = context, asms = asms, concl = concl, params = params, prems = prems},
    1.37 -      Goal.init concl)
    1.38 +    ({context = context, schematics = schematics, params = params,
    1.39 +      asms = asms, concl = concl, prems = prems}, Goal.init concl)
    1.40    end;
    1.41  
    1.42  fun SUBPROOF ctxt tac i st =
    1.43    if Thm.nprems_of st < i then Seq.empty
    1.44    else
    1.45      let
    1.46 -      val (args as {context, ...}, st') = focus ctxt i st
    1.47 -      val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
    1.48 -    in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
    1.49 +      val (args as {context, params, ...}, st') = focus ctxt i st;
    1.50 +      fun export_closed th =
    1.51 +        let
    1.52 +          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
    1.53 +          val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params';
    1.54 +        in Drule.forall_intr_list vs th' end;
    1.55 +      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
    1.56 +    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
    1.57  
    1.58  end;
    1.59